mk_equation in hept computes the stateful field.

compiler/heptagon/analysis/statefull.ml

@@ -30,12 +30,22 @@ let message loc kind =
   end;
   raise Errors.Error
 
+
+let stateful_mapfold f acc l =
+  let map_or (l,acc) e =
+    let e,acc' = f false e in
+    e::l, acc or acc'
+  in
+  let l,acc = List.fold_left map_or ([],acc) l in
+  List.rev l, acc
+
+
 let last _ stateful l = match l with
   | Var -> l, stateful
   | Last _ -> l, true
 
-(** @returns whether the exp is stateful. Replaces node calls with
-    the correct Efun or Enode depending on the node signature. *)
+(* Returns whether the exp is stateful.
+   Replaces node calls with the correct Efun or Enode depending on the node signature. *)
 let edesc funs stateful ed =
   let ed, stateful = Hept_mapfold.edesc funs stateful ed in
     match ed with
@@ -47,30 +57,30 @@ let edesc funs stateful ed =
           Eapp({ app with a_op = op }, e_list, r), ty_desc.node_stateful or stateful
       | _ -> ed, stateful
 
-let eqdesc funs acc eqd =
-  let eqd, _ = Hept_mapfold.eqdesc funs acc eqd in
-  match eqd with
-    | Eautomaton st_h_l ->
-      let st_h_l, _ = Misc.mapfold (state_handler_it funs) acc st_h_l in
-      Eautomaton st_h_l, true
-    | _ -> raise Errors.Fallback
+(* Automatons have an hidden state whatever *)
+let eqdesc funs stateful eqd =
+  let eqd, stateful = Hept_mapfold.eqdesc funs stateful eqd in
+  let is_automaton = match eqd with | Eautomaton _ -> true | _ -> false in
+  eqd, stateful or is_automaton
 
+(* update eq_stateful field *)
 let eq funs acc eq =
-  let eq, stateful = Hept_mapfold.eq funs acc eq in
-    { eq with eq_stateful = stateful }, stateful
+  let eq, stateful = Hept_mapfold.eq funs false eq in
+    { eq with eq_stateful = stateful }, stateful or acc
 
+(* update b_stateful field *)
 let block funs acc b =
   let b, stateful = Hept_mapfold.block funs false b in
     { b with b_stateful = stateful }, acc or stateful
 
-(** Strong preemption should be decided with stateless expressions *)
+(* Strong preemption should be decided with stateles expressions *)
 let escape_unless funs acc esc =
   let esc, stateful = Hept_mapfold.escape funs false esc in
     if stateful then
       message esc.e_cond.e_loc Eexp_should_be_stateless;
     esc, acc or stateful
 
-(** Present conditions should be stateless *)
+(* Present conditions should be stateless *)
 let present_handler funs acc ph =
   let p_cond, stateful = Hept_mapfold.exp_it funs false ph.p_cond in
     if stateful then
@@ -79,24 +89,27 @@ let present_handler funs acc ph =
     { ph with p_cond = p_cond; p_block = p_block }, acc
 
 
-(** Funs with states are rejected, nodes without state are set as funs *)
+(* Funs with states are rejected, nodes without state are set as funs *)
 let node_dec funs _ n =
   Idents.enter_node n.n_name;
   let n, stateful = Hept_mapfold.node_dec funs false n in
   if stateful & (not n.n_stateful) then message n.n_loc Eshould_be_a_node;
   if not stateful & n.n_stateful (* update the global env if stateful is not necessary *)
-  then Modules.replace_value n.n_name { (Modules.find_value n.n_name) with Signature.node_stateful = false };
+  then Modules.replace_value n.n_name
+         { (Modules.find_value n.n_name) with Signature.node_stateful = false };
   { n with n_stateful = stateful }, false (* set stateful only if needed *)
 
