struct: fixes, full untested version of synt (without memoization, strightforward rewrite without testing)

model_with_structures/analyzer.ml

@@ -91,6 +91,14 @@ struct
    | x :: xs, _ -> x :: list_replace xs (id - 1) y
    | [], _ -> raise Not_found
 
+  (* TODO: FIXME: check if this foldl or foldr *)
+  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
+    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
+    | [], [], [] -> acc
+    | _, _, _ -> raise Cant_fold3_error
+
+  (* --- *)
+
   (* NOTE: old variant with assoc array *)
   (* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
   (* let mem_add (mem : mem) (v : value) : mem * memid = *)
@@ -147,31 +155,32 @@ struct
 
   (* --- eval rules --- *)
 
-  (* TODO: FIXME: check if this foldl or foldr *)
-  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
-    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
-    | [], [], [] -> acc
-    | _, _, _ -> raise Cant_fold3_error
-
   (* - value construction *)
 
-  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with
-    | UnitT (Rd, w), ZeroV -> (mem, v)
-    | UnitT (Rd, w), SmthV -> (mem, v)
-    | UnitT (Rd, w), BotV -> (mem, v)
-    | UnitT (NRd, w), ZeroV -> (mem, BotV)
-    | UnitT (NRd, w), SmthV -> (mem, BotV)
-    | UnitT (NRd, w), BotV -> (mem, BotV)
+  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
+    if is_trivial_v v
+    then match t with
+    | UnitT (Rd, _) -> (mem, v)
+    | UnitT (NRd, _) -> (mem, BotV)
+    | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
+    else match t, v with
+    (* NOTE: replaced with if | best choice ?? *)
+    (* | UnitT (Rd, w), ZeroV -> (mem, v) *)
+    (* | UnitT (Rd, w), SmthV -> (mem, v) *)
+    (* | UnitT (Rd, w), BotV -> (mem, v) *)
+    (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
+    (* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
+    (* | UnitT (NRd, w), BotV -> (mem, BotV) *)
     | FunT _, FunV _ -> (mem, v)
     | RefT (Rf, _), RefV _ -> (mem, v)
     | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
                                let (mem'', id'') = mem_add mem' v' in
                                (mem'', RefV id'') 
     | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
-                                                                 mem, v' :: vs' in 
+                                                                 (mem, v' :: vs') in 
                               let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
                               (mem', TupleV vs')
-    | _, _ -> raise @@ Typing_error "valcopy"
+    | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
 
   (* - value update *)
 
@@ -287,7 +296,7 @@ struct
 
   (* full spoil *)
 
-  let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
+  let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
     match state with (mem, types, vals) ->
     let x = pathvar p in
     let id = List.assoc x vals in
@@ -301,6 +310,8 @@ struct
     match state with (mem, types, vals) -> match e, t with
       | UnitE, UnitT _ -> mem
       | PathE p, t -> argsspoilp state m t p
+      | RefE x, t -> argsspoilp state m t (VarP x)
+      (* TODO: FIXME: check RefE case ? *)
       | TupleE es, TupleT ts -> List.fold_left2
                                   (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
                                   mem ts es
@@ -313,11 +324,10 @@ struct
     let v = exprval mem oldvals e in
     (* let t' = pathtype types p in *)
     let (mem', v') = valcopy mem v t in
-    let (mem'', id) = mem_add mem' v in
+    let (mem'', id) = mem_add mem' v' in
     (mem'', (x, t) :: types, (x, id) :: vals)
 
   (* - function evaluation *)
-
   (* NOTE: not needed due to performed optimization in stmt_eval *)
   (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
 
@@ -325,21 +335,26 @@ struct
 
   let rec stmt_eval (state : state) (s : stmt) : state =
     match state with (mem, types, vals) -> match s with
-    (* TODO: FIXME: Add memoisation *)
+    (* TODO: FIXME: Add memoization *)
     | SkipS -> state
-    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in
-                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in
+    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
+                               pathval mem vals f in
+                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
+                               pathtype types f in
                        let types' : types = [] in
                        let vals' : vals = [] in
                        (match v, t with
                           | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                             (* TODO: memoisation of the called functions *)
-                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *)
-                              (fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1))
+                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
+                                                       List.fold_left2 (* TODO: FIXME: check x's order *)
+                              (fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
                               ((mem, types', vals'), 0) ts es in
                             (* NOTE: same x's, so can use same args for all the statements *)
-                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in
-                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2
+                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *)
+                                                 List.map (stmt_eval state_with_args) fstmts in
+                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
+                                              List.fold_left2
                               (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
                               mem ts es in
                             (mem_spoiled, types, vals)
@@ -368,15 +383,15 @@ struct
                           then raise @@ Eval_error "choice"
                           else (memcomb meml memr, typesl, valsl)
 
- (* --- program execution --- *)
+  (* --- program execution --- *)
 
- let prog_eval (prog : prog) : state =
-   match prog with (decls, s) ->
-   let init_state = prog_init prog in
-   stmt_eval init_state s
+  let prog_eval (prog : prog) : state =
+    match prog with (decls, s) ->
+    let init_state = prog_init prog in
+    stmt_eval init_state s
 
- let prog_eval_noret (prog : prog) : unit =
-   ignore @@ prog_eval prog
+  let prog_eval_noret (prog : prog) : unit =
+    ignore @@ prog_eval prog
 
   (* --- tests --- *)
 

model_with_structures/model.typ

@@ -926,7 +926,7 @@ $s in stmt, f in X, x in X, a in X$
     $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
 
     // TODO:: is c important ?
-    $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$,
+    $mu stretch(=>)^(m space rf c space t space rf x)_(cl vals, types cr) mu'$,
   )
 ))
 
@@ -1042,21 +1042,6 @@ $s in stmt, f in X, x in X, a in X$
 
 #h(10pt)
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ READ $p$],
-
-    $vals, mu tval p eqmu 0$,
-
-    $cl types, vals, mu cr
-     xarrow("READ" p)
-     cl types, vals, mu cr$,
-  )
-))
-
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -1074,6 +1059,21 @@ $s in stmt, f in X, x in X, a in X$
   )
 ))
 
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ READ $p$],
+
+    $vals, mu tval p eqmu 0$,
+
+    $cl types, vals, mu cr
+     xarrow("READ" p)
+     cl types, vals, mu cr$,
+  )
+))
+
+#h(10pt)
+
 #h(10pt)
 
 #align(center, prooftree(

