Add bindings to apron. Next : work on abstract interpret.

3 files changed, 53 insertions, 54 deletions

diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
index 80411d8..f5a1978 100644
--- a/interpret/ast_util.ml
+++ b/interpret/ast_util.ml
@@ -27,6 +27,17 @@ 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 *)
 
 (* extract_instances :
diff --git a/interpret/interface.ml b/interpret/interface.ml
deleted file mode 100644
index 621bfa2..0000000
--- a/interpret/interface.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-open Ast
-open Util
-
-
-module type INTERPRET = sig
-
-
-  exception Bad_datatype
-  type value
-
-  val int_value : int -> value
-  val bool_value : bool -> value
-  val real_value : float -> value
-
-  val as_int : value -> int
-  val as_bool : value -> bool
-  val as_real : value -> float
-
-  val str_repr_of_val : value -> string
-
-  type state
-
-  val print_state : Format.formatter -> state -> unit
-
-  type io = (id * value) list
-
-  (*
-    Get the constants only
-  *)
-  val consts : prog -> id -> 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
-
-  (*
-    Run a step of the program (not necessary to specify the program,
-      it should be encoded in the state).
-    State -> Inputs -> Next state, Outputs
-  *)
-  val step : state -> io -> (state * io)
-
-end
-
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 24903f1..f28bce0 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,9 +1,47 @@
 open Ast
 open Util
 open Ast_util
-open Interface
 
-module I : INTERPRET = struct
+module I : sig
+
+  exception Bad_datatype
+  type value
+
+  val int_value : int -> value
+  val bool_value : bool -> value
+  val real_value : float -> value
+
+  val as_int : value -> int
+  val as_bool : value -> bool
+  val as_real : value -> float
+
+  val str_repr_of_val : value -> string
+
+  type state
+
+  val print_state : Format.formatter -> state -> unit
+
+  type io = (id * value) list
+
+  (*
+    Get the constants only
+  *)
+  val consts : prog -> id -> 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
+
+  (*
+    Run a step of the program (not necessary to specify the program,
+      it should be encoded in the state).
+    State -> Inputs -> Next state, Outputs
+  *)
+  val step : state -> io -> (state * io)
+
+end = struct
 
   (* Values for variables *)
 
@@ -48,8 +86,6 @@ module I : INTERPRET = struct
 
   (* States of the interpret *)
 
-  (* path to node * subscope prefix in node * equations in scope *)
-  type scope = id * id * eqn ext list
 
   type state = {
     p          : prog;
@@ -407,11 +443,9 @@ module I : INTERPRET = struct
   *)
   let init_state p root =
     let (n, _) = find_node_decl p root in
-    let root_scope = ("", "", n.body) in
-
     let st = {
         p = p;
-        root_scope = root_scope;
+        root_scope = get_root_scope p root;
         save = VarMap.empty;
         outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
     } in
@@ -433,7 +467,7 @@ module I : INTERPRET = struct
         | _ -> ())
       p;
 
-    reset_scope env root_scope;
+    reset_scope env st.root_scope;
     { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
 
   (*