Added when and merge to heptagon. Need tests !

Clocking is still done in minils since it is way simpler.

compiler/global/clocks.ml

@@ -33,7 +33,7 @@ let index = ref 0
 let gen_index () = (incr index; !index)
 
 (** returns a new clock variable *)
-let new_var () = Cvar { contents = Cindex (gen_index ()); }
+let fresh_clock () = Cvar { contents = Cindex (gen_index ()); }
 
 (** returns the canonic (short) representant of a [ck]
     and update it to this value. *)

compiler/global/global_mapfold.ml

@@ -50,6 +50,7 @@ and static_exp_desc funs acc sd = match sd with
       let f_se_l, acc = mapfold aux acc f_se_l in
       Srecord f_se_l, acc
 
+
 and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t
 and ty funs acc t = match t with
   | Tid _ -> t, acc
@@ -58,7 +59,6 @@ and ty funs acc t = match t with
       let t, acc = ty_it funs acc t in
       let se, acc = static_exp_it funs acc se in
       Tarray (t, se), acc
-
 (*
 and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t
 and ct funs acc c = match c with

compiler/global/global_printer.ml

@@ -1,4 +1,5 @@
 open Names
+open Idents
 open Signature
 open Types
 open Clocks
@@ -107,3 +108,17 @@ let print_interface ff =
     (fun key sigtype -> print_interface_value ff key sigtype) m.m_values;
   Format.fprintf ff "@."
 
+let print_ident ff id = Format.fprintf ff "%s" (name id)
+
+ let rec print_ck ff = function
+  | Cbase -> fprintf ff "base"
+  | Con (ck, c, n) ->
+      fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
+  | Cvar { contents = Cindex _ } -> fprintf ff "base"
+  | Cvar { contents = Clink ck } -> print_ck ff ck
+
+let rec print_clock ff = function
+  | Ck ck -> print_ck ff ck
+  | Cprod ct_list ->
+      fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
+

compiler/global/idents.mli

@@ -46,6 +46,3 @@ sig
   include (Set.S with type elt = ident)
   val fprint_t : Format.formatter -> t -> unit
 end
-
-
-val print_ident : Format.formatter -> ident -> unit

compiler/heptagon/analysis/causality.ml

@@ -108,6 +108,13 @@ let rec typing e =
         candlist l
     | Eiterator (_, _, _, e_list, _) ->
         ctuplelist (List.map typing e_list)
+    | Ewhen (e, c, n) ->
+        let t = typing e in
+        cseq (read n) t
+    | Emerge (n, c_e_list) ->
+        let tl = List.map (fun (_,e) -> typing e) c_e_list in
+        cseq (read n) (candlist tl)
+
 
 (** Typing an application *)
 and apply op e_list =

compiler/heptagon/analysis/initialization.ml

@@ -169,6 +169,7 @@ let rec less left_ty right_ty =
 module Printer = struct
   open Format
   open Pp_tools
+  open Global_printer
 
   let rec print_init ff i = match !i with
     | Izero -> fprintf ff "initialized"
@@ -223,7 +224,7 @@ let less_exp e actual_ty expected_ty =
 (** Main typing function *)
 let rec typing h e =
   match e.e_desc with
-    | Econst c -> skeleton izero e.e_ty
+    | Econst _ -> skeleton izero e.e_ty
     | Evar(x) -> IEnv.find_var_typ x h
     | Elast(x) -> IEnv.find_last_typ x h
     | Epre(None, e1) ->
@@ -248,6 +249,16 @@ let rec typing h e =
     | Eiterator (_, _, _, e_list, _) ->
         List.iter (fun e -> initialized_exp h e) e_list;
         skeleton izero e.e_ty
+    | Ewhen (e, _, n) ->
+        let i = imax (itype (IEnv.find_var_typ n h)) (itype (typing h e)) in
+        skeleton i e.e_ty
+    | Emerge (n, c_e_list) ->
+        let i =
+          List.fold_left
+            (fun acc (_, e) -> imax acc (itype (typing h e))) izero c_e_list in
+        let i = imax (itype (IEnv.find_var_typ n h)) i in
+        skeleton i e.e_ty
+
 
 (** Typing an application *)
 and apply h app e_list =

compiler/heptagon/analysis/typing.ml

@@ -20,6 +20,7 @@ open Types
 open Global_printer
 open Heptagon
 open Hept_mapfold
+open Pp_tools
 
 type value = { ty: ty; mutable last: bool }
 
@@ -46,6 +47,9 @@ type error =
   | Eempty_record
   | Eempty_array
   | Efoldi_bad_args of ty
+  | Emerge_missing_constrs of qualname list
+  | Emerge_not_enum of name * ty
+  | Emerge_unexpected_constr of qualname
 
 exception Unify
 exception TypingError of error
@@ -91,6 +95,21 @@ let message loc kind =
         Format.eprintf "%aThe name %s is already defined.@."
           print_location loc
           s
+    | Emerge_missing_constrs cl ->
+        Format.eprintf "%aSome constructors are missing in this merge :@\n\
+            @[%a@]@."
+          print_location loc
+          (print_list_r print_qualname """,""") cl
+    | Emerge_not_enum (n,t) ->
+        Format.eprintf
+          "%aThe merge variable %a should be of an enum type (found %a)@."
+          print_location loc
+          print_name n
+          print_type t
+    | Emerge_unexpected_constr c ->
+        Format.eprintf "%aThe constructor %a is unexpected.@."
+          print_location loc
+          print_qualname c
     | Enon_exaustive ->
         Format.eprintf "%aSome constructors are missing in this \
                         pattern/matching.@."
@@ -166,9 +185,9 @@ let find_with_error find_fun f =
   try find_fun f
   with Not_found -> error (Eundefined(fullname f))
 
-let find_value = find_with_error find_value
-let find_constrs = find_with_error find_constrs
-let find_field = find_with_error find_field
+let find_value v = find_with_error find_value v
+let find_constrs c = Tid (find_with_error find_constrs c)
+let find_field f = find_with_error find_field f
 
 (** Constraints related functions *)
 let (curr_size_constr : size_constraint list ref) = ref []
@@ -393,7 +412,7 @@ and typing_static_exp const_env se =
              Svar ln, cd.Signature.c_type
          with Not_found -> (* or a static parameter *)
            Svar ln, QualEnv.find ln const_env)
