struct: relational interpreter: complex test (in forward direction, no synt, no complex annotations)

model_with_structures/synthesizer.ml

@@ -529,12 +529,11 @@ struct
 
   let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
     ocanren {
-      fresh mem, vs, mem', v', mem_with_v', vs' in
+      fresh mem, vs, mem', v', vs' in
       Std.pair mem vs == mem_with_vs &
-      valcopyo mem v tp mem_with_v' &
+      valcopyo mem v tp (Std.pair mem' v') &
-      Std.pair mem' v' == mem_with_v' &
       vs' == v' :: vs &
-      mem_with_vs' == Std.pair mem vs'
+      mem_with_vs' == Std.pair mem' vs'
   }
   and valcopyo mem v tp mem_with_id' = 
     let open Type in
@@ -561,12 +560,11 @@ struct
             valcopyo mem v' 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 vs, tps, mem', vs', vs'' in
+      { fresh vs, tps, mem', vs' in
         v == TupleV vs &
         tp == TupleT tps &
-        list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
+        list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
-        List.reverso vs' vs'' &
+        mem_with_id' == Std.pair mem' (TupleV vs') }
-        mem_with_id' == Std.pair mem' (TupleV vs'') }
   }
 
   (* - value update *)
@@ -634,7 +632,14 @@ struct
 
   (* - expression evaluation *)
 
