Move a lot of things.

4 files changed, 151 insertions, 40 deletions

diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
new file mode 100644
index 0000000..db9a76f
--- /dev/null
+++ b/interpret/ast_util.ml
@@ -0,0 +1,35 @@
+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.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.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)
+    []
+
+(* 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)
+
diff --git a/interpret/data.ml b/interpret/data.ml
index 51afcc3..cf7d820 100644
--- a/interpret/data.ml
+++ b/interpret/data.ml
@@ -2,13 +2,7 @@
 
 open Util
 open Ast
-
-exception Combinatorial_cycle of string
-exception No_variable of string
-exception Type_error of string
-let type_error e = raise (Type_error e)
-exception Not_implemented of string
-let not_implemented e = raise (Not_implemented e)
+open Ast_util
 
 type scope = string
 
@@ -38,10 +32,10 @@ let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) =
       let r = f (VarMap.add id VBusy st) c in
       (* Format.printf "]%s " id; *)
       r
-    with Not_found -> raise (No_variable id)
+    with Not_found -> no_variable id
   in
     match VarMap.find id st with
-    | VBusy -> raise (Combinatorial_cycle id)
+    | VBusy -> combinatorial_cycle id
     | v -> st, v
 
 (* pretty-printing *)
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 373ed5f..6ff125c 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,32 +1,17 @@
 open Ast
 open Data
 open Util
+open Ast_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.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.name = id -> true
-                   | _ -> false) 
-                  p with
-  | AST_node_decl d -> d
-  | _ -> assert false
-
-(* Utility : build subscopes of equation ; extract pre declarations *)
+(* Utility : extract subscopes of equation ; extract pre declarations *)
 
 (* subscopes :
       prog -> expr ext -> (id * eqs * (id * expr ext) list) list
 *)
 let rec subscopes p e = match fst e with
-  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | AST_idconst _ | AST_identifier _
+  | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
   | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e'
   | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
   | AST_arrow(e1, e2) ->
@@ -41,7 +26,8 @@ let rec subscopes p e = match fst e with
 
 (* extract_pre : expr ext -> (id * expr ext) list *)
 let rec extract_pre e = match fst e with
-  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | 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) ->
@@ -69,13 +55,13 @@ let rec eval_expr env st exp =
   let sub_eval = eval_expr env in
   let scope = List.hd env.scopes in
   match fst exp with
-  | AST_identifier (id, _) ->
+  | AST_identifier (id, _) | AST_idconst(id, _) ->
     let rec aux = function
       | [] ->
         let st, v = get_var st env.c ("cst/"^id) in st, [v]
       | sc::q ->
         try let st, v = get_var st env.c (sc^"/"^id) in st, [v]
-        with No_variable _ -> aux q
+        with _ -> aux q
     in aux env.scopes
   (* on numerical values *)
   | AST_int_const (i, _) -> st, [VInt (int_of_string i)]
@@ -172,18 +158,13 @@ let rec calc_const p d st c =
   | _ -> type_error ("Cannot assign tuple to constant" ^ d.name)
 
 let program_consts p =
-  let cdecl = List.fold_left
-    (fun l d -> match d with
-      | AST_const_decl (d, _) -> d::l
-      | _ -> l)
-    [] p
-  in
+  let cdecl = extract_const_decls p in
   let ccmap = List.fold_left
-    (fun c d -> VarMap.add ("cst/"^d.name) (F (calc_const p d)) c)
+    (fun c (d, _) -> VarMap.add ("cst/"^d.name) (F (calc_const p d)) c)
     VarMap.empty cdecl
   in
   List.fold_left
-    (fun st d -> let st, _ = get_var st ccmap ("cst/"^d.name) in st)
+    (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.name) in st)
     VarMap.empty
     cdecl
 
@@ -211,8 +192,8 @@ let program_init_state p root_node =
   in
     aux (program_consts p) p "" n.body
 
-(* Program execution *)
 
+(* Program execution *)
 
 (* build calc map *)
 let rec build_prog_ccmap p scopes eqs st =
diff --git a/interpret/sca.ml b/interpret/sca.ml
new file mode 100644
index 0000000..4a012ae
--- /dev/null
+++ b/interpret/sca.ml
@@ -0,0 +1,101 @@
+(* 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.name (d.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_ext 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.name^".") rn st.locals in
+        { st with
+          locals = List.map (rename_var_def rn) 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.id^".") rn b.locals in
+          AST_activate_body{ b with
+            locals = List.map (rename_var_def rn) b.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
+