Do some typing ; support multiple pre in abstract interpretation.

9 files changed, 270 insertions, 126 deletions

diff --git a/Makefile b/Makefile
index 7645849..6386a97 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,9 @@ SRC= 	main.ml \
 		frontend/parser.mly \
 		frontend/lexer.mll \
 		frontend/ast_printer.ml \
+		frontend/typing.ml \
+		frontend/ast_util.ml \
+		frontend/rename.ml \
 		abstract/formula.ml \
 		abstract/formula_printer.ml \
 		abstract/transform.ml \
@@ -17,8 +20,6 @@ SRC= 	main.ml \
 		abstract/nonrelational.ml \
 		abstract/intervals_domain.ml \
 		interpret/interpret.ml \
-		interpret/ast_util.ml \
-		interpret/rename.ml
 
 all: $(BIN)
 
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 00f7fad..c621734 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -1,6 +1,7 @@
 open Ast
 open Ast_util
 open Formula
+open Typing
 
 open Util
 open Environment_domain
@@ -9,15 +10,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : int -> prog -> id -> unit
+    val do_prog     : int -> rooted_prog -> unit
 
 end = struct
 
     type st = {
-        p           : prog;
+        rp          : rooted_prog;
         widen_delay : int;
-        root_scope  : scope;
-        all_vars    : var_def list;
         env         : E.t;
         f           : bool_expr;
         cl          : conslist;
@@ -27,75 +26,29 @@ end = struct
     }
 
 
-    let node_vars p f nid =
-      let (n, _) = find_node_decl p f in
-      List.map (fun (p, id, t) -> p, nid^"/"^id, t)
-        (n.args @ n.ret @ n.var)
 
-    (*
-        extract_all_vars : prog -> scope -> var_decl list
-
-        Extracts all variables with names given according to
-        naming convention used here and in transform.ml :
-        - pre variables are not prefixed by scope
-        - next values for variables are prefixed by capital N
-    *)
-    let rec extract_all_vars p (node, prefix, eqs) =
-        let vars_of_expr e =
-          List.flatten
-            (List.map
-              (fun (f, id, eqs, args) ->
-                node_vars p f (node^"/"^id) @
-                extract_all_vars p (node^"/"^id, "", eqs))
-              (extract_instances p e))
-          @
-          List.flatten
-            (List.map
-              (fun (id, _) -> [false, id, AST_TINT; false, "N"^id, AST_TINT])
-                  (* TODO : type of pre value ? *)
-              (extract_pre e))
-        in
-        let vars_of_eq e = match fst e with
-          | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
-          | AST_activate (b, _) ->
-            let rec do_branch = function
-              | AST_activate_body b ->
-                List.map (fun (p, id, t) -> p, node^"/"^id, t) b.act_locals
-                @
-                extract_all_vars p (node, b.act_id^".", b.body)
-              | AST_activate_if(c, a, b) ->
-                vars_of_expr c @ do_branch a @ do_branch b
-            in do_branch b
-          | AST_automaton _ -> not_implemented "extract_all vars automaton"
-        in
-        (false, node^"/"^prefix^"time", AST_TINT)::
-        (false, "N"^node^"/"^prefix^"time", AST_TINT)::
-        (List.flatten (List.map vars_of_eq eqs))
 
     (* init state *)
-    let init_state widen_delay p root =
-      let root_scope = get_root_scope p root in
-
-      let f = Formula.eliminate_not (Transform.f_of_prog p root false) in
+    let init_state widen_delay rp =
+      let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
       let cl = Formula.conslist_of_f f in
-      let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in
+      let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
       let cl_g = Formula.conslist_of_f f_g in
 
-      let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
       let env = List.fold_left
         (fun env (_, id, ty) ->
-          E.addvar env id (ty = AST_TREAL))
+          E.addvar env id (ty = TReal))
         E.init
-        all_vars
+        rp.all_vars
       in
-      let init_f = Transform.init_f_of_prog p root in
-      let guarantees = Transform.guarantees_of_prog p root in
+      let init_f = Transform.init_f_of_prog rp in
+      let guarantees = Transform.guarantees_of_prog rp in
 
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
       Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
       Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
 
-      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
 
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
@@ -105,9 +58,9 @@ end = struct
 
       let env = E.apply_f env init_f in
 
