diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | frontend/ast.ml | 34 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 10 | ||||
| -rw-r--r-- | frontend/parser.mly | 14 | ||||
| -rw-r--r-- | interpret/ast_util.ml | 42 | ||||
| -rw-r--r-- | interpret/bad_interpret.ml (renamed from interpret/interpret.ml) | 108 | ||||
| -rw-r--r-- | interpret/data.ml | 49 | ||||
| -rw-r--r-- | interpret/interface.ml | 40 | ||||
| -rw-r--r-- | interpret/interpret2.ml | 359 | ||||
| -rw-r--r-- | interpret/rename.ml (renamed from interpret/sca.ml) | 10 | ||||
| -rw-r--r-- | main.ml | 46 |
11 files changed, 566 insertions, 152 deletions
@@ -9,8 +9,10 @@ SRC= main.ml \ frontend/lexer.mll \ frontend/ast_printer.ml \ interpret/data.ml \ - interpret/interpret.ml \ - interpret/sca.ml + interpret/bad_interpret.ml \ + interpret/interface.ml \ + interpret/interpret2.ml \ + interpret/rename.ml all: $(BIN) diff --git a/frontend/ast.ml b/frontend/ast.ml index 8392bc6..fbf099c 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -62,18 +62,18 @@ type var_def = bool * (id ext) * typ type automaton = id * state ext list * id list and state = { - initial : bool; - name : id; - locals : var_def list; - body : eqn ext list; - until : transition list; + initial : bool; + st_name : id; + st_locals : var_def list; + body : eqn ext list; + until : transition list; } and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *) and activate_block = { - id : id; - locals : var_def list; - body : eqn ext list; + act_id : id; + act_locals : var_def list; + body : eqn ext list; } and activate_if = | AST_activate_body of activate_block @@ -82,23 +82,23 @@ and activate = activate_if * id list and eqn = | AST_assign of (id ext list) * (expr ext) - | AST_guarantee of (id ext) * (expr ext) | AST_assume of (id ext) * (expr ext) + | AST_guarantee of (id ext) * (expr ext) | AST_automaton of automaton | AST_activate of activate type node_decl = { - name : id; - args : var_def list; - ret : var_def list; - var : var_def list; - body : eqn ext list; + n_name : id; + args : var_def list; + ret : var_def list; + var : var_def list; + body : eqn ext list; } type const_decl = { - name : id; - typ : typ; - value : expr ext; + c_name : id; + typ : typ; + value : expr ext; } type toplevel = diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index edd27e9..08f4fb4 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -205,7 +205,7 @@ and print_activate_if ind fmt = function Format.fprintf fmt "%selse@\n" ind; print_activate_if (indent ind) fmt e | AST_activate_body(b) -> - print_vars ind fmt b.locals; + print_vars ind fmt b.act_locals; print_body ind fmt b.body and print_automaton ind fmt (n, sts, r) = @@ -215,8 +215,8 @@ and print_automaton ind fmt (n, sts, r) = and print_state ind fmt (st, _) = Format.fprintf fmt "%s%sstate %s@\n" - ind (if st.initial then "initial " else "") st.name; - print_vars ind fmt st.locals; + ind (if st.initial then "initial " else "") st.st_name; + print_vars ind fmt st.st_locals; print_body ind fmt st.body; if st.until <> [] then begin Format.fprintf fmt "%suntil@\n" ind; @@ -233,7 +233,7 @@ and print_block ind fmt b = and print_node_decl fmt (d : node_decl) = Format.fprintf fmt "node %s(%a) returns(%a)@\n" - d.name + d.n_name (print_list print_var_decl "; ") d.args (print_list print_var_decl "; ") d.ret; print_vars "" fmt d.var; @@ -242,7 +242,7 @@ and print_node_decl fmt (d : node_decl) = let print_const_decl fmt (d : const_decl) = Format.fprintf fmt "const %s: %s = %a@\n@\n" - d.name (string_of_typ d.typ) + d.c_name (string_of_typ d.typ) print_expr (fst d.value) let print_toplevel fmt = function diff --git a/frontend/parser.mly b/frontend/parser.mly index 2483f09..0d257dd 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -118,8 +118,8 @@ state: until=trans(UNTIL) { if unless <> [] then failwith "UNLESS transitions not supported."; { initial = i; - name = n; - locals = (match v with Some v -> v | None -> []); + st_name = n; + st_locals = (match v with Some v -> v | None -> []); body = b; until = until; } } @@ -138,8 +138,8 @@ activate_if: | IF c=ext(expr) THEN t=activate_if ELSE e=activate_if { AST_activate_if(c, t, e) } | lv=option(var_decl) b=body { AST_activate_body { - id = "activate"^uid(); - locals = (match lv with Some v -> v | None -> []); + act_id = "act"^uid(); + act_locals = (match lv with Some v -> v | None -> []); body = b; } } @@ -179,7 +179,7 @@ vars: const_decl: | CONST i=IDENT COLON t=typ EQUAL e=ext(expr) SEMICOLON { { - name = i; + c_name = i; typ = t; value = e; } } @@ -195,7 +195,7 @@ node_decl: | node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN e = dbody -{ { name = id; +{ { n_name = id; args = v; ret = rv; var = []; @@ -205,7 +205,7 @@ node_decl: RETURNS LPAREN rv=vars RPAREN lv=var_decl b=body -{ { name = id; +{ { n_name = id; args = v; ret = rv; var = lv; diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml index db9a76f..e7428bd 100644 --- a/interpret/ast_util.ml +++ b/interpret/ast_util.ml @@ -5,7 +5,7 @@ open Util let find_const_decl p id = match List.find (function - | AST_const_decl (c, _) when c.name = id -> true + | AST_const_decl (c, _) when c.c_name = id -> true | _ -> false) p with | AST_const_decl d -> d @@ -13,7 +13,7 @@ let find_const_decl p id = let find_node_decl p id = match List.find (function - | AST_node_decl (c, _) when c.name = id -> true + | AST_node_decl (c, _) when c.n_name = id -> true | _ -> false) p with | AST_node_decl d -> d @@ -26,6 +26,44 @@ let extract_const_decls = | _ -> l) [] + +(* Utility : find instances declared in an expression *) + +(* extract_instances : + prog -> expr ext -> (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 + (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) diff --git a/interpret/interpret.ml b/interpret/bad_interpret.ml index 6ff125c..08ccf85 100644 --- a/interpret/interpret.ml +++ b/interpret/bad_interpret.ml @@ -3,41 +3,57 @@ open Data open Util open Ast_util +(* Data structures for the interpret *) + +type scope = string + +type svalue = + | VInt of int + | VBool of bool + | VReal of float + | VState of id + | VPrevious of value + | VBusy (* intermediate value : calculating ! for detection of cycles *) +and value = svalue list + +type state = svalue VarMap.t + +(* functions for recursively getting variables *) + +type calc_fun = + | F of (state -> calc_map -> state) +and calc_map = calc_fun VarMap.t + +let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) = + let st = + if VarMap.mem id st then st + else match VarMap.find id c with + | F f -> + (* Format.printf "%s[ " id; *) + let r = f (VarMap.add id VBusy st) c in + (* Format.printf "]%s " id; *) + r + in + match VarMap.find id st with + | VBusy -> combinatorial_cycle id + | v -> st, v + +(* pretty-printing *) + +let rec str_of_value = function + | VInt i -> string_of_int i + | VReal r -> string_of_float r + | VBool b -> if b then "true" else "false" + | VState s -> "state " ^ s + | VPrevious p -> + "[" ^ + List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p + ^ "]" + | VBusy -> "#" +let print_state st = + VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st -(* 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_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) -> - subscopes p e1 @ subscopes p e2 - | AST_if(e1, e2, e3) -> - subscopes p e1 @ subscopes p e2 @ subscopes p e3 - | AST_instance((f, _), args, id) -> - let more = List.flatten (List.map (subscopes 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 - (id, node.body, args_x)::more - -(* 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') (* Expression evaluation *) @@ -55,14 +71,16 @@ 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_idconst(id, _) -> + | AST_identifier (id, _) -> let rec aux = function | [] -> - let st, v = get_var st env.c ("cst/"^id) in st, [v] + no_variable id | sc::q -> try let st, v = get_var st env.c (sc^"/"^id) in st, [v] - with _ -> aux q - in aux env.scopes + with Not_found -> aux q + in loc_error (snd exp) aux env.scopes + | AST_idconst (id, _) -> + let st, v = get_var st env.c ("cst/"^id) in st, [v] (* on numerical values *) | AST_int_const (i, _) -> st, [VInt (int_of_string i)] | AST_real_const (r, _) -> st, [VReal (float_of_string r)] @@ -131,7 +149,7 @@ let rec eval_expr env st exp = | VBool true -> sub_eval st before | VBool false -> sub_eval st after | _ -> assert false - with Not_found -> assert false + with Not_found -> error ("Internal: could not find init for scope " ^ scope) end (* other *) | AST_if(cond, a, b) -> @@ -154,17 +172,17 @@ let rec eval_expr env st exp = let rec calc_const p d st c = let env = { p = p; c = c; scopes = ["cst"] } in match eval_expr env st d.value with - | st, [v] -> VarMap.add ("cst/"^d.name) v st - | _ -> type_error ("Cannot assign tuple to constant" ^ d.name) + | st, [v] -> VarMap.add ("cst/"^d.c_name) v st + | _ -> type_error ("Cannot assign tuple to constant" ^ d.c_name) let program_consts p = 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.c_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.c_name) in st) VarMap.empty cdecl @@ -177,7 +195,7 @@ let program_init_state p root_node = List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs) in let add_eq st eq = match fst eq with - | AST_assign(_, e) -> add_subscopes st (subscopes p e) + | AST_assign(_, e) -> add_subscopes st (extract_instances p e) | AST_assume _ | AST_guarantee _ -> st | AST_automaton (aid, astates, ret) -> let (initial, _) = List.find (fun (s, _) -> s.initial) astates in @@ -225,7 +243,7 @@ let rec build_prog_ccmap p scopes eqs st = in List.fold_left add_v c ss_args in - List.fold_left add_subscope c (subscopes p e) + List.fold_left add_subscope c (extract_instances p e) | AST_assume _ | AST_guarantee _ -> c | AST_automaton _ -> not_implemented "build_prog_ccmap for automaton" | AST_activate _ -> not_implemented "build_prog_ccmap for activate" @@ -251,7 +269,7 @@ let extract_next_state active env eqs st = in let add_eq (st, nst) eq = match fst eq with | AST_assign(vars, e) -> - let st, nst = add_subscopes active (st, nst) (subscopes env.p e) in + let st, nst = add_subscopes active (st, nst) (extract_instances env.p e) in List.fold_left (fun (st, nst) (pn, pe) -> let st, v = if active then eval_expr { env with scopes = scopes } st pe else st, diff --git a/interpret/data.ml b/interpret/data.ml index cf7d820..1d91e93 100644 --- a/interpret/data.ml +++ b/interpret/data.ml @@ -4,52 +4,3 @@ open Util open Ast open Ast_util -type scope = string - -type svalue = - | VInt of int - | VBool of bool - | VReal of float - | VState of id - | VPrevious of value - | VBusy (* intermediate value : calculating ! for detection of cycles *) -and value = svalue list - -type state = svalue VarMap.t - -(* functions for recursively getting variables *) - -type calc_fun = - | F of (state -> calc_map -> state) -and calc_map = calc_fun VarMap.t - -let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) = - let st = - if VarMap.mem id st then st - else try match VarMap.find id c with - | F f -> - (* Format.printf "%s[ " id; *) - let r = f (VarMap.add id VBusy st) c in - (* Format.printf "]%s " id; *) - r - with Not_found -> no_variable id - in - match VarMap.find id st with - | VBusy -> combinatorial_cycle id - | v -> st, v - -(* pretty-printing *) - -let rec str_of_value = function - | VInt i -> string_of_int i - | VReal r -> string_of_float r - | VBool b -> if b then "true" else "false" - | VState s -> "state " ^ s - | VPrevious p -> - "[" ^ - List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p - ^ "]" - | VBusy -> "#" -let print_state st = - VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st - diff --git a/interpret/interface.ml b/interpret/interface.ml new file mode 100644 index 0000000..7b84396 --- /dev/null +++ b/interpret/interface.ml @@ -0,0 +1,40 @@ +open Ast + + +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 + + (* + 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/interpret2.ml b/interpret/interpret2.ml new file mode 100644 index 0000000..33439e6 --- /dev/null +++ b/interpret/interpret2.ml @@ -0,0 +1,359 @@ +open Ast +open Util +open Ast_util +open Interface + +module I : INTERPRET = struct + + (* Values for variables *) + + exception Bad_datatype + + type value = + | VInt of int + | VBool of bool + | VReal of float + | VState of id + | VPrevious of value list + | VBusy (* intermediate value : calculating ! *) + | VCalc of (unit -> value) + + let int_value i = VInt i + let bool_value b = VBool b + let real_value r = VReal r + + let as_int = function + | VInt i -> i + | _ -> raise Bad_datatype + let as_bool = function + | VBool b -> b + | _ -> raise Bad_datatype + let as_real = function + | VReal r -> r + | _ -> raise Bad_datatype + + let rec str_repr_of_val = function + | VInt i -> string_of_int i + | VReal r -> string_of_float r + | VBool b -> if b then "true" else "false" + | VState s -> "state " ^ s + | VPrevious p -> + "[" ^ + List.fold_left (fun s v -> + (if s = "" then "" else s ^ ", ") ^ str_repr_of_val v) + "" p + ^ "]" + | VBusy -> "#" + | VCalc _ -> "()" + + (* 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; + root_scope : scope; + outputs : id list; + save : value VarMap.t; + } + + let print_state fmt st = + VarMap.iter + (fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v)) + st.save + + type io = (id * value) list + + + (* Internal type env : contains the environment for state calculation *) + type env = { + st : state; + vars : (id, value) Hashtbl.t; + } + + + (* + get_var : env -> id -> id -> value + + Gets the value of a variable relative to a node path. + *) + let get_var env node id = + let p = node^"/"^id in + try match Hashtbl.find env.vars p with + | VCalc f -> + Hashtbl.replace env.vars p VBusy; + f () + | VBusy -> combinatorial_cycle p + | x -> x + with + | Not_found -> no_variable p + + (* + eval_expr : env -> (id * id) -> expr ext -> value list + *) + let rec eval_expr env (node, prefix) exp = + let sub_eval = eval_expr env (node, prefix) in + match fst exp with + | AST_identifier (id, _) -> + [loc_error (snd exp) (get_var env node) id] + | AST_idconst (id, _) -> + begin try [VarMap.find ("cst/"^id) env.st.save] + with Not_found -> loc_error (snd exp) no_variable id end + (* on numerical values *) + | AST_int_const (i, _) -> [VInt (int_of_string i)] + | AST_real_const (r, _) -> [VReal (float_of_string r)] + | AST_unary(AST_UPLUS, e) -> sub_eval e + | AST_unary(AST_UMINUS, e) -> + begin match sub_eval e with + | [VInt x] -> [VInt (-x)] + | [VReal x] -> [VReal(-. x)] + | _ -> type_error "Unary on non-numerical." + end + | AST_binary(op, e1, e2) -> + let iop, fop = match op with + | AST_PLUS -> (+), (+.) + | AST_MINUS -> (-), (-.) + | AST_MUL -> ( * ), ( *. ) + | AST_DIV -> (/), (/.) + | AST_MOD -> (mod), mod_float + in + begin match sub_eval e1, sub_eval e2 with + | [VInt a], [VInt b] -> [VInt (iop a b)] + | [VReal a], [VReal b] -> [VReal(fop a b)] + | _ -> type_error "Invalid arguments for numerical binary." + end + (* on boolean values *) + | AST_bool_const b -> [VBool b] + | AST_binary_rel(op, e1, e2) -> + let r = match op with + | AST_EQ -> (=) | AST_NE -> (<>) + | AST_LT -> (<) | AST_LE -> (<=) + | AST_GT -> (>) | AST_GE -> (>=) + in + begin match sub_eval e1, sub_eval e2 with + | [VInt a], [VInt b] -> [VBool (r a b)] + | [VReal a], [VReal b] -> [VBool (r a b)] + | [VBool a], [VBool b] -> [VBool (r a b)] + | _ -> type_error "Invalid arguments for binary relation." + end + | AST_binary_bool(op, e1, e2) -> + let r = match op with + | AST_AND -> (&&) | AST_OR -> (||) + in + begin match sub_eval e1, sub_eval e2 with + | [VBool a], [VBool b] -> [VBool (r a b)] + | _ -> type_error "Invalid arguments for boolean relation." + end + | AST_not(e) -> + begin match sub_eval e with + | [VBool b] -> [VBool (not b)] + | _ -> type_error "Invalid arguments for boolean negation." + end + (* temporal primitives *) + | AST_pre(exp, n) -> + begin try match VarMap.find (node^"/"^prefix^n) env.st.save with + | VPrevious x -> x + | _ -> assert false + with Not_found -> [] + end + | AST_arrow(before, after) -> + begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with + | VBool true -> sub_eval before + | VBool false -> sub_eval after + | _ -> assert false + with Not_found -> assert false + end + (* other *) + | AST_if(cond, a, b) -> + begin match sub_eval cond with + | [VBool true] -> sub_eval a + | [VBool false] -> sub_eval b + | _ -> type_error "Invalid condition in if." + end + | AST_instance((f, _), args, nid) -> + let (n, _) = find_node_decl env.st.p f in + List.map + (fun (_, (id, _), _) -> get_var env (node^"/"^nid) id) + n.ret + + (* + reset_scope : env -> scope -> unit + + Sets all the init variables to true, and all the state variables + to initial state. Does this recursively. + *) + let rec reset_scope env (node, prefix, eqs) = + Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true); + let do_exp e = + List.iter + (fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs)) + (extract_instances env.st.p e) + in + let do_eq (e, _) = match e with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e + | AST_automaton (aid, states, _) -> + let (init_state, _) = List.find (fun (st, _) -> st.initial) states in + Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name); + List.iter + (fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body)) + states + | AST_activate (x, _) -> + let rec aux = function + | AST_activate_if (_, a, b) -> aux a; aux b + | AST_activate_body b -> + reset_scope env (node, b.act_id^".", b.body) + in aux x + in + List.iter do_eq eqs + + (* + activate_scope : env -> scope -> unit + + Adds functions for calculating the variables in this scope. + For assign : simple ! + For automaton : lazily select+activate automaton state (would enable + implementation of strong transitions) + For activate : lazily select+activate active block + *) + let rec activate_scope env (node, prefix, eqs) = + Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true); + let do_expr e = + List.iter + (fun (id, eqs, args) -> + activate_scope env (node^"/"^id, "", eqs); + let do_arg ((_,(name,_),_), expr) = + let apath = node^"/"^id^"/"^name in + let calc () = + match eval_expr env (node, prefix) expr with + | [v] -> Hashtbl.replace env.vars apath v; v + | _ -> loc_error (snd expr) error "Unsupported arity for argument." + in + Hashtbl.replace env.vars apath (VCalc calc) + in + List.iter do_arg args) + (extract_instances env.st.p e) + in + let do_eq (e, _) = match e with + | AST_assign(vars, e) -> + do_expr e; + let calc i () = + let vals = eval_expr env (node, prefix) e in + List.iter2 (fun (id, _) v -> + Hashtbl.replace env.vars (node^"/"^id) v) vars vals; + List.nth vals i + in + List.iteri + (fun i (id, _) -> + Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc i))) + vars + | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e + | _ -> not_implemented "activate_scope" + in + List.iter do_eq eqs + + (* + is_scope_active : env -> scope -> bool + *) + let is_scope_active env (node, prefix, _) = + try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act")) + with Not_found -> false + + (* + do_weak_transitions : env -> scope -> unit + *) + let do_weak_transitions env (node, prefix, eqs) = + not_implemented "do_weak_transitions" + + (* + extract_st : env -> state + *) + let extract_st env = + let rec aux (node, prefix, eqs) save = + + let init = + try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init")) + with Not_found -> + let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save) + in pre_init && (not (is_scope_active env (node, prefix, eqs))) + in + let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in + + let save_expr save e = + let save = List.fold_left + (fun save (id, expr) -> + VarMap.add + (node^"/"^prefix^id) + (VPrevious (eval_expr env (node, prefix) expr)) + save) + save (extract_pre e) in + let save = List.fold_left + (fun save (n, eqs, _) -> + aux (node^"/"^n, "", eqs) save) + save (extract_instances env.st.p e) + in save + in + let save_eq save eq = match fst eq with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> + save_expr save e + | AST_automaton(aid, states, _) -> not_implemented "save_eq automaton" + | AST_activate(r, _) -> not_implemented "save_eq activate" + in + List.fold_left save_eq save eqs + + in + let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in + { env.st with save = aux env.st.root_scope consts } + + (* + init_state : prog -> id -> state + *) + 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; + save = VarMap.empty; + outputs = (List.map (fun (_,(n,_),_) -> n) n.ret); + } in + + let env = { st = st; vars = Hashtbl.create 42 } in + + (* calculate constants *) + List.iter (function + | AST_const_decl(d, l) -> + let cpath = "cst/" ^ d.c_name in + Hashtbl.replace env.vars cpath (VCalc (fun () -> + match eval_expr env ("cst", "") d.value with + | [v] -> Hashtbl.replace env.vars cpath v; v + | _ -> loc_error l error "Arity error in constant expression.")) + | _ -> ()) + p; + List.iter (function + | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name) + | _ -> ()) + p; + + reset_scope env root_scope; + { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty } + + (* + step : state -> io -> (state * io) + *) + let step st i = + let vars = Hashtbl.create 10 in + List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i; + let env = { st = st; vars = vars } in + + activate_scope env st.root_scope; + (* + Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars; + *) + let out = List.map (fun id -> id, get_var env "" id) st.outputs in + (* do_weak_transitions env st.root_scope; *) + extract_st env, out + + +end diff --git a/interpret/sca.ml b/interpret/rename.ml index 4a012ae..46c6f04 100644 --- a/interpret/sca.ml +++ b/interpret/rename.ml @@ -10,7 +10,7 @@ type renaming = (id * bool) VarMap.t 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) + (fun rn (d,_) -> VarMap.add d.c_name (d.c_name, true) rn) VarMap.empty cdecl @@ -60,9 +60,9 @@ let rec rename_eqn rn e = | 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 + let rn = add_var_defs (aid^"."^st.st_name^".") rn st.st_locals in { st with - locals = List.map (rename_var_def rn) st.locals; + 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 @@ -73,9 +73,9 @@ let rec rename_eqn rn e = | 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 + let rn = add_var_defs (b.act_id^".") rn b.act_locals in AST_activate_body{ b with - locals = List.map (rename_var_def rn) b.locals; + act_locals = List.map (rename_var_def rn) b.act_locals; body = List.map (rename_eqn rn) b.body; } in @@ -1,5 +1,7 @@ open Ast +module Interpret = Interpret2.I + (* command line options *) let dump = ref false let dumprn = ref false @@ -28,40 +30,44 @@ let () = let prog = File_parser.parse_file !ifile in if !dump then Ast_printer.print_prog Format.std_formatter prog; - let prog = Sca.rename_prog prog in + let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; if !vtest then begin - let s0 = Interpret.program_init_state prog "test" in + let s0 = Interpret.init_state prog "test" in Format.printf "Init state:@."; - Data.print_state s0; + Interpret.print_state Format.std_formatter s0; let rec it i st = - let st, outputs, next_st = - Interpret.program_step prog st - ["i", Data.VInt i] "test" + let next_st, out = + Interpret.step st + ["i", Interpret.int_value i] in Format.printf "@.> Step %d:@." i; - Data.print_state st; - match List.assoc "exit" outputs with - | Data.VBool false -> it (i+1) next_st - | _ -> () + Interpret.print_state Format.std_formatter st; + Format.printf "Outputs:@."; + List.iter + (fun (k, v) -> Format.printf "%s = %s@." + k (Interpret.str_repr_of_val v)) + out; + if not (Interpret.as_bool (List.assoc "exit" out)) then + it (i+1) next_st in it 0 s0 end; + if !test then begin - let s0 = Interpret.program_init_state prog "test" in + let s0 = Interpret.init_state prog "test" in let rec it i st = - let st, outputs, next_st = - Interpret.program_step prog st - ["i", Data.VInt i] "test" + let next_st, outputs = + Interpret.step st + ["i", Interpret.int_value i] in Format.printf "%d. %s %s %s@." i - (Data.str_of_value (List.assoc "a" outputs)) - (Data.str_of_value (List.assoc "b" outputs)) - (Data.str_of_value (List.assoc "c" outputs)); - match List.assoc "exit" outputs with - | Data.VBool false -> it (i+1) next_st - | _ -> () + (Interpret.str_repr_of_val (List.assoc "a" outputs)) + (Interpret.str_repr_of_val (List.assoc "b" outputs)) + (Interpret.str_repr_of_val (List.assoc "c" outputs)); + if not (Interpret.as_bool (List.assoc "exit" outputs)) then + it (i+1) next_st in it 0 s0 end |