-    | Sconstructor c -> Sconstructor c, Tid (find_constrs c)
+    | Sconstructor c -> Sconstructor c, find_constrs c
     | Sfield c -> Sfield c, Tid (find_field c)
     | Sop (op, se_list) ->
         let ty_desc = find_value op in
@@ -423,10 +442,9 @@ and typing_static_exp const_env se =
              | [] -> error (Eempty_record)
              | (f,_)::_ -> struct_info_from_field f
           ) in
-
+          check_static_field_unicity f_se_list;
           if List.length f_se_list <> List.length fields then
             message se.se_loc Esome_fields_are_missing;
-          check_static_field_unicity f_se_list;
           let f_se_list =
             List.map (typing_static_field const_env fields
                         (Tid q)) f_se_list in
@@ -539,6 +557,40 @@ let rec typing const_env h e =
                         , typed_n, typed_e_list, reset), ty
 
       | Eiterator _ -> assert false
+
+      | Ewhen (e, c, n) ->
+          let typed_e, t = typing const_env h e in
+          let tn_expected = find_constrs c in
+          let tn_actual = typ_of_name h n in
+          unify tn_actual tn_expected;
+          Ewhen (typed_e, c, n), t
+
+      | Emerge (n, (c1,e1)::c_e_list) ->
+          let tn_actual = typ_of_name h n in
+          unify tn_actual (find_constrs c1);
+          let typed_e1, t = typing const_env h e1 in
+          let expected_c_list = (* constructors from the type of n *)
+            (match tn_actual with
+              | Tid tc ->
+                  (match find_type tc with
+                    | Tenum cl -> cl
+                    | _ -> message e.e_loc (Emerge_not_enum (name n,tn_actual)))
+              | _ -> message e.e_loc (Emerge_not_enum (name n,tn_actual))) in
+          let expected_c_set =
+            List.fold_left
+              (fun acc c -> QualSet.add c acc) QualSet.empty expected_c_list in
+          let typed_c_e_list, left_c_set =
+            let check_c_e expected_c_set (c,e) =
+              if not (QualSet.mem c expected_c_set)
+              then message e.e_loc (Emerge_unexpected_constr c);
+              (c, expect const_env h t e), QualSet.remove c expected_c_set in
+            mapfold check_c_e expected_c_set c_e_list in
+          if not (QualSet.is_empty left_c_set)
+          then message e.e_loc
+                       (Emerge_missing_constrs (QualSet.elements left_c_set));
+          Emerge (n, (c1,typed_e1)::typed_c_e_list), t
+      | Emerge (_, []) -> assert false
+
     in
       { e with e_desc = typed_desc; e_ty = ty; }, ty
   with
@@ -1017,8 +1069,7 @@ let typing_const_dec cd =
     { cd with c_value = se; c_type = ty }
 
 let program
-    ({ p_opened = opened; p_types = p_type_list;
-       p_nodes = p_node_list; p_consts = p_consts_list } as p) =
+    ({ p_nodes = p_node_list; p_consts = p_consts_list } as p) =
   let typed_cd_list = List.map typing_const_dec p_consts_list in
   let typed_node_list = List.map node p_node_list in
     { p with p_nodes = typed_node_list; p_consts = typed_cd_list }

