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/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)]);