-  let rec exprvalo mem vals e v' = 
+  (* let rec exprval_foldero mem vals vs e vs' = ocanren { *)
+    (* fresh v' in *)
+    (* exprvalo mem vals e v' & *)
+    (* vs' == v' :: vs *)
+  (* } *)
+  (* and *)
+  let rec
+  exprvalo mem vals e v' = 
     let open Expr in
     let open Value in
     ocanren {
@@ -648,6 +653,7 @@ struct
         v' == RefV v } |
       { fresh es, vs' in
         e == TupleE es &
+        (* list_foldro (exprval_foldero mem vals) [] es vs' & *)
         List.mapo (exprvalo mem vals) es vs' &
         v' == TupleV vs' }
   }
@@ -692,9 +698,14 @@ struct
                 types', vals' in
           d == VarD (tp, e) &
           exprvalo mem vals e v &
+          (* v == TupleV [ZeroV; ZeroV] & (* FIXME TMP *) *)
           valcopyo mem v tp (Pair.pair mem_cp v_cp) &
+          (* mem_cp == mem & v_cp == v & *)
           mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
+          (* mem_add == mem_cp & *)
           types_glob_addo types x tp types' &
+          (* types == types' & *)
+          (* vals == vals' & *)
           vals_glob_addo vals x id_add vals' &
           st' == StEnv (mem_add, types', vals', visited) } |
         { fresh tps, s,
@@ -813,15 +824,14 @@ struct
         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, vs_sp' in
+      { fresh tps, us, vs, mem_sp, vs_sp in
         tp == TupleT tps &
         u == TupleT us &
         v == TupleV vs &
-        list_foldl3o (valspoil_foldero m c)
+        list_foldr3o (valspoil_foldero m c)
                      (Std.pair mem []) tps us vs
                      (Std.pair mem_sp vs_sp) &
-        List.reverso vs_sp vs_sp' &
+        mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
-        mem_with_v' == Std.pair mem_sp (TupleV vs_sp')
       }
   }
 

model_with_structures/tests_f.ml

@@ -17,8 +17,10 @@ open InCap
 open OutCap
 open Mode
 
-@type answer = StEnv.ground GT.list with show
+@type answer =
-@type answerCpCap = CopyCap.ground GT.list with show
+  StEnv.ground GT.list with show
+@type answerCpCap =
+  CopyCap.ground GT.list with show
 
 (* - shortcuts *)
 
@@ -501,3 +503,155 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
                                                ReadS (DerefP (VarP yg)))) &
               prog_evalo prog st })
   (fun q -> q#reify (CopyCap.prj_exn))))
+
+(* - complex tests *)
+
+let deref_accesso id v p' = ocanren {
+    p' == DerefP (AccessP (VarP v, id))
+  }
+
+let access_deref_accesso id_ext id_int v p' = ocanren {
+    p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
+  }
+
+let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren {
+    p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
+  }
+
+(* TODO *)
+let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh (* types *)
+                    uT_r_aw,
+                    user_utilsT, user_infoT,
+                    userT, versionT, utilsT,
+                    requestT,
+                    moded_requestT,
+                    (* global vars init exprs *)
+                    user_utilsE, user_infoE,
+                    userE, versionE, utilsE,
+                    requestE,
+                    (* global vars ids *)
+                    user_utilsID, user_infoID,
+                    userID, versionID, utilsID,
+                    dataID, requestID,
+                    (* function ids *)
+                    get_version_idID,
+                    updated_versionID,
+                    sendID,
+                    send_allID,
+                    (* function definitions *)
+                    get_version_idF,
+                    updated_versionF,
+                    sendFBranch,
+                    sendF,
+                    send_allF,
+                    (* other *)
+                    prog in
+              (* types *)
+              uT_r_aw == UnitT (Rd, AlwaysWr) &
+              user_utilsT == TupleT [uT_r_aw (* 0 id *); uT_r_aw] &
+              user_infoT ==  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] &
+              userT == TupleT [RefT (Cp, user_utilsT) (* 0 utils *);
+                               RefT (Cp, user_infoT) (* 1 info *)] &
+              versionT == TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] &
+              utilsT == TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] &
+              requestT == TupleT [RefT (Cp, userT) (* 0 user *);
+                                  RefT (Cp, versionT) (* 1 version *);
+                                  RefT (Cp, utilsT) (* 2 utils *);
+                                  RefT (Cp, uT_r_aw) (* 3 data *);
+                                  uT_r_aw (* 4 operation_date *)] &
+              moded_requestT == (Mode (In, NOut), requestT) &
+              (* global vars init exprs *)
+              user_utilsE == TupleE [UnitE (* 0 id *); UnitE] &
+              user_infoE ==  TupleE [UnitE (* 0 name *); UnitE; UnitE] &
+              userE == TupleE [RefE user_utilsID (* 0 utils *);
+                               RefE user_infoID (* 1 info *)] &
+              versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] &
+              utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] &
+              requestE == TupleE [RefE userID (* 0 user *);
+                                  RefE versionID (* 1 version *);
+                                  RefE utilsID (* 2 utils *);
+                                  RefE dataID (* 3 data *);
+                                  UnitE (* 4 operation_date *)] &
+              (* global vars ids *)
+              globals_min_ido user_utilsID &
+              user_infoID == Nat.s user_utilsID &
+              userID == Nat.s user_infoID &
+              versionID == Nat.s userID &
+              utilsID == Nat.s versionID &
+              dataID == Nat.s utilsID &
+              requestID == Nat.s dataID &
+              (* function ids *)
+              get_version_idID == Nat.s requestID &
+              updated_versionID == Nat.s get_version_idID &
+              sendID == Nat.s updated_versionID &
+              send_allID == Nat.s sendID &
+              (* function definitions *)
+              fresh gvi_access0 in
+              access_deref_accesso 0 1 0 gvi_access0 &
+              get_version_idF == ChoiceS (ReadS gvi_access0, SkipS) &
+
+              fresh uv_access0, uv_access1, uv_access2 in
+              access_deref_accesso 0 2 0 uv_access0 &
+              access_deref_accesso 0 1 0 uv_access1 &
+              access_deref_accesso 1 1 0 uv_access2 &
+              seqo [ReadS uv_access0;
+                    ReadS uv_access1;
+                    ReadS uv_access2]
+                   updated_versionF &
+
+              fresh sb_access0, sb_access1, sb_access2, sb_access3 in
+              access_deref_accesso 0 2 0 sb_access0 &
+              deref_accesso 3 0 sb_access1 &
+              deref_accesso 3 0 sb_access2 &
+              access_deref_access_deref_accesso 0 1 0 0 sb_access3 &
+              seqo [WriteS sb_access0;
+                    ReadS sb_access1;
+                    WriteS sb_access2;
+                    ReadS sb_access3]
+                   sendFBranch &
+              seqo [ChoiceS (sendFBranch, SkipS);
+                    WriteS (AccessP (VarP 0, 4));
+                    (* TODO: read all the substructure ?? *)
+                    ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *)
+                   sendF &
+
+              fresh sa_access0, sa_access1, sa_access2, sa_access3 in
+              access_deref_accesso 0 1 0 sa_access0 &
+              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 (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *)
+                    CallS (VarP sendID, [PathE (VarP 0)]);
+                    CallS (VarP get_version_idID, [PathE (VarP 0)]);
+                    CallS (VarP updated_versionID, [PathE (VarP 0)]);
+                    (* TODO: read all the substructure ?? *)
+                    WriteS sa_access0;
+                    WriteS sa_access1;
+                    ChoiceS (
+                      ReadS sa_access2,
+                      ReadS sa_access3
+                    )]
+                   send_allF &
+
+              prog == Prg ([
+                VarD (user_utilsT, user_utilsE);
+                VarD (user_infoT, user_infoE);
+                VarD (userT, userE);
+                VarD (versionT, versionE);
+                VarD (utilsT, utilsE);
+                VarD (uT_r_aw, UnitE); (* data *)
+                VarD (requestT, requestE);
+                FunD ([moded_requestT], get_version_idF);
+                FunD ([moded_requestT], updated_versionF);
+                FunD ([moded_requestT], sendF);
+                FunD ([moded_requestT], send_allF)
+              ],
+              (* SkipS *)
+              CallS (VarP send_allID, [PathE (VarP requestID)])
+              ) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+(* TODO: + synth. test *)