-      { p; root_scope; widen_delay;
+      { rp; widen_delay;
         f; cl; f_g; cl_g;
-        guarantees; all_vars; env }
+        guarantees; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -138,7 +91,7 @@ end = struct
 
     (* cycle : st -> cl -> env -> env *)
     let cycle st cl i =
-      (pass_cycle st.all_vars (E.apply_cl i cl)) 
+      (pass_cycle st.rp.all_vars (E.apply_cl i cl)) 
 
     (*
       loop : st -> env -> env -> env
@@ -173,10 +126,10 @@ end = struct
       y, z
 
     (*
-      do_prog : prog -> id -> unit
+      do_prog : rooted_prog -> unit
     *)
-    let do_prog widen_delay p root =
-      let st = init_state widen_delay p root in
+    let do_prog widen_delay rp =
+      let st = init_state widen_delay rp in
 
       let pnew = st.env in
       let pnew_c = E.apply_cl pnew st.cl in
@@ -209,13 +162,13 @@ end = struct
         Format.printf "@]@."
       end;
 
-      if List.exists (fun (p, _, _) -> p) st.all_vars then begin
+      if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
         Format.printf "Probes:@[<v>";
         List.iter (fun (p, id, _) ->
           if p then Format.printf " %a ∊ %a@ "
                 Formula_printer.print_id id
                 E.print_itv (E.var_itv final id))
-          st.all_vars;
+          st.rp.all_vars;
         Format.printf "@]@."
       end
 
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 25e4b43..890f598 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -2,6 +2,7 @@ open Ast
 open Util
 open Ast_util
 open Formula
+open Typing
 
 open Interpret  (* used for constant evaluation ! *)
 
@@ -12,9 +13,8 @@ open Interpret  (* used for constant evaluation ! *)
 type scope = id * id * eqn ext list
 
 type transform_data = {
-    p           : Ast.prog;
+    rp          : rooted_prog;
     consts      : I.value VarMap.t;
-    root_scope  : scope;
     (* future : the automata state *)
 }
 
@@ -47,7 +47,9 @@ let rec f_of_nexpr td (node, prefix) where expr =
           | _ -> invalid_arity "binary_operator") b
       | _ -> invalid_arity "binary operator") a
   (* temporal *)
-  | AST_pre(_, id) -> where [NIdent id]
+  | AST_pre(expr, id) ->
+    let typ = type_expr td.rp node expr in
+      where (List.mapi (fun i _ -> NIdent (id^"."^(string_of_int i))) typ)
   | AST_arrow(a, b) ->
     f_or
       (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
@@ -60,7 +62,7 @@ let rec f_of_nexpr td (node, prefix) where expr =
       (f_and (f_of_expr td (node, prefix) c) (sub where a))
       (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
-    let (n, _) = find_node_decl td.p f in
+    let (n, _) = find_node_decl td.rp.p f in
     where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
     
   (* boolean values treated as integers *)
@@ -140,16 +142,22 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
         eq
     in
     let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
-      eq (extract_instances td.p e)
+      eq (extract_instances td.rp.p e)
     in
     let pre_expr (id, expr) =
       if active then
-        f_of_nexpr td (node, prefix) (function
-            | [v] -> BRel(AST_EQ, NIdent("N"^id), v)
-            | _ -> invalid_arity "pre on complex data not supported")
+        f_of_nexpr td (node, prefix) (fun elist ->
+            list_fold_op f_and
+              (List.mapi
+                (fun i v -> BRel(AST_EQ, NIdent("N"^id^"."^(string_of_int i)), v))
+                elist))
           expr
       else
-        BRel(AST_EQ, NIdent("N"^id), NIdent id)
+        let typ = type_expr td.rp node expr in
+        list_fold_op f_and
+          (List.mapi
+            (fun i _ -> let x = string_of_int i in BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x)))
+            typ)
     in
     List.fold_left (fun x i -> f_and (pre_expr i) x)
       eq (extract_pre e)
@@ -224,25 +232,24 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     time_incr_eq
     (List.map do_eq eqs)
 
-and f_of_prog p root assume_guarantees =
+and f_of_prog rp assume_guarantees =
     let td = {
-      root_scope = get_root_scope p root;
-      p = p;
-      consts = I.consts p root;
+      rp = rp;
+      consts = I.consts rp;
     } in
 
-    f_of_scope true td td.root_scope assume_guarantees
+    f_of_scope true td td.rp.root_scope assume_guarantees
 
 (*
     Translate init state into a formula
 *)