model_with_structures/synthesizer.ml

@@ -145,16 +145,16 @@ struct
   module Decl = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('d, 't, 'e, 'dl, 'mtl, 's) t = VarD of 'd * 't * 'e | FunD of 'd * 'dl * 'mtl * 's
+      type nonrec ((* 'd, *) 't, 'e, 'dl, 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * *) 'dl * 'mtl * 's
       [@@deriving gt ~options:{ show; gmap }]
-      type ground = (Nat.ground, Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
+      type ground = ((* Nat.ground, *) Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
     ]
   end
 
-  module Prog = struct
+  module Prg = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('dl, 's) t = Prog of 'dl * 's
+      type nonrec ('dl, 's) t = Prg of 'dl * 's
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = (Decl.ground List.ground, Stmt.ground) t
     ]
@@ -173,39 +173,39 @@ struct
 
   (* --- *)
 
-  module Mem = struct
+  module MemEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('vl, 'd) t = Mem of 'vl * 'd
+      type nonrec ('vl, 'd) t = MemEnv of 'vl * 'd
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = (Value.ground List.ground, Nat.ground) t
     ]
   end
 
-  module Types = struct
+  module TypesEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'dtl t = Types of 'dtl
+      type nonrec 'dtl t = TypesEnv of 'dtl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
     ]
   end
 
