summaryrefslogtreecommitdiff
path: root/interpret
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 11:35:12 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 11:35:12 +0200
commit4e66de932b91e91e4cadd943ff8859d6f69f57e1 (patch)
treeced73719216f2f1fd2eb9057001079a39dbad68e /interpret
parent7205927e18ea355a619e95b1036aac9b94a22667 (diff)
downloadscade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.tar.gz
scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.zip
Clean up & comment a bit.
Diffstat (limited to 'interpret')
-rw-r--r--interpret/bad_interpret.ml308
-rw-r--r--interpret/interpret.ml7
2 files changed, 7 insertions, 308 deletions
diff --git a/interpret/bad_interpret.ml b/interpret/bad_interpret.ml
deleted file mode 100644
index 08ccf85..0000000
--- a/interpret/bad_interpret.ml
+++ /dev/null
@@ -1,308 +0,0 @@
-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/interpret.ml b/interpret/interpret.ml
index 8bdf650..f14d6e2 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,3 +1,10 @@
+(*
+ Interpret for a portion of the concrete semantics of the Scade language.
+ (basically, interpretation is handled for all the subset of the language
+ that we can parse).
+*)
+
+
open Ast
open Util
open Ast_util