struct: complex example synt, too many wars to chek full synt

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' &
-      Std.pair mem' v' == mem_with_v' &
+      valcopyo mem v tp (Std.pair mem' 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.reverso vs' vs'' &
-        mem_with_id' == Std.pair mem' (TupleV vs'') }
+        list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' 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)
       }
   }
 
@@ -1023,11 +1033,4 @@ struct
       prog_inito prog init_st &
       stmt_evalo init_st s st'
   }
-
-  (* --- tests --- *)
-  (* TODO *)
-
-  (* - shortcuts *)
-  (* TODO *)
-
 end

model_with_structures/tests_f.ml

@@ -17,8 +17,12 @@ open InCap
 open OutCap
 open Mode
 
-@type answer = StEnv.ground GT.list with show
-@type answerCpCap = CopyCap.ground GT.list with show
+@type answer =
+  StEnv.ground GT.list with show
+@type answerCpCap =
+  CopyCap.ground GT.list with show
+@type answerCpCapList =
+  (CopyCap.ground GT.list) GT.list with show
 
 (* - shortcuts *)
 
@@ -501,3 +505,379 @@ 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)
+  }
+
+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))))
+
+let rw_unitTo tp = ocanren {
+    (* fresh r, w in *)
+    tp == UnitT (Rd, AlwaysWr)
+  }
+
+let any_unitTo tp = ocanren {
+    fresh r, w in
+    tp == UnitT (r, w)
+  }
+
+let any_user_utilsTo tp = ocanren {
+    fresh x, y in
+    rw_unitTo x &
+    rw_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let any_user_infoTo tp = ocanren {
+    fresh x, y, z in
+    rw_unitTo x &
+    rw_unitTo y &
+    rw_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let any_versionTo tp = ocanren {
+    fresh x, y, z in
+    rw_unitTo x &
+    rw_unitTo y &
+    rw_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let any_utilsTo tp = ocanren {
+    fresh x, y in
+    rw_unitTo x &
+    rw_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let any_dataTo tp = ocanren {
+    rw_unitTo tp
+  }
+
+let any_op_dateTo tp = ocanren {
+    rw_unitTo tp
+  }
+
+let any_userTo cu ci tp = ocanren {
+    fresh utilsT, infoT in
+    any_user_infoTo infoT &
+    any_user_utilsTo utilsT &
+    tp == TupleT [RefT (cu, utilsT) (* 0 utils *);
+                  RefT (ci, infoT) (* 1 info *)]
+  }
+
+let any_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
+    fresh userT, versionT, utilsT, dataT, op_dateT in
+    any_userTo cus_u cus_i userT &
+    any_versionTo versionT &
+    any_utilsTo utilsT &
+    any_dataTo dataT &
+    any_op_dateTo op_dateT &
+    tp == TupleT [RefT (cus, userT) (* 0 user *);
+                  RefT (cv, versionT) (* 1 version *);
+                  RefT (cut, utilsT) (* 2 utils *);
+                  RefT (cd, dataT) (* 3 data *);
+                  op_dateT (* 4 operation_date *)]
+  }
+let any_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
+    fresh requestT in
+    any_requestTo cus cv cut cd cus_u cus_i requestT &
+    tp == (Mode (In, NOut), requestT)
+  }
+let any_boxed_moded_requestTo tp = ocanren {
+    fresh cus, cv, cut, cd, cus_u, cus_i in
+    any_moded_requestTo cus cv cut cd cus_u cus_i tp
+  }
+
+(* TODO: synt all modifiers, etc *)
+let prog_synt_compl_test_send _ = show(answerCpCapList) (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,
+                    (* synt *)
+                    st in
+              (* types *)
+              any_unitTo uT_r_aw &
+              any_user_utilsTo user_utilsT &
+              any_user_infoTo user_infoT &
+              any_userTo Cp Cp userT &
+              any_versionTo versionT &
+              any_utilsTo utilsT &
+              any_requestTo Cp Cp Cp Cp Cp Cp requestT &
+              (* moded_requestTo moded_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 &
+
+              fresh mrT_gvi, mrT_uv, mrT_s, mrT_sa in
+              fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in
+              any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' &
+              (* TODO *)
+              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & *)
+              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & *)
+              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & *)
+              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & *)
+
+              q == [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] &
+
+              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 ([mrT'], get_version_idF);
+                FunD ([mrT'], updated_versionF);
+                FunD ([mrT'], sendF);
+                FunD ([mrT'], send_allF)
+                (* FunD ([mrT_gvi], get_version_idF); *)
+                (* FunD ([mrT_uv], updated_versionF); *)
+                (* FunD ([mrT_s], sendF); *)
+                (* FunD ([mrT_sa], send_allF) *)
+              ],
+              (* SkipS *)
+              CallS (VarP send_allID, [PathE (VarP requestID)])
+              ) &
+              prog_evalo prog st })
+  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)