summaryrefslogtreecommitdiff
path: root/interpret
diff options
context:
space:
mode:
Diffstat (limited to 'interpret')
-rw-r--r--interpret/ast_util.ml35
-rw-r--r--interpret/data.ml12
-rw-r--r--interpret/interpret.ml43
-rw-r--r--interpret/sca.ml101
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
+