+let funs =
+  { Hept_mapfold.defaults with
+      edesc = edesc;
+      escape_unless = escape_unless;
+      present_handler = present_handler;
+      eqdesc = eqdesc;
+      last = last;
+      eq = eq;
+      block = block;
+      node_dec = node_dec; }
 
 let program p =
-  let funs =
-    { Hept_mapfold.defaults with
-        edesc = edesc;
-        escape_unless = escape_unless;
-        present_handler = present_handler;
-        eqdesc = eqdesc;
-        last = last;
-        eq = eq; block = block; node_dec = node_dec } in
   let p, _ = Hept_mapfold.program_it funs false p in
-    p
+  p

compiler/heptagon/heptagon.ml

@@ -143,7 +143,7 @@ type contract = {
 
 type node_dec = {
   n_name      : qualname;
-  n_stateful : bool;
+  n_stateful  : bool;
   n_input     : var_dec list;
   n_output    : var_dec list;
   n_contract  : contract option;
@@ -172,7 +172,7 @@ and program_desc =
 type signature = {
   sig_name      : qualname;
   sig_inputs    : arg list;
-  sig_stateful : bool;
+  sig_stateful  : bool;
   sig_outputs   : arg list;
   sig_params    : param list;
   sig_loc       : location }
@@ -188,7 +188,7 @@ and interface_desc =
   | Itypedef of type_dec
   | Iconstdef of const_dec
   | Isignature of signature
-
+(*
 (* Helper functions to create AST. *)
 let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty  =
   { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
@@ -203,14 +203,14 @@ let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args =
 let mk_type_dec name desc =
   { t_name = name; t_desc = desc; t_loc = no_location; }
 
-let mk_equation ?(stateful = true) desc =
+let mk_equation stateful desc =
   { eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
 
 let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty =
   { v_ident = name; v_type = ty; v_clock = clock;
     v_last = last; v_loc = no_location }
 
-let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs =
+let mk_block stateful ?(defnames = Env.empty) ?(locals = []) eqs =
   { b_local = locals; b_equs = eqs; b_defnames = defnames;
     b_stateful = stateful; b_loc = no_location; }
 
@@ -222,11 +222,12 @@ let dtrue =
 let mk_ifthenelse e1 e2 e3 =
   { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }
 
-let mk_simple_equation pat e =
-  mk_equation ~stateful:false (Eeq(pat, e))
+let mk_simple_equation stateful pat e =
+  mk_equation stateful (Eeq(pat, e))
+
+let mk_switch_equation stateful e l =
+  mk_equation stateful (Eswitch (e, l))
 
-let mk_switch_equation ?(stateful = true) e l =
-  mk_equation ~stateful:stateful (Eswitch (e, l))
 
 let mk_signature name ins outs stateful params loc =
   { sig_name = name;
@@ -265,3 +266,4 @@ let vars_pat pat =
 let rec vd_mem n = function
   | [] -> false
   | vd::l -> vd.v_ident = n or (vd_mem n l)
+*)

compiler/heptagon/parsing/hept_scoping.ml

@@ -150,6 +150,18 @@ struct
 end
 
 
+let mk_app ?(params=[]) ?(unsafe=false) op =
+  { Heptagon.a_op = op; Heptagon.a_params = params; Heptagon.a_unsafe = unsafe }
+
+let mk_signature name ins outs stateful params loc =
+  { Heptagon.sig_name = name;
+    Heptagon.sig_inputs = ins;
+    Heptagon.sig_stateful = stateful;
+    Heptagon.sig_outputs = outs;
+    Heptagon.sig_params = params;
+    Heptagon.sig_loc = loc }
+
+
 (** Function to build the defined static parameters set *)
 let build_const loc vd_list =
   let _add_const_var loc c local_const =
@@ -250,7 +262,7 @@ and translate_desc loc env = function
   | Eapp ({ a_op = op; a_params = params; }, e_list) ->
       let e_list = List.map (translate_exp env) e_list in
       let params = List.map (expect_static_exp) params in
-      let app = Heptagon.mk_app ~params:params (translate_op op) in
+      let app = mk_app ~params:params (translate_op op) in
       Heptagon.Eapp (app, e_list, None)
 
   | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) ->
@@ -258,7 +270,7 @@ and translate_desc loc env = function
       let pe_list = List.map (translate_exp env) pe_list in
       let n = expect_static_exp n in
       let params = List.map (expect_static_exp) params in
-      let app = Heptagon.mk_app ~params:params (translate_op op) in
+      let app = mk_app ~params:params (translate_op op) in
       Heptagon.Eiterator (translate_iterator_type it,
                           app, n, pe_list, e_list, None)
   | Ewhen (e, c, ce) ->
@@ -477,7 +489,7 @@ let translate_signature s =
   let o = List.map translate_arg s.sig_outputs in
   let p = params_of_var_decs s.sig_params in
   add_value n (Signature.mk_node i o s.sig_stateful p);
-  Heptagon.mk_signature n i o s.sig_stateful p s.sig_loc
+  mk_signature n i o s.sig_stateful p s.sig_loc
 
 
 let translate_interface_desc = function

compiler/heptagon/transformations/automata.ml

@@ -15,6 +15,7 @@ open Types
 open Names
 open Idents
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 open Initial
 open Modules

compiler/heptagon/transformations/completion.ml

@@ -11,6 +11,7 @@
 open Misc
 open Heptagon
 open Global_mapfold
+open Hept_utils
 open Hept_mapfold
 open Idents
 

compiler/heptagon/transformations/inline.ml

@@ -13,6 +13,7 @@ open Signature
 open Types
 open Names
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 
 let to_be_inlined s = !Misc.flatten || (List.mem s !Misc.inline)
@@ -56,8 +57,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
   | Eapp ({ a_op = Enode nn; } as op, argl, rso) when to_be_inlined nn ->
       let add_reset eq = match rso with
         | None -> eq
-        | Some x -> mk_equation ~stateful:false
-            (Ereset (mk_block [eq], x)) in
+        | Some x -> mk_equation (Ereset (mk_block [eq], x)) in
 
       let ni = mk_unique_node (env nn) in
 
@@ -79,8 +79,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
 
         fst (Hept_mapfold.node_dec funs () ni) in
 
-      let mk_input_equ vd e =
-        mk_equation ~stateful:false (Eeq (Evarpat vd.v_ident, e)) in
+      let mk_input_equ vd e = mk_equation (Eeq (Evarpat vd.v_ident, e)) in
       let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in
 
       let newvars = ni.n_input @ ni.n_block.b_local @ ni.n_output @ newvars

compiler/heptagon/transformations/itfusion.ml

@@ -4,6 +4,7 @@ open Names
 open Static
 open Hept_mapfold
 open Heptagon
+open Hept_utils
 (* Iterator fusion *)
 
 let is_stateful app =
@@ -87,8 +88,7 @@ let mk_call app acc_eq_list =
     | 1 -> new_inp, e, acc_eq_list
     | _ ->
         (*more than one output, we need to create a new equation *)
-        let eq = mk_equation ~stateful:(is_stateful app)
-                               (Eeq(pat_of_vd_list new_outp, e)) in
+        let eq = mk_equation (Eeq(pat_of_vd_list new_outp, e)) in
         let e = tuple_of_vd_list new_outp in
           new_inp, e, eq::acc_eq_list
 
@@ -125,8 +125,7 @@ let edesc funs acc ed =
           let _, outp = get_node_inp_outp f in
           let f_out_type = Types.prod (List.map (fun v -> v.v_type) outp) in
           let call = mk_exp (Eapp(f, largs, None)) f_out_type in
-          let eq = mk_equation ~stateful:(is_stateful f)
-                             (Eeq(pat_of_vd_list outp, call)) in
+          let eq = mk_equation (Eeq(pat_of_vd_list outp, call)) in
           (* create the lambda *)
           let anon = mk_app
             (Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in

compiler/heptagon/transformations/last.ml

@@ -8,6 +8,7 @@
 (**************************************************************************)
 (* removing accessed to shared variables (last x)      *)
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 open Idents
 
@@ -23,8 +24,7 @@ let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } =
     | Last(default) ->
         let lastn = fresh n in
         let eq = mk_equation (Eeq (Evarpat lastn,
-                                   mk_exp (Epre (default,
-                                                 mk_exp (Evar n) t)) t)) in
+                                   mk_exp (Epre (default, mk_exp (Evar n) t)) t)) in
         eq:: eq_list,
         Env.add n lastn env,
         (mk_var_dec lastn t) :: v

compiler/heptagon/transformations/normalize.ml

@@ -11,6 +11,7 @@ open Names
 open Idents
 open Location
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 open Types
 open Clocks
@@ -75,16 +76,14 @@ let equation (d_list, eq_list) e =
           let var_list, d_list =
             mapfold (fun d_list ty -> add_one_var ty d_list) d_list ty_list in
           let pat_list = List.map (fun n -> Evarpat n) var_list in
-          let eq_list = (mk_equation ~stateful:(is_stateful e)
-                            (Eeq (Etuplepat pat_list, e))) :: eq_list in
+          let eq_list = (mk_equation (Eeq (Etuplepat pat_list, e))) :: eq_list in
           let e_list = List.map2
             (fun n ty -> mk_exp (Evar n) ty) var_list ty_list in
           let e = Eapp(mk_app Etuple, e_list, None) in
             (d_list, eq_list), e
       | _ ->
           let n, d_list = add_one_var e.e_ty d_list in
-          let eq_list = (mk_equation ~stateful:(is_stateful e)
-                            (Eeq (Evarpat n, e))) :: eq_list in
+          let eq_list = (mk_equation (Eeq (Evarpat n, e))) :: eq_list in
             (d_list, eq_list), Evar n
 
 (* [(e1,...,ek) when C(n) = (e1 when C(n),...,ek when C(n))] *)
@@ -243,7 +242,7 @@ and merge context e x c_e_list =
 and distribute ((d_list, eq_list) as context) eq pat e =
   let dist_e_list pat_list e_list =
     let mk_eq pat e =
-      mk_equation ~stateful:eq.eq_stateful (Eeq (pat, e))
+      mk_equation (Eeq (pat, e))
     in
     let dis context eq = match eq.eq_desc with
       | Eeq (pat, e) -> distribute context eq pat e
@@ -258,7 +257,7 @@ and distribute ((d_list, eq_list) as context) eq pat e =
       | Etuplepat(pat_list), Econst { se_desc = Stuple se_list } ->
           dist_e_list pat_list (exp_list_of_static_exp_list se_list)
       | _ ->
-          let eq = { eq with eq_desc = Eeq(pat, e) } in
+          let eq = mk_equation ~loc:eq.eq_loc (Eeq(pat, e)) in
             d_list,  eq :: eq_list
 
 and translate_eq ((d_list, eq_list) as context) eq = match eq.eq_desc with
@@ -267,8 +266,10 @@ and translate_eq ((d_list, eq_list) as context) eq = match eq.eq_desc with
         distribute context eq pat e
   | Eblock b ->
       let v, eqs = translate_eq_list [] b.b_equs in
-      let eq = { eq with eq_desc = Eblock { b with b_local = v @ b.b_local; b_equs = eqs} } in
-        d_list, eq :: eq_list
+      let eq =
+        mk_equation ~loc:eq.eq_loc (Eblock { b with b_local = v @ b.b_local; b_equs = eqs})
+      in
+      d_list, eq :: eq_list
   | _ -> Misc.internal_error "normalize" 0
 
 and translate_eq_list d_list eq_list =

compiler/heptagon/transformations/present.ml

@@ -9,14 +9,14 @@
 (* removing present statements *)
 
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 
 let translate_present_handlers handlers cont =
   let translate_present_handler { p_cond = e; p_block = b } cont =
     let stateful = b.b_stateful or cont.b_stateful in
-      mk_block ~stateful:stateful ~defnames:b.b_defnames
-        [mk_switch_equation
-           ~stateful:stateful e
+      mk_block ~defnames:b.b_defnames
+        [mk_switch_equation e
            [{ w_name = Initial.ptrue; w_block = b };
             { w_name = Initial.pfalse; w_block = cont }]] in
   let b = List.fold_right translate_present_handler handlers cont in

compiler/heptagon/transformations/reset.ml

@@ -13,6 +13,7 @@
 open Misc
 open Idents
 open Heptagon
+open Hept_utils
 open Types
 open Initial
 
@@ -51,15 +52,13 @@ let default e =
     | _ -> None
 
 
-(* Stop mapfold if not stateful *)
-let exp funs (res,s) e = if s then Hept_mapfold.exp funs (res,s) e else e, (res,s)
-
-let edesc funs (res,s) ed =
-  let ed, _ = Hept_mapfold.edesc funs (res,s) ed in
+let edesc funs res ed =
+  let ed, _ = Hept_mapfold.edesc funs res ed in
   let ed = match ed with
     | Efby (e1, e2) ->
         (match res, e1 with
-         | None, { e_desc = Econst c } -> (* no reset : [if res] useless, the initialization is suffisant *)
+         | None, { e_desc = Econst c } ->
+            (* no reset : [if res] useless, the initialization is sufficient *)
             Epre(Some c, e2)
          | _ -> ifres res e1 { e2 with e_desc = Epre(default e1, e2) })
     | Eapp({ a_op = Earrow }, [e1;e2], _) ->
@@ -70,26 +69,27 @@ let edesc funs (res,s) ed =
         Eiterator(it, op, n, pe_list, e_list, merge_resets res re)
     | _ -> ed
   in
-    ed, (res,s)
+    ed, res
 
 
+(* do nothing when not stateful *)
+let eq funs res eq =
+  if eq.eq_stateful then Hept_mapfold.eq funs res eq else eq, res
 
-let eq funs (res,_) eq = Hept_mapfold.eq funs (res,eq.eq_stateful) eq
+(* do nothing when not stateful *)
+let block funs res b =
+  if b.b_stateful then Hept_mapfold.block funs res b else b, res
 
-(* Transform reset blocks in blocks with reseted exps, create a var to store the reset condition evaluation. *)
-let eqdesc funs (res,stateful) = function
+(* Transform reset blocks in blocks with reseted exps,
+   create a var to store the reset condition evaluation. *)
+let eqdesc funs res = function
   | Ereset(b, e) ->
-      if stateful
-      then (
-        let e, _ = Hept_mapfold.exp_it funs (res,true) e in
+        let e, _ = Hept_mapfold.exp_it funs res e in
         let e, vd, eq = bool_var_from_exp e in
         let r = merge_resets res (Some e) in
-        let b, _ = Hept_mapfold.block_it funs (r,true) b in
+        let b, _ = Hept_mapfold.block_it funs r b in
         let b = { b with b_equs = eq::b.b_equs; b_local = vd::b.b_local; b_stateful = true } in
-        Eblock(b), (res,true))
-      else (
-        let b, _ = Hept_mapfold.block_it funs (res,false) b in
-        Eblock(b), (res,false))
+        Eblock(b), res
   | Eswitch _ | Eautomaton _ | Epresent _ ->
       Format.eprintf "[reset] should be done after [switch automaton present]";
       assert false
@@ -97,8 +97,10 @@ let eqdesc funs (res,stateful) = function
 
 
 let program p =
+  Printf.printf "program :\n";
+  Hept_printer.print stdout p;
   let funs = { Hept_mapfold.defaults with
                  Hept_mapfold.eq = eq; Hept_mapfold.eqdesc = eqdesc;
-                 Hept_mapfold.edesc = edesc; Hept_mapfold.exp = exp } in
-  let p, _ = Hept_mapfold.program_it funs (None,false) p in
+                 Hept_mapfold.edesc = edesc } in
+  let p, _ = Hept_mapfold.program_it funs None p in
     p

compiler/heptagon/transformations/switch.ml

@@ -41,6 +41,7 @@ with one defined var y ( defnames = {y} ) and used var x
 
 open Misc
 open Heptagon
+open Hept_utils
 open Hept_mapfold
 
 (** Give the var [name] and a [constructor], returns fresh [name_constr] *)
@@ -127,7 +128,7 @@ let level_up defnames constr h =
   fold (fun n _ new_h -> ident_level_up n new_h) defnames empty
 
 let add_to_vds defnames h vds =
-  fold (fun n nn acc -> (Heptagon.mk_var_dec nn (find n defnames))::acc) vds h
+  fold (fun n nn acc -> (mk_var_dec nn (find n defnames))::acc) vds h
 
 end
 
@@ -170,8 +171,8 @@ let eqdesc funs (env,h) eqd = match eqd with
       let ck = fresh_clock_id () in
       let e, (env,h) = exp_it funs (env,h) e in
       let ck_e = { e with e_desc = Evar ck } in
-      let locals = [Heptagon.mk_var_dec ck e.e_ty] in
-      let equs = [Heptagon.mk_equation (Eeq (Evarpat ck, e))] in
+      let locals = [mk_var_dec ck e.e_ty] in
+      let equs = [mk_equation (Eeq (Evarpat ck, e))] in
 
       (* typing have proved that defined variables are the same among states *)
       let defnames = (List.hd sw_h_l).w_block.b_defnames in
@@ -186,7 +187,7 @@ let eqdesc funs (env,h) eqd = match eqd with
         (* mapfold with updated envs *)
         let b_eq, (_,h) = block_it funs (env,h) sw_h.w_block in
         (* inline the handler as a block *)
-        let equs = (Heptagon.mk_equation (Eblock b_eq))::equs in
+        let equs = (mk_equation (Eblock b_eq))::equs in
         (* add to the locals the new vars from leveling_up *)
         let locals = Rename.add_to_vds defnames locals h  in
         ((constr,h)::c_h_l, locals, equs) in
@@ -197,15 +198,15 @@ let eqdesc funs (env,h) eqd = match eqd with
       let new_merge n equs =
         let ty = (Idents.Env.find n defnames) in
         let c_h_to_c_e (constr,h) =
-          constr, Heptagon.mk_exp (Evar (Rename.rename n h)) ty in
+          constr, mk_exp (Evar (Rename.rename n h)) ty in
         let c_e_l = List.map c_h_to_c_e c_h_l in
-        let merge = Heptagon.mk_exp (Emerge (ck_e, c_e_l)) ty in
-        (Heptagon.mk_equation (Eeq (Evarpat n, merge))) :: equs in
+        let merge = mk_exp (Emerge (ck_e, c_e_l)) ty in
+        (mk_equation (Eeq (Evarpat n, merge))) :: equs in
       let equs =
         Idents.Env.fold (fun n _ equs -> new_merge n equs) defnames equs in
 
       (* return the transformation in a block *)
-      let b = Heptagon.mk_block ~defnames:defnames ~locals:locals equs in
+      let b = mk_block ~defnames:defnames ~locals:locals equs in
       Eblock b, (env,h)
   | _ -> raise Errors.Fallback
 

compiler/minils/minils.ml

@@ -49,8 +49,7 @@ and extvalue_desc =
   | Wconst of static_exp
   | Wvar of var_ident
   | Wfield of extvalue * field_name
-  | Wwhen of extvalue * constructor_name * var_ident
-                       (** extvalue when Constructor(ident) *)
+  | Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *)
 
 and exp = {
   e_desc      : edesc;