CristalCaveGem » LustreC

let is_memory m id = List.exists (fun o -> o.var_id = id.var_id) m.mmemory

let is_reset_flag id = id.var_id = "_reset"

let pp_vdecl fmt v = pp_print_string fmt v.var_id

  | Cst c ->

    Printers.pp_const fmt c

  | Var v ->

      if print_statelocaltag then fprintf fmt "{%s}" v.var_id

      else pp_print_string fmt v.var_id

    else if print_statelocaltag then fprintf fmt "%s" v.var_id

    else pp_vdecl fmt v

  | Array vl ->

    pp_print_bracketed pp_val fmt vl

  | Access (t, i) ->

    fprintf fmt "%a[%a]" pp_val t pp_val i

  | Power (v, n) ->

    fprintf fmt "(%a^%a)" pp_val v pp_val n

  | Fun (n, vl) ->

    fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl

  | ResetFlag ->

    fprintf fmt "RESET"

    | ResetFlag ->

      pp_print_string fmt "{RESET}"

    | StateVar v ->

      fprintf fmt "{OUT:%a}" pp_vdecl v

  let pp_expr :

      type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =

   fun m fmt -> function

    | Val v ->

      pp_val m fmt v

    | Tag t ->

      pp_print_string fmt t

    | Var v ->

      pp_vdecl fmt v

    | Memory r ->

      pp_reg fmt r

    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =

     fun fmt e -> pp_expr m fmt e

      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f

        (pp_print_option

           ~none:(fun fmt () -> pp_print_string fmt "SELF")

           pp_print_string)

        inst

        (pp_print_option pp_print_int)

        i

        (pp_print_parenthesized pp_expr)

        (inputs @ locals @ outputs)

      fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst

      fprintf fmt "MemoryPack_%a<%a>%a" pp_print_string f

        (pp_print_option

           ~none:(fun fmt () -> pp_print_string fmt "SELF")

           pp_print_string)

        inst

        (pp_print_option pp_print_int)

        i

    | Initialization ->

      ()

    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =

     fun fmt e -> pp_expr m fmt e

      | True ->

        pp_print_string fmt "true"

      | False ->

        pp_print_string fmt "false"

        pp_print_list

          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")

          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)

          fmt fs

        pp_print_list

          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")

          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)

          fmt fs

          (pp_comma_list Printers.pp_var)

          xs pp_spec a

          (pp_comma_list Printers.pp_var)

          xs pp_spec a

        fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])" pp_expr e

          pp_spec a pp_spec b

        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])

    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut

  else pp_print_nothing

  (match i.instr_desc with

  | MLocalAssign (i, v) ->

    fprintf fmt "%s := %a" i.var_id pp_val v

  | MStateAssign (i, v) ->

    fprintf fmt "{%s} := %a" i.var_id pp_val v

  | MResetAssign b ->

    fprintf fmt "RESET := %a" pp_print_bool b

  | MSetReset i ->

    fprintf fmt "set_reset %s" i

  | MClearReset ->

    fprintf fmt "clear_reset %s" m.mname.node_id

  | MNoReset i ->

    fprintf fmt "noreset %s" i

  | MStep (il, i, vl) ->

    fprintf fmt "%a := %s%a" (pp_comma_list pp_vdecl) il i

      (pp_print_parenthesized pp_val)

      vl

  | MBranch (g, hl) ->

    fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}" pp_val g

      (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch)

      hl

  | MComment s ->

    pp_print_string fmt s

  | MSpec s ->

    pp_print_string fmt ("@" ^ s));

  (* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original

     expr: %a" Printers.pp_expr e *)

  (match i.lustre_eq with

  | None ->

    ()

  | Some eq ->

    fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq);

    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m))

    h

let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)

    let decl, _ = List.assoc id m.mcalls in

  with Not_found ->

    (* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n))

       m.mcalls *)

