From ce4f339ced19e2ff7d79c2c8ec5b3ee478d5d365 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 17 Jun 2014 15:31:47 +0200 Subject: Add bindings to apron. Next : work on abstract interpret. --- interpret/ast_util.ml | 11 +++++++++++ interpret/interface.ml | 46 ---------------------------------------------- interpret/interpret.ml | 50 ++++++++++++++++++++++++++++++++++++++++++-------- 3 files changed, 53 insertions(+), 54 deletions(-) delete mode 100644 interpret/interface.ml (limited to 'interpret') 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 } (* -- cgit v1.2.3