compiler/heptagon/hept_mapfold.ml

@@ -135,6 +135,16 @@ and edesc funs acc ed = match ed with
       let args, acc = mapfold (exp_it funs) acc args in
       let reset, acc = optional_wacc (exp_it funs) acc reset in
       Eiterator (i, app, param, args, reset), acc
+  | Ewhen (e, c, n) ->
+      let e, acc = exp_it funs acc e in
+      Ewhen (e, c, n), acc
+  | Emerge (n, c_e_list) ->
+      let aux acc (c,e) =
+        let e, acc = exp_it funs acc e in
+        (c,e), acc in
+      let c_e_list, acc = mapfold aux acc c_e_list in
+      Emerge (n, c_e_list), acc
+
 
 
 and app_it funs acc a = funs.app funs acc a

compiler/heptagon/hept_printer.ml

@@ -96,14 +96,14 @@ and print_exp_desc ff = function
   | Econst c -> print_static_exp ff c
   | Epre(None, e) -> fprintf ff "pre %a" print_exp e
   | Epre(Some c, e) ->
-    fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c  print_exp e
+      fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c  print_exp e
   | Efby(e1, e2) ->
-    fprintf ff "@[<2>%a fby@ %a@]" print_exp e1  print_exp e2
+      fprintf ff "@[<2>%a fby@ %a@]" print_exp e1  print_exp e2
   | Eapp(app, args, reset) ->
-    fprintf ff "@[<2>%a@,%a@]"
+      fprintf ff "@[<2>%a@,%a@]"
         print_app (app, args) print_every reset
   | Estruct(f_e_list) ->
-    print_record (print_couple print_qualname print_exp """ = """) ff f_e_list
+      print_record (print_couple print_qualname print_exp """ = """) ff f_e_list
   | Eiterator (it, f, param, args, reset) ->
       fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
         (iterator_to_string it)
@@ -111,6 +111,18 @@ and print_exp_desc ff = function
         print_static_exp param
         print_exp_tuple args
         print_every reset
+  | Ewhen (e, c, n) ->
+      fprintf ff "@[<2>(%a@ when %a(%a))@]"
+        print_exp e print_qualname c print_ident n
+  | Emerge (x, tag_e_list) ->
+      fprintf ff "@[<2>merge %a@ %a@]"
+        print_ident x print_tag_e_list tag_e_list
+
+and print_handler ff c =
+  fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c
+
+and print_tag_e_list ff tag_e_list =
+  fprintf ff "@[%a@]" (print_list print_handler """""") tag_e_list
 
 and print_every ff reset =
   print_opt (fun ff id -> fprintf ff " every %a" print_exp id) ff reset

compiler/heptagon/heptagon.ml

@@ -14,6 +14,7 @@ open Idents
 open Static
 open Signature
 open Types
+open Clocks
 open Initial
 
 type state_name = name
@@ -36,6 +37,10 @@ and desc =
   | Epre of static_exp option * exp
   | Efby of exp * exp
   | Estruct of (field_name * exp) list
+  | Ewhen of exp * constructor_name * var_ident
+    (** exp when Constructor(ident) *)
+  | Emerge of var_ident * (constructor_name * exp) list
+    (** merge ident (Constructor -> exp)+ *)
   | Eapp of app * exp list * exp option
   | Eiterator of iterator_type * app * static_exp * exp list * exp option
 
@@ -106,6 +111,7 @@ and present_handler = {
 and var_dec = {
   v_ident : var_ident;
   v_type  : ty;
+  v_clock : ck;
   v_last  : last;
   v_loc   : location }
 
@@ -187,16 +193,18 @@ let mk_type_dec name desc =
 let mk_equation ?(statefull = true) desc =
   { eq_desc = desc; eq_statefull = statefull; eq_loc = no_location; }
 
-let mk_var_dec ?(last = Var) name ty  =
-  { v_ident = name; v_type = ty;
+let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty =
+  { v_ident = name; v_type = ty; v_clock = ck;
     v_last = last; v_loc = no_location }
 
 let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs =
   { b_local = []; b_equs = eqs; b_defnames = defnames;
     b_statefull = statefull; b_loc = no_location }
 
-let dfalse = mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
-let dtrue = mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
+let dfalse =
+  mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
+let dtrue =
+  mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
 
 let mk_ifthenelse e1 e2 e3 =
   { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }

compiler/heptagon/main/hept_compiler.ml

@@ -36,8 +36,8 @@ let parse_interface lexbuf =
 
 let compile_impl pp p =
   (* Typing *)
-  let p = pass "Typing" true Typing.program p pp in
   let p = silent_pass "Statefullness check" true Statefull.program p in
+  let p = pass "Typing" true Typing.program p pp in
 
   if !print_types then print_interface Format.std_formatter;
 

compiler/heptagon/parsing/hept_scoping.ml

@@ -368,6 +368,7 @@ and translate_var_dec local_const env vd =
     { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name;
       Heptagon.v_type = translate_type vd.v_loc local_const vd.v_type;
       Heptagon.v_last = translate_last local_const vd.v_last;
+      Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *)
       Heptagon.v_loc = vd.v_loc }
 
 and translate_vd_list local_const env =

compiler/heptagon/transformations/reset.ml

@@ -45,10 +45,8 @@ open Initial
    e1 -> e2 is translated into if (true fby false) then e1 else e2
 *)
 
