diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 57b4207..99de175 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -529,11 +529,12 @@ struct let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = ocanren { - fresh mem, vs, mem', v', vs' in + fresh mem, vs, mem', v', mem_with_v', vs' in Std.pair mem vs == mem_with_vs & - valcopyo mem v tp (Std.pair mem' v') & + valcopyo mem v tp mem_with_v' & + Std.pair mem' v' == mem_with_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 @@ -560,11 +561,12 @@ 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' in + { fresh vs, tps, mem', vs', vs'' in v == TupleV vs & tp == TupleT tps & - list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & - mem_with_id' == Std.pair mem' (TupleV vs') } + 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'') } } (* - value update *) @@ -632,14 +634,7 @@ struct (* - expression evaluation *) - (* 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 rec exprvalo mem vals e v' = let open Expr in let open Value in ocanren { @@ -653,7 +648,6 @@ 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' } } @@ -698,14 +692,9 @@ 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, @@ -824,14 +813,15 @@ 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 in + { fresh tps, us, vs, mem_sp, vs_sp, vs_sp' in tp == TupleT tps & u == TupleT us & v == TupleV vs & - list_foldr3o (valspoil_foldero m c) + list_foldl3o (valspoil_foldero m c) (Std.pair mem []) tps us vs (Std.pair mem_sp vs_sp) & - mem_with_v' == Std.pair mem_sp (TupleV vs_sp) + List.reverso vs_sp vs_sp' & + mem_with_v' == Std.pair mem_sp (TupleV vs_sp') } } @@ -1033,4 +1023,11 @@ 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 db667a7..85ff5ad 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -79,12 +79,3 @@ 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 adfad04..1452cf4 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -17,12 +17,8 @@ open InCap open OutCap open Mode -@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 +@type answer = StEnv.ground GT.list with show +@type answerCpCap = CopyCap.ground GT.list with show (* - shortcuts *) @@ -505,379 +501,3 @@ 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 *)