struct: analyzer & synthesizer val build, small fixes

model_with_structures/analyzer.ml

@@ -195,6 +195,19 @@ struct
 
   (* - value construction *)
 
+  let rec valbuild (mem : mem) (t : atype) : mem * value =
+    match t with
+    | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
+    | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
+    | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported"
+    | RefT (_, t) -> let (mem', v') = valbuild mem t in
+                     let (mem'', id'') = mem_add mem' v' in
+                     (mem'', RefV id'') 
+    | TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in
+                                                        (mem', v' :: vs') in 
+                   let mem', vs' = List.fold_right folder ts (mem, []) in
+                   (mem', TupleV vs')
+
   let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
     match t, v with
     | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
@@ -204,10 +217,10 @@ struct
     | RefT (_, 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
+    | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in
                                                                  (mem', v' :: vs') in 
-                              let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
+                              let mem', vs' = List.fold_right2 folder vs ts (mem, []) in
-                              (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
+                              (mem', TupleV vs')
     | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
 
   (* - action rules *)

model_with_structures/model.typ

@@ -540,9 +540,69 @@ $action$ - действия, совершаемые с примитивным з
 
 === Value Construction
 
+#let build = `build`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build trivial read value],
+
+    $mu xarrowSquiggly(cl Read \, w cr)_build
+     cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build trivial $not$ read value],
+
+    $mu xarrowSquiggly(cl not Read \, w cr)_build
+     cl cdl bot, 0_r, 0_w cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+// TODO: function pointer type ??
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build reference value],
+
+    $mu xarrowSquiggly(t)_build cl v, mu_v cr$,
+
+    $mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
+
+    $mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build tuple value],
+
+    $mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
+    $...$,
+    $mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
+
+    $mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
+  )
+))
+
+#h(10pt)
+
+// ---
+
 // TODO: FIXME:add ref / copy modes correctness check ??
 
-#let new = `new`
+// #let copy = `copy`
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -551,22 +611,26 @@ $action$ - действия, совершаемые с примитивным з
 
     $v_m in {0, ?, bot}$,
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl Read \, w cr)_new
+     xarrowSquiggly(cl Read \, w cr)_copy
-     cl cdl v_m, 0, 0 cdr, mu cr$,
+     cl cdl v_m, 0_r, 0_w cdr, mu cr$,
   )
 ))
 
+#h(10pt)
+
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
 //     name: [ new trivial read $top$ value],
 
 //     $cl cdl top, v_r, v_w cdr, mu cr
-//      xarrowSquiggly(cl Read \, w cr)_new
+//      xarrowSquiggly(cl Read \, w cr)_copy
 //      cl cdl 0, 0, 0 cdr, mu cr$,
 //   )
 // ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -574,53 +638,61 @@ $action$ - действия, совершаемые с примитивным з
 
     $v_m in {0, ?, bot/*, top */}$,
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl not Read \, w cr)_new
+     xarrowSquiggly(cl not Read \, w cr)_copy
-     cl cdl bot, 0, 0 cdr, mu cr$,
+     cl cdl bot, 0_r, 0_w cdr, mu cr$,
   )
 ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new funciton pointer value],
 
-    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
+    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$,
   )
 ))
 
+#h(10pt)
+
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
 //     name: [ new reference ref value],
 
-//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
+//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$,
 //   )
 // ))
 
+// #h(10pt)
+
 // NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new reference /* copy */ value],
 
-    $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
+    $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$,
 
     $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
 
-    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
+    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$,
   )
 ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new tuple value],
 
-    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
+    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$,
     $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
+    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$,
 
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
+    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$,
   )
 ))
 
@@ -1067,7 +1139,7 @@ $action$ - действия, совершаемые с примитивным з
     // expect well typed program
 
     $vals, mu texpre e eqmu v$,
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?)
+    $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?)
     $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
 
     $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
@@ -1354,7 +1426,7 @@ $action$ - действия, совершаемые с примитивным з
     // TODO: check type compatibility for t and type for path p (?)
     // [*TODO: check t ~ t' in sme way (?)*],
     // <- programs considired to be well-typed
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
+    $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$,
     $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
 
     // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??

model_with_structures/synthesizer.ml

@@ -588,6 +588,44 @@ struct
 
   (* - value construction *)
 
+  let rec valbuild_foldero mem_with_vs tp mem_with_vs' =
+    ocanren {
+      fresh mem, vs, mem', v', vs' in
+      Std.pair mem vs == mem_with_vs &
+      valbuildo mem tp (Std.pair mem' v') &
+      vs' == v' :: vs &
+      mem_with_vs' == Std.pair mem' vs'
+  }
+  and valbuildo mem tp mem_with_id' = 
+    let open Type in
+    let open Value in
+    let open ReadCap in
+    (* let open CopyCap in *)
+    let open MemVal in
+    let open ReadVal in
+    let open WriteVal in
+    ocanren {
+      { fresh r, w in
+        tp == UnitT (r, w) &
+        { { r == Rd &
+            mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } |
+          { r == NRd &
+            mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
+      (* { fresh ts in *)
+        (* tp == FunT ts & *)
+        (* ??? } | *)
+      { fresh c, tp' in
+        tp == RefT (c, tp') &
+        { fresh mem_cp, v_cp, mem_add, id_add in
+          valbuildo mem tp' (Std.pair mem_cp v_cp) &
+          mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
+          mem_with_id' == (mem_add, RefV id_add) } } |
+      { fresh tps, mem', vs' in
+        tp == TupleT tps &
+        list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') &
+        mem_with_id' == Std.pair mem' (TupleV vs') }
+  }
+
   let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
     ocanren {
       fresh mem, vs, mem', v', vs' in
@@ -606,7 +644,6 @@ struct
     let open WriteVal in
     ocanren {
       { fresh r, w in
-        is_trivial_vo v &
         tp == UnitT (r, w) &
         { { fresh v_m, _v_r, _v_w in
             r == Rd &

model_with_structures/tests_f.ml

@@ -1018,8 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
                     ReadS sb_access3]
                    sendFBranch &
               seqo [ChoiceS (sendFBranch, SkipS);
-                    WriteS (VarP 0));
+                    WriteS (VarP 0);
-                    ReadS (VarP 0))]
+                    ReadS (VarP 0)]
                    sendF &
 
               fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@@ -1027,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
               access_deref_accesso 1 1 0 sa_access1 &
               access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
               access_deref_accesso 0 1 0 sa_access3 &
-              seqo [WriteS (VarP 0));
+              seqo [WriteS (VarP 0);
                     CallS (VarP sendID, [PathE (VarP 0)]);
                     CallS (VarP get_version_idID, [PathE (VarP 0)]);
                     CallS (VarP updated_versionID, [PathE (VarP 0)]);