let machine_vars m =

  m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory

    "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ \

    (pp_comma_list Printers.pp_var)

    s.step_inputs

    (pp_comma_list Printers.pp_var)

    s.step_outputs

    (pp_comma_list Printers.pp_var)

    s.step_locals

    s.step_checks (pp_instrs m) s.step_instrs

    (pp_comma_list (pp_val m))

    s.step_asserts

  fprintf fmt "%s<%a>" (node_name node)

    (pp_comma_list Dimension.pp_dimension)

    args

let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2

  fprintf fmt "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]" pp_print_string

    mp.mpname.node_id

    (pp_print_option pp_print_int)

    mp.mpindex (PrintSpec.pp_spec m) mp.mpformula

    fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m))

  else pp_print_nothing fmt

  fprintf fmt "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" pp_print_string

    t.tname.node_id

    (pp_print_option pp_print_int)

    t.tindex

    (pp_print_parenthesized pp_vdecl)

    (t.tinputs @ t.tlocals @ t.toutputs)

    fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))

  else pp_print_nothing fmt

    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    \

     : %a@ step     :@   @[<v 2>%a@]@ spec     : @[<v>%t@ %a@ @ %a@]@ annot    \

     : @[%a@]@]@ "

    (pp_comma_list Printers.pp_var)

    m.mmemory

    (pp_comma_list pp_instance)

    m.minstances (pp_instrs m) m.minit (pp_instrs m) m.mconst (pp_step m)

    m.mstep

    (fun fmt ->

      match m.mspec.mnode_spec with

      | None ->

        ()

      | Some (NodeSpec id) ->

        fprintf fmt "cocospec: %s" id

      | Some (Contract spec) ->

        Printers.pp_spec fmt spec)

    (pp_memory_packs m) m.mspec.mmemory_packs (pp_transitions m)

    m.mspec.mtransitions

    (pp_print_list Printers.pp_expr_annot)

    m.mannot

let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine

  | Cst _ ->

    true

  | Fun (_, args) ->

    Basic_library.is_value_internal_fun v && List.for_all is_const_value args

  | _ ->

    false

  ( n.node_dec_stateless,

    try Utils.desome n.node_stateless

    with _ ->

      failwith ("stateless status of machine " ^ n.node_id ^ " not computed") )

let get_stateless_status_top_decl td =

  match td.top_decl_desc with

  | Node n ->

    get_stateless_status_node n

  | ImportedNode n ->

    n.nodei_stateless, false

  | _ ->

    true, false

let get_stateless_status m = get_stateless_status_node m.mname

let mk_val v t = { value_desc = v; value_type = t; value_annot = None }

let vdecl_to_val vd = mk_val (Var vd) vd.var_type

let vdecls_to_vals = List.map vdecl_to_val

    (MBranch (c, [ tag_true, t; tag_false, e ]))