-let mk_bool_var n =
-  mk_exp (Evar n) (Tid Initial.pbool)
-let mk_bool_param n =
-  mk_var_dec n (Tid Initial.pbool)
+let mk_bool_var n = mk_exp (Evar n) (Tid Initial.pbool)
+let mk_bool_param n = mk_var_dec n (Tid Initial.pbool)
 
 let or_op_call e_list = mk_op_app (Efun Initial.por) e_list
 

compiler/main/hept2mls.ml

@@ -247,6 +247,11 @@ let rec translate env
     | Heptagon.Efby _
     | Heptagon.Elast _ ->
         Error.message loc Error.Eunsupported_language_construct
+    | Heptagon.Ewhen (e, c, n) ->
+        mk_exp ~loc:loc ~ty:ty (Ewhen (translate env e, c, n))
+    | Heptagon.Emerge (n, c_e_list) ->
+        mk_exp ~loc:loc ~ty:ty
+          (Emerge (n, List.map (fun (c,e) -> c, translate env e) c_e_list))
 
 let rec translate_pat = function
   | Heptagon.Evarpat(n) -> Evarpat n

compiler/main/mls2obc.ml

@@ -422,8 +422,6 @@ let translate_contract map mem_vars =
         {
           Minils.c_eq = eq_list;
           Minils.c_local = d_list;
-          Minils.c_assume = e_a;
-          Minils.c_enforce = e_c
         } ->
         let (v, si, j, s_list) = translate_eq_list map
           empty_call_context eq_list in

compiler/minils/analysis/clocking.ml

@@ -35,17 +35,17 @@ let typ_of_name h x = Env.find x h
 
 let rec typing h e =
   let ct = match e.e_desc with
-    | Econst se -> skeleton (new_var ()) se.se_ty
+    | Econst se -> skeleton (fresh_clock ()) se.se_ty
     | Evar x -> Ck (typ_of_name h x)
     | Efby (_, e) -> typing h e
     | Eapp({a_op = op}, args, r) ->
         let ck = match r with
-          | None -> new_var ()
+          | None -> fresh_clock ()
           | Some(reset) -> typ_of_name h reset in
         typing_op op args h e ck
     | Eiterator (_, _, _, args, r) -> (* Typed exactly as a fun or a node... *)
         let ck = match r with
-          | None -> new_var()
+          | None -> fresh_clock()
           | Some(reset) -> typ_of_name h reset
         in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty)
     | Ewhen (e, c, n) ->
@@ -55,14 +55,14 @@ let rec typing h e =
         let ck_c = typ_of_name h n in
         (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
     | Estruct l ->
-        let ck = new_var () in
+        let ck = fresh_clock () in
         (List.iter
            (fun (_, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l;
          Ck ck)
   in (e.e_ck <- ckofct ct; ct)
 
 and typing_op op e_list h e ck = match op with
-  | (Eequal | Efun _ | Enode _) ->
+  | (Eequal | Efun _ | Enode _) -> (*LA*)
       List.iter (fun e -> expect h (skeleton ck e.e_ty) e) e_list;
       skeleton ck e.e_ty
   | Etuple ->
@@ -128,7 +128,7 @@ let typing_eqs h eq_list = (*TODO FIXME*)
   in List.iter typing_eq eq_list
 
 let build h dec =
-  List.fold_left (fun h { v_ident = n } -> Env.add n (new_var ()) h) h dec
+  List.fold_left (fun h { v_ident = n } -> Env.add n (fresh_clock ()) h) h dec
 
 let sbuild h dec base =
   List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec

compiler/minils/transformations/singletonvars.ml

@@ -14,6 +14,7 @@ open Signature
 open Minils
 open Mls_utils
 open Mls_printer
+open Global_printer
 open Types
 open Clocks
 open Pp_tools

compiler/minils/transformations/tomato.ml

@@ -14,6 +14,7 @@ open Signature
 open Minils
 open Mls_utils
 open Mls_printer
+open Global_printer
 open Types
 open Clocks
 open Pp_tools