-let rec init_f_of_scope p (node, prefix, eqs) =
+let rec init_f_of_scope rp (node, prefix, eqs) =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
-     init_f_of_scope p (node^"/"^id, "", eqs)
+     init_f_of_scope rp (node^"/"^id, "", eqs)
     in
     List.fold_left (fun x i -> f_and (instance_eq i) x)
-      (BConst true) (extract_instances p e)
+      (BConst true) (extract_instances rp.p e)
   in
   let do_eq eq = match fst eq with
     | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
@@ -250,7 +257,7 @@ let rec init_f_of_scope p (node, prefix, eqs) =
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b ->
-          init_f_of_scope p (node, b.act_id^".", b.body)
+          init_f_of_scope rp (node, b.act_id^".", b.body)
         | AST_activate_if(c, a, b) ->
           f_and (expr_eq c)
             (f_and (cond_eq a) (cond_eq b))
@@ -265,8 +272,8 @@ let rec init_f_of_scope p (node, prefix, eqs) =
   in
   List.fold_left f_and time_eq (List.map do_eq eqs)
 
-and init_f_of_prog p root =
-    init_f_of_scope p (get_root_scope p root)
+and init_f_of_prog rp =
+    init_f_of_scope rp rp.root_scope
 
 (*
     Get expressions for guarantee violation
@@ -277,7 +284,7 @@ let rec g_of_scope td (node, prefix, eqs) cond =
         g_of_scope td (node^"/"^id, "", eqs) cond
     in
     List.fold_left (fun x i -> (instance_g i) @ x)
-      [] (extract_instances td.p e)
+      [] (extract_instances td.rp.p e)
   in
   let do_eq eq = match fst eq with
     | AST_assign(_, e) | AST_assume(_, e) ->
@@ -299,11 +306,10 @@ let rec g_of_scope td (node, prefix, eqs) cond =
   in
   List.fold_left (@) [] (List.map do_eq eqs)
 
-and guarantees_of_prog p root =
+and guarantees_of_prog rp =
     let td = {
-      root_scope = get_root_scope p root;
-      p = p;
-      consts = I.consts p root;
+      rp = rp;
+      consts = I.consts rp;
     } in
 
-    g_of_scope td (get_root_scope p root) (BConst true)
+    g_of_scope td rp.root_scope (BConst true)
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 3ac881e..7ddcb67 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -1,5 +1,6 @@
 open Ast
 open Lexing
+open Typing
 
 
 (* Locations *)
@@ -252,3 +253,14 @@ let print_toplevel fmt = function
 
 let print_prog fmt p =
     List.iter (print_toplevel fmt) p
+
+
+(* Typed variable *)
+
+let print_type fmt = function
+    | TInt -> Format.fprintf fmt "int"
+    | TReal -> Format.fprintf fmt "real"
+    | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e
+
+let print_typed_var fmt (p, id, t) =
+    Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t
diff --git a/interpret/ast_util.ml b/frontend/ast_util.ml
index 9cfe995..a7953ad 100644
--- a/interpret/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -1,6 +1,14 @@
 open Ast
 open Util
 
+(* Some errors *)
+
+let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
+let no_variable e = error ("No such variable: " ^ e)
+let type_error e = error ("Type error: " ^ e)
+let not_implemented e = error ("Not implemented: " ^ e)
+let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
+
 (* Utility : find declaration of a const / a node *)
 
 let find_const_decl p id =
@@ -27,16 +35,6 @@ let extract_const_decls =
     []
 
 
-(* Utility : scopes *)
-
-
-(* path to node * subscope prefix in node * equations in scope *)
-type scope = id * id * eqn ext list
-
-let get_root_scope p root =
-    let (n, _) = find_node_decl p root in
-    ("", "", n.body)
-
 
 (* Utility : find instances declared in an expression *)
 
@@ -75,10 +73,3 @@ let rec extract_pre e = match fst e with
   | AST_pre(e', n) ->
     (n, e')::(extract_pre e')
 
-(* Some errors *)
-
-let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
-let no_variable e = error ("No such variable: " ^ e)
-let type_error e = error ("Type error: " ^ e)
-let not_implemented e = error ("Not implemented: " ^ e)
-let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
diff --git a/interpret/rename.ml b/frontend/rename.ml
index 654b101..9c4cc31 100644
--- a/interpret/rename.ml
+++ b/frontend/rename.ml
@@ -3,8 +3,9 @@
 open Ast
 open Util
 open Ast_util
+open Typing
 
-type renaming = (id * bool) VarMap.t
+type renaming = (id * bool) VarMap.t    (* bool: is const ? *)
 
 (* consts_renaming : prog -> renaming *)
 let consts_renaming p =
diff --git a/frontend/typing.ml b/frontend/typing.ml
new file mode 100644
index 0000000..07b3bcd
--- /dev/null
+++ b/frontend/typing.ml
@@ -0,0 +1,178 @@
+(* 
+    - Instanciate a program with a root node
+    - Enumerate all the variables, give them a type
+    - Give a type to expressions
+*)
+
+open Ast
+open Ast_util
+open Util
+
+type typ =
+    | TInt
+    | TReal
+    | TEnum of string list
+
+let bool_true = "T"
+let bool_false = "F"
+let bool_type = TEnum [bool_true; bool_false]
+
+let t_of_ast_t = function
+    | AST_TINT -> TInt
+    | AST_TREAL -> TReal
+    | AST_TBOOL -> bool_type
+
+
+(* probe? * variable full name * variable type *)
+type var = bool * id * typ
+
+(* path to node * subscope prefix in node * equations in scope *)
+type scope = id * id * eqn ext list
+
+type rooted_prog = {
+    p           : prog;
+    root_node   : node_decl;
+    root_scope  : scope;
+    all_vars    : var list;
+    const_vars  : var list;
+}
+
+(* Typing *)
+
+(*
+    type_expr_vl : prog -> var list -> string -> typ list
+*)
+let rec type_expr_vl p vl cvl node expr =
+    let sub = type_expr_vl p vl cvl node in
+    let err = loc_error (snd expr) type_error in
+    match fst expr with
+    (* Identifiers *)
+    | AST_identifier(id, _) ->
+        let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) vl in [t]
+    | AST_idconst(id, _) ->
+        let _, _, t = List.find (fun (_, x, _) -> x = id) cvl in [t]
+    (* On numerical values *)
+    | AST_int_const _ -> [TInt]
+    | AST_real_const _ -> [TReal]
+    | AST_unary (_, se) ->
+        begin match sub se with
+        | [TInt] -> [TInt]
+        | [TReal] -> [TReal]
+        | _ -> err "Invalid argument for unary."
+        end
+    | AST_binary(_, a, b) ->
+        begin match sub a, sub b with
+        | [TInt], [TInt] -> [TInt]
+        | [TReal], [TReal] -> [TReal]
+        | [TInt], [TReal] | [TReal], [TInt] -> [TReal]
+        | _ -> err "Invalid argument for binary."
+        end
+    (* On boolean values *)
+    | AST_bool_const _ -> [bool_type]
+    | AST_binary_rel _ -> [bool_type] (* do not check subtypes... TODO? *)
+    | AST_binary_bool _ -> [bool_type] (* the same *)
+    | AST_not _ -> [bool_type] (* the same *)
+    (* Temporal primitives *) 
+    | AST_pre(e, _) -> sub e
+    | AST_arrow(a, b) ->
+      let ta, tb = sub a, sub b in
+      if ta = tb then ta
+        else err "Arrow does not have same type on both sides."
+    (* other *)
+    | AST_if(c, a, b) ->
+      let ta, tb = sub a, sub b in
+      if ta = tb then ta
+        else err "If does not have same type on both branches."
+    | AST_instance((f, _), _, _) ->
+      (* do not check types of arguments... TODO? *)
+      let (n, _) = find_node_decl p f in
+      List.map (fun (_, _, t) -> t_of_ast_t t) n.ret
+
+
+(* type_expr : tp -> string -> typ list *)
+let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars
+
+
+(* Program rooting *)
+
+
+(*  decls_of_node : node_decl -> var_decl list       *)
+let decls_of_node n = n.args @ n.ret @ n.var
+
+(*  vars_in_node string -> var_decl list -> var list *)
+let vars_in_node nid =
+  List.map (fun (p, id, t) -> p, nid^"/"^id, t_of_ast_t t)
+
+(* node_vars : prog -> id -> string -> var list      *)
+let node_vars p f nid =
+    let (n, _) = find_node_decl p f in
+    vars_in_node nid (decls_of_node n)
+
+(*
+    extract_all_vars : prog -> scope -> var list
+
+    Extracts all variables with names given according to
+    naming convention used here and in transform.ml :
+    - pre variables are not prefixed by scope
+    - next values for variables are prefixed by capital N
+*)
+let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars =
+    let vars_of_expr e =
+      List.flatten
+        (List.map
+          (fun (f, id, eqs, args) ->
+            let nv = node_vars p f (node^"/"^id) in
+            nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars)
+          (extract_instances p e))
+      @
+      List.flatten
+        (List.map
+          (fun (id, expr) ->
+              let vd =
+                List.mapi
+                  (fun i t -> false, id^"."^(string_of_int i), t)
+                  (type_expr_vl p n_vars const_vars node expr)
+              in
+              vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+          (extract_pre e))
+    in
+    let vars_of_eq e = match fst e with
+      | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
+      | AST_activate (b, _) ->
+        let rec do_branch = function
+          | AST_activate_body b ->
+            let bvars = vars_in_node node b.act_locals in
+            bvars @
+              extract_all_vars p
+                (node, b.act_id^".", b.body)
+                (bvars@n_vars)
+                const_vars
+          | AST_activate_if(c, a, b) ->
+            vars_of_expr c @ do_branch a @ do_branch b
+        in do_branch b
+      | AST_automaton _ -> not_implemented "extract_all vars automaton"
+    in
+      (false, node^"/"^prefix^"time", TInt)::
+      (false, "N"^node^"/"^prefix^"time", TInt)::
+      (List.flatten (List.map vars_of_eq eqs))
+
+
+(*
+    root_prog : prog -> id -> rooted_prog
+*)
+let root_prog p root =
+    let (n, _) = find_node_decl p root in
+    let root_scope = ("", "", n.body) in
+
+    let const_vars = List.map
+        (fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ))
+        (extract_const_decls p)
+    in
+
+    let root_vars = vars_in_node "" (decls_of_node n) in
+    
+    { p; root_scope; root_node = n;
+      const_vars = const_vars;
+      all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars }
+
+
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 6f7c90e..b9a5576 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,6 +1,7 @@
 open Ast
 open Util
 open Ast_util
+open Typing
 
 module I : sig
 
@@ -26,13 +27,13 @@ module I : sig
   (*
     Get the constants only
   *)
-  val consts : prog -> id -> value VarMap.t
+  val consts : rooted_prog -> value VarMap.t
 
   (*
     Construct initial state for a program.
     The id is the root node of the program evaluation.
   *)
-  val init_state : prog -> id -> state
+  val init_state : rooted_prog -> state
 
   (*
     Run a step of the program (not necessary to specify the program,
@@ -88,6 +89,7 @@ end = struct
 
 
   type state = {
+    rp         : rooted_prog;
     p          : prog;
     root_scope : scope;
     outputs    : id list;
@@ -441,13 +443,13 @@ end = struct
   (*
     init_state : prog -> id -> state
   *)
-  let init_state p root =
-    let (n, _) = find_node_decl p root in
+  let init_state rp =
     let st = {
-        p = p;
-        root_scope = get_root_scope p root;
+        rp = rp;
+        p = rp.p;
+        root_scope = rp.root_scope;
         save = VarMap.empty;
-        outputs = (List.map (fun (_,n,_) -> n) n.ret);
+        outputs = (List.map (fun (_,n,_) -> n) rp.root_node.ret);
     } in
 
     let env = { st = st; vars = Hashtbl.create 42 } in
@@ -461,11 +463,11 @@ end = struct
             | [v] -> Hashtbl.replace env.vars cpath v
             | _ -> loc_error l error "Arity error in constant expression."))
         | _ -> ())
-      p;
+      rp.p;
     List.iter (function
         | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name)
         | _ -> ())
-      p;
+      rp.p;
 
     reset_scope env st.root_scope;
     { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
@@ -485,7 +487,7 @@ end = struct
     do_weak_transitions env st.root_scope;
     extract_st env, out
 
-  let consts p root =
-    (init_state p root).save
+  let consts rp =
+    (init_state rp).save
 
 end
diff --git a/main.ml b/main.ml
index e98dd5f..b63b35f 100644
--- a/main.ml
+++ b/main.ml
@@ -31,7 +31,7 @@ let options = [
 ]
 
 let do_test_interpret prog verbose =
-    let s0 = Interpret.init_state prog "test" in
+    let s0 = Interpret.init_state (Typing.root_prog prog "test") in
     if verbose then begin
       Format.printf "Init state:@.";
       Interpret.print_state Format.std_formatter s0;
@@ -75,8 +75,8 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_itv then AI_Itv.do_prog !ai_widen_delay prog !ai_root;
-      if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root;
+      if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
+      if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
 
       if !vtest then do_test_interpret prog true
       else if !test then do_test_interpret prog false;