diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 99de175..57b4207 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -529,12 +529,11 @@ struct let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = ocanren { - fresh mem, vs, mem', v', mem_with_v', vs' in + fresh mem, vs, mem', v', vs' in Std.pair mem vs == mem_with_vs & - valcopyo mem v tp mem_with_v' & - Std.pair mem' v' == mem_with_v' & + valcopyo mem v tp (Std.pair mem' v') & vs' == v' :: vs & - mem_with_vs' == Std.pair mem vs' + mem_with_vs' == Std.pair mem' vs' } and valcopyo mem v tp mem_with_id' = let open Type in @@ -561,12 +560,11 @@ struct valcopyo mem v' tp' (Std.pair mem_cp v_cp) & mem_addo mem_cp v_cp (Std.pair mem_add id_add) & mem_with_id' == (mem_add, RefV id_add) } } } | - { fresh vs, tps, mem', vs', vs'' in + { fresh vs, tps, mem', vs' in v == TupleV vs & tp == TupleT tps & - list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & - List.reverso vs' vs'' & - mem_with_id' == Std.pair mem' (TupleV vs'') } + list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & + mem_with_id' == Std.pair mem' (TupleV vs') } } (* - value update *) @@ -634,7 +632,14 @@ struct (* - expression evaluation *) - let rec exprvalo mem vals e v' = + (* let rec exprval_foldero mem vals vs e vs' = ocanren { *) + (* fresh v' in *) + (* exprvalo mem vals e v' & *) + (* vs' == v' :: vs *) + (* } *) + (* and *) + let rec + exprvalo mem vals e v' = let open Expr in let open Value in ocanren { @@ -648,6 +653,7 @@ struct v' == RefV v } | { fresh es, vs' in e == TupleE es & + (* list_foldro (exprval_foldero mem vals) [] es vs' & *) List.mapo (exprvalo mem vals) es vs' & v' == TupleV vs' } } @@ -692,9 +698,14 @@ struct types', vals' in d == VarD (tp, e) & exprvalo mem vals e v & + (* v == TupleV [ZeroV; ZeroV] & (* FIXME TMP *) *) valcopyo mem v tp (Pair.pair mem_cp v_cp) & + (* mem_cp == mem & v_cp == v & *) mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & + (* mem_add == mem_cp & *) types_glob_addo types x tp types' & + (* types == types' & *) + (* vals == vals' & *) vals_glob_addo vals x id_add vals' & st' == StEnv (mem_add, types', vals', visited) } | { fresh tps, s, @@ -813,15 +824,14 @@ struct valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) & mem_seto mem_sp id' v_sp mem_set & mem_with_v' == Std.pair mem_set (RefV id') } | - { fresh tps, us, vs, mem_sp, vs_sp, vs_sp' in + { fresh tps, us, vs, mem_sp, vs_sp in tp == TupleT tps & u == TupleT us & v == TupleV vs & - list_foldl3o (valspoil_foldero m c) + list_foldr3o (valspoil_foldero m c) (Std.pair mem []) tps us vs (Std.pair mem_sp vs_sp) & - List.reverso vs_sp vs_sp' & - mem_with_v' == Std.pair mem_sp (TupleV vs_sp') + mem_with_v' == Std.pair mem_sp (TupleV vs_sp) } } @@ -1023,11 +1033,4 @@ struct prog_inito prog init_st & stmt_evalo init_st s st' } - - (* --- tests --- *) - (* TODO *) - - (* - shortcuts *) - (* TODO *) - end diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 85ff5ad..db667a7 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -79,3 +79,12 @@ 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; Cp; Cp; Cp] |}] + +(* - complex test: send example *) + +let%expect_test "complex test: send" = print_endline(prog_eval_compl_test_send ()); + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]); FunV ([SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O))))))))]); FunV ([SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O)))))]); FunV ([ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS)]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); RefV (S (S (S (S (S (S (S (S (S (O)))))))))); RefV (S (S (S (S (S (S (S (S (O))))))))); ZeroV]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV]); ZeroV; ZeroV; TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([RefV (S (S (S (O)))); RefV (S (S (O)))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV])], S (S (S (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 (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(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), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (O))))))))))))))), 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 (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 (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]))] |}] + +let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); + [%expect {| [Cp] |}] +(* TODO *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 1452cf4..adfad04 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -17,8 +17,12 @@ open InCap open OutCap open Mode -@type answer = StEnv.ground GT.list with show -@type answerCpCap = CopyCap.ground GT.list with show +@type answer = + StEnv.ground GT.list with show +@type answerCpCap = + CopyCap.ground GT.list with show +@type answerCpCapList = + (CopyCap.ground GT.list) GT.list with show (* - shortcuts *) @@ -501,3 +505,379 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak ReadS (DerefP (VarP yg)))) & prog_evalo prog st }) (fun q -> q#reify (CopyCap.prj_exn)))) + +(* - complex tests *) + +let deref_accesso id v p' = ocanren { + p' == DerefP (AccessP (VarP v, id)) + } + +let access_deref_accesso id_ext id_int v p' = ocanren { + p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) + } + +let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren { + p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext) + } + +let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh (* types *) + uT_r_aw, + user_utilsT, user_infoT, + userT, versionT, utilsT, + requestT, + moded_requestT, + (* global vars init exprs *) + user_utilsE, user_infoE, + userE, versionE, utilsE, + requestE, + (* global vars ids *) + user_utilsID, user_infoID, + userID, versionID, utilsID, + dataID, requestID, + (* function ids *) + get_version_idID, + updated_versionID, + sendID, + send_allID, + (* function definitions *) + get_version_idF, + updated_versionF, + sendFBranch, + sendF, + send_allF, + (* other *) + prog in + (* types *) + uT_r_aw == UnitT (Rd, AlwaysWr) & + user_utilsT == TupleT [uT_r_aw (* 0 id *); uT_r_aw] & + user_infoT == TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] & + userT == TupleT [RefT (Cp, user_utilsT) (* 0 utils *); + RefT (Cp, user_infoT) (* 1 info *)] & + versionT == TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] & + utilsT == TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] & + requestT == TupleT [RefT (Cp, userT) (* 0 user *); + RefT (Cp, versionT) (* 1 version *); + RefT (Cp, utilsT) (* 2 utils *); + RefT (Cp, uT_r_aw) (* 3 data *); + uT_r_aw (* 4 operation_date *)] & + moded_requestT == (Mode (In, NOut), requestT) & + (* global vars init exprs *) + user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & + user_infoE == TupleE [UnitE (* 0 name *); UnitE; UnitE] & + userE == TupleE [RefE user_utilsID (* 0 utils *); + RefE user_infoID (* 1 info *)] & + versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] & + utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] & + requestE == TupleE [RefE userID (* 0 user *); + RefE versionID (* 1 version *); + RefE utilsID (* 2 utils *); + RefE dataID (* 3 data *); + UnitE (* 4 operation_date *)] & + (* global vars ids *) + globals_min_ido user_utilsID & + user_infoID == Nat.s user_utilsID & + userID == Nat.s user_infoID & + versionID == Nat.s userID & + utilsID == Nat.s versionID & + dataID == Nat.s utilsID & + requestID == Nat.s dataID & + (* function ids *) + get_version_idID == Nat.s requestID & + updated_versionID == Nat.s get_version_idID & + sendID == Nat.s updated_versionID & + send_allID == Nat.s sendID & + (* function definitions *) + fresh gvi_access0 in + access_deref_accesso 0 1 0 gvi_access0 & + get_version_idF == ChoiceS (ReadS gvi_access0, SkipS) & + + fresh uv_access0, uv_access1, uv_access2 in + access_deref_accesso 0 2 0 uv_access0 & + access_deref_accesso 0 1 0 uv_access1 & + access_deref_accesso 1 1 0 uv_access2 & + seqo [ReadS uv_access0; + ReadS uv_access1; + ReadS uv_access2] + updated_versionF & + + fresh sb_access0, sb_access1, sb_access2, sb_access3 in + access_deref_accesso 0 2 0 sb_access0 & + deref_accesso 3 0 sb_access1 & + deref_accesso 3 0 sb_access2 & + access_deref_access_deref_accesso 0 1 0 0 sb_access3 & + seqo [WriteS sb_access0; + ReadS sb_access1; + WriteS sb_access2; + ReadS sb_access3] + sendFBranch & + seqo [ChoiceS (sendFBranch, SkipS); + WriteS (AccessP (VarP 0, 4)); + (* TODO: read all the substructure ?? *) + ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *) + sendF & + + fresh sa_access0, sa_access1, sa_access2, sa_access3 in + access_deref_accesso 0 1 0 sa_access0 & + access_deref_accesso 1 1 0 sa_access1 & + access_deref_access_deref_accesso 0 0 0 0 sa_access2 & + access_deref_accesso 0 1 0 sa_access3 & + seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *) + CallS (VarP sendID, [PathE (VarP 0)]); + CallS (VarP get_version_idID, [PathE (VarP 0)]); + CallS (VarP updated_versionID, [PathE (VarP 0)]); + (* TODO: read all the substructure ?? *) + WriteS sa_access0; + WriteS sa_access1; + ChoiceS ( + ReadS sa_access2, + ReadS sa_access3 + )] + send_allF & + + prog == Prg ([ + VarD (user_utilsT, user_utilsE); + VarD (user_infoT, user_infoE); + VarD (userT, userE); + VarD (versionT, versionE); + VarD (utilsT, utilsE); + VarD (uT_r_aw, UnitE); (* data *) + VarD (requestT, requestE); + FunD ([moded_requestT], get_version_idF); + FunD ([moded_requestT], updated_versionF); + FunD ([moded_requestT], sendF); + FunD ([moded_requestT], send_allF) + ], + (* SkipS *) + CallS (VarP send_allID, [PathE (VarP requestID)]) + ) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let rw_unitTo tp = ocanren { + (* fresh r, w in *) + tp == UnitT (Rd, AlwaysWr) + } + +let any_unitTo tp = ocanren { + fresh r, w in + tp == UnitT (r, w) + } + +let any_user_utilsTo tp = ocanren { + fresh x, y in + rw_unitTo x & + rw_unitTo y & + tp == TupleT [x; y] + } + +let any_user_infoTo tp = ocanren { + fresh x, y, z in + rw_unitTo x & + rw_unitTo y & + rw_unitTo z & + tp == TupleT [x; y; z] + } + +let any_versionTo tp = ocanren { + fresh x, y, z in + rw_unitTo x & + rw_unitTo y & + rw_unitTo z & + tp == TupleT [x; y; z] + } + +let any_utilsTo tp = ocanren { + fresh x, y in + rw_unitTo x & + rw_unitTo y & + tp == TupleT [x; y] + } + +let any_dataTo tp = ocanren { + rw_unitTo tp + } + +let any_op_dateTo tp = ocanren { + rw_unitTo tp + } + +let any_userTo cu ci tp = ocanren { + fresh utilsT, infoT in + any_user_infoTo infoT & + any_user_utilsTo utilsT & + tp == TupleT [RefT (cu, utilsT) (* 0 utils *); + RefT (ci, infoT) (* 1 info *)] + } + +let any_requestTo cus cv cut cd cus_u cus_i tp = ocanren { + fresh userT, versionT, utilsT, dataT, op_dateT in + any_userTo cus_u cus_i userT & + any_versionTo versionT & + any_utilsTo utilsT & + any_dataTo dataT & + any_op_dateTo op_dateT & + tp == TupleT [RefT (cus, userT) (* 0 user *); + RefT (cv, versionT) (* 1 version *); + RefT (cut, utilsT) (* 2 utils *); + RefT (cd, dataT) (* 3 data *); + op_dateT (* 4 operation_date *)] + } +let any_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren { + fresh requestT in + any_requestTo cus cv cut cd cus_u cus_i requestT & + tp == (Mode (In, NOut), requestT) + } +let any_boxed_moded_requestTo tp = ocanren { + fresh cus, cv, cut, cd, cus_u, cus_i in + any_moded_requestTo cus cv cut cd cus_u cus_i tp + } + +(* TODO: synt all modifiers, etc *) +let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q + (fun q -> ocanren { + fresh (* types *) + uT_r_aw, + user_utilsT, user_infoT, + userT, versionT, utilsT, + requestT, + (* moded_requestT, *) + (* global vars init exprs *) + user_utilsE, user_infoE, + userE, versionE, utilsE, + requestE, + (* global vars ids *) + user_utilsID, user_infoID, + userID, versionID, utilsID, + dataID, requestID, + (* function ids *) + get_version_idID, + updated_versionID, + sendID, + send_allID, + (* function definitions *) + get_version_idF, + updated_versionF, + sendFBranch, + sendF, + send_allF, + (* other *) + prog, + (* synt *) + st in + (* types *) + any_unitTo uT_r_aw & + any_user_utilsTo user_utilsT & + any_user_infoTo user_infoT & + any_userTo Cp Cp userT & + any_versionTo versionT & + any_utilsTo utilsT & + any_requestTo Cp Cp Cp Cp Cp Cp requestT & + (* moded_requestTo moded_requestT & *) + (* global vars init exprs *) + user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & + user_infoE == TupleE [UnitE (* 0 name *); UnitE; UnitE] & + userE == TupleE [RefE user_utilsID (* 0 utils *); + RefE user_infoID (* 1 info *)] & + versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] & + utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] & + requestE == TupleE [RefE userID (* 0 user *); + RefE versionID (* 1 version *); + RefE utilsID (* 2 utils *); + RefE dataID (* 3 data *); + UnitE (* 4 operation_date *)] & + (* global vars ids *) + globals_min_ido user_utilsID & + user_infoID == Nat.s user_utilsID & + userID == Nat.s user_infoID & + versionID == Nat.s userID & + utilsID == Nat.s versionID & + dataID == Nat.s utilsID & + requestID == Nat.s dataID & + (* function ids *) + get_version_idID == Nat.s requestID & + updated_versionID == Nat.s get_version_idID & + sendID == Nat.s updated_versionID & + send_allID == Nat.s sendID & + (* function definitions *) + fresh gvi_access0 in + access_deref_accesso 0 1 0 gvi_access0 & + get_version_idF == ChoiceS (ReadS gvi_access0, SkipS) & + + fresh uv_access0, uv_access1, uv_access2 in + access_deref_accesso 0 2 0 uv_access0 & + access_deref_accesso 0 1 0 uv_access1 & + access_deref_accesso 1 1 0 uv_access2 & + seqo [ReadS uv_access0; + ReadS uv_access1; + ReadS uv_access2] + updated_versionF & + + fresh sb_access0, sb_access1, sb_access2, sb_access3 in + access_deref_accesso 0 2 0 sb_access0 & + deref_accesso 3 0 sb_access1 & + deref_accesso 3 0 sb_access2 & + access_deref_access_deref_accesso 0 1 0 0 sb_access3 & + seqo [WriteS sb_access0; + ReadS sb_access1; + WriteS sb_access2; + ReadS sb_access3] + sendFBranch & + seqo [ChoiceS (sendFBranch, SkipS); + WriteS (AccessP (VarP 0, 4)); + (* TODO: read all the substructure ?? *) + ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *) + sendF & + + fresh sa_access0, sa_access1, sa_access2, sa_access3 in + access_deref_accesso 0 1 0 sa_access0 & + access_deref_accesso 1 1 0 sa_access1 & + access_deref_access_deref_accesso 0 0 0 0 sa_access2 & + access_deref_accesso 0 1 0 sa_access3 & + seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *) + CallS (VarP sendID, [PathE (VarP 0)]); + CallS (VarP get_version_idID, [PathE (VarP 0)]); + CallS (VarP updated_versionID, [PathE (VarP 0)]); + (* TODO: read all the substructure ?? *) + WriteS sa_access0; + WriteS sa_access1; + ChoiceS ( + ReadS sa_access2, + ReadS sa_access3 + )] + send_allF & + + fresh mrT_gvi, mrT_uv, mrT_s, mrT_sa in + fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in + any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' & + (* TODO *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & *) + + q == [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & + + prog == Prg ([ + VarD (user_utilsT, user_utilsE); + VarD (user_infoT, user_infoE); + VarD (userT, userE); + VarD (versionT, versionE); + VarD (utilsT, utilsE); + VarD (uT_r_aw, UnitE); (* data *) + VarD (requestT, requestE); + FunD ([mrT'], get_version_idF); + FunD ([mrT'], updated_versionF); + FunD ([mrT'], sendF); + FunD ([mrT'], send_allF) + (* FunD ([mrT_gvi], get_version_idF); *) + (* FunD ([mrT_uv], updated_versionF); *) + (* FunD ([mrT_s], sendF); *) + (* FunD ([mrT_sa], send_allF) *) + ], + (* SkipS *) + CallS (VarP send_allID, [PathE (VarP requestID)]) + ) & + prog_evalo prog st }) + (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)