Normalize in Heptagon compiles

compiler/heptagon/heptagon.ml

@@ -202,8 +202,8 @@ let mk_type_dec name desc =
 let mk_equation ?(stateful = true) desc =
   { eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
 
-let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty =
+let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty =
-  { v_ident = name; v_type = ty; v_clock = ck;
+  { 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 =
@@ -256,4 +256,8 @@ let vars_pat pat =
     | Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
   in _vars_pat IdentSet.empty IdentSet.empty pat
 
-
+(** @return whether an object of name [n] belongs to
+    a list of [var_dec]. *)
+let rec vd_mem n = function
+  | [] -> false
+  | vd::l -> vd.v_ident = n or (vd_mem n l)

compiler/heptagon/transformations/normalize.ml

@@ -7,14 +7,14 @@
 (*                                                                        *)
 (**************************************************************************)
 open Misc
-open Initial
 open Names
 open Idents
+open Location
 open Heptagon
 open Hept_mapfold
 open Types
 open Clocks
-
+open Format
 
 (** Normalization pass
     The normal form of the language is given in the manual *)
@@ -33,15 +33,27 @@ struct
     raise Errors.Error
 end
 
+let is_stateful e = match e.e_desc with 
+  | Efby _ | Epre _ -> true
+  | Eapp({ a_op = Enode _ }, _, _) -> true
+  | _ -> false
+
+let exp_list_of_static_exp_list se_list =
+  let mk_one_const se =
+    mk_exp (Econst se) se.se_ty
+  in
+    List.map mk_one_const se_list
+
 let is_list e = match e.e_desc with 
- | Eapp({ a_op = Etuple }, e_list, _) 
+ | Eapp({ a_op = Etuple }, _, _) 
- | Econst { se_desc = Stuple se_list } -> true
+ | Econst { se_desc = Stuple _ } -> true
  | _ -> false
 
 let e_to_e_list e = match e.e_desc with
   | Eapp({ a_op = Etuple }, e_list, _) -> e_list
   | Econst { se_desc = Stuple se_list } ->
       exp_list_of_static_exp_list se_list
+  | _ -> assert false
 
 let flatten_e_list l =
   let flatten = function
@@ -55,7 +67,7 @@ let flatten_e_list l =
 let equation (d_list, eq_list) e =
   let add_one_var ty d_list =
     let n = Idents.gen_var "normalize" "v" in
-    let d_list = (mk_var_dec ~clock:e.e_ck n ty) :: d_list in
+    let d_list = (mk_var_dec n ty) :: d_list in
       n, d_list
   in
     match e.e_ty with
@@ -63,43 +75,36 @@ 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 (Etuplepat pat_list) e) :: eq_list in
+          let eq_list = (mk_equation ~stateful:(is_stateful e)
+			    (Eeq (Etuplepat pat_list, e))) :: eq_list in
           let e_list = List.map2
-            (fun n ty -> mk_exp ~ty:ty (Evar n)) var_list ty_list in
+            (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 (Evarpat n) e) :: eq_list in
+          let eq_list = (mk_equation ~stateful:(is_stateful e) 
+			    (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))] *)
 let rec whenc context e c n =
   let when_on_c c n e =
-    { e with e_desc = Ewhen(e, c, n); e_ck = Con(e.e_ck, c, n) }
+    { e with e_desc = Ewhen(e, c, n) }
   in
     if is_list e then (
       let e_list = List.map (when_on_c c n) (e_to_e_list e) in
-          context, { e with e_desc = Eapp (app, e_list, r);
+          context, { e with e_desc = Eapp(mk_app Etuple, e_list, None) }
-                            e_ck = Con(e.e_ck, c, n) }
     ) else
       context, when_on_c c n e
 
-let const e c =
-  let rec const = function
-    | Cbase | Cvar { contents = Cindex _ } -> c
-    | Con(ck_on, tag, x) ->
-        Ewhen({ e with e_desc = const ck_on; e_ck = ck_on }, tag, x)
-    | Cvar { contents = Clink ck } -> const ck in
-  const e.e_ck
-
 type kind = ExtValue | Any
 
 (** Creates an equation and add it to the context if necessary. *)
 let add context expected_kind ({ e_desc = de } as e) =
   let up = match de, expected_kind with
     | (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
-      | Eapp ({ a_op = Etuple }, _, _) | Econst) , ExtValue -> false
+      | Eapp ({ a_op = Etuple }, _, _) | Econst _) , ExtValue -> false
     | _ , ExtValue -> true
     | _ -> false in
   if up then