let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)

  mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))

  let var_state =

    dummy_var_decl state Type_predef.type_bool

    (* (Types.new_ty Types.Tbool) *)

  in

  assert (var_input1.var_type = var_input2.var_type);

  let t_arg = var_input1.var_type in

  (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de

     reprendre le type des variables non ? *)

    mmemory = [ var_state ];

    minit = [ mkinstr (MStateAssign (var_state, cst true)) ];

    mstep =

      {

        step_inputs = Arrow.arrow_desc.node_inputs;

        step_outputs = Arrow.arrow_desc.node_outputs;

        step_locals = [];

        step_checks = [];

        step_instrs =

          [

            mk_conditional

              (mk_val (Var var_state) Type_predef.type_bool)

              (List.map mkinstr

                 [

                   MStateAssign (var_state, cst false);

                   MLocalAssign (var_output, mk_val (Var var_input1) t_arg);

                 ])

              (List.map mkinstr

                 [ MLocalAssign (var_output, mk_val (Var var_input2) t_arg) ]);

          ];

        step_asserts = [];

      };

    msch = None;

    node_inputs = [];

    node_outputs = [];

    node_locals = [];

    node_stmts = [];

  }

    mstep =

      {

        step_inputs = [];

        step_outputs = [];

        step_locals = [];

        step_checks = [];

        step_instrs = [];

        step_asserts = [];

      };

    msch = None;

    let o =

      if Stateless.check_node callee then node_name callee

      else

        Printf.sprintf "ni_%d"

          (incr cpt;

           !cpt)

    in

    let o =

      if !Options.ansi && is_generic_node callee then

        Printf.sprintf "%s_inst_%d" o

          (incr cpt;

           !cpt)

      else o

    in

    o

      | Some _ ->

        res

      | None ->

        if m.mname.node_id = name then Some m else None)

  try Utils.desome (get_machine_opt machines node_name)

  with Utils.DeSome ->

    eprintf "Unable to find machine %s in machines %a@.@?" node_name

      (Utils.fprintf_list ~sep:", " (fun fmt m ->

           pp_print_string fmt m.mname.node_id))

      machines;

    assert false

    match

      get_instr_desc

        (List.find

           (fun instr ->

             match get_instr_desc instr with

             | MLocalAssign (v, _) ->

               v == id

             | _ ->

               false)

           m.mconst)

    with

    | MLocalAssign (_, e) ->

      e

    | _ ->

      assert false

    let v = List.find (fun v -> v.var_id = id) m.mmemory in

    mk_val (Var v) v.var_type

  with Not_found -> (

    try

      (* id is a node var *)

      let v = get_node_var id m.mname in

      mk_val (Var v) v.var_type

    with Not_found -> (

      try

        (* id is a constant *)

        let c =

          Corelang.var_decl_of_const

            (const_of_top (Hashtbl.find Corelang.consts_table id))

        in

        mk_val (Var c) c.var_type

      with Not_found ->

        (* id is a tag *)

        let t = Const_tag id in

        mk_val (Cst t) (Typing.type_const loc t)))

  if List.mem f Basic_library.arith_funs then (List.hd args).value_type

  | Dimension.Dbool b ->

    mk_val

      (Cst (Const_tag (if b then tag_true else tag_false)))

      Type_predef.type_bool

  | Dimension.Dint i ->

    mk_val (Cst (Const_int i)) Type_predef.type_int

  | Dimension.Dident v ->

    value_of_ident dim.Dimension.dim_loc m v

    let vargs = List.map (value_of_dimension m) args in

    mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)

  | Dimension.Dite (i, t, e) -> (

    match List.map (value_of_dimension m) [ i; t; e ] with

    | [ vi; vt; ve ] ->

      mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type

    | _ ->

      assert false)

  | Dimension.Dlink dim' ->

    value_of_dimension m dim'

  | _ ->

    assert false

  | Cst (Const_tag t) when t = tag_true ->

    Dimension.mkdim_bool Location.dummy_loc true

  | Cst (Const_tag t) when t = tag_false ->

    Dimension.mkdim_bool Location.dummy_loc false

  | Cst (Const_int i) ->

    Dimension.mkdim_int Location.dummy_loc i

  | Var v ->

    Dimension.mkdim_ident Location.dummy_loc v.var_id

  | Fun (f, args) ->

    Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)

  | _ ->

    assert false

  match hl1, hl2 with

  | [], _ ->

    hl2

  | _, [] ->

    hl1

  | (t1, h1) :: q1, (t2, h2) :: q2 ->

    if t1 < t2 then (t1, h1) :: join_branches q1 hl2

    else if t1 > t2 then (t2, h2) :: join_branches hl1 q2

    else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2

  match get_instr_desc inst1, insts2 with

  | ( MBranch (x1, hl1),

      ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )

    when x1 = x2 ->

    mkinstr

      ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)

      (* TODO on pourrait uniquement concatener les lustres de inst1 et

         hd(inst2) *)

      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))

    :: insts2

  | _ ->

    inst1 :: insts2

let join_guards_list insts = List.fold_right join_guards insts []