Added a new static scoping pass

This pass transforms exps that should be static 
to Econst se. The regular scoping then only has
to check this case.

The conversion is done in a single traversal of
the AST (unlike the old solution).

compiler/heptagon/main/heptcheck.ml

@@ -31,6 +31,9 @@ let check_implementation modname filename =
     (* Parsing of the file *)
     let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in
 
+    (* Fuse static exps together *)
+    let p = do_silent_pass "Static Scoping"
+      Hept_static_scoping.program p in
     (* Convert the parse tree to Heptagon AST *)
     let p = do_pass "Scoping" Hept_scoping.translate_program p pp in
 

compiler/heptagon/parsing/hept_parsetree_mapfold.ml

@@ -127,6 +127,15 @@ and edesc funs acc ed = match ed with
         (n,e), acc in
       let n_e_list, acc = mapfold aux acc n_e_list in
       Estruct n_e_list, acc
+  | Emerge (x, 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(x, c_e_list), acc
+  | Ewhen (e, c, x) ->
+    let e, acc = exp_it funs acc e in
+      Ewhen (e, c, x), acc
   | Eapp (app, args) ->
       let app, acc = app_it funs acc app in
       let args, acc = mapfold (exp_it funs) acc args in

compiler/heptagon/parsing/hept_scoping.ml

@@ -114,7 +114,6 @@ let qualify_const local_const c = match c with
               with Not_found -> error (Equal_unbound ("constant",c )))
   | Q q -> if check_const q then q else raise Not_static
 
-
 module Rename =
 struct
   open Error
@@ -178,17 +177,18 @@ let static_app_from_app app args=
         q, (app.a_params @ args)
     | _ -> raise Not_static
 
-let rec translate_static_exp local_const se =
+let rec translate_static_exp se =
   try
-    let se_d = translate_static_exp_desc local_const se.se_desc in
+    let se_d = translate_static_exp_desc se.se_desc in
     Types.mk_static_exp ~loc:se.se_loc se_d
   with
     | ScopingError err -> message se.se_loc err
 
-and translate_static_exp_desc local_const ed =
-  let t = translate_static_exp local_const in
+and translate_static_exp_desc ed =
+  let t = translate_static_exp in
   match ed with
-    | Svar q -> Types.Svar (qualify_const local_const q)
+    | Svar (Q q) -> Types.Svar q
+    | Svar (ToQ _) -> assert false
     | Sint i -> Types.Sint i
     | Sfloat f -> Types.Sfloat f
     | Sbool b -> Types.Sbool b
@@ -202,91 +202,58 @@ and translate_static_exp_desc local_const ed =
         Types.Srecord (List.map qualf se_f_list)
     | Sop (fn, se_list) -> Types.Sop (qualify_value fn, List.map t se_list)
 
-let rec static_exp_of_exp local_const e =
-  try
-    let t = static_exp_of_exp local_const in
-    let desc = match e.e_desc with
-      | Evar n -> Types.Svar (qualify_const local_const (ToQ n))
-      | Econst se -> translate_static_exp_desc local_const se.se_desc
-      | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) ->
-          Types.Sarray_power (t e, t n)
-      | Eapp({ a_op = Earray }, e_list) ->
-          Types.Sarray (List.map t e_list)
-      | Eapp({ a_op = Etuple }, e_list) ->
-          Types.Stuple (List.map t e_list)
-      | Eapp(app, e_list) ->
-          let op, args = static_app_from_app app e_list in
-          Types.Sop (op, List.map t args)
-      | Estruct e_list ->
-          Types.Srecord (List.map (fun (f,e) -> qualify_field f, t e) e_list)
-      | _ -> raise Not_static in
-    Types.mk_static_exp ~loc:e.e_loc desc
-  with
-    | ScopingError err -> message e.e_loc err
+let expect_static_exp e = match e.e_desc with
+  | Econst se -> translate_static_exp se
+  | _ ->  message e.e_loc Estatic_exp_expected
 
