projct structure refactoring

experiments/old_model_init.ml

@@ -0,0 +1,169 @@
+open OCanren
+
+(* TODO: lift to logic domain *)
+type tag = Ref | ConstRef | ShallowCopy | ConstShallowCopy | DeepCopy | NoneRef;;
+(* MoveShallowCopy ? *)
+
+type typ = UnitT | IntT | BoolT | RefT of typ | PairT of typ * typ;;
+type mode = InM | OutM | InOutM;;
+type arg = {
+  tag: tag;
+  mode: mode;
+  typ: typ;
+};;
+
+type op = AddOp | SubOp | NotOp | LessOp | MoreOp | LessEqOp | MoreEqOp | EqOp | NotEqOp;;
+
+type expr = IntE of int
+          | BoolE of bool
+          | VarE of string
+          (* pair *)
+          | PairE of expr * expr
+          | FstE of expr
+          | SndE of expr
+          (* pointers *)
+          | DerefE of expr
+          | RefE of expr
+          ;; (* TODO: op *)
+
+type stmt = DeclS of string * typ
+          | AssignS of string * expr (* TODO: rvalue exprs *)
+          | SeqS of stmt * stmt
+          | ExprS of expr
+          | CallS of string * string list (* TODO: exprs?? *)
+          | IfS of expr * stmt * stmt;;
+
+type func_def = {
+  f_args: arg list;
+  f_body: stmt;
+};;
+
+type prog = {
+  p_func: (string * func_def) list;
+  p_code: stmt;
+};;
+
+(* ------ *)
+
+type value = IntV of int
+           | BoolV of bool
+           | BoxV of string (* ref to box, lvalue *)
+           | RefV of value
+           | PairV of value * value
+           | UnitV;;
+
+module M = Map.Make (String);;
+
+type func_env = func_def M.t;;
+type 'a frame = {
+  f_vars: 'a M.t;
+};;
+type 'a state = {
+  s_func: func_env;
+  s_frames: 'a frame list;
+  (* s_value: 'a; *)
+};;
+
+let init_state prog = { s_func = prog.p_func |> List.to_seq |> M.of_seq;
+                        s_frames = [];
+                        (* s_value = UnitV; *)
+                      };;
+
+let find_func name state = M.find_opt name state.s_func;;
+
+let find_frame_var name frame = M.find_opt name frame.f_vars;;
+let rec find_frames_var name frames =
+  match frames with
+  | [] -> None
+  | fr :: frs -> (match find_frame_var name fr with
+                  | Some x -> Some x
+                  | None -> find_frames_var name frs);;
+let find_var name state = find_frames_var name state.s_frames;;
+
+let add_var name value state =
+  match state.s_frames with
+  | [] -> failwith "No frames found"
+  | fr :: frs -> { state with s_frames = {f_vars = M.add name value fr.f_vars} :: frs};;
+
+let update_frame_var name value frame =
+  if M.find_opt name frame.f_vars != None then Some {f_vars = M.add name value frame.f_vars} else None;;
+let rec update_frames_var name value frames =
+  match frames with
+  | [] -> None
+  | fr :: frs -> (match update_frame_var name value fr with
+                  | Some fr -> Some (fr :: frs)
+                  | None -> Option.map (fun frs -> fr :: frs) @@ update_frames_var name value frs);;
+let update_var name value state =
+  Option.map (fun frs -> {state with s_frames = frs}) @@
+             update_frames_var name value state.s_frames ;;
+
+let check_op_types expr state = ();;
+
+(* TODO *)
+(* let ( let* ) = Option.bind;; *)
+
+(* TODO *)
+(* TODO: handle refs in proper way *)
+(* NOTE: exprs are pure and do not change state *)
+let rec check_expr_types expr state =
+  match expr with
+  | IntE _ -> IntT
+  | BoolE b -> BoolT
+  | VarE name -> RefT (Option.get @@ find_var name state)
+  (* pair *)
+  | PairE (fst_e, snd_e) -> PairT (check_expr_types fst_e state, check_expr_types snd_e state)
+  | FstE e ->
+    (match check_expr_types e state with
+     | PairT (t, _) -> t
+     | _ -> failwith "Fst type error")
+  | SndE e ->
+    (match check_expr_types e state with
+     | PairT (_, t) -> t
+     | _ -> failwith "Snd type error")
+  (* pointers *)
+  | DerefE e ->
+    (match check_expr_types e state with
+     | RefT t -> t
+     | _ -> failwith "Deref type eror")
+  | RefE e -> RefT (check_expr_types e state);;
+
+let expect_eq fst_val snd_val msg =
+ if fst_val == snd_val then fst_val else failwith msg;;
+
+let expect_neq fst_val snd_val msg =
+ if fst_val != snd_val then fst_val else failwith msg;;
+
+let expect_some value msg =
+ if value != None then Option.get value else failwith msg;;
+
+(* TODO *)
+let rec check_stmt_types stmt (state : typ state) =
+  match stmt with
+  | DeclS (name, typ) -> add_var name typ state
+  | AssignS (name, val_e) ->
+    let val_t = check_expr_types val_e state in
+    (match find_var name state with
+     | Some t -> ignore @@ expect_eq t val_t "Can't assign value of the different type"
+     | None -> failwith "Varible to assign to is not found");
+    state
+  | SeqS (fst_s, snd_s) ->
+    let state = check_stmt_types fst_s state in
+    check_stmt_types snd_s state
+  | ExprS e -> ignore @@ check_expr_types e state; state
+  | CallS (name, args) ->
+    let func = expect_some (find_func name state) "Called function not found" in
+    List.iter2 (fun arg_t arg_v ->
+    let arg_vt = expect_some (find_var arg_v state) "Call: arg var not found" in
+    ignore @@ expect_eq arg_t.typ arg_vt "Call: wrong argument type"
+    ) func.f_args args;
+    state
+  | IfS (cond_e, then_s, else_s) ->
+    ignore @@ expect_eq (check_expr_types cond_e state) BoolT "If condition is not bool";
+    ignore @@ check_stmt_types then_s state;
+    ignore @@ check_stmt_types else_s state;
+    state
+
+(* TODO *)
+let parse str = ();;
+(* TODO *)
+let eval stmt state = ();;