-  module Vals = struct
+  module ValsEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'ddl t = Vals of 'ddl
+      type nonrec 'ddl t = ValsEnv of 'ddl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
     ]
   end
 
-  module St = struct
+  module StEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('mem, 'types, 'vals) t = St of 'mem * 'types * 'vals
+      type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
       [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t
+      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
     ]
   end
 
@@ -238,30 +238,651 @@ struct
       list_ntho xs' id' x' }
   }
 
-  let mem_geto mem id v = ocanren {
-    fresh mem_data, mem_len, rev_id  in
-    Std.pair mem_data mem_len == mem &
-    Nat.addo (Nat.s rev_id) id mem_len &
-    list_ntho mem_data rev_id v
+
+  let rec list_foldlo f acc xs acc' = ocanren {
+    xs == [] & acc' == acc |
+    { fresh x', xs', acc_upd in
+      xs == x' :: xs' &
+      list_foldlo f acc xs' acc_upd &
+      f acc_upd x' acc' }
   }
 
-  let mem_addo mem v mem_with_id' = ocanren {
-    fresh mem_data, mem_len, mem' in
-    Std.pair mem_data mem_len == mem &
-    mem' == Std.pair (v :: mem_data) (Nat.s mem_len) &
-    Std.pair mem' mem_len == mem_with_id'
+  let rec list_foldro f acc xs acc' = ocanren {
+    xs == [] & acc' == acc |
+    { fresh x', xs', acc_upd in
+      xs == x' :: xs' &
+      f acc x' acc_upd &
+      list_foldro f acc_upd xs' acc' }
+    (* TODO: inf search on swap, investigate *)
   }
 