-let expect_static_exp local_const e =
-  try static_exp_of_exp local_const e
-  with Not_static -> message e.e_loc Estatic_exp_expected
-
-let rec translate_type loc local_const ty =
+let rec translate_type loc ty =
   try
     (match ty with
       | Tprod ty_list ->
-          Types.Tprod(List.map (translate_type loc local_const) ty_list)
+          Types.Tprod(List.map (translate_type loc) ty_list)
       | Tid ln -> Types.Tid (qualify_type ln)
       | Tarray (ty, e) ->
-          let ty = translate_type loc local_const ty in
-          Types.Tarray (ty, expect_static_exp local_const e))
+          let ty = translate_type loc ty in
+          Types.Tarray (ty, expect_static_exp e))
   with
     | ScopingError err -> message loc err
 
-
-and translate_exp local_const env e =
+let rec translate_exp env e =
   try
-    let desc =
-      (*try (* try to see if the exp is a constant *)
-        Heptagon.Econst (static_exp_of_exp local_const e)
-        with
-        Not_static -> *) translate_desc e.e_loc local_const env e.e_desc in
-    { Heptagon.e_desc = desc;
+    { Heptagon.e_desc = translate_desc e.e_loc env e.e_desc;
       Heptagon.e_ty = Types.invalid_type;
       Heptagon.e_loc = e.e_loc }
   with ScopingError(error) -> message e.e_loc error
 
-and translate_desc loc local_const env = function
-  | Econst c -> Heptagon.Econst (translate_static_exp local_const c)
-  | Evar x -> (
-      try (* First check if it is a const var *)
-        Heptagon.Econst
-          (Types.mk_static_exp
-             ~loc:loc (Types.Svar (qualify_var_as_const local_const x)))
-      with Not_found -> Heptagon.Evar (Rename.var loc env x))
+and translate_desc loc env = function
+  | Econst c -> Heptagon.Econst (translate_static_exp c)
+  | Evar x -> Heptagon.Evar (Rename.var loc env x)
   | Elast x -> Heptagon.Elast (Rename.last loc env x)
-  | Epre (None, e) -> Heptagon.Epre (None, translate_exp local_const env e)
+  | Epre (None, e) -> Heptagon.Epre (None, translate_exp env e)
   | Epre (Some c, e) ->
-      Heptagon.Epre (Some (expect_static_exp local_const c),
-                     translate_exp local_const env e)
-  | Efby (e1, e2) -> Heptagon.Efby (translate_exp local_const env e1,
-                                    translate_exp local_const env e2)
+      Heptagon.Epre (Some (expect_static_exp c),
+                     translate_exp env e)
+  | Efby (e1, e2) -> Heptagon.Efby (translate_exp env e1,
+                                    translate_exp env e2)
   | Estruct f_e_list ->
       let f_e_list =
-        List.map (fun (f,e) -> qualify_field f, translate_exp local_const env e)
+        List.map (fun (f,e) -> qualify_field f, translate_exp env e)
           f_e_list in
       Heptagon.Estruct f_e_list
   | Eapp ({ a_op = op; a_params = params }, e_list) ->
-      let e_list = List.map (translate_exp local_const env) e_list in
-      let params = List.map (expect_static_exp local_const) params in
+      let e_list = List.map (translate_exp env) e_list in
+      let params = List.map (expect_static_exp) params in
       let app = Heptagon.mk_op ~params:params (translate_op op) in
       Heptagon.Eapp (app, e_list, None)
   | Eiterator (it, { a_op = op; a_params = params }, n, e_list) ->
-      let e_list = List.map (translate_exp local_const env) e_list in
-      let n = expect_static_exp local_const n in
-      let params = List.map (expect_static_exp local_const) params in
+      let e_list = List.map (translate_exp env) e_list in
+      let n = expect_static_exp n in
+      let params = List.map (expect_static_exp) params in
       let app = Heptagon.mk_op ~params:params (translate_op op) in
       Heptagon.Eiterator (translate_iterator_type it,
                           app, n, e_list, None)
   | Ewhen (e, c, n) ->
-      let e = translate_exp local_const env e in
+      let e = translate_exp env e in
       let c = qualify_constrs c in
       let n = Rename.var loc env n in
       Heptagon.Ewhen (e, c, n)
@@ -294,7 +261,7 @@ and translate_desc loc local_const env = function
       let n = Rename.var loc env n in
       let c_e_list =
         let fun_c_e (c, e) =
-          let e = translate_exp local_const env e in
+          let e = translate_exp env e in
           let c = qualify_constrs c in
           (c, e) in
         List.map fun_c_e c_e_list in
@@ -321,112 +288,110 @@ and translate_pat loc env = function
   | Evarpat x -> Heptagon.Evarpat (Rename.var loc env x)
   | Etuplepat l -> Heptagon.Etuplepat (List.map (translate_pat loc env) l)
 
-let rec translate_eq local_const env eq =
-  { Heptagon.eq_desc = translate_eq_desc eq.eq_loc local_const env eq.eq_desc ;
+let rec translate_eq env eq =
+  { Heptagon.eq_desc = translate_eq_desc eq.eq_loc env eq.eq_desc ;
     Heptagon.eq_statefull = false;
     Heptagon.eq_loc = eq.eq_loc }
 
-and translate_eq_desc loc local_const env = function
+and translate_eq_desc loc env = function
   | Eswitch(e, switch_handlers) ->
       let sh = List.map
-        (translate_switch_handler loc local_const env)
+        (translate_switch_handler loc env)
         switch_handlers in
-      Heptagon.Eswitch (translate_exp local_const env e, sh)
+      Heptagon.Eswitch (translate_exp env e, sh)
   | Eeq(p, e) ->
-      Heptagon.Eeq (translate_pat loc env p, translate_exp local_const env e)
+      Heptagon.Eeq (translate_pat loc env p, translate_exp env e)
   | Epresent (present_handlers, b) ->
       Heptagon.Epresent
-        (List.map (translate_present_handler local_const env) present_handlers
-           , fst (translate_block local_const env b))
+        (List.map (translate_present_handler env) present_handlers
+           , fst (translate_block env b))
   | Eautomaton state_handlers ->
-      Heptagon.Eautomaton (List.map (translate_state_handler local_const env)
+      Heptagon.Eautomaton (List.map (translate_state_handler env)
                              state_handlers)
   | Ereset (b, e) ->
-      let b, _ = translate_block local_const env b in
-      Heptagon.Ereset (b, translate_exp local_const env e)
+      let b, _ = translate_block env b in
+      Heptagon.Ereset (b, translate_exp env e)
 
-and translate_block local_const env b =
+and translate_block env b =
   let env = Rename.append env b.b_local in
-  { Heptagon.b_local = translate_vd_list local_const env b.b_local;
-    Heptagon.b_equs = List.map (translate_eq local_const env) b.b_equs;
+  { Heptagon.b_local = translate_vd_list env b.b_local;
+    Heptagon.b_equs = List.map (translate_eq env) b.b_equs;
     Heptagon.b_defnames = Env.empty;
     Heptagon.b_statefull = false;
     Heptagon.b_loc = b.b_loc }, env
 
-and translate_state_handler local_const env sh =
-  let b, env = translate_block local_const env sh.s_block in
+and translate_state_handler env sh =
+  let b, env = translate_block env sh.s_block in
   { Heptagon.s_state = sh.s_state;
     Heptagon.s_block = b;
-    Heptagon.s_until = List.map (translate_escape local_const env) sh.s_until;
+    Heptagon.s_until = List.map (translate_escape env) sh.s_until;
     Heptagon.s_unless =
-      List.map (translate_escape local_const env) sh.s_unless; }
+      List.map (translate_escape env) sh.s_unless; }
 
-and translate_escape local_const env esc =
-  { Heptagon.e_cond = translate_exp local_const env esc.e_cond;
+and translate_escape env esc =
+  { Heptagon.e_cond = translate_exp env esc.e_cond;
     Heptagon.e_reset = esc.e_reset;
     Heptagon.e_next_state = esc.e_next_state }
 
-and translate_present_handler local_const env ph =
-  { Heptagon.p_cond = translate_exp local_const env ph.p_cond;
-    Heptagon.p_block = fst (translate_block local_const env ph.p_block) }
+and translate_present_handler env ph =
+  { Heptagon.p_cond = translate_exp env ph.p_cond;
+    Heptagon.p_block = fst (translate_block env ph.p_block) }
 
-and translate_switch_handler loc local_const env sh =
+and translate_switch_handler loc env sh =
   try
     { Heptagon.w_name = qualify_constrs sh.w_name;
-      Heptagon.w_block = fst (translate_block local_const env sh.w_block) }
+      Heptagon.w_block = fst (translate_block env sh.w_block) }
   with
     | ScopingError err -> message loc err
 
-and translate_var_dec local_const env vd =
+and translate_var_dec env vd =
   (* env is initialized with the declared vars before their translation *)
     { 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_type = translate_type vd.v_loc vd.v_type;
+      Heptagon.v_last = translate_last 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 =
-  List.map (translate_var_dec local_const env)
+and translate_vd_list env =
+  List.map (translate_var_dec env)
 
-and translate_last local_const = function
+and translate_last = function
   | Var -> Heptagon.Var
   | Last (None) -> Heptagon.Last None
-  | Last (Some e) -> Heptagon.Last (Some (expect_static_exp local_const e))
+  | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e))
 
-let translate_contract local_const env ct =
-  let b, _ = translate_block local_const env ct.c_block in
-  { Heptagon.c_assume = translate_exp local_const env ct.c_assume;
-    Heptagon.c_enforce = translate_exp local_const env ct.c_enforce;
+let translate_contract env ct =
+  let b, _ = translate_block env ct.c_block in
+  { Heptagon.c_assume = translate_exp env ct.c_assume;
+    Heptagon.c_enforce = translate_exp env ct.c_enforce;
     Heptagon.c_block = b }
 
-let params_of_var_decs local_const =
+let params_of_var_decs =
   List.map (fun vd -> Signature.mk_param
                         vd.v_name
-                        (translate_type vd.v_loc local_const vd.v_type))
+                        (translate_type vd.v_loc vd.v_type))
 
-let args_of_var_decs local_const =
+let args_of_var_decs =
   List.map (fun vd -> Signature.mk_arg
                         (Some vd.v_name)
-                        (translate_type vd.v_loc local_const vd.v_type))
+                        (translate_type vd.v_loc vd.v_type))
 
 let translate_node node =
   Idents.new_function ();
-  (* Node's params go to local_const env *)
-  let local_const = build_const node.n_loc node.n_params in
   (* Inputs and outputs define the initial local env *)
   let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in
-  let params = params_of_var_decs local_const node.n_params in
-  let inputs = translate_vd_list local_const env0 node.n_input in
-  let outputs = translate_vd_list local_const env0 node.n_output in
-  let b, env = translate_block local_const env0 node.n_block in
+  let params = params_of_var_decs node.n_params in
+  let inputs = translate_vd_list env0 node.n_input in
+  let outputs = translate_vd_list env0 node.n_output in
+  let b, env = translate_block env0 node.n_block in
   let contract =
-    Misc.optional (translate_contract local_const env) node.n_contract in
+    Misc.optional (translate_contract env) node.n_contract in
   (* the env of the block is used in the contract translation *)
   let n = current_qual node.n_name in
   (* add the node signature to the environment *)
-  let i = args_of_var_decs local_const node.n_input in
-  let o = args_of_var_decs local_const node.n_output in
-  let p = params_of_var_decs local_const node.n_params in
+  let i = args_of_var_decs node.n_input in
+  let o = args_of_var_decs node.n_output in
+  let p = params_of_var_decs node.n_params in
   add_value n (Signature.mk_node i o node.n_statefull p);
   { Heptagon.n_name = n;
     Heptagon.n_statefull = node.n_statefull;
@@ -445,7 +410,7 @@ let translate_typedec ty =
           add_type n Signature.Tabstract;
           Heptagon.Type_abs
       | Type_alias t ->
-          let t = translate_type ty.t_loc S.empty t in
+          let t = translate_type ty.t_loc t in
           add_type n (Signature.Talias t);
           Heptagon.Type_alias t
       | Type_enum(tag_list) ->
@@ -456,7 +421,7 @@ let translate_typedec ty =
       | Type_struct(field_ty_list) ->
           let translate_field_type (f,t) =
             let f = current_qual f in
-            let t = translate_type ty.t_loc S.empty t in
+            let t = translate_type ty.t_loc t in
             add_field f n;
             Signature.mk_field f t in
           let field_list = List.map translate_field_type field_ty_list in
@@ -469,9 +434,8 @@ let translate_typedec ty =
 
 let translate_const_dec cd =
   let c_name = current_qual cd.c_name in
-  let c_type = translate_type cd.c_loc S.empty cd.c_type in
-  let c_value = expect_static_exp S.empty cd.c_value in
-  add_const c_name (Signature.mk_const_def c_type c_value);
+  let c_type = translate_type cd.c_loc cd.c_type in
+  let c_value = expect_static_exp cd.c_value in
   { Heptagon.c_name = c_name;
     Heptagon.c_type = c_type;
     Heptagon.c_value = c_value;
@@ -489,13 +453,12 @@ let translate_program p =
     Heptagon.p_consts = consts; }
 
 let translate_signature s =
-  let local_const = build_const s.sig_loc s.sig_params in
   let translate_arg a =
-    Signature.mk_arg a.a_name (translate_type s.sig_loc local_const a.a_type) in
+    Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type) in
   let n = current_qual s.sig_name in
   let i = List.map translate_arg s.sig_inputs in
   let o = List.map translate_arg s.sig_outputs in
-  let p = params_of_var_decs local_const s.sig_params in
+  let p = params_of_var_decs s.sig_params in
   add_value n (Signature.mk_node i o s.sig_statefull p);
   Heptagon.mk_signature n i o s.sig_statefull p s.sig_loc
 

compiler/heptagon/parsing/hept_static_scoping.ml

@@ -0,0 +1,68 @@
+open Modules
+open Hept_parsetree
+open Hept_parsetree_mapfold
+open Hept_scoping
+
+(* Convert expressions that should be static to the corresponding
+   static expression. After this pass, all the static expressions
+   (including variables) are of type Econst se. *)
+
+exception Not_static
+
+let assert_se e = match e.e_desc with
+  | Econst se -> se
+  | _ -> raise Not_static
+
+(** convention : static params are set as the first static args,
+    op<a1,a2> (a3) == op <a1> (a2,a3) == op (a1,a2,a3) *)
+let static_app_from_app app args =
+  match app.a_op with
+    | Efun ((Q { Names.qual = "Pervasives" }) as q)
+    | Enode ((Q { Names.qual = "Pervasives" }) as q) ->
+        q, (app.a_params @ args)
+    | _ -> raise Not_static
+
+let exp funs local_const e =
+  let e, _ = Hept_parsetree_mapfold.exp funs local_const e in
+    try
+      let sed =
+        match e.e_desc with
+          | Evar n ->
+            (try
+                 Svar (Q (qualify_const local_const (ToQ n)))
+            with
+              | Error.ScopingError _ -> raise Not_static)
+          | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) ->
+            Sarray_power (assert_se e, assert_se n)
+          | Eapp({ a_op = Earray }, e_list) ->
+            Sarray (List.map assert_se e_list)
+          | Eapp({ a_op = Etuple }, e_list) ->
+            Stuple (List.map assert_se e_list)
+          | Eapp(app, e_list) ->
+            let op, e_list = static_app_from_app app e_list in
+              Sop (op, List.map assert_se e_list)
+          | Estruct e_list ->
+            Srecord (List.map (fun (f,e) -> f, assert_se e) e_list)
+          | _ -> raise Not_static
+      in
+        { e with e_desc = Econst (mk_static_exp sed e.e_loc) }, local_const
+    with
+        Not_static -> e, local_const
+
+let node funs _ n =
+  let local_const = Hept_scoping.build_const n.n_loc n.n_params in
+    Hept_parsetree_mapfold.node_dec funs local_const n
+
+let const_dec funs local_const cd =
+  let cd, _ = Hept_parsetree_mapfold.const_dec funs local_const cd in
+  let c_name = current_qual cd.c_name in
+  let c_type = Hept_scoping.translate_type cd.c_loc cd.c_type in
+  let c_value = Hept_scoping.expect_static_exp cd.c_value in
+    add_const c_name (Signature.mk_const_def c_type c_value);
+    cd, local_const
+
+let program p =
+  let funs = { Hept_parsetree_mapfold.defaults
+               with node_dec = node; exp = exp; const_dec = const_dec } in
+  let p, _ = Hept_parsetree_mapfold.program_it funs Names.S.empty p in
+    p

compiler/main/heptc.ml

@@ -40,6 +40,9 @@ let compile_impl modname filename =
     (* Parsing of the file *)
     let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in
 
+    (* Fuse static exps together *)
+    let p = do_silent_pass "Static Scoping"
+      Hept_static_scoping.program p in
     (* Convert the parse tree to Heptagon AST *)
     let p = do_pass "Scoping" Hept_scoping.translate_program p pp in