experiments/simplest_model_init.ml

@@ -0,0 +1,130 @@
+open OCanren
+
+type data = int
+
+type tag = Ref | ConstRef | Value
+type stmt = Call of data * data list | Read of data | Write of data
+
+type body = stmt list
+
+type fun_decl = tag list * body
+
+type prog = fun_decl list * body
+
+(* --- interpreter --- *)
+
+(*
+init vals values: 0
+write: ++value
+read: print value with name
+*)
+
+module M = Map.Make (Int);;
+
+let read_var env id = env.(id);;
+let inc_var env id = env.(id) <- env.(id) + 1; env;;
+let replace_var env id value = env.(id) <- value; env;;
+
+let apply_env f_env args env =
+  List.fold_left2 replace_var env args (Array.to_list f_env);;
+
+let rec eval_stmt env prog stmt =
+  match stmt with
+    | Call (f_id, args) -> eval_fun env prog (List.nth prog f_id) args
+    | Read id -> Printf.printf "var.%i = %i\n" id @@ read_var env id; env
+    | Write id -> inc_var env id
+
+and eval_body env prog body = List.fold_left (fun env stmt -> eval_stmt env prog stmt) env body
+
+and eval_fun env prog decl args =
+  match decl with (arg_tags, body) ->
+  let f_env = Array.map (fun x -> read_var env x) @@ Array.of_list args in
+  let f_env_result = eval_body f_env prog body in
+  apply_env f_env_result args env;;
+
+(* --- abstracted types --- *)
+
+type 'a a_stmt = ACall of 'a * 'a list | ARead of 'a | AWrite of 'a
+type 'stmt a_body = 'stmt list
+type ('id, 'stmt) a_fun_decl = 'id list * 'stmt a_body
+type ('fun_decl, 'body) a_prog = 'fun_decl list * 'body
+
+(* --- logic types --- *)
+
+type l_data = Std.Nat.logic
+type l_tag = tag ilogic
+type l_stmt  = l_data a_stmt ilogic
+type l_body  = l_data a_stmt ilogic
+type l_fun_decl = (l_data, l_stmt) a_fun_decl ilogic
+type l_prog  = (l_fun_decl, l_body) a_prog ilogic
+
+(* --- relational verifier --- *)
+
+(* TODO *)
+
+(* --- comments --- *)
+
+(*
+f 0:
+ WRITE(0)
+
+f' 0:
+ READ(0)
+
+main:
+ f(0)
+ READ(0)
+
+*)
+
+(*
+>> ref | const ref | copy:
+
+-> write into the arg => != const ref
+
+-> call function with ref => != const ref
+
+-> read var right after function call (no write between) => != ref
+
+-> call function on var right after function call (no write between) => != ref
+
+// TODO: check that vvar used to read before write inside? <- probably could be assumed correct
+// TODO: intruduce Unused tag ?
+
+------
+
+>> :ref | copy:
+write argument in function & write after any function call => !ref
+call function with arg ref that modifies & write after any function call => !ref
+
+*)
+
+(* TODO: example *)
+(* module Tree = struct *)
+  (* ocanren type 'a tree = Leaf | Node of 'a * 'a tree * 'a tree *)
+
+  (* type int tree = GT.int tree [@@deriving gt ~options:{show}] *)
+  (* A shortcut for "ground" tree we're going to work with in "functional" code *)
+  (* type rtree = Std.Nat.ground tree [@@deriving gt ~options:{show}] *)
+
+  (* Logic counterpart *)
+  (* type ltree = Std.Nat.logic tree_logic [@@deriving gt ~options:{show}] *)
+
+  (* let leaf    () : Std.Nat.injected tree_injected = inj Leaf *)
+  (* let node a b c : Std.Nat.injected tree_injected = inj @@ Node (a,b,c) *)
+
+  (* Injection *)
+  (* let rec inj_tree : inttree -> Std.Nat.injected tree_injected = fun tree -> *)
+     (* inj @@ GT.(gmap tree_fuly Std.nat inj_tree tree) *)
+
+  (* Projection *)
+  (* let rec prj_tree : rtree -> inttree = *)
+    (* fun eta -> GT.(gmap tree_fuly) Std.Nat.to_int prj_tree eta *)
+
+  (* let reify_tree : (Std.Nat.injected tree_injected, ltree) Reifier.t = *)
+    (* tree_reify Std.Nat.reify *)
+
+  (* let prj_exn_tree : (Std.Nat.injected tree_injected, inttree) Reifier.t = *)
+    (* let rec tree_to_int x = GT.gmap tree_fuly Std.Nat.to_int (tree_to_int) x in *)
+    (* Reifier.fmap tree_to_int (tree_prj_exn Std.Nat.prj_exn) *)
+(* end *)