diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 9b0c27a..f7c3759 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 (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in + | RefT (Rf, _), RefV _ -> (mem, v) + | RefT (Cp, 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,7 +570,6 @@ 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 @@ -988,117 +987,6 @@ 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! |}] - - (* 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/model.typ b/model_with_structures/model.typ index 42d7b14..b1c3d9e 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,26 +581,28 @@ $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 /* copy */ value], + 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], $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 c /*Copy*/ t)_new cl rf l', mu_a cr$, + $cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$, ) )) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index f4216ff..323f9ee 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 --- *) @@ -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 | { u == ZeroMV & v =/= ZeroMV } } & - { u =/= BotMV | { u == BotMV & v =/= BotMV } } & + { u =/= ZeroMV & v =/= ZeroMV & + 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 | { u == ZeroWV & v =/= ZeroWV } } & - { u =/= OneWV | { u == OneWV & v =/= OneWV } } & + { u =/= ZeroWV & v =/= ZeroWV & + u =/= OneWV & v =/= OneWV & u' == SmthWV } } @@ -775,8 +775,7 @@ struct { fresh a, b in u == RefV a & v == RefV b & - a == b & - u' == RefV a } | + a == b } | { 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 3c73dcb..ecf4ff9 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))))), 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)))))]))] |}] + [%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))))))))))]))] |}] 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))))), 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))))]))] |}] + [%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)))))))))]))] |}] (* - 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 {| [Cp; Rf] |}] + [%expect {| [Rf; Cp] |}] let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ()); [%expect {| [Cp] |}] @@ -80,20 +80,6 @@ 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 ([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 *) (* TODO: correct tags (at least rw) *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 4690159..63900a5 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -28,30 +28,16 @@ open StEnv (* - shortcuts *) (* NOTE: redo with fold ?? *) -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') *) - (* } *) - (* } *) - -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 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') + } } (* - basic var tests *) @@ -531,158 +517,7 @@ 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 *) - -(* simple types *) - -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 type *) +(* - complex tests *) let deref_accesso id v p' = ocanren { p' == DerefP (AccessP (VarP v, id)) @@ -692,256 +527,6 @@ 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) } @@ -1380,4 +965,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)))) + (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)