Do some typing ; support multiple pre in abstract interpretation.

3 files changed, 13 insertions, 196 deletions

diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
deleted file mode 100644
index 9cfe995..0000000
--- a/interpret/ast_util.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-open Ast
-open Util
-
-(* Utility : find declaration of a const / a node *)
-
-let find_const_decl p id =
-  match List.find (function
-                   | AST_const_decl (c, _) when c.c_name = id -> true
-                   | _ -> false) 
-                  p with
-  | AST_const_decl d -> d
-  | _ -> assert false
-
-let find_node_decl p id =
-  match List.find (function
-                   | AST_node_decl (c, _) when c.n_name = id -> true
-                   | _ -> false) 
-                  p with
-  | AST_node_decl d -> d
-  | _ -> assert false
-
-let extract_const_decls =
-  List.fold_left
-    (fun l d -> match d with
-      | AST_const_decl d -> d::l
-      | _ -> l)
-    []
-
-
-(* 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 *)
-
-(* extract_instances :
-      prog -> expr ext -> (id * id * eqs * (var_def * expr ext) list) list
-*)
-let rec extract_instances p e = match fst e with
-  | AST_idconst _ | AST_identifier _
-  | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> extract_instances p e'
-  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
-  | AST_arrow(e1, e2) ->
-    extract_instances p e1 @ extract_instances p e2
-  | AST_if(e1, e2, e3) ->
-    extract_instances p e1 @ extract_instances p e2 @ extract_instances p e3
-  | AST_instance((f, _), args, id) ->
-    let more = List.flatten (List.map (extract_instances p) args) in
-    let (node, _) = find_node_decl p f in
-    let args_x = List.map2 (fun id arg -> id, arg) node.args args in
-    (f, id, node.body, args_x)::more
-
-(* Utility : find pre declarations in an expression *)
-
-(* extract_pre : expr ext -> (id * expr ext) list *)
-let rec extract_pre e = match fst e with
-  | AST_identifier _ | AST_idconst _
-  | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_not e' -> extract_pre e'
-  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
-  | AST_arrow(e1, e2) ->
-    extract_pre e1 @ extract_pre e2
-  | AST_if(e1, e2, e3) ->
-    extract_pre e1 @ extract_pre e2 @ extract_pre e3
-  | AST_instance((f, _), args, id) ->
-    List.flatten (List.map extract_pre args)
-  | 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/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/interpret/rename.ml b/interpret/rename.ml
deleted file mode 100644
index 654b101..0000000
--- a/interpret/rename.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(* Scope analyzer *)
-
-open Ast
-open Util
-open Ast_util
-
-type renaming = (id * bool) VarMap.t
-
-(* consts_renaming : prog -> renaming *)
-let consts_renaming p =
-  let cdecl = extract_const_decls p in
-  List.fold_left
-    (fun rn (d,_) -> VarMap.add d.c_name (d.c_name, true) rn)
-    VarMap.empty
-    cdecl
-
-(* add_var_defs : string -> renaming -> var_def list -> renaming *)
-let add_var_defs prefix =
-  List.fold_left
-    (fun rn (_,n,_) -> VarMap.add n (prefix^n, false) rn)
-
-(* rename_expr : expr ext -> renaming -> expr ext *)
-let rec rename_expr exp rn =
-  let sub e = rename_expr e rn in
-  let a = match fst exp with
-    | AST_identifier(id, l) ->
-      begin try let (nn, const) = VarMap.find id rn in
-          if const then AST_idconst(nn, l) else AST_identifier(nn, l)
-      with Not_found -> loc_error l no_variable id
-      end
-    | AST_idconst(id, l) -> assert false (* expression not already renamed *)
-    | AST_unary(op, e) -> AST_unary(op, sub e)
-    | AST_binary(op, a, b) -> AST_binary(op, sub a, sub b)
-    | AST_binary_rel(op, a, b) -> AST_binary_rel(op, sub a, sub b)
-    | AST_binary_bool(op, a, b) -> AST_binary_bool(op, sub a, sub b)
-    | AST_not(e) -> AST_not(sub e)
-    | AST_pre (e, x) -> AST_pre(sub e, x)
-    | AST_arrow(a, b) -> AST_arrow(sub a, sub b)
-    | AST_if(a, b, c) -> AST_if(sub a, sub b, sub c)
-    | AST_instance(i, l, s) -> AST_instance(i, List.map sub l, s)
-    | x -> x  (* other cases : constant literals *)
-  in a, snd exp
-
-(* rename_var : renaming -> id -> id *)
-let rename_var rn id =
-  try let (nn, const)= VarMap.find id rn in
-      if const then error ("Constant "^id^" cannot be defined in node.");
-      nn
-  with Not_found -> no_variable id
-
-let rename_var_ext rn (id, loc) = (rename_var rn id, loc)
-
-let rename_var_def rn (p, id, t) = (p, rename_var rn id, t)
-
-(* rename_eqn : renaming -> eqn ext -> eqn ext *)
-let rec rename_eqn rn e =
-  let a = match fst e with
-    | AST_assign(s, e) -> AST_assign (List.map (rename_var_ext rn) s, rename_expr e rn)
-    | AST_guarantee(g, e) -> AST_guarantee(g, rename_expr e rn)
-    | AST_assume(a, e) -> AST_assume(a, rename_expr e rn)
-    | AST_automaton(aid, states, ret) ->
-      let rename_state ((st:Ast.state),l) =
-        let rn = add_var_defs (aid^"."^st.st_name^".") rn st.st_locals in
-        { st with
-          st_locals = List.map (rename_var_def rn) st.st_locals;
-          body = List.map (rename_eqn rn) st.body;
-          until = List.map (fun (c, n, r) -> (rename_expr c rn, n, r)) st.until;
-        }, l
-      in 
-      AST_automaton(aid, List.map rename_state states, List.map (rename_var rn) ret)
-    | AST_activate (c, ret) ->
-      let rec rename_activate_if = function
-        | AST_activate_if(c, a, b) ->
-          AST_activate_if(rename_expr c rn, rename_activate_if a, rename_activate_if b)
-        | AST_activate_body b ->
-          let rn = add_var_defs (b.act_id^".") rn b.act_locals in
-          AST_activate_body{ b with
-            act_locals = List.map (rename_var_def rn) b.act_locals;
-            body = List.map (rename_eqn rn) b.body;
-          }
-      in
-      AST_activate(rename_activate_if c, List.map (rename_var rn) ret)
-  in a, snd e
-
-(* rename_node : renaming -> node_decl -> node_decl *)
-let rename_node const_rn node =
-  let rn = add_var_defs "" const_rn node.args in
-  let rn = add_var_defs "" rn node.ret in
-  let rn = add_var_defs "" rn node.var in
-  { node with
-    body = List.map (rename_eqn rn) node.body }
-
-(* rename_prog : prog -> prog *)
-let rename_prog p =
-  let const_rn = consts_renaming p in
-  let rn_toplevel = function
-  | AST_node_decl (n, l) -> AST_node_decl (rename_node const_rn n, l)
-  | x -> x
-  in
-  List.map rn_toplevel p
-