diff options
Diffstat (limited to 'interpret')
| -rw-r--r-- | interpret/ast_util.ml | 84 | ||||
| -rw-r--r-- | interpret/interpret.ml | 24 | ||||
| -rw-r--r-- | interpret/rename.ml | 101 |
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 - |