From 0ef7ebdad231c565bf44408ba0b819a5f4ac465b Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 15 May 2026 10:06:42 +0000 Subject: [PATCH 1/2] struct: fixes, ref memcopy test (need to copy due to new memory model), test from presentation --- model_with_structures/analyzer.ml | 71 ++++++++++- model_with_structures/model.typ | 28 ++--- model_with_structures/synthesizer.ml | 27 ++-- model_with_structures/tests.ml | 18 ++- model_with_structures/tests_f.ml | 177 +++++++++++++++++++++++++-- 5 files changed, 277 insertions(+), 44 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index f7c3759..799e75d 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -200,8 +200,8 @@ struct | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) | FunT _, FunV _ -> (mem, v) - | RefT (Rf, _), RefV _ -> (mem, v) - | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in + (* | RefT (Rf, _), RefV _ -> (mem, v) *) + | 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 @@ -570,6 +570,7 @@ struct let vg8 = VarP (globals_min_id + 8) let vg9 = VarP (globals_min_id + 9) let vg10 = VarP (globals_min_id + 10) + let vg11 = VarP (globals_min_id + 11) let rf0E = RefE 0 let rf1E = RefE 1 @@ -987,6 +988,72 @@ struct Printf.printf "done!"; [%expect {| done! |}] + (* - tests for presentation *) + + let%expect_test "presentation test 1 (simple types), dsl" = + prog_eval_noret ( + [ + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg0E; (* x *) + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg2E; (* y *) + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg4E; (* z *) + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg6E; (* k *) + FunD ( (* f *) + [ + (moded @@ rfT @@ uT_r_aw); + (moded @@ rfT @@ uT_r); + ], + (rdS @@ drf @@ v0) #. + (wrS @@ drf @@ v0) #. + (rdS @@ drf @@ v1) + ); + FunD ( (* w *) + [ + (moded @@ cpT @@ uT_mw); + ], + (wrS @@ drf @@ v0) |. skp + ); + FunD ( (* g *) + [ + (moded @@ rfT @@ uT_aw); + (moded @@ cpT @@ uT_r_mw); + ], + (wrS @@ drf @@ v0) #. + ((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #. + (rdS @@ drf @@ v0) #. + (rdS @@ drf @@ v1) + ); + FunD ( (* r *) + [ + (moded @@ rfT @@ uT_r); + ], + (rdS @@ drf @@ v0) + ) + ], + let xV = vg1 in + let yV = vg3 in + let zV = vg5 in + let kV = vg7 in + let fF = vg8 in + let wF = vg9 in + let gF = vg10 in + let rF = vg11 in + (callS wF [pE xV]) #. + (callS rF [pE xV]) #. + (callS fF [pE xV; pE yV]) #. + (callS rF [pE yV]) #. + (callS gF [pE zV; pE kV]) #. + (wrS @@ drf @@ zV) #. + (callS wF [pE zV]) #. + (callS fF [pE yV; pE zV]) #. + (callS rF [pE kV]) + ); + Printf.printf "done!"; + [%expect {| done! |}] + (* - complex tests *) (* TODO: FIXME: rw tags *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index b1c3d9e..42d7b14 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -13,7 +13,7 @@ == Syntax -*TODO: top-level value copy mode ??* // TODO: FIXME +// *TODO: top-level value copy mode ??* // TODO: FIXME *TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME @@ -581,28 +581,26 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ ) )) +// #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$, +// ) +// )) + +// 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 ref value], - - // TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??) - // <- forbidden ?? - - $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$, - ) -)) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ new reference copy value], + name: [ new reference /* copy */ value], $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$, $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, - $cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$, + $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$, ) )) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 323f9ee..85a3f4c 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -592,7 +592,7 @@ struct let open Type in let open Value in let open ReadCap in - let open CopyCap in + (* let open CopyCap in *) let open MemVal in let open ReadVal in let open WriteVal in @@ -613,13 +613,13 @@ struct { fresh c, tp', id in v == RefV id & tp == RefT (c, tp') & - { { c == Rf & mem_with_id' == Std.pair mem v } | - { fresh v', mem_cp, v_cp, mem_add, id_add in - c == Cp & - mem_geto mem id v' & - 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) } } } | + (* { c == Rf & mem_with_id' == Std.pair mem v } | *) + { fresh v', mem_cp, v_cp, mem_add, id_add in + (* c == Cp & *) + mem_geto mem id v' & + 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' in v == TupleV vs & tp == TupleT tps & @@ -727,8 +727,8 @@ struct ocanren { { u == ZeroMV & v == ZeroMV & u' == ZeroMV } | { u == BotMV & v == BotMV & u' == BotMV } | - { u =/= ZeroMV & v =/= ZeroMV & - u =/= BotMV & v =/= BotMV & + { { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } & + { u =/= BotMV | { u == BotMV & v =/= BotMV } } & u' == SmthMV } } @@ -749,8 +749,8 @@ struct ocanren { { u == OneWV & v == OneWV & u' == OneWV } | { u == ZeroWV & v == ZeroWV & u' == ZeroWV } | - { u =/= ZeroWV & v =/= ZeroWV & - u =/= OneWV & v =/= OneWV & + { { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } & + { u =/= OneWV | { u == OneWV & v =/= OneWV } } & u' == SmthWV } } @@ -775,7 +775,8 @@ struct { fresh a, b in u == RefV a & v == RefV b & - a == b } | + a == b & + u' == RefV a } | { fresh us, vs, us' in u == TupleV us & v == TupleV vs & diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index ecf4ff9..96e86ed 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -61,10 +61,10 @@ let%expect_test "simple call with read & write (2 args)" = print_endline(prog_ev [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (O))); UnitV (BotMV, TopRV, OneWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O)))))))))))))), S (S (S (S (O))))); (S (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 (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 (O))))); (S (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 (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 (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}] let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), 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 (O)))))))); (S (S (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 (S (S (O))))))))))))))), 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 (O))))); (S (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 (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 (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 (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 (S (S (S (O)))))))))))))))), 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 (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (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 (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 (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), 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 (O)))))))); (S (S (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 (S (S (O))))))))))))))), 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 (O))))); (S (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 (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 (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 (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 (S (S (S (O)))))))))))))))), 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 (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (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 (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 (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]))] |}] let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), 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 (O)))))))); (S (S (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 (S (S (O))))))))))))))), 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 (O))))); (S (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 (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 (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 (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 (S (S (S (O)))))))))))))))), 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 (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (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 (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 (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (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 (O)))))))))))))))))), 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 (O)))))))); (S (S (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 (S (S (O))))))))))))))), 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 (O))))); (S (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 (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 (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 (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 (S (S (S (O)))))))))))))))), 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 (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (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 (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 (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]))] |}] (* - basic synthesis tests *) @@ -72,7 +72,7 @@ let%expect_test "simple synthesis test" = print_endline(prog_cp_cap_synt_t_simpl [%expect {| [Cp; Rf] |}] let%expect_test "simple synthesis test, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr' ()); - [%expect {| [Rf; Cp] |}] + [%expect {| [Cp; Rf] |}] let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ()); [%expect {| [Cp] |}] @@ -80,6 +80,18 @@ let%expect_test "simple synthesis test, reference forbidden write" = print_endli let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ()); [%expect {| [Cp] |}] +(* - presentation tests *) + +let%expect_test "presentation test 1 (simple types), eval" = print_endline(prog_eval_t_presentation_simple_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 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)]))] |}] *) + + (* - complex test: send example *) (* TODO: correct tags (at least rw) *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 63900a5..301a934 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -28,17 +28,23 @@ open StEnv (* - shortcuts *) (* NOTE: redo with fold ?? *) -let rec seqo stmts stmt' = ocanren { - { stmts == [] & stmt' == SkipS } | - { fresh s in - stmts == [s] & - stmt' == s } | - { fresh s, s', ss, stmt_rest' in - stmts == s :: s' :: ss & - seqo (s' :: ss) stmt_rest' & - stmt' == SeqS(s, stmt_rest') - } +let seq_foldero stmt_acc stmt stmt_acc' = ocanren { + stmt_acc' == SeqS(stmt, stmt_acc) } +let seqo stmts stmt' = ocanren { + list_foldro seq_foldero SkipS stmts stmt' + } +(* ocanren { *) + (* { stmts == [] & stmt' == SkipS } | *) + (* { fresh s in *) + (* stmts == [s] & *) + (* stmt' == s } | *) + (* { fresh s, s', ss, stmt_rest' in *) + (* stmts == s :: s' :: ss & *) + (* seqo (s' :: ss) stmt_rest' & *) + (* stmt' == SeqS(s, stmt_rest') *) + (* } *) + (* } *) (* - basic var tests *) @@ -517,6 +523,155 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak prog_evalo prog st }) (fun q -> q#reify (CopyCap.prj_exn)))) +(* - presentation tests *) + +let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xbg, xg, + ybg, yg, + zbg, zg, + kbg, kg, + fg, wg, gg, rg, + xbd, xd, + ybd, yd, + zbd, zd, + kbd, kd, + fd, wd, gd, rd, + fstmts, gstmts, + stmts in + globals_min_ido xbg & + xg == Nat.s xbg & + ybg == Nat.s xg & + yg == Nat.s ybg & + zbg == Nat.s yg & + zg == Nat.s zbg & + kbg == Nat.s zg & + kg == Nat.s kbg & + fg == Nat.s kg & + wg == Nat.s fg & + gg == Nat.s wg & + rg == Nat.s gg & + xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) & + ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) & + zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) & + kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) & + seqo [ReadS (DerefP (VarP 0)); + WriteS (DerefP (VarP 0)); + ReadS (DerefP (VarP 1))] fstmts & + fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); + (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], + fstmts) & + wd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))], + ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) & + seqo [WriteS (DerefP (VarP 0)); + ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0))); + ReadS (DerefP (VarP 0)); + ReadS (DerefP (VarP 1))] gstmts & + gd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); + (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], + gstmts) & + rd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], + ReadS (DerefP (VarP 0))) & + seqo [ + CallS (VarP wg, [PathE (VarP xg)]); + CallS (VarP rg, [PathE (VarP xg)]); + CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]); + CallS (VarP rg, [PathE (VarP yg)]); + CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]); + CallS (VarP wg, [PathE (VarP zg)]); + WriteS (DerefP (VarP zg)); + CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); + CallS (VarP rg, [PathE (VarP kg)]) + ] stmts & + prog == Prg ([xbd; xd; + ybd; yd; + zbd; zd; + kbd; kd; + fd; wd; gd; rd], + stmts) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xbg, xg, + ybg, yg, + zbg, zg, + kbg, kg, + fg, wg, gg, rg, + xbd, xd, + ybd, yd, + zbd, zd, + kbd, kd, + fd, wd, gd, rd, + fstmts, gstmts, + stmts, + c_fx, c_fy, c_wx, c_gx, c_gy, c_rx, + st in + globals_min_ido xbg & + xg == Nat.s xbg & + ybg == Nat.s xg & + yg == Nat.s ybg & + zbg == Nat.s yg & + zg == Nat.s zbg & + kbg == Nat.s zg & + kg == Nat.s kbg & + fg == Nat.s kg & + wg == Nat.s fg & + gg == Nat.s wg & + rg == Nat.s gg & + xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) & + ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) & + zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) & + kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) & + seqo [ReadS (DerefP (VarP 0)); + WriteS (DerefP (VarP 0)); + ReadS (DerefP (VarP 1))] fstmts & + fd == FunD ([(Mode (In, NOut), RefT (c_fx, UnitT (Rd, AlwaysWr))); + (Mode (In, NOut), RefT (c_fy, UnitT (Rd, NeverWr)))], + fstmts) & + wd == FunD ([(Mode (In, NOut), RefT (c_wx, UnitT (NRd, MayWr)))], + ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) & + seqo [WriteS (DerefP (VarP 0)); + ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0))); + ReadS (DerefP (VarP 0)); + ReadS (DerefP (VarP 1))] gstmts & + gd == FunD ([(Mode (In, NOut), RefT (c_gx, UnitT (NRd, AlwaysWr))); + (Mode (In, NOut), RefT (c_gy, UnitT (Rd, MayWr)))], + gstmts) & + rd == FunD ([(Mode (In, NOut), RefT (c_rx, UnitT (Rd, NeverWr)))], + ReadS (DerefP (VarP 0))) & + seqo [ + CallS (VarP wg, [PathE (VarP xg)]); + CallS (VarP rg, [PathE (VarP xg)]); + CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]); + CallS (VarP rg, [PathE (VarP yg)]); + CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]); + CallS (VarP wg, [PathE (VarP zg)]); + WriteS (DerefP (VarP zg)); + CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); + CallS (VarP rg, [PathE (VarP kg)]) + ] stmts & + prog == Prg ([xbd; xd; + ybd; yd; + zbd; zd; + kbd; kd; + fd; wd; gd; rd], + stmts) & + prog_evalo prog st & + q == [c_fx; c_fy; c_wx; c_gx; c_gy; c_rx] + }) + (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) + (* - complex tests *) let deref_accesso id v p' = ocanren { @@ -965,4 +1120,4 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q CallS (VarP send_allID, [PathE (VarP requestID)]) ) & prog_evalo prog st }) - (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *) + (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) From 8fc0ffa805bc383c47b9c0bad35171ee24835421 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 15 May 2026 11:41:59 +0000 Subject: [PATCH 2/2] 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) }