Working prototype for an interpret ! But very messy.

2 files changed, 334 insertions, 0 deletions

diff --git a/interpret/data.ml b/interpret/data.ml
new file mode 100644
index 0000000..2721528
--- /dev/null
+++ b/interpret/data.ml
@@ -0,0 +1,61 @@
+(* Data structures for representing the state of a system *)
+
+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)
+
+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 -> raise (No_variable id)
+  in
+    match VarMap.find id st with
+    | VBusy -> raise (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/interpret.ml b/interpret/interpret.ml
new file mode 100644
index 0000000..4584fa4
--- /dev/null
+++ b/interpret/interpret.ml
@@ -0,0 +1,273 @@
+open Ast
+open Data
+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
+
+(* Expression evaluation *)
+
+(*
+  eval_expr : calc_map -> state -> string -> expr ext -> (state * value)
+*)
+let rec eval_expr c scope st exp =
+  let sub_eval = eval_expr c scope in
+  match fst exp with
+  | AST_identifier (id, _) ->
+    begin try let st, v = get_var st c (scope^"/"^id) in st, [v]
+    with No_variable _ -> let st, v = get_var st c ("cst/"^id) in st, [v]
+    end
+  (* 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, id) -> not_implemented "instance"
+
+(* Constant calculation *)
+
+let rec calc_const d st c =
+  match eval_expr c "cst" 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 = List.fold_left
+    (fun l d -> match d with
+      | AST_const_decl (d, _) -> d::l
+      | _ -> l)
+    [] p
+  in
+  let ccmap = List.fold_left
+    (fun c d -> VarMap.add ("cst/"^d.name) (F (calc_const 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
+
+(* Program execution *)
+
+(* 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_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_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')
+
+
+(* build calc map *)
+let rec build_prog_ccmap p scope eqs st =
+  let add_eq c eq = match fst eq with
+    | AST_assign(vars, e) ->
+      let calc st c =
+        let st, vals = eval_expr c scope 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 (fun _ a b -> match a, b with
+          | Some x, None -> Some x
+          | None, Some y -> Some y
+          | _ -> assert false) c
+          (build_prog_ccmap p (scope^"/"^ss_id) ss_eqs st)
+        in
+        let add_v c ((_, (id, _), _), eq) =
+          let calc st c =
+            let st, vals = eval_expr c scope 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"
+  in
+  List.fold_left add_eq VarMap.empty eqs
+
+let extract_next_state active p scope eqs st ccmap =
+  let csts = VarMap.filter
+    (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/")
+    st
+  in
+  let rec aux active scope eqs st nst =
+    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 p e) in
+        List.fold_left (fun (st, nst) (pn, pe) ->
+            let st, v = if active then eval_expr ccmap scope 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"
+    in
+    List.fold_left add_eq (st, r) eqs
+  in aux active scope eqs st csts
+
+let program_init_state p root_node =
+  let (n, _) = find_node_decl p root_node in
+  let rec prog_init_state_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, _) -> prog_init_state_aux st p (scope^"/"^ss_id) ss_eqs)
+    in
+    List.fold_left (fun st eq -> match fst eq with
+        | AST_assign(_, e) -> add_subscopes st (subscopes p e)
+        | AST_assume _ | AST_guarantee _ -> st
+        | AST_automaton _ -> not_implemented "prog_init_state_aux automaton")
+      st eqs
+  in
+    prog_init_state_aux (program_consts p) p "" n.body
+
+
+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 "" n.body st ccmap in
+
+  st, outputs, next_st
+  
+