From 8fc0ffa805bc383c47b9c0bad35171ee24835421 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 15 May 2026 11:41:59 +0000 Subject: [PATCH] struct: fixes, test 2 from presentation (mostly, choice removed for now) --- model_with_structures/analyzer.ml | 45 +++++ model_with_structures/synthesizer.ml | 6 +- model_with_structures/tests.ml | 6 +- model_with_structures/tests_f.ml | 262 ++++++++++++++++++++++++++- 4 files changed, 313 insertions(+), 6 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 799e75d..9b0c27a 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -1054,6 +1054,51 @@ struct Printf.printf "done!"; [%expect {| done! |}] + (* TODO tags, access *) + (* let%expect_test "presentation test 2 (complex types), dsl" = *) + (* prog_eval_noret ( *) + (* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *) + (* let dataT = TupleT [uT_r_aw; uT_r_aw] in *) + (* let requestT = TupleT [cpT userT; *) + (* cpT dataT; *) + (* cpT dataT] in *) + (* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *) + (* cpT dataT; *) + (* cpT dataT] in *) + (* let userE = TupleE [UnitE; UnitE; UnitE] in *) + (* let dataE = TupleE [UnitE; UnitE] in *) + (* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *) + (* [ *) + (* defg userT userE; *) + (* defg dataT dataE; *) + (* defgu uT_r_aw; (* time *) *) + (* defg requestT requestE; *) + (* FunD ( (* send *) *) + (* [ *) + (* (moded @@ requestArgsT) *) + (* ], *) + (* ( *) + (* ( (* TODO access *) *) + (* (rdS @@ drf @@ v0) #. *) + (* (wrS @@ drf @@ v0) #. *) + (* (rdS @@ drf @@ v0) #. *) + (* (wrS @@ drf @@ v0) *) + (* ) |. *) + (* skp) #. *) + (* TODO access *) + (* (wrS @@ drf @@ v0) #. *) + (* (rdS @@ drf @@ v1) *) + (* ); *) + (* ], *) + (* (callS vg4 [pE vg3]) #. *) + (* TODO access *) + (* (wrS @@ drf @@ vg3) #. *) + (* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *) + (* (rdS @@ drf @@ vg3) *) + (* ); *) + (* Printf.printf "done!"; *) + (* [%expect {| done! |}] *) + (* - complex tests *) (* TODO: FIXME: rw tags *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 85a3f4c..f4216ff 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -569,11 +569,11 @@ struct pathvalo mem vals p' v' & v' == RefV id & mem_geto mem id v } | - { fresh p', id, v', vs in - p == AccessP (p', id) & + { fresh p', id', v', vs in + p == AccessP (p', id') & pathvalo mem vals p' v' & v' == TupleV vs & - list_ntho vs id v } + list_ntho vs id' v } } (* --- eval rules --- *) diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 96e86ed..3c73dcb 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -88,9 +88,11 @@ let%expect_test "presentation test 1 (simple types), eval" = print_endline(prog_ let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_synt_t_presentation_simple_tp ()); [%expect {| [[Cp; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Rf]; [Cp; Cp; Cp; Rf; Cp; Cp]; [Cp; Cp; Cp; Rf; Cp; Rf]; [Cp; Rf; Cp; Cp; Cp; Cp]; [Cp; Rf; Cp; Cp; Cp; Rf]; [Cp; Rf; Cp; Rf; Cp; Cp]; [Cp; Rf; Cp; Rf; Cp; Rf]; [Rf; Cp; Cp; Cp; Cp; Cp]; [Rf; Rf; Cp; Cp; Cp; Cp]; [Rf; Cp; Cp; Cp; Cp; Rf]; [Rf; Rf; Cp; Cp; Cp; Rf]; [Rf; Cp; Cp; Rf; Cp; Cp]; [Rf; Rf; Cp; Rf; Cp; Cp]; [Rf; Cp; Cp; Rf; Cp; Rf]; [Rf; Rf; Cp; Rf; Cp; Rf]] |}] -(* let%expect_test "presentation test 2 (complex types), eval" = print_endline(prog_eval_t_presentation_complex_tp ()); *) - (* [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); FunV ([SeqS (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))))]); FunV ([ChoiceS (WriteS (DerefP (VarP (O))), SkipS)]); FunV ([SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))]); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))); SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))); ReadS (DerefP (VarP (O))); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); SeqS (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))); SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))); ReadS (DerefP (VarP (O))); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); ChoiceS (WriteS (DerefP (VarP (O))), SkipS)]))] |}] *) +let%expect_test "presentation test 2 (complex types), eval" = print_endline(prog_eval_t_presentation_complex_tp ()); + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]); TupleV ([RefV (S (S (S (S (S (O)))))); RefV (S (S (S (S (O))))); RefV (S (S (S (O))))]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)])], S (S (S (S (S (S (S (S (O))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]))] |}] +let%expect_test "presentation test 2 (complex types), esynt" = print_endline(prog_synt_t_presentation_complex_tp ()); + [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] (* - complex test: send example *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 301a934..4690159 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -46,6 +46,14 @@ let seqo stmts stmt' = ocanren { (* } *) (* } *) +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) + } + (* - basic var tests *) let prog_eval_t_empty _ = show(answer) (Stream.take (run q @@ -525,6 +533,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak (* - presentation tests *) +(* simple types *) + let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xbg, xg, @@ -672,7 +682,7 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r }) (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) -(* - complex tests *) +(* complex type *) let deref_accesso id v p' = ocanren { p' == DerefP (AccessP (VarP v, id)) @@ -682,6 +692,256 @@ let access_deref_accesso id_ext id_int v p' = ocanren { p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) } +(* --- *) + +let p_rw_unitTo tp = ocanren { + (* fresh r, w in *) + tp == UnitT (Rd, AlwaysWr) + } + +let p_rw_userTo tp = ocanren { + fresh x, y, z in + p_rw_unitTo x & + p_rw_unitTo y & + p_rw_unitTo z & + tp == TupleT [x; y; z] + } + +let p_rw_dataTo tp = ocanren { + fresh x, y in + p_rw_unitTo x & + p_rw_unitTo y & + tp == TupleT [x; y] + } + +let p_rw_timeTo tp = ocanren { + p_rw_unitTo tp + } + +let p_rw_requestTo cu cd ct tp = ocanren { + fresh userT, dataT, timeT in + p_rw_userTo userT & + p_rw_dataTo dataT & + p_rw_timeTo timeT & + tp == TupleT [RefT (cu, userT); + RefT (cd, dataT); + RefT (ct, timeT)] + } + +(* --- *) + +let p_any_unitTo tp = ocanren { + fresh r, w in + tp == UnitT (r, w) + } + +let p_any_userTo tp = ocanren { + fresh x, y, z in + p_any_unitTo x & + p_any_unitTo y & + p_any_unitTo z & + tp == TupleT [x; y; z] + } + +let p_any_dataTo tp = ocanren { + fresh x, y in + p_any_unitTo x & + p_any_unitTo y & + tp == TupleT [x; y] + } + +let p_any_timeTo tp = ocanren { + p_any_unitTo tp + } + +let p_any_requestTo cu cd ct tp = ocanren { + fresh userT, dataT, timeT in + p_any_userTo userT & + p_any_dataTo dataT & + p_any_timeTo timeT & + tp == TupleT [RefT (cu, userT); + RefT (cd, dataT); + RefT (ct, timeT)] + } + +(* --- *) + +let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, + userT, dataT, timeT, requestT, + requestArgsT, + userE, dataE, timeE, requestE, + userVID, dataVID, timeVID, requestVID, + sendFID, sendD, sendBranchStmts, sendStmts, + stmts in + globals_min_ido userVID & + dataVID == Nat.s userVID & + timeVID == Nat.s dataVID & + requestVID == Nat.s timeVID & + sendFID == Nat.s requestVID & + + p_rw_userTo userT & + p_rw_dataTo dataT & + p_rw_timeTo timeT & + p_rw_requestTo Cp Cp Cp requestT & + p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *) + + userE == TupleE [UnitE; UnitE; UnitE] & + dataE == TupleE [UnitE; UnitE] & + timeE == UnitE & + requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & + + fresh data_p0, data_p1, time_p, + user_id_p, user_name_p, user_surname_p in + access_deref_accesso 0 1 0 data_p0 & + access_deref_accesso 1 1 0 data_p1 & + deref_accesso 2 0 time_p & + access_deref_accesso 0 0 0 user_id_p & + access_deref_accesso 1 0 0 user_name_p & + access_deref_accesso 2 0 0 user_surname_p & + seqo [ReadS data_p0; + ReadS data_p1; + WriteS data_p0; + WriteS data_p1; + + ReadS user_name_p; + WriteS user_name_p] sendBranchStmts & + seqo [sendBranchStmts; (* TMP *) + (* TODO: FIXME *) + (* ChoiceS (sendBranchStmts, SkipS); *) + WriteS time_p; + + ReadS data_p0; + ReadS data_p1; + ReadS time_p; + ReadS user_id_p; + ReadS user_name_p; + ReadS user_surname_p] sendStmts & + (* sendStmts == SkipS & *) + sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & + + fresh time_gp, user_name_gp, user_surname_gp in + deref_accesso 2 requestVID time_gp & + access_deref_accesso 1 0 requestVID user_name_gp & + access_deref_accesso 2 0 requestVID user_surname_gp & + seqo [ + CallS (VarP sendFID, [PathE (VarP requestVID)]); + WriteS time_gp; + (* TODO: FIXME *) + (* ChoiceS (ReadS user_name_gp, *) + (* ReadS user_surname_gp); *) + ReadS user_name_gp; (* TMP *) + ReadS user_surname_gp; (* TMP *) + ReadS time_gp + ] stmts & + prog == Prg ([ + VarD (userT, userE); + VarD (dataT, dataE); + VarD (timeT, timeE); + VarD (requestT, requestE); + sendD + ], + stmts + ) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (run q + (fun q -> ocanren { + fresh prog, + userT, dataT, timeT, requestT, + requestArgsT, + userE, dataE, timeE, requestE, + userVID, dataVID, timeVID, requestVID, + sendFID, sendD, sendBranchStmts, sendStmts, + stmts, + st, c_u, c_d, c_t in + globals_min_ido userVID & + dataVID == Nat.s userVID & + timeVID == Nat.s dataVID & + requestVID == Nat.s timeVID & + sendFID == Nat.s requestVID & + + p_rw_userTo userT & + p_rw_dataTo dataT & + p_rw_timeTo timeT & + p_rw_requestTo Cp Cp Cp requestT & + p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *) + + userE == TupleE [UnitE; UnitE; UnitE] & + dataE == TupleE [UnitE; UnitE] & + timeE == UnitE & + requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & + + fresh data_p0, data_p1, time_p, + user_id_p, user_name_p, user_surname_p in + access_deref_accesso 0 1 0 data_p0 & + access_deref_accesso 1 1 0 data_p1 & + deref_accesso 2 0 time_p & + access_deref_accesso 0 0 0 user_id_p & + access_deref_accesso 1 0 0 user_name_p & + access_deref_accesso 2 0 0 user_surname_p & + seqo [ReadS data_p0; + ReadS data_p1; + WriteS data_p0; + WriteS data_p1; + + ReadS user_name_p; + WriteS user_name_p] sendBranchStmts & + seqo [sendBranchStmts; (* TMP *) + (* TODO: FIXME *) + (* ChoiceS (sendBranchStmts, SkipS); *) + WriteS time_p; + + ReadS data_p0; + ReadS data_p1; + ReadS time_p; + ReadS user_id_p; + ReadS user_name_p; + ReadS user_surname_p] sendStmts & + (* sendStmts == SkipS & *) + sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & + + fresh time_gp, user_name_gp, user_surname_gp in + deref_accesso 2 requestVID time_gp & + access_deref_accesso 1 0 requestVID user_name_gp & + access_deref_accesso 2 0 requestVID user_surname_gp & + seqo [ + CallS (VarP sendFID, [PathE (VarP requestVID)]); + WriteS time_gp; + (* TODO: FIXME *) + (* ChoiceS (ReadS user_name_gp, *) + (* ReadS user_surname_gp); *) + ReadS user_name_gp; (* TMP *) + ReadS user_surname_gp; (* TMP *) + ReadS time_gp + ] stmts & + prog == Prg ([ + VarD (userT, userE); + VarD (dataT, dataE); + VarD (timeT, timeE); + VarD (requestT, requestE); + sendD + ], + stmts + ) & + prog_evalo prog st & + q == [c_u; c_d; c_t] + }) + (fun q -> q#reify (List.prj_exn 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) }