From 617231f214ace1bc3a2aa48e18db319575166047 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 13 Jun 2014 17:45:00 +0200 Subject: Begin of new interpret with more imperative concepts. Scope activation 'n stuff. --- interpret/ast_util.ml | 42 +++++- interpret/bad_interpret.ml | 308 ++++++++++++++++++++++++++++++++++++++ interpret/data.ml | 49 ------- interpret/interface.ml | 40 +++++ interpret/interpret.ml | 290 ------------------------------------ interpret/interpret2.ml | 359 +++++++++++++++++++++++++++++++++++++++++++++ interpret/rename.ml | 101 +++++++++++++ interpret/sca.ml | 101 ------------- 8 files changed, 848 insertions(+), 442 deletions(-) create mode 100644 interpret/bad_interpret.ml create mode 100644 interpret/interface.ml delete mode 100644 interpret/interpret.ml create mode 100644 interpret/interpret2.ml create mode 100644 interpret/rename.ml delete mode 100644 interpret/sca.ml (limited to 'interpret') 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/bad_interpret.ml b/interpret/bad_interpret.ml new file mode 100644 index 0000000..08ccf85 --- /dev/null +++ b/interpret/bad_interpret.ml @@ -0,0 +1,308 @@ +open Ast +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 + + + + +(* Expression evaluation *) + +type eval_env = { + p: prog; + c: calc_map; + scopes: string list; +} + +(* + eval_expr : eval_env -> string -> expr ext -> (state * value) +*) +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, _) -> + let rec aux = function + | [] -> + no_variable id + | sc::q -> + try let st, v = get_var st env.c (sc^"/"^id) in st, [v] + 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)] + | AST_unary(AST_UPLUS, e) -> sub_eval st e + | AST_unary(AST_UMINUS, e) -> + begin match sub_eval st e with + | st, [VInt x] -> st, [VInt (-x)] + | st, [VReal x] -> st, [VReal(-. x)] + | _ -> type_error "Unary on non-numerical." + end + | AST_binary(op, e1, e2) -> + let st, v1 = sub_eval st e1 in + let st, v2 = sub_eval st e2 in + let iop, fop = match op with + | AST_PLUS -> (+), (+.) + | AST_MINUS -> (-), (-.) + | AST_MUL -> ( * ), ( *. ) + | AST_DIV -> (/), (/.) + | AST_MOD -> (mod), mod_float + in + begin match v1, v2 with + | [VInt a], [VInt b] -> st, [VInt (iop a b)] + | [VReal a], [VReal b] -> st, [VReal(fop a b)] + | _ -> type_error "Invalid arguments for numerical binary." + end + (* on boolean values *) + | AST_bool_const b -> st, [VBool b] + | AST_binary_rel(op, e1, e2) -> + let st, v1 = sub_eval st e1 in + let st, v2 = sub_eval st e2 in + let r = match op with + | AST_EQ -> (=) | AST_NE -> (<>) + | AST_LT -> (<) | AST_LE -> (<=) + | AST_GT -> (>) | AST_GE -> (>=) + in + begin match v1, v2 with + | [VInt a], [VInt b] -> st, [VBool (r a b)] + | [VReal a], [VReal b] -> st, [VBool (r a b)] + | [VBool a], [VBool b] -> st, [VBool (r a b)] + | _ -> type_error "Invalid arguments for binary relation." + end + | AST_binary_bool(op, e1, e2) -> + let st, v1 = sub_eval st e1 in + let st, v2 = sub_eval st e2 in + let r = match op with + | AST_AND -> (&&) | AST_OR -> (||) + in + begin match v1, v2 with + | [VBool a], [VBool b] -> st, [VBool (r a b)] + | _ -> type_error "Invalid arguments for boolean relation." + end + | AST_not(e) -> + begin match sub_eval st e with + | st, [VBool b] -> st, [VBool (not b)] + | _ -> type_error "Invalid arguments for boolean negation." + end + (* temporal primitives *) + | AST_pre(exp, n) -> + begin try match VarMap.find (scope^"/"^n) st with + | VPrevious x -> st, x + | _ -> st, [] + with Not_found -> st, [] + end + | AST_arrow(before, after) -> + begin try match VarMap.find (scope^"/init") st with + | VBool true -> sub_eval st before + | VBool false -> sub_eval st after + | _ -> assert false + with Not_found -> error ("Internal: could not find init for scope " ^ scope) + end + (* other *) + | AST_if(cond, a, b) -> + let st, cv = sub_eval st cond in + begin match cv with + | [VBool true] -> sub_eval st a + | [VBool false] -> sub_eval st b + | _ -> type_error "Invalid condition in if." + end + | AST_instance((f, _), args, nid) -> + let (n, _) = find_node_decl env.p f in + List.fold_left + (fun (st, vs) (_, (id,_), _) -> + let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in + st, vs @ [v]) + (st, []) n.ret + +(* Constant calculation *) + +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.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.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.c_name) in st) + VarMap.empty + cdecl + +(* get initial state for program *) +let program_init_state p root_node = + let (n, _) = find_node_decl p root_node in + let rec aux st p scope eqs = + let st = VarMap.add (scope^"/init") (VBool true) st in + let add_subscopes = + 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 (extract_instances p e) + | AST_assume _ | AST_guarantee _ -> st + | AST_automaton (aid, astates, ret) -> + let (initial, _) = List.find (fun (s, _) -> s.initial) astates in + let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in + let add_astate st ((astate:Ast.state), _) = + aux st p (scope^":"^aid^"."^astate.name) astate.body + in + List.fold_left add_astate st astates + | AST_activate _ -> not_implemented "program_init_state activate" + in + List.fold_left add_eq st eqs + in + aux (program_consts p) p "" n.body + + +(* Program execution *) + +(* build calc map *) +let rec build_prog_ccmap p scopes eqs st = + let scope = List.hd scopes in + let add_eq c eq = match fst eq with + | AST_assign(vars, e) -> + let calc st c = + let env = { p = p; c = c; scopes = scopes } in + let st, vals = eval_expr env st e in + List.fold_left2 + (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st) + st vars vals + in + let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in + + let add_subscope c (ss_id, ss_eqs, ss_args) = + let c = VarMap.merge disjoint_union c + (build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st) + in + let add_v c ((_, (id, _), _), eq) = + let calc st c = + let env = { p = p; c = c; scopes = scopes } in + let st, vals = eval_expr env st eq in + match vals with + | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st + | _ -> type_error "invalid arity" + in + VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c + in + List.fold_left add_v c ss_args + in + 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" + in + List.fold_left add_eq VarMap.empty eqs + +let extract_next_state active env eqs st = + let csts = VarMap.filter + (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/") + st + in + let rec aux active scopes eqs st nst = + let scope = List.hd env.scopes in + + let r = VarMap.add (scope^"/init") + (if active then VBool false + else try VarMap.find (scope^"/init") st with Not_found -> assert false) + nst + in + let add_subscopes active = + List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) -> + aux active [scope^"/"^ss_id] ss_eqs st nst) + in + let add_eq (st, nst) eq = match fst eq with + | AST_assign(vars, e) -> + 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, + try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> [] + with Not_found -> [] + in + st, VarMap.add (scope^"/"^pn) (VPrevious v) nst) + (st, nst) (extract_pre e) + | AST_assume _ | AST_guarantee _ -> st, nst + | AST_automaton _ -> not_implemented "extract_next_state automaton" + | AST_activate _ -> not_implemented "extract_next_state activate" + in + List.fold_left add_eq (st, r) eqs + in aux active env.scopes eqs st csts + + + +let program_step p st inputs root_node = + let (n, _) = find_node_decl p root_node in + let st = List.fold_left + (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in + + let ccmap = build_prog_ccmap p [""] n.body st in + + let st = List.fold_left + (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st) + st n.ret in + let outputs = List.map + (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v)) + n.ret in + + let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in + + st, outputs, next_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/interpret.ml b/interpret/interpret.ml deleted file mode 100644 index 6ff125c..0000000 --- a/interpret/interpret.ml +++ /dev/null @@ -1,290 +0,0 @@ -open Ast -open Data -open Util -open Ast_util - - -(* 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 *) - -type eval_env = { - p: prog; - c: calc_map; - scopes: string list; -} - -(* - eval_expr : eval_env -> string -> expr ext -> (state * value) -*) -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, _) -> - 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 _ -> aux q - in aux env.scopes - (* on numerical values *) - | AST_int_const (i, _) -> st, [VInt (int_of_string i)] - | AST_real_const (r, _) -> st, [VReal (float_of_string r)] - | AST_unary(AST_UPLUS, e) -> sub_eval st e - | AST_unary(AST_UMINUS, e) -> - begin match sub_eval st e with - | st, [VInt x] -> st, [VInt (-x)] - | st, [VReal x] -> st, [VReal(-. x)] - | _ -> type_error "Unary on non-numerical." - end - | AST_binary(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let iop, fop = match op with - | AST_PLUS -> (+), (+.) - | AST_MINUS -> (-), (-.) - | AST_MUL -> ( * ), ( *. ) - | AST_DIV -> (/), (/.) - | AST_MOD -> (mod), mod_float - in - begin match v1, v2 with - | [VInt a], [VInt b] -> st, [VInt (iop a b)] - | [VReal a], [VReal b] -> st, [VReal(fop a b)] - | _ -> type_error "Invalid arguments for numerical binary." - end - (* on boolean values *) - | AST_bool_const b -> st, [VBool b] - | AST_binary_rel(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let r = match op with - | AST_EQ -> (=) | AST_NE -> (<>) - | AST_LT -> (<) | AST_LE -> (<=) - | AST_GT -> (>) | AST_GE -> (>=) - in - begin match v1, v2 with - | [VInt a], [VInt b] -> st, [VBool (r a b)] - | [VReal a], [VReal b] -> st, [VBool (r a b)] - | [VBool a], [VBool b] -> st, [VBool (r a b)] - | _ -> type_error "Invalid arguments for binary relation." - end - | AST_binary_bool(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let r = match op with - | AST_AND -> (&&) | AST_OR -> (||) - in - begin match v1, v2 with - | [VBool a], [VBool b] -> st, [VBool (r a b)] - | _ -> type_error "Invalid arguments for boolean relation." - end - | AST_not(e) -> - begin match sub_eval st e with - | st, [VBool b] -> st, [VBool (not b)] - | _ -> type_error "Invalid arguments for boolean negation." - end - (* temporal primitives *) - | AST_pre(exp, n) -> - begin try match VarMap.find (scope^"/"^n) st with - | VPrevious x -> st, x - | _ -> st, [] - with Not_found -> st, [] - end - | AST_arrow(before, after) -> - begin try match VarMap.find (scope^"/init") st with - | VBool true -> sub_eval st before - | VBool false -> sub_eval st after - | _ -> assert false - with Not_found -> assert false - end - (* other *) - | AST_if(cond, a, b) -> - let st, cv = sub_eval st cond in - begin match cv with - | [VBool true] -> sub_eval st a - | [VBool false] -> sub_eval st b - | _ -> type_error "Invalid condition in if." - end - | AST_instance((f, _), args, nid) -> - let (n, _) = find_node_decl env.p f in - List.fold_left - (fun (st, vs) (_, (id,_), _) -> - let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in - st, vs @ [v]) - (st, []) n.ret - -(* Constant calculation *) - -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) - -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) - VarMap.empty cdecl - in - List.fold_left - (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.name) in st) - VarMap.empty - cdecl - -(* get initial state for program *) -let program_init_state p root_node = - let (n, _) = find_node_decl p root_node in - let rec aux st p scope eqs = - let st = VarMap.add (scope^"/init") (VBool true) st in - let add_subscopes = - 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_assume _ | AST_guarantee _ -> st - | AST_automaton (aid, astates, ret) -> - let (initial, _) = List.find (fun (s, _) -> s.initial) astates in - let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in - let add_astate st ((astate:Ast.state), _) = - aux st p (scope^":"^aid^"."^astate.name) astate.body - in - List.fold_left add_astate st astates - | AST_activate _ -> not_implemented "program_init_state activate" - in - List.fold_left add_eq st eqs - in - aux (program_consts p) p "" n.body - - -(* Program execution *) - -(* build calc map *) -let rec build_prog_ccmap p scopes eqs st = - let scope = List.hd scopes in - let add_eq c eq = match fst eq with - | AST_assign(vars, e) -> - let calc st c = - let env = { p = p; c = c; scopes = scopes } in - let st, vals = eval_expr env st e in - List.fold_left2 - (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st) - st vars vals - in - let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in - - let add_subscope c (ss_id, ss_eqs, ss_args) = - let c = VarMap.merge disjoint_union c - (build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st) - in - let add_v c ((_, (id, _), _), eq) = - let calc st c = - let env = { p = p; c = c; scopes = scopes } in - let st, vals = eval_expr env st eq in - match vals with - | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st - | _ -> type_error "invalid arity" - in - VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c - in - List.fold_left add_v c ss_args - in - List.fold_left add_subscope c (subscopes 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" - in - List.fold_left add_eq VarMap.empty eqs - -let extract_next_state active env eqs st = - let csts = VarMap.filter - (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/") - st - in - let rec aux active scopes eqs st nst = - let scope = List.hd env.scopes in - - let r = VarMap.add (scope^"/init") - (if active then VBool false - else try VarMap.find (scope^"/init") st with Not_found -> assert false) - nst - in - let add_subscopes active = - List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) -> - aux active [scope^"/"^ss_id] ss_eqs st nst) - 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 - List.fold_left (fun (st, nst) (pn, pe) -> - let st, v = if active then eval_expr { env with scopes = scopes } st pe - else st, - try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> [] - with Not_found -> [] - in - st, VarMap.add (scope^"/"^pn) (VPrevious v) nst) - (st, nst) (extract_pre e) - | AST_assume _ | AST_guarantee _ -> st, nst - | AST_automaton _ -> not_implemented "extract_next_state automaton" - | AST_activate _ -> not_implemented "extract_next_state activate" - in - List.fold_left add_eq (st, r) eqs - in aux active env.scopes eqs st csts - - - -let program_step p st inputs root_node = - let (n, _) = find_node_decl p root_node in - let st = List.fold_left - (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in - - let ccmap = build_prog_ccmap p [""] n.body st in - - let st = List.fold_left - (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st) - st n.ret in - let outputs = List.map - (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v)) - n.ret in - - let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in - - st, outputs, next_st - - 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/rename.ml b/interpret/rename.ml new file mode 100644 index 0000000..46c6f04 --- /dev/null +++ b/interpret/rename.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.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_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.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 + diff --git a/interpret/sca.ml b/interpret/sca.ml deleted file mode 100644 index 4a012ae..0000000 --- a/interpret/sca.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.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 - -- cgit v1.2.3