@@ -110,24 +115,24 @@ let add context expected_kind ({ e_desc = de } as e) =
 
 let rec translate kind context e =
   let context, e = match e.e_desc with
-    | Econst c -> context, { e with e_desc = const e (Econst c) }
+    | Econst _
     | Evar _ -> context, e
     | Epre(v, e1) -> fby kind context e v e1
     | Efby({ e_desc = Econst v }, e1) -> fby kind context e (Some v) e1
     | Estruct l ->
-	let translate_field (f, e) context =
+	let translate_field context (f, e) =
 	  let context, e = translate ExtValue context e in
-            context, (f, e)
+            (f, e), context
 	in
-        let context, l = mapfold translate_field context l in
+        let l, context = mapfold translate_field context l in
           context, { e with e_desc = Estruct l }
     | Ewhen(e1, c, n) ->
         let context, e1 = translate kind context e1 in
           whenc context e1 c n
     | Emerge(n, tag_e_list) ->
-	merge context n tag_e_list
+	merge context e n tag_e_list
     | Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
-        ifthenelse context e1 e2 e3
+        ifthenelse context e e1 e2 e3
     | Eapp(app, e_list, r) ->
         let context, e_list = translate_list ExtValue context e_list in
           context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }
@@ -136,15 +141,18 @@ let rec translate kind context e =
       (match app.a_op with
         | Enode f when Itfusion.is_anon_node f ->
 	    let nd = Itfusion.find_anon_node f in
-            let d_list, eq_list = translate_eq_list nd.n_local nd.n_equs in
+            let d_list, eq_list = 
-	    let nd = { nd with n_equs = eq_list; n_local = d_list } in
+	      translate_eq_list nd.n_block.b_local nd.n_block.b_equs in
+	    let b = { nd.n_block with b_local = d_list; b_equs = eq_list } in
+	    let nd = { nd with n_block = b } in
 	      Itfusion.replace_anon_node f nd
         | _ -> () );
         let context, pe_list = translate_list ExtValue context pe_list in
         let context, e_list = translate_list ExtValue context e_list in
         context, { e with e_desc = Eiterator(it, app, n, flatten_e_list pe_list,
                                              flatten_e_list e_list, reset) }
-    | Elast _ | Efby _ -> message e.e_loc Eunsupported_language_construct
+    | Elast _ | Efby _ ->
+	Error.message e.e_loc Error.Eunsupported_language_construct
   in add context kind e
 
 and translate_list kind context e_list =
@@ -157,10 +165,10 @@ and translate_list kind context e_list =
 
 and fby kind context e v e1 =
   let mk_fby c e =
-    mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(Some c, e)) in
+    mk_exp ~loc:e.e_loc (Epre(Some c, e)) e.e_ty in
   let mk_pre e =
-    mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(None, e)) in
+    mk_exp ~loc:e.e_loc (Epre(None, e)) e.e_ty in
-  let e1 = translate ExtValue context e1 in
+  let context, e1 = translate ExtValue context e1 in
   match e1.e_desc, v with
     | Eapp({ a_op = Etuple } as app, e_list, r),
       Some { se_desc = Stuple se_list } ->
@@ -179,9 +187,9 @@ and fby kind context e v e1 =
           translate kind context e
     | Econst { se_desc = Stuple se_list }, None ->
         let e_list = List.map mk_pre (exp_list_of_static_exp_list se_list) in
-        let e = { e with e_desc = Eapp(app, e_list, r) } in
+        let e = { e with e_desc = Eapp(mk_app Etuple, e_list, None) } in
           translate kind context e
-    | _ -> context, { e with e_desc = Efby(v, e1) }
+    | _ -> context, { e with e_desc = Epre(v, e1) }
 
 (** transforms [if x then e1, ..., en else e'1,..., e'n] 
     into [if x then e1 else e'1, ..., if x then en else e'n]  *)
@@ -191,66 +199,83 @@ and ifthenelse context e e1 e2 e3 =
   let context, e3 = translate ExtValue context e3 in
   let mk_ite_list e2_list e3_list =
     let mk_ite e2 e3 = 
-      mk_exp ~ty:e2.e_ty ~loc:e.e_loc (Eifthenelse(e1, e2, e3)) 
+      mk_exp ~loc:e.e_loc 
+	(Eapp (mk_app Eifthenelse, [e1; e2; e3], None)) e2.e_ty
     in
     let e_list = List.map2 mk_ite e2_list e3_list in
       { e with e_desc = Eapp(mk_app Etuple, e_list, None) }
   in