-  let mem_seto mem id v mem' = ocanren {
-    fresh mem_data, mem_len, rev_id, mem_data' in
-    Std.pair mem_data mem_len == mem &
-    Nat.addo (Nat.s rev_id) id mem_len &
-    list_replaceo mem_data rev_id v mem_data' &
-    Std.pair mem_data' mem_len == mem'
+
+  let rec list_foldr2o f acc xs ys acc' = ocanren {
+    xs == [] & ys == [] & acc' == acc |
+    { fresh x', xs', y', ys', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      f acc x' y' acc_upd &
+      list_foldr2o f acc_upd xs' ys' acc' }
+  }
+
+  let rec list_foldl2o f acc xs ys acc' = ocanren {
+    xs == [] & ys == [] & acc' == acc |
+    { fresh x', xs', y', ys', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      list_foldl2o f acc xs' ys' acc_upd &
+      f acc_upd x' y' acc' }
+  }
+
+  let rec list_foldr3o f acc xs ys zs acc' = ocanren {
+    xs == [] & ys == [] & zs == [] & acc' == acc |
+    { fresh x', xs', y', ys', z', zs', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      zs == z' :: zs' &
+      f acc x' y' z' acc_upd &
+      list_foldr3o f acc_upd xs' ys' zs' acc' }
+  }
+
+  let rec list_foldl3o f acc xs ys zs acc' = ocanren {
+    xs == [] & ys == [] & zs == [] & acc' == acc |
+    { fresh x', xs', y', ys', z', zs', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      zs == z' :: zs' &
+      list_foldl3o f acc xs' ys' zs' acc_upd &
+      f acc_upd x' y' z' acc' }
+  }
+
+  let rec list_zip_witho f xs ys zs = ocanren {
+    { fresh x, xs', y, ys', z, zs' in
+      xs == x :: xs' &
+      ys == y :: ys' &
+      zs == z :: zs' &
+      f x y z &
+      list_zip_witho f xs' ys' zs' } |
+    { fresh x, xs' in
+      xs == x :: xs' &
+      ys == [] &
+      zs == [] } |
+    { fresh y, ys' in
+      xs == [] &
+      ys == y :: ys' &
+      zs == [] } |
+    { xs == [] & ys == [] & zs == [] }
+  }
+
+  (* --- *)
+
+  let mem_geto mem id v =
+    let open MemEnv in
+    ocanren {
+      fresh mem_data, mem_len, rev_id in
+      MemEnv (mem_data, mem_len) == mem &
+      Nat.addo (Nat.s rev_id) id mem_len &
+      list_ntho mem_data rev_id v
+  }
+
+  let mem_addo mem v mem_with_id' =
+    let open MemEnv in
+    ocanren {
+      fresh mem_data, mem_len, mem' in
+      MemEnv (mem_data, mem_len) == mem &
+      mem' == MemEnv (v :: mem_data, Nat.s mem_len) &
+      Std.pair mem' mem_len == mem_with_id'
+  }
+
+  let mem_seto mem id v mem' =
+    let open MemEnv in
+    ocanren {
+      fresh mem_data, mem_len, rev_id, mem_data' in
+      MemEnv (mem_data, mem_len) == mem &
+      Nat.addo (Nat.s rev_id) id mem_len &
+      list_replaceo mem_data rev_id v mem_data' &
+      MemEnv (mem_data', mem_len) == mem'
+  }
+
+  let is_trivial_vo v =
+    let open Value in
+    ocanren {
+    v == ZeroV | v == SmthV | v == BotV
+  }
+
+  let rec pathvaro p x =
+    let open Path in
+    ocanren {
+      p == VarP x |
+      { fresh p' in p == DerefP p' & pathvaro p' x } |
+      { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
+  }
+
+  let types_assoco id types tp =
+    let open TypesEnv in
+    ocanren {
+      fresh tps in
+      types == TypesEnv tps &
+      List.assoco id tps tp
+    }
+
+  let vals_assoco id vals v =
+    let open ValsEnv in
+    ocanren {
+      fresh vs in
+      vals == ValsEnv vs &
+      List.assoco id vs v
+    }
+
+  let rec pathtypeo types p tp =
+    let open Path in
+    let open Type in
+    ocanren {
+      { fresh x in
+        p == VarP x &
+        types_assoco x types tp } |
+      { fresh p', tp', _c in
+        p == DerefP p' &
+        pathtypeo types p' tp' &
+        tp' == RefT (_c, tp) } |
+      { fresh p', id', tp', tps in
+        p == AccessP (p', id') &
+        pathtypeo types p' tp' &
+        tp' == TupleT tps &
+        list_ntho tps id' tp }
+  }
+
+  let rec pathvalo mem vals p v =
+    let open Path in
+    let open Value in
+    ocanren {
+      { fresh x, id in
+        p == VarP x &
+        vals_assoco x vals id &
+        mem_geto mem id v } |
+      { fresh p', v', id in
+        p == DerefP p' &
+        pathvalo mem vals p' v' &
+        v' == RefV id &
+        mem_geto mem id v } |
+      { fresh p', id, v', vs in
+        p == AccessP (p', id) &
+        pathvalo mem vals p' v' &
+        v' == TupleV vs &
+        list_ntho vs id v }
+  }
+
+  (* --- eval rules --- *)
+
+  (* - value construction *)
+
+  let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
+    ocanren {
+      fresh mem, vs, mem', v', mem_with_v', vs' in
+      Std.pair mem vs == mem_with_vs &
+      valcopyo mem v tp mem_with_v' &
+      Std.pair mem' v' == mem_with_v' &
+      vs' == v' :: vs &
+      mem_with_vs' == Std.pair mem vs'
+  }
+  and valcopyo mem v tp mem_with_id' = 
+    let open Type in
+    let open Value in
+    let open ReadCap in
+    let open CopyCap in
+    ocanren {
+      { fresh r, w in
+        is_trivial_vo v &
+        tp == UnitT (r, w) &
+        { { r == Rd & mem_with_id' == Std.pair mem v } |
+          { r == NRd & mem_with_id' == Std.pair mem BotV } } } |
+      { fresh stmts, ts in
+        v == FunV stmts &
+        tp == FunT ts &
+        mem_with_id' == Std.pair mem v } |
+      { fresh c, tp', id in
+        v == RefV id &
+        tp == RefT (c, tp') &
+        { { c == Rf & mem_with_id' == Std.pair mem v } |
+          { fresh v, mem_cp, v_cp, mem_with_v_cp,
+                  mem_add, id_add, mem_with_id_add in
+            c == Cp &
+            mem_geto mem id v &
+            valcopyo mem v tp mem_with_v_cp &
+            Std.pair mem v_cp == mem_with_v_cp &
+            mem_addo mem_cp v_cp mem_with_id_add &
+            Std.pair mem_add id_add == mem_with_id_add &
+            mem_with_id' == (mem_add, RefV id_add) } } } |
+      { fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in
+        v == TupleV vs &
+        tp == TupleT tps &
+        init_mem_with_vs == Std.pair mem [] &
+        list_foldl2o valcopy_foldero init_mem_with_vs vs tps mem_with_vs' &
+        Std.pair mem' vs' == mem_with_vs' &
+        mem_with_id' == Std.pair mem' (TupleV vs') }
+  }
+
+  (* - value update *)
+
+  let rec valupdo mem v p b mem_with_v' =
+    let open Path in
+    let open Value in
+    ocanren {
+      { fresh x in
+        p == VarP x &
+        mem_with_v' == Std.pair mem b } |
+      { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
+        p == DerefP p' &
+        v == RefV id &
+        mem_geto mem id v' &
+        valupdo mem v' p' b mem_with_v_upd &
+        Std.pair mem_upd v_upd == mem_with_v_upd &
+        mem_seto mem_upd id v_upd mem_st &
+        mem_with_v' == Std.pair mem_st (RefV id) } |
+      { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
+        p == AccessP (p', id) &
+        v == TupleV vs' &
+        list_ntho vs' id v' &
+        valupdo mem v' p' b mem_with_v_upd &
+        Std.pair mem_upd v_upd == mem_with_v_upd &
+        list_replaceo vs' id v_upd vs_upd &
+        mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
+  }
+
+  (* - value combination *)
+
+  let rec valcombo u v u' =
+    let open Value in
+    ocanren {
+    { is_trivial_vo u &
+      is_trivial_vo v &
+      (* TODO: do not use disequality constraint ? *)
+      { { u == v & u' == u } | { u =/= v & u' == BotV } } } |
+    { fresh ustmts, vstmts, ustmts' in
+      u == FunV ustmts &
+      v == FunV vstmts &
+      (* TODO: swap stmts order o efficiency ? *)
+      List.appendo ustmts vstmts ustmts' &
+      u' == FunV ustmts' } |
+    { fresh a, b in
+      u == RefV a &
+      v == RefV b &
+      a == b } |
+    { fresh us, vs, us' in
+      u == TupleV us &
+      v == TupleV vs &
+      list_zip_witho valcombo us vs us' &
+      u' == TupleV us' }
+  }
+
+  let memcombo m n m' =
+    let open MemEnv in
+    ocanren {
+    fresh mm, ml, nm, nl, mm' in
+    MemEnv (mm, ml) == m &
+    MemEnv (nm, nl) == n &
+    list_zip_witho valcombo mm nm mm' &
+    m' == MemEnv (mm', ml)
+  }
+
+  (* - expression evaluation *)
+
+  let rec exprvalo mem vals e v' = 
+    let open Expr in
+    let open Value in
+    ocanren {
+      { e == UnitE & v' == ZeroV } |
+      { fresh p in
+        e == PathE p &
+        pathvalo mem vals p v' } |
+      { fresh x, v in
+        e == RefE x &
+        vals_assoco x vals v &
+        v' == RefV v } |
+      { fresh es, vs' in
+        e == TupleE es &
+        List.mapo (exprvalo mem vals) es vs' &
+        v' == TupleV vs' }
+  }
+
+  (* - expression typing *)
+
+  let rec exprtypeo types e tp' = 
+    let open Expr in
+    let open Type in
+    let open ReadCap in
+    let open WriteCap in
+    let open CopyCap in
+    ocanren {
+      { e == UnitE & tp' == UnitT (Rd, NeverWr) } |
+      { fresh p in
+        e == PathE p &
+        pathtypeo types p tp' } |
+      { fresh x, tp in
+        e == RefE x &
+        types_assoco x types tp &
+        tp' == RefT (Rf, tp) } |
+      { fresh es, tps' in
+        e == TupleE es &
+        List.mapo (exprtypeo types) es tps' &
+        tp' == TupleT tps' }
+  }
+
+  (* - context initialization *)
+
+  let add_declo st x d st' =
+    let open StEnv in
+    let open Decl in
+    let open TypesEnv in
+    let open ValsEnv in
+    ocanren {
+      fresh mem, types, vals in
+      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
+      {
+        { fresh tp, e, v,
+                mem_with_v_cp, mem_cp, v_cp,
+                mem_with_id_add, mem_add, id_add in
+          d == VarD (tp, e) &
+          exprvalo mem (ValsEnv vals) e v &
+          valcopyo mem v tp mem_with_v_cp &
+          Pair.pair mem_cp v_cp == mem_with_v_cp &
+          mem_addo mem_cp v_cp mem_with_id_add &
+          Pair.pair mem_add id_add == mem_with_id_add &
+          st' == StEnv (mem_add,
+                        TypesEnv ((Pair.pair x tp) :: types),
+                        ValsEnv ((Pair.pair x id_add) :: vals))
+          }
+      }
+  }
+
+  let empty_memo m =
+    let open MemEnv in
+    ocanren { m == MemEnv ([], 0) }
+
+  let empty_stateo st =
+    let open StEnv in
+    let open TypesEnv in
+    let open ValsEnv in
+    ocanren {
+      fresh m in
+      empty_memo m &
+      st == StEnv (m, TypesEnv [], ValsEnv [])
+  }
+
+  (* TODO: better way ??? *)
+  let globals_min_ido x = ocanren { x == 1000 }
+
+  let prog_init_foldero st_with_id d st_with_id' =
+    ocanren {
+      fresh st, x, st' in
+      Std.pair st x == st_with_id &
+      add_declo st x d st' &
+      st_with_id' == Std.pair st' (Nat.s x)
+  }
+
+  let prog_inito prog st' =
+    let open Prg in
+    ocanren {
+      fresh decls, s, st_init, min_id, st_with_id', _id' in
+      prog == Prg (decls, s) &
+      empty_stateo st_init &
+      globals_min_ido min_id &
+      list_foldlo prog_init_foldero (Std.pair st_init min_id) decls st_with_id' &
+      Std.pair st' _id' == st_with_id'
+  }
+
+  (* - call values spoil *)
+
+  (* TODO: check that negation is interpreted correctly *)
+  let is_correct_tagso v r w _r' w' m c =
+    let open Value in
+    let open ReadCap in
+    let open WriteCap in
+    let open Mode in
+    let open CopyCap in
+    ocanren {
+      { r == NRd | v == ZeroV } &
+      { r == NRd | is_ino m } &
+      { is_not_outo m | w == AlwaysWr } &
+      { w == NeverWr |
+        { is_not_outo m & c == Cp } |
+        w' == AlwaysWr } &
+      is_trivial_vo v
+  }
+
+  let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
+    fresh mem, vs, mem', v' in
+    Std.pair mem vs == mem_with_vs &
+    valspoilo mem v tp u m c (Std.pair mem' v') &
+    mem_with_vs' == Std.pair mem' (v' :: vs)
+  }
+  and valspoilo mem v tp u m c mem_with_v' =
+    let open Type in
+    let open Value in
+    let open Mode in
+    let open WriteCap in
+    let open CopyCap in
+    ocanren {
+      { fresh r, w, r', w' in
+        tp == UnitT (r, w) &
+        u == UnitT (r', w') &
+        is_trivial_vo v &
+        is_correct_tagso v r w r' w' m c &
+        {
+          { is_not_outo m &
+            c == Rf &
+            { w == AlwaysWr | w == MayWr } &
+            mem_with_v' == Std.pair mem BotV } |
+          { is_outo m &
+            w == AlwaysWr &
+            mem_with_v' == Std.pair mem ZeroV } |
+          { { is_outo m | c == Cp | w == NeverWr } &
+            { is_not_outo m | w == MayWr | w == NeverWr } &
+            mem_with_v' == Std.pair mem v }
+        } } |
+      { fresh ts, us, _stmts in
+        tp == FunT ts &
+        u == FunT us &
+        v == FunV _stmts &
+        ts == us &
+        mem_with_v' == Std.pair mem v } |
+      { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
+        tp == RefT (ctp', tp') &
+        u == RefT (cu', u') &
+        v == RefV id' &
+        mem_geto mem id' v' &
+        valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
+        mem_seto mem_sp id' v_sp mem_set &
+        mem_with_v' == Std.pair mem_set (RefV id') } |
+      { fresh tps, us, vs, mem_sp,vs_sp in
+        tp == TupleT tps &
+        u == TupleT us &
+        v == TupleV vs &
+        list_foldl3o (valspoil_foldero m c)
+                     (Std.pair mem []) tps us vs
+                     (Std.pair mem_sp vs_sp) &
+        mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
+      }
+  }
+
+  (* full spoil *)
+
+  let argspoilpo st m tp p mem' =
+    let open StEnv in
+    let open CopyCap in
+    ocanren {
+      fresh mem, types, vals, x, id, b, tp',
+            mem_sp, b_sp, v_sp, mem_upd, v_upd in
+      st == StEnv (mem, types, vals) &
+      pathvaro p x &
+      vals_assoco x vals id &
+      pathvalo mem vals p b &
+      pathtypeo types p tp' &
+      valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) &
+      mem_geto mem_sp id v_sp &
+      valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
+      mem_seto mem_upd id v_upd mem'
+  }
+
+  let rec argspoile_foldero types vals m mem tp e mem' =
+    let open StEnv in
+    ocanren {
+      fresh st in
+      st == StEnv (mem, types, vals) &
+      argspoileo st m tp e mem'
+  }
+  and argspoileo st m tp e mem' =
+    let open StEnv in
+    let open Expr in
+    let open Type in
+    let open Path in
+    ocanren {
+      fresh _r, _w, mem, types, vals in
+      st == StEnv (mem, types, vals) &
+      {
+        { e == UnitE &
+          tp == UnitT (_r, _w) &
+          mem' == mem } |
+        { fresh p in
+          e == PathE p &
+          argspoilpo st m tp p mem' } |
+        { fresh x in
+          e == RefE x &
+          argspoilpo st m tp (VarP x) mem' } |
+        { fresh es, tps in
+          e == TupleE es &
+          tp == TupleT tps &
+          list_foldl2o (argspoile_foldero types vals m) mem tps es mem'}
+      }
+  }
+
+  (* - funciton argument addition *)
+
+  let addargo st oldvals x tp e st' =
+    let open StEnv in
+    let open TypesEnv in
+    let open ValsEnv in
+    ocanren {
+      fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in
+      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
+      exprvalo mem oldvals e v &
+      valcopyo mem v tp (Std.pair mem_cp v_cp) &
+      mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
+      st' == StEnv (mem_add,
+                    TypesEnv ((Std.pair x tp) :: types),
+                    ValsEnv ((Std.pair x id_add) :: vals))
+  }
+
+  (* - function evaluation *)
+  (* NOTE: not needed due to performed optimization in stmt_eval ? *)
+
+  (* - statement evaluation *)
+  (* TODO *)
+
+  let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
+    fresh st, x, m, tp, st' in
+    Std.pair st x == st_with_id &
+    Std.pair m tp == mtp &
+    addargo st vals x tp e st' &
+    st_with_id' == Std.pair st' (Nat.s x)
+  }
+  and stmt_eval_spoil_foldero types vals mem mtp e mem' =
+    let open StEnv in
+    ocanren {
+      fresh m, tp, st in
+      Std.pair m tp == mtp &
+      st == StEnv (mem, types, vals) &
+      argspoileo st m tp e mem'
+  }
+  and stmt_evalo st s st' =
+    let open StEnv in
+    let open Stmt in
+    let open Value in
+    let open Type in
+    let open WriteCap in
+    let open TypesEnv in
+    let open ValsEnv in
+    ocanren {
+      fresh mem, types, vals in
+      st == StEnv (mem, types, vals) &
+      {
+        { s == SkipS & st == st' } |
+        { fresh f, es, v, tp, types', vals',
+                fstmts, tps, st',
+                state_with_args, _arg_id,
+                _states_evaled,
+                mem_spoiled in
+          s == CallS (f, es) &
+          pathvalo mem vals f v &
+          pathtypeo types f tp &
+          types' == TypesEnv [] &
+          vals' == ValsEnv [] &
+          v == FunV fstmts &
+          tp == FunT tps &
+          st' == StEnv (mem, types', vals') &
+          (* TODO: type error, fix required *)
+          list_foldl2o (stmt_addarg_foldero vals)
+                       (Std.pair st' 0) tps es
+                       (Std.pair state_with_args _arg_id) &
+          List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
+          (* TODO: FIXME check left or right order *)
+          list_foldl2o (stmt_eval_spoil_foldero types vals)
+                      mem tps es mem_spoiled &
+          st' == StEnv (mem_spoiled, types, vals) } |
+        { fresh p, tp, _r, w, x, id, v,
+                mem_upd, v_upd, mem_set in
+          s == WriteS p &
+          pathtypeo types p tp &
+          tp == UnitT (_r, w) &
+          { w == AlwaysWr | w == MayWr } &
+          pathvaro p x &
+          vals_assoco x vals id &
+          mem_geto mem id v &
+          valupdo mem v p ZeroV (Std.pair mem_upd v_upd) &
+          mem_seto mem_upd id v_upd mem_set &
+          st' == StEnv (mem_set, types, vals) } |
+        { fresh p in
+          s == ReadS p &
+          pathvalo mem vals p ZeroV &
+          st == st' } |
+        { fresh sl, sr, stl in
+          s == SeqS (sl, sr) &
+          stmt_evalo st sl stl &
+          stmt_evalo stl sr st' } |
+        { fresh sl, sr, stl, str,
+                meml, typesl, valsl,
+                memr, typesr, valsr,
+                mem' in
+          s == ChoiceS (sl, sr) &
+          stmt_evalo st sl stl &
+          stmt_evalo st sr str &
+          str == StEnv (memr, typesr, valsr) &
+          stl == StEnv (meml, typesl, valsl) &
+          typesl == typesr &
+          valsl == valsr &
+          memcombo meml memr mem' &
+          st' == StEnv (mem', typesl, valsl) }
+      }
+  }
+
+  (* --- program execution --- *)
+
+  let prog_evalo prog st' =
+    let open Prg in
+    ocanren {
+      fresh decls, s, init_st in 
+      prog == Prg (decls, s) &
+      prog_inito prog init_st &
+      stmt_evalo init_st s st'
   }
 
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
+  (* --- tests --- *)
+  (* TODO *)
+
+  (* - shortcuts *)
+  (* TODO *)
+
   (* --- *)
 
   (* let rec list_zip_witho f xs ys zs = ocanren { *)