CristalCaveGem » LustreC

let ff = Format.fprintf

module LustrePrinter (Vars : sig

  val state_vars : ActiveStates.Vars.t

  val global_vars : GlobalVarDef.t list

end) : TransformerType = struct

  type t_base = {

    statements : Lustre_types.statement list;

    assert_false : bool;

  }

  type t = name_t -> name_t -> ActiveStates.Vars.t * t_base

    ( (fun () ->

        incr cpt;

        Format.sprintf "loc_%i" !cpt),

      fun () -> cpt := 0 )

    ( (fun () ->

        incr cpt;

        Format.sprintf "aut_%i" !cpt),

      fun () -> cpt := 0 )

    Format.fprintf fmt "%s%t" prefix (fun fmt ->

        Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)

  let vars_to_ident_list ?(prefix = "") vars =

    List.map (fun p -> var_to_ident prefix p) (ActiveStates.Vars.elements vars)

  let mkvar name typ =

    Corelang.mkvar_decl loc

      ( name,

        typ,

        Corelang.mkclock loc Lustre_types.Ckdec_any,

        false,

        None,

        None (*"__no_parent__" *) )

  let var_to_vdecl ?(prefix = "") var typ = mkvar (var_to_ident prefix var) typ

  let state_vars_to_vdecl_list ?(prefix = "") vars =

    List.map

      (fun v -> var_to_vdecl ~prefix v bool_type)

    ActiveStates.Vars.fold

      (fun v accu ->

        state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars @ accu)

      locs []

  (* TODO: declare global vars *)

  let expr_of_bool b =

    mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))

  let mkstmt_eq lhs_vars ?(prefix_lhs = "") rhs =

    {

      statements =

        [

          Lustre_types.Eq

            (mkeq

               ( vars_to_ident_list ~prefix:prefix_lhs lhs_vars,

                 (* lhs *)

                 rhs (* rhs *) ));

        ];

      assert_false = false;

      [

        {

          Lustre_types.assert_expr = expr_of_bool false;

          assert_loc = Location.dummy_loc;

        };

      ]

    else []

  let var_to_expr ?(prefix = "") p =

  let vars_to_exprl ?(prefix = "") vars =

    List.map (fun p -> var_to_expr ~prefix p) (ActiveStates.Vars.elements vars)

      (Lustre_types.TypeDef

         {

           Lustre_types.tydef_id = "event_type";

           tydef_desc = Lustre_types.Tydec_int;

         })

  let event_type =

    {

      Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";

      Lustre_types.ty_dec_loc = Location.dummy_loc;

    }

  let event_var = mkvar "event" event_type

    with Not_found ->

      nb

    ( ActiveStates.Vars.empty,

      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs )

    ActiveStates.Vars.empty, { tr with assert_false = true }

    ( ActiveStates.Vars.add [ l ] (ActiveStates.Vars.union vars1 vars2),

      {

        statements = tr1.statements @ tr2.statements;

        assert_false = tr1.assert_false || tr2.assert_false;

      } )

  let pp_name : type c. c call_t -> c -> unit =

   fun call ->

    match call with

    | Ecall ->

      fun (p, p', f) ->

        Format.fprintf Format.str_formatter "theta%a%a%a_%a" pp_call call

          (pp_path "_from_") p (pp_path "_to_") p' pp_frontier f

    | Dcall ->

      fun p ->

        Format.fprintf Format.str_formatter "theta%a%a" pp_call call

          (pp_path "_from_") p

    | Xcall ->

      fun (p, f) ->

        Format.fprintf Format.str_formatter "theta%a%a_%a" pp_call call

          (pp_path "_from_") p pp_frontier f

  let mkcall' : type c. name_t -> name_t -> c call_t -> c -> t_base =

   fun sin sout call arg ->

    pp_name call arg;

    let funname = Format.flush_str_formatter () in

    let args =

      Corelang.expr_of_vdecl event_var

      :: vars_to_exprl ~prefix:sin Vars.state_vars

    in

    let rhs = mkpredef_call funname args in

    mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

    | Action.Call (c, a) ->

      mkcall' sin sout c a

    | Action.Quote a ->

      (* TODO: check. This seems to be innappropriate *)

      (* let funname = "action_" ^ a.ident in let args = vars_to_exprl

         ~prefix:sin Vars.state_vars in let rhs = mkpredef_call funname args in

         mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs *)

      { statements = a.defs; assert_false = false }

    | Action.Open p ->

      let vars' = ActiveStates.Vars.remove p Vars.state_vars in

      (* eq1: sout_p = true *)

      let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool true) in

      (* eq2: sout_xx = sin_xx *)

      let expr_list = vars_to_exprl ~prefix:sin vars' in

      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

      let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in

      {

        statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];

        assert_false = false;

      }

    | Action.Close p ->

      let vars' = ActiveStates.Vars.remove p Vars.state_vars in

      (* eq1: sout_p = false *)

      let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool false) in

      (* eq2: sout_xx = sin_xx *)

      let expr_list = vars_to_exprl ~prefix:sin vars' in

      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

      let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in

      {

        statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];

        assert_false = false;

      }

    | Action.Nil ->

      let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in

      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

  let eval_act _kenv (action : act_t)

      (*Format.printf "----- action = %a@." Action.pp_act action;*)

        sin sout =

    ActiveStates.Vars.empty, mkact' action sin sout

    | Condition.True ->

      expr_of_bool true

    | Condition.Active p ->

      var_to_expr ~prefix:sin p

    | Condition.Event e ->

      mkpredef_call "="

        [

          Corelang.expr_of_vdecl event_var;

          mkexpr

            (Lustre_types.Expr_const

               (Lustre_types.Const_int (get_event_const e)));

        ]

    | Condition.Neg cond ->

      mkpredef_call "not" [ mkcond' sin cond ]

    | Condition.And (cond1, cond2) ->

      mkpredef_call "&&" [ mkcond' sin cond1; mkcond' sin cond2 ]

    | Condition.Quote c ->

      c.expr

  (* TODO: shall we prefix with sin ? *)

  let eval_cond condition (ok : t) ko sin sout =

    ( ActiveStates.Vars.empty,

      {

        statements =

          [

            (let handler_default_mode =

               (* Default mode : CenterPoint *)

               let handler_default_mode_unless =

                 [

                   loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut;

                   ( loc,

                     mkcond' sin (Condition.Neg condition),

                     true (* restart *),

                     "NotCond_" ^ aut );

                 ]

               in

               Automata.mkhandler loc

                 (* location *)

                 ("CenterPoint_" ^ aut)

                 (* state name *)

                 handler_default_mode_unless (* unless *) [] (* until *) []

                 (* locals *)

                 (tr0.statements, base_to_assert tr0, [])

               (* stmts, asserts, annots *)

             in

             let handler_cond_mode =

               (* Cond mode *)

               let handler_cond_mode_until =

                 [

                   ( loc,

                     expr_of_bool true,

                     true (* restart *),

                     "CenterPoint_" ^ aut );

                 ]

               in

               Automata.mkhandler loc

                 (* location *)

                 ("Cond_" ^ aut)

                 (* state name *)

                 [] (* unless *) handler_cond_mode_until

                 (* until *)

                 (mk_locals vars1)

                 (* locals *)

                 (tr1.statements, base_to_assert tr1, [])

               (* stmts, asserts, annots *)

             in

             let handler_notcond_mode =

               (* NotCond mode *)

               let handler_notcond_mode_until =

                 [

                   ( loc,

                     expr_of_bool true,

                     true (* restart *),

                     "CenterPoint_" ^ aut );

                 ]

               in

               Automata.mkhandler loc

                 (* location *)

                 ("NotCond_" ^ aut)

                 (* state name *)

                 [] (* unless *) handler_notcond_mode_until

                 (* until *)

                 (mk_locals vars2)

                 (* locals *)

                 (tr2.statements, base_to_assert tr2, [])

               (* stmts, asserts, annots *)

             in

             let handlers =

               [ handler_default_mode; handler_cond_mode; handler_notcond_mode ]

             in

             Aut (Automata.mkautomata loc aut handlers));

          ];

        assert_false = false;

      } )

   *   in tr *)

  let mkcomponent : type c. c call_t -> c -> t -> Lustre_types.program_t =

   fun call args tr ->

    reset_loc ();

    let vars', tr' = tr "sin_" "sout_" in

    pp_name call args;

    let funname = Format.flush_str_formatter () in

    let inputs =

      event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars

    in

    let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in

    let node =

      Corelang.mktop

        (Lustre_types.Node

           {

             Lustre_types.node_id = funname;

             node_type = Types.new_var ();

             node_clock = Clocks.new_var true;

             node_inputs = inputs;

             node_outputs = outputs;

             node_locals = mk_locals vars';

             (* TODO: add global vars *)

             node_gencalls = [];

             node_checks = [];

             node_stmts = tr'.statements;

             node_asserts = base_to_assert tr';

             node_dec_stateless = false;

             node_stateless = None;

             node_spec = None;

             node_annot = [];

             node_iscontract = false;

           })

    in

    [ node ]

  (* TODO C'est pas evident. Il faut faire les choses suivantes: - rajouter dans

     un ensemble les variables manipulées localement - on doit comprendre

     comment les variables globales sont injectées dans le modele final: - le

     node principal doit uniquement les afficher. Il peut les initialiser avec

     les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.

     - elles peuvent/doivent etre dans input et output de ce node thetacallD *)

        let init_state_false =

          List.map

            (fun _ -> expr_of_bool false)

            (ActiveStates.Vars.elements Vars.state_vars)

        in

        let init_globals =

          List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars

        in

        mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))

      let args =

        Corelang.expr_of_vdecl event_var

        :: vars_to_exprl ~prefix:"sout_" Vars.state_vars

      let pre_call_expr = mkexpr (Lustre_types.Expr_pre call_expr) in

    let inputs = List.map Corelang.copy_var_decl [ event_var ] in

      Corelang.mktop

        (Lustre_types.Node

           {

             Lustre_types.node_id = "principal_loop";

             node_type = Types.new_var ();

             node_clock = Clocks.new_var true;

             node_inputs = inputs;

             node_outputs = outputs;

             node_locals = [];

             (* TODO: add global vars *)

             node_gencalls = [];

             node_checks = [];

             node_asserts = base_to_assert call_stmt;

             node_stmts = call_stmt.statements;

             node_dec_stateless = false;

             node_stateless = None;

             node_spec = None;

             node_annot = [];

             node_iscontract = false;

           })

    event_type_decl :: mkcomponent Dcall [ "principal" ] tr

    @ [ mk_main_loop () ]