-    if is_list e2 then 
+    if is_list e2 then (
-      context, mk_ite_list context (e_to_e_list e2) (e_to_e_list e2)
+      context, mk_ite_list (e_to_e_list e2) (e_to_e_list e2)
-    else
+    ) else
-      context, { e with e_desc = Eifthenelse(e1, e2, e3)}
+      context, { e with e_desc = Eapp (mk_app Eifthenelse, [e1; e2; e3], None) }
 
 (** transforms [merge x (c1, (e11,...,e1n));...;(ck, (ek1,...,ekn))] into
     [merge x (c1, e11)...(ck, ek1),..., merge x (c1, e1n)...(ck, ekn)]    *)
 and merge context e x c_e_list =
-    let translate_tag (tag, e) context =
+    let translate_tag context (tag, e) =
       let context, e = translate ExtValue context e in
-        context, (tag, e)
+        (tag, e), context
     in
     let mk_merge x c_list e_list =
-      let ty = (hd e_list).e_e_ty in
+      let ty = (List.hd e_list).e_ty in
       let t_e_list = List.map2 (fun t e -> (t,e)) c_list e_list in
-	mk_exp ~ty:ty ~loc:e.e_loc (Emerge(x, t_e_list))
+	mk_exp ~loc:e.e_loc (Emerge(x, t_e_list)) ty
     in
     let context, x = translate ExtValue context x in
-    let context, c_e_list = mapfold translate_tag context ta_list in
+    let c_e_list, context = mapfold translate_tag context c_e_list in
       match c_e_list with
 	| [] -> assert false
 	| (_,e)::_ ->
-	    if is_list e then 
+	    if is_list e then (
 	      let c_list = List.map (fun (t,_) -> t) c_e_list in
 	      let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in
 	      let e_list = List.map (mk_merge x c_list) e_lists in
 		context, { e with e_desc = Eapp(mk_app Etuple, e_list, None) }
-	    else
+	    ) else
 	      context, { e with e_desc = Emerge(x, c_e_list) }
 
 (* applies distribution rules *)
 (* [x = v fby e] should verifies that x is local *)
 (* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *)
-and distribute ((d_list, eq_list) as context) pat e =
+and distribute ((d_list, eq_list) as context) eq pat e =
   match pat, e.e_desc with
     | Evarpat(x), Efby _ when not (vd_mem x d_list) ->
         let (d_list, eq_list), n = equation context e in
-          d_list,
+	let eq = { eq with eq_desc = Eeq(pat, { e with e_desc = n }) } in
-        { eq with eq_rhs = { e with e_desc = n } } :: eq_list
+          d_list,  eq::eq_list
     | Etuplepat(pat_list), Eapp({ a_op = Etuple }, e_list, _) ->
-        let eqs = List.map2 mk_equation pat_list e_list in
+	let mk_eq pat e = 
-          List.fold_left distribute context eqs
+	  mk_equation ~stateful:eq.eq_stateful (Eeq (pat, e))
-    | _ -> d_list, Eeq(pat, e) :: eq_list 
+	in
+	let dis context eq = match eq.eq_desc with 
+	  | Eeq (pat, e) -> distribute context eq pat e 
+	  | _ -> assert false
+	in
+        let eqs = List.map2 mk_eq pat_list e_list in
+          List.fold_left dis context eqs
+    | _ -> d_list, eq :: eq_list 
 
-and translate_eq context eq = match eq with
+and translate_eq context eq = match eq.eq_desc with
   | Eeq (pat, e) -> 
       let context, e = translate Any context e in
-	distribute context pat e
+	distribute context eq pat e
-  | _ -> raise Fallback
+  | _ -> raise Errors.Fallback
+
+and translate_eq_list d_list eq_list =
+  List.fold_left
+    (fun context eq -> translate_eq context eq)
+    (d_list, []) eq_list
+
+let eq funs context eq =
+  let context = translate_eq context eq in
+    eq, context
 
 let block funs _ b =
   let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in
     { b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], [])
 
 let program p =
-  let funs = { defaults with eq = translate_eq; } in
+  let funs = { defaults with block = block; eq = eq } in
   let p, _ = Hept_mapfold.program funs ([], []) p in
     p

compiler/minils/mls_utils.ml

@@ -55,12 +55,6 @@ let is_record_type ty = match ty with
 let is_op = function
   | { qual = Pervasives; name = _ } -> true | _ -> false
 
-let exp_list_of_static_exp_list se_list =
-  let mk_one_const se =
-    Minils.mk_exp ~ty:se.se_ty (Minils.Econst se)
-  in
-    List.map mk_one_const se_list
-
 module Vars =
 struct
   let add x acc = if List.mem x acc then acc else x :: acc