From eff48a1c6e993a9d2bfa2b07453a90504a32820b Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 17:09:14 +0000 Subject: [PATCH 01/10] struct: minor model fixes, read combination fix --- model_with_structures/model.typ | 19 ++++++--- model_with_structures/synthesizer.ml | 3 +- model_with_structures/tests.ml | 2 +- model_with_structures/tests_f.ml | 64 +++++++++++----------------- 4 files changed, 39 insertions(+), 49 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 937a1f5..1912a7b 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -286,18 +286,25 @@ $X$ - можество переменных #let types = $Gamma$ #let envv = $#[env]_Sigma$ #let envt = $#[env]_Gamma$ -$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] -$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] +$envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] +$envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] $revpath$ - путь в обратную сторону, используется для обновления значений $action$ - действия, совершаемые с примитивным значением, модифицирующие содержащуюся таминформацию -// $DD : X -> decl$ - глобальные определения, частично определённая функция - -// $d in decl, $ -$s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ +- $r in readTag, w in writeTag$ +- $c in copyTag$ +- $i in inTag, o in outTag$ +- $s in stmt$ +- $f, x, a in X$ +- $a in action$ +- $p in path$ +- $v in value$ +- $v_m in vmem, v_r in vread, v_w in vwrite$ +- $t, u in type$ +- $pi in revpath$ === Path Accessors diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 19a93e2..a60eafd 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -757,8 +757,7 @@ struct { u == ZeroRV & v == ZeroRV & u' == ZeroRV } | { u == TopRV & v == ZeroRV & u' == ZeroRV } | { u == ZeroRV & v == TopRV & u' == ZeroRV } | - { u =/= TopRV & v =/= TopRV & - u =/= ZeroRV & v =/= ZeroRV & + { { u == OneRV | { u =/= OneRV & v == OneRV } } & u' == OneRV } } diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 2325fee..5433e74 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -89,7 +89,7 @@ let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_ [%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))))))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (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, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); 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, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); 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 (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS)))]))] |}] let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog_synt_t_presentation_complex_tp ()); [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 8022138..dccaa23 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -792,32 +792,27 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q 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 & + fresh data_p, time_p, + user_id_p, user_name_p in + deref_accesso 1 0 data_p & 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; - + seqo [ReadS data_p; + WriteS data_p; ReadS user_name_p; WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* TODO: FIXME *) - (* ChoiceS (sendBranchStmts, SkipS); *) + seqo [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 & + ReadS (VarP 0) + (* 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) & @@ -828,11 +823,8 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q 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 *) + ChoiceS (ReadS user_name_gp, + ReadS user_surname_gp); ReadS time_gp ] stmts & prog == Prg ([ @@ -884,12 +876,9 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( access_deref_accesso 2 0 0 user_surname_p & seqo [ReadS data_p; WriteS data_p; - ReadS user_name_p; WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* TODO: FIXME *) - (* ChoiceS (sendBranchStmts, SkipS); *) + seqo [ChoiceS (sendBranchStmts, SkipS); WriteS time_p; ReadS (VarP 0) ] sendStmts & @@ -903,10 +892,8 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( 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 *) + ChoiceS (ReadS user_name_gp, + ReadS user_surname_gp); ReadS user_surname_gp; (* TMP *) ReadS time_gp ] stmts & @@ -1031,9 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q 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 *) + WriteS (VarP 0)); + ReadS (VarP 0))] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1041,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q 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 *) + seqo [WriteS (VarP 0)); CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]); @@ -1317,8 +1303,7 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q 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 *) + ReadS (VarP 0)] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1326,11 +1311,10 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q 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 *) + seqo [WriteS (AccessP (VarP 0, 4)); 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 ( From 7d8ab196752e951154451f529e37e75e25679421 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 18:09:39 +0000 Subject: [PATCH 02/10] struct: model: build rule --- model_with_structures/model.typ | 102 +++++++++++++++++++++++++++----- 1 file changed, 87 insertions(+), 15 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 1912a7b..c2fec46 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -540,9 +540,69 @@ $action$ - действия, совершаемые с примитивным з === Value Construction +#let build = `build` + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build trivial read value], + + $mu xarrowSquiggly(cl Read \, w cr)_build + cl cdl 0_m, 0_r, 0_w cdr, mu cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build trivial $not$ read value], + + $mu xarrowSquiggly(cl not Read \, w cr)_build + cl cdl bot, 0_r, 0_w cdr, mu cr$, + ) +)) + +#h(10pt) + +// TODO: function pointer type ?? + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build reference value], + + $mu xarrowSquiggly(t)_build cl v, mu_v cr$, + + $mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$, + + $mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build tuple value], + + $mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$, + $...$, + $mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$, + + $mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$, + ) +)) + +#h(10pt) + +// --- + // TODO: FIXME:add ref / copy modes correctness check ?? -#let new = `new` +// #let copy = `copy` #align(center, prooftree( vertical-spacing: 4pt, @@ -551,22 +611,26 @@ $action$ - действия, совершаемые с примитивным з $v_m in {0, ?, bot}$, $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl Read \, w cr)_new - cl cdl v_m, 0, 0 cdr, mu cr$, + xarrowSquiggly(cl Read \, w cr)_copy + cl cdl v_m, 0_r, 0_w cdr, mu cr$, ) )) +#h(10pt) + // #align(center, prooftree( // vertical-spacing: 4pt, // rule( // name: [ new trivial read $top$ value], // $cl cdl top, v_r, v_w cdr, mu cr -// xarrowSquiggly(cl Read \, w cr)_new +// xarrowSquiggly(cl Read \, w cr)_copy // cl cdl 0, 0, 0 cdr, mu cr$, // ) // )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( @@ -574,53 +638,61 @@ $action$ - действия, совершаемые с примитивным з $v_m in {0, ?, bot/*, top */}$, $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl not Read \, w cr)_new - cl cdl bot, 0, 0 cdr, mu cr$, + xarrowSquiggly(cl not Read \, w cr)_copy + cl cdl bot, 0_r, 0_w cdr, mu cr$, ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new funciton pointer value], - $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$, + $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$, ) )) +#h(10pt) + // #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$, +// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$, // ) // )) +// #h(10pt) + // 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], - $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$, + $cl mu[l], mu cr xarrowSquiggly(t)_copy 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 c /*Copy*/ t)_copy cl rf l', mu_a cr$, ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new tuple value], - $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$, + $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$, $...$, - $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$, + $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$, - $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$, + $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$, ) )) @@ -1067,7 +1139,7 @@ $action$ - действия, совершаемые с примитивным з // expect well typed program $vals, mu texpre e eqmu v$, - $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?) + $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?) $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ @@ -1354,7 +1426,7 @@ $action$ - действия, совершаемые с примитивным з // TODO: check type compatibility for t and type for path p (?) // [*TODO: check t ~ t' in sme way (?)*], // <- programs considired to be well-typed - $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, + $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ?? From fac507bebf28e5dd9e48fda6a59756b9ba8b6282 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 18:19:31 +0000 Subject: [PATCH 03/10] struct: analyzer & synthesizer val build, small fixes --- model_with_structures/analyzer.ml | 19 +++++++++++--- model_with_structures/synthesizer.ml | 39 +++++++++++++++++++++++++++- model_with_structures/tests_f.ml | 6 ++--- 3 files changed, 57 insertions(+), 7 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 0c74973..602f81a 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -195,6 +195,19 @@ struct (* - value construction *) + let rec valbuild (mem : mem) (t : atype) : mem * value = + match t with + | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) + | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) + | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported" + | RefT (_, t) -> let (mem', v') = valbuild mem t in + let (mem'', id'') = mem_add mem' v' in + (mem'', RefV id'') + | TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in + (mem', v' :: vs') in + let mem', vs' = List.fold_right folder ts (mem, []) in + (mem', TupleV vs') + let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) @@ -204,10 +217,10 @@ struct | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in let (mem'', id'') = mem_add mem' v' in (mem'', RefV id'') - | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in + | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in (mem', v' :: vs') in - let mem', vs' = List.fold_left2 folder (mem, []) vs ts in - (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *) + let mem', vs' = List.fold_right2 folder vs ts (mem, []) in + (mem', TupleV vs') | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" (* - action rules *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index a60eafd..2d699bc 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -588,6 +588,44 @@ struct (* - value construction *) + let rec valbuild_foldero mem_with_vs tp mem_with_vs' = + ocanren { + fresh mem, vs, mem', v', vs' in + Std.pair mem vs == mem_with_vs & + valbuildo mem tp (Std.pair mem' v') & + vs' == v' :: vs & + mem_with_vs' == Std.pair mem' vs' + } + and valbuildo mem tp mem_with_id' = + let open Type in + let open Value in + let open ReadCap in + (* let open CopyCap in *) + let open MemVal in + let open ReadVal in + let open WriteVal in + ocanren { + { fresh r, w in + tp == UnitT (r, w) & + { { r == Rd & + mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } | + { r == NRd & + mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | + (* { fresh ts in *) + (* tp == FunT ts & *) + (* ??? } | *) + { fresh c, tp' in + tp == RefT (c, tp') & + { fresh mem_cp, v_cp, mem_add, id_add in + valbuildo mem 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 tps, mem', vs' in + tp == TupleT tps & + list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') & + mem_with_id' == Std.pair mem' (TupleV vs') } + } + let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = ocanren { fresh mem, vs, mem', v', vs' in @@ -606,7 +644,6 @@ struct let open WriteVal in ocanren { { fresh r, w in - is_trivial_vo v & tp == UnitT (r, w) & { { fresh v_m, _v_r, _v_w in r == Rd & diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index dccaa23..6f65938 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -1018,8 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q ReadS sb_access3] sendFBranch & seqo [ChoiceS (sendFBranch, SkipS); - WriteS (VarP 0)); - ReadS (VarP 0))] + WriteS (VarP 0); + ReadS (VarP 0)] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1027,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q 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 (VarP 0)); + seqo [WriteS (VarP 0); CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]); From 2d6516c105197f62bc3b428677bd4a6a9f2ba5d7 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 12:49:29 +0000 Subject: [PATCH 04/10] struct: small exmple fixes --- model_with_structures/send_example.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/model_with_structures/send_example.md b/model_with_structures/send_example.md index 0926245..85e7777 100644 --- a/model_with_structures/send_example.md +++ b/model_with_structures/send_example.md @@ -49,19 +49,19 @@ struct Request { Version* version; Utils* utils; Data* data; - DateTime operaiton_date; + DateTime time; }; // example itself -int get_version_id(Request /*[?]*/ r) { +int get_version_id(Request /*[?]*/ r) { if (r.utils.has_version) { return r.version.id; } return old_version_placeholder().id; } -Version updated_version(Request /*[?]*/ r) { +Version updated_version(Request /*[?]*/ r) { if (not r.utils.has_version) { return old_version_placeholder(); } @@ -114,12 +114,12 @@ Request := [& User; # user & Version; # version & Utils; # utils & (); # data - ()] # operation_date + ()] # time # or Request := [& [& [(); ()], & [(); (); ()]]; # user # & [(); (); ()]; # version # & [(); ()]; # utils # & (); # data -# ()] # operation_date +# ()] # time # example itself From d567cfd2957961fa0322c5387d20223c6f4aafca Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 13:39:16 +0000 Subject: [PATCH 05/10] struct: model change for lambdas to not include statements (+ as a result all program is now a function & there is no glob variables) --- model_with_structures/model.typ | 211 ++++++++++++++------------------ 1 file changed, 89 insertions(+), 122 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index c2fec46..85756ca 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -15,8 +15,6 @@ // *TODO: top-level value copy mode ??* // TODO: FIXME -*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME - #h(10pt) #let rf = $\& #h(3pt)$ @@ -140,14 +138,14 @@ `decl`, { // TODO: path not allowed ?? - Or[$"var" X : type = expr$][global variable declaration] + // Or[$"var" X : type = expr$][global variable declaration] Or[$"fun" X ((X : modedType)+) = stmt$][function declaration] } ), Prod( `prog`, { - Or[$decl+ space stmt$][declarations and executed statement] + Or[$decl+$][all program definitions] } ), ) @@ -203,7 +201,7 @@ $value_mu$, { Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit` - Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun` + Or[$lambda$][function pointer value, carries no information] // `Fun` Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref` Or[$[value+]$][tuple value] // `Prod` } @@ -276,8 +274,6 @@ $v in value$ - произвольное значение ), ) -// TODO: FIXME: add vars & funcs from global context in the beginnning - // $V := memelem$ - значения памяти $X$ - можество переменных @@ -568,6 +564,17 @@ $action$ - действия, совершаемые с примитивным з // TODO: function pointer type ?? +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build funciton pointer value], + + $cl mu cr xarrowSquiggly(lambda space c space overline(t))_build cl lambda, mu cr$, + ) +)) + +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( @@ -604,97 +611,75 @@ $action$ - действия, совершаемые с примитивным з // #let copy = `copy` -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ new trivial read value], - - $v_m in {0, ?, bot}$, - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl Read \, w cr)_copy - cl cdl v_m, 0_r, 0_w cdr, mu cr$, - ) -)) - -#h(10pt) - // #align(center, prooftree( // vertical-spacing: 4pt, // rule( -// name: [ new trivial read $top$ value], +// name: [ new trivial read value], -// $cl cdl top, v_r, v_w cdr, mu cr +// // NOTE: should not be important to copy v_m, because spoil & tags +// // should care for this instead +// $v_m in {0, ?, bot}$, +// $cl cdl v_m, v_r, v_w cdr, mu cr // xarrowSquiggly(cl Read \, w cr)_copy -// cl cdl 0, 0, 0 cdr, mu cr$, +// cl cdl v_m, 0_r, 0_w cdr, mu cr$, // ) // )) -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ new trivial $not$ read value], - - $v_m in {0, ?, bot/*, top */}$, - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl not Read \, w cr)_copy - cl cdl bot, 0_r, 0_w cdr, mu cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ new funciton pointer value], - - $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$, - ) -)) - -#h(10pt) +// #h(10pt) // #align(center, prooftree( // vertical-spacing: 4pt, // rule( -// name: [ new reference ref value], +// name: [ new trivial $not$ read value], -// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$, +// $v_m in {0, ?, bot/*, top */}$, +// $cl cdl v_m, v_r, v_w cdr, mu cr +// xarrowSquiggly(cl not Read \, w cr)_copy +// cl cdl bot, 0_r, 0_w cdr, mu cr$, +// ) +// )) + +// #h(10pt) + +// #align(center, prooftree( +// vertical-spacing: 4pt, +// rule( +// name: [ new funciton pointer value], + +// $cl lambda, mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda, mu cr$, // ) // )) // #h(10pt) // 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], +// #align(center, prooftree( +// vertical-spacing: 4pt, +// rule( +// name: [ new reference /* copy */ value], - $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$, +// $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$, - $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, +// $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, - $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$, - ) -)) +// $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$, +// ) +// )) -#h(10pt) +// #h(10pt) -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ new tuple value], +// #align(center, prooftree( +// vertical-spacing: 4pt, +// rule( +// name: [ new tuple value], - $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$, - $...$, - $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$, +// $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$, +// $...$, +// $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$, - $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$, - ) -)) +// $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$, +// ) +// )) === Action Rules @@ -977,12 +962,7 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ combine lambda values], - $overline(x_1) = overline(x_2)$, - $s_1 = s_2$, - $lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1] - plus.o lambda space [overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2] - = lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1, - overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]$ + $lambda plus.o lambda = lambda$ ) )) @@ -1130,30 +1110,30 @@ $action$ - действия, совершаемые с примитивным з #let init = `init` -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ add variable declaration], +// #align(center, prooftree( +// vertical-spacing: 4pt, +// rule( +// name: [ add variable declaration], - // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) - // expect well typed program +// // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) +// // expect well typed program - $vals, mu texpre e eqmu v$, - $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?) - $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, +// $vals, mu texpre e eqmu v$, +// $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?) +// $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, - $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ - ) -)) +// $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ +// ) +// )) -#h(10pt) +// #h(10pt) #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ add function declaration], - $mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, mu' cr$, + $mu xarrowSquiggly(lambda)_#[add] cl l, mu' cr$, $cl types, vals, mu cr xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init @@ -1333,8 +1313,6 @@ $action$ - действия, совершаемые с примитивным з ) )) -#h(10pt) - #align(center, prooftree( vertical-spacing: 4pt, @@ -1421,17 +1399,13 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ add argument], - $vals_#[ctx], mu texpre e eqmu v$, - // $types ttype p : t'$, // TODO: not required if there is no check - // TODO: check type compatibility for t and type for path p (?) - // [*TODO: check t ~ t' in sme way (?)*], - // <- programs considired to be well-typed - $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, - $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, + // programs considired to be well-typed + $cl v, mu cr xarrowSquiggly(t)_build cl v, mu' cr$, + $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$, // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ?? $cl types, vals, mu cr - xarrowDashed(x space t space e)_(vals_#[ctx]) + xarrowDashed(x space t) cl types[x <- t], vals[x <- l], mu'' cr$, ) )) @@ -1490,7 +1464,7 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ lambda check], - $mu ttags lambda space overline(s) : lambda overline(t)$, + $mu ttags lambda : lambda overline(t)$, ) )) #align(center, prooftree( @@ -1520,18 +1494,13 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ new reference copy value], - // TODO: FIXME: introduce global types and vals - $types_0 = types_#[glob]$, - $vals_0 = vals_#[glob]$, - $mu_0 = mu$, - // NOTE: dashed arrow to fill context $cl types_0, vals_0, mu_0 cr - xarrowDashed(x_1 space t_1 space e_1)_vals + xarrowDashed(x_1 space t_1) cl types', vals_1, mu_1 cr$, $...$, $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr - xarrowDashed(x_n space t_n space e_n)_vals + xarrowDashed(x_n space t_n) cl types_n, vals_n, mu_n cr$, // NOTE: eval function body @@ -1544,7 +1513,7 @@ $action$ - действия, совершаемые с примитивным з $...$, $mu' ttags mu'[vals'[x_n]] : t_n$, - $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$, + $types_0, vals_0, mu_0 tfunceval cl "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$, ) )) @@ -1633,13 +1602,14 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ CALL $f space [e_1, ... e_n]$], - $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$, + // $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$, $types ttype f : lambda [m_1 t_1, ... m_n t_n] $, + // NOTE: should be done on decl eval now // NOTE: check that all the possible bodies are possible to eval - $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$, - $...$, - $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$, + // $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$, + // $...$, + // $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$, // NOTE: "spoil" context for each argument usage $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$, @@ -1755,14 +1725,11 @@ $action$ - действия, совершаемые с примитивным з $...$, $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$, - // TODO: FIXME: some easy way to pass to eval ?? - $types_#[glob] = types_n$, - $vals_#[glob] = vals_n$, - $mu_#[glob] = mu_n$, + $cl types_n, vals_n, mu_n tfunceval d_1$, + $...$, + $cl types_n, vals_n, mu_n tfunceval d_n$, - $cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$, - - $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n s)_prog_eval cl types', vals', mu' cr$ + $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n)_prog_eval cl types_n, vals_n, mu_n cr$ ) )) From b6568704f0c569a14f28acbe4b49af03706977e5 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 14:03:03 +0000 Subject: [PATCH 06/10] struct: model: fix tfunceval rule header --- model_with_structures/model.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 85756ca..8d989b7 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -1492,7 +1492,7 @@ $action$ - действия, совершаемые с примитивным з #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ new reference copy value], + name: [ function evaluation], // NOTE: dashed arrow to fill context $cl types_0, vals_0, mu_0 cr From b8d704d0d0dbec69b717fff8d31acfa7b9943fed Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 14:24:30 +0000 Subject: [PATCH 07/10] struct: model: final model fixes (+ ret glob val decland stmt) to match analyzer --- model_with_structures/model.typ | 49 +++++++++++++++++---------------- 1 file changed, 25 insertions(+), 24 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 8d989b7..bc169ac 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -138,14 +138,14 @@ `decl`, { // TODO: path not allowed ?? - // Or[$"var" X : type = expr$][global variable declaration] + Or[$"var" X : type$][global variable declaration] Or[$"fun" X ((X : modedType)+) = stmt$][function declaration] } ), Prod( `prog`, { - Or[$decl+$][all program definitions] + Or[$decl+ stmt$][all program definitions and executed statement] } ), ) @@ -1110,23 +1110,22 @@ $action$ - действия, совершаемые с примитивным з #let init = `init` -// #align(center, prooftree( -// vertical-spacing: 4pt, -// rule( -// name: [ add variable declaration], +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ add variable declaration], -// // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) -// // expect well typed program + // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) + // expect well typed program -// $vals, mu texpre e eqmu v$, -// $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?) -// $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, + $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$, // TODO: FIXME check (required?) + $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$, -// $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ -// ) -// )) + $cl types, vals, mu cr xarrowSquiggly("var" x : t)_init cl types[x <- t], vals[x <- l], mu'' cr$ + ) +)) -// #h(10pt) +#h(10pt) #align(center, prooftree( vertical-spacing: 4pt, @@ -1492,7 +1491,7 @@ $action$ - действия, совершаемые с примитивным з #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ function evaluation], + name: [ function declaration evaluation], // NOTE: dashed arrow to fill context $cl types_0, vals_0, mu_0 cr @@ -1513,7 +1512,16 @@ $action$ - действия, совершаемые с примитивным з $...$, $mu' ttags mu'[vals'[x_n]] : t_n$, - $types_0, vals_0, mu_0 tfunceval cl "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$, + $types_0, vals_0, mu_0 tfunceval "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$, + ) +)) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ var declaration evaluation (skip)], + + $types, vals, mu tfunceval "var" x : t$, ) )) @@ -1602,15 +1610,8 @@ $action$ - действия, совершаемые с примитивным з rule( name: [ CALL $f space [e_1, ... e_n]$], - // $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$, $types ttype f : lambda [m_1 t_1, ... m_n t_n] $, - // NOTE: should be done on decl eval now - // NOTE: check that all the possible bodies are possible to eval - // $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$, - // $...$, - // $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$, - // NOTE: "spoil" context for each argument usage $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$, $...$, From e718ccb24bfd178cc19b0e12078791364561fa78 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 14:24:57 +0000 Subject: [PATCH 08/10] struct: analyzer: fixes to match model with lambdas without stmts --- model_with_structures/analyzer.ml | 187 ++++++++++++++---------------- 1 file changed, 85 insertions(+), 102 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 602f81a..6ddc6ad 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -38,7 +38,7 @@ struct | SeqS of stmt * stmt | ChoiceS of stmt * stmt - type decl = VarD of (* data * *) atype * expr + type decl = VarD of (* data * *) atype (* * expr *) | FunD of (* data * *) (* (data * *) mtype (* ) *) list * stmt type prog = decl list * stmt @@ -71,7 +71,7 @@ struct type writeval = ZeroWV | SmthWV | OneWV type value = UnitV of memval * readval * writeval - | FunV of ((* data list * *) stmt) list + | FunV (* of ((* data list * *) stmt) list *) | RefV of memid | TupleV of value list @@ -84,10 +84,9 @@ struct (* --- *) type mem = value list * memid (* NOTE: memory and first free elem *) - type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *) - type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *) - type visited = stmt list (* TODO: FIXME: optimize, use ids *) - type state = mem * types * vals * visited + type types = (data * atype) list + type vals = (data * memid) list + type state = mem * types * vals (* --- *) @@ -96,23 +95,17 @@ struct let types_assoc (x : data) (types : types) : atype = (* try ( List.assoc x (fst types) ) *) (* with Not_found -> *) - List.assoc x (snd types) + List.assoc x types let vals_assoc (x : data) (vals : vals) : memid = (* try ( List.assoc x (fst vals) ) *) (* with Not_found -> *) - List.assoc x (snd vals) - - let types_glob_add (types : types) (x : data) (t : atype) = - ((x, t) :: fst types, (x, t) :: snd types) + List.assoc x vals let types_add (types : types) (x : data) (t : atype) = - (fst types, (x, t) :: snd types) - - let vals_glob_add (vals : vals) (x : data) (id : memid) = - ((x, id) :: fst vals, (x, id) :: snd vals) + (x, t) :: types let vals_add (vals : vals) (x : data) (id : memid) = - (fst vals, (x, id) :: snd vals) + (x, id) :: vals (* - utils *) @@ -208,20 +201,21 @@ struct let mem', vs' = List.fold_right folder ts (mem, []) in (mem', TupleV vs') - let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = - match t, v with - | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) - | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) - | FunT _, FunV _ -> (mem, v) + (* NOTE: not needed now *) + (* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = *) + (* match t, v with *) + (* | 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 - let (mem'', id'') = mem_add mem' v' in - (mem'', RefV id'') - | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in - (mem', v' :: vs') in - let mem', vs' = List.fold_right2 folder vs ts (mem, []) in - (mem', TupleV vs') - | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" + (* | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in *) + (* let (mem'', id'') = mem_add mem' v' in *) + (* (mem'', RefV id'') *) + (* | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in *) + (* (mem', v' :: vs') in *) + (* let mem', vs' = List.fold_right2 folder vs ts (mem, []) in *) + (* (mem', TupleV vs') *) + (* | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" *) (* - action rules *) @@ -299,7 +293,7 @@ struct match u, v with | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) -> UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w) - | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) + | FunV, FunV -> FunV | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref" | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs) | _, _ -> raise @@ Typing_error "valcomb" @@ -331,16 +325,15 @@ struct (* TODO: check new in vars *) let add_decl (state : state) (x : data) (d : decl) : state = - match state with (mem, types, vals, visited) -> match d with - | VarD (t, e) -> let v = exprval mem vals e in - let (mem', v') = valcopy mem v t in - let (mem'', id) = mem_add mem' v' in - (mem'', types_glob_add types x t, vals_glob_add vals x id, visited) - | FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in - (mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited) + match state with (mem, types, vals) -> match d with + | VarD t -> let (mem', v) = valbuild mem t in + let (mem'', id) = mem_add mem' v in + (mem'', types_add types x t, vals_add vals x id) + | FunD (ts, s) -> let (mem', id) = mem_add mem FunV in + (mem', types_add types x (FunT ts), vals_add vals x id) let empty_mem : mem = ([], 0) - let empty_state : state = (empty_mem, ([], []), ([], []), []) + let empty_state : state = (empty_mem, [], []) (* TODO: better way ??? *) let globals_min_id : data = 1000 @@ -401,7 +394,7 @@ struct let v_m''' = tryspoil m w v_m'' in (mem, UnitV (v_m''', v_r'', v_w'')) | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit") - | FunT ts, FunV _ -> (mem, v) + | FunT ts, FunV -> (mem, v) | RefT (ct, t), RefV id -> let (mem', v') = valspoil mem (mem_get mem id) t m ct in (mem_set mem id v', RefV id) @@ -415,7 +408,7 @@ struct (* full spoil *) let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = - match state with (mem, types, vals, visited) -> + match state with (mem, types, vals) -> let x = pathvar p in let id = vals_assoc x vals in (* base var address *) let b = pathval mem vals p in (* subvalue in var *) @@ -427,29 +420,23 @@ struct mem_set mem'' id v'' let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = - match state with (mem, types, vals, visited) -> match e, t with + match state with (mem, types, vals) -> match e, t with | UnitE, UnitT _ -> mem | PathE p, t -> argsspoilp state m t p | RefE x, t -> argsspoilp state m t (VarP x) (* TODO: FIXME: check RefE case ? *) | TupleE es, TupleT ts -> List.fold_left2 - (fun mem' t' e' -> argsspoile (mem', types, vals, visited) m t' e') + (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e') mem ts es | _, _ -> raise @@ Typing_error "valspoile" (* - funciton argument addition *) - let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state = - match state with (mem, types, vals, visited) -> - let v = exprval mem oldvals e in - (* let t' = pathtype types p in *) - let (mem', v') = valcopy mem v t in - let (mem'', id) = mem_add mem' v' in - (mem'', types_add types x t, vals_add vals x id, visited) - - (* - function evaluation *) - (* NOTE: not needed due to performed optimization in stmt_eval *) - (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *) + let addarg (state : state) (x : data) (t : atype) : state = + match state with (mem, types, vals) -> + let (mem', v) = valbuild mem t in + let (mem'', id) = mem_add mem' v in + (mem'', types_add types x t, vals_add vals x id) let writeval_to_cap (v_w : writeval) : write_cap = match v_w with @@ -467,7 +454,7 @@ struct else if writeval_to_cap v_w != w then raise @@ Eval_error "tags_check: wrong write tag" else () - | FunV _, FunT _ -> () + | FunV, FunT _ -> () | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts | _, _ -> raise @@ Typing_error "tags_check" @@ -481,45 +468,40 @@ struct | RefT (_, t) -> is_all_type_writable t | TupleT ts -> List.for_all is_all_type_writable ts + + (* - function evaluation *) + + let rec func_eval (state : state) (d : decl) : unit = + match d with + | FunD (ts, stmt) -> + (match state with (mem, types, vals) -> + let (state_with_args, _) = List.fold_left + (fun (st, x) (m, t) -> (addarg st x t, x + 1)) + (state, 0) ts in + (* NOTE: same x's, so can use same args for all the statements *) + match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) -> + ignore @@ List.fold_left + (fun x (_, t) -> + let id = vals_assoc x vals_after_stmt in + let v = mem_get mem_after_stmt id in + tags_check mem_after_stmt v t; x + 1) + 0 ts) + | VarD _ -> () + (* - statement evaluation *) - let rec stmt_eval (state : state) (s : stmt) : state = - match state with (mem, types, vals, visited) -> match s with + and stmt_eval (state : state) (s : stmt) : state = + match state with (mem, types, vals) -> match s with | SkipS -> state | CallS (f, es) -> let v = pathval mem vals f in let t = pathtype types f in - let types' : types = (fst types, fst types) in - let vals' : vals = (fst vals, fst vals) in (match v, t with - | FunV (* xs, *) fstmts (* ) *), FunT ts -> - let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) - List.fold_left2 (* TODO: FIXME: check x's order *) - (fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1)) - ((mem, types', vals', visited), 0) ts es in - (* NOTE: same x's, so can use same args for all the statements *) - (match state_with_args with (mem_swa, types_swa, vals_swa, visited_swa) -> - let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *) - List.fold_left - (fun visited_old stmt -> - if List.mem stmt visited_old - then stmt :: visited_old - else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with - (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) -> - ignore @@ List.fold_left - (fun x (_, t) -> - let id = vals_assoc x vals_after_stmt in - let v = mem_get mem_after_stmt id in - tags_check mem_after_stmt v t; x + 1) - 0 ts; - visited_after_stmt) - visited_swa - fstmts in - let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) - List.fold_left2 - (fun mem (m, t) e -> argsspoile (mem, types, vals, (* NOTE: not important *) visited_new) m t e) + | FunV, FunT ts -> + let mem_spoiled = List.fold_left2 + (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e) mem ts es in - (mem_spoiled, types, vals, visited_new)) - | FunV _, _ -> raise @@ Eval_error "call: function type" + (mem_spoiled, types, vals) + | FunV, _ -> raise @@ Eval_error "call: function type" | _, FunT _ -> raise @@ Eval_error "call: function val" | _, _ -> raise @@ Eval_error "call: function type & val") | WriteS p -> if not @@ is_all_type_writable @@ pathtype types p @@ -528,12 +510,12 @@ struct let id = vals_assoc x vals in let pi = pathrev p VarRP in let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in - (mem_set mem' id v', types, vals, visited) + (mem_set mem' id v', types, vals) | ReadS p -> let x = pathvar p in let id = vals_assoc x vals in let pi = pathrev p VarRP in let (mem', v') = valupd mem (mem_get mem id) pi ReadA in - (mem_set mem' id v', types, vals, visited) + (mem_set mem' id v', types, vals) (* NOTE: handled inside through undefined in memvmod *) (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) (* then raise @@ Eval_error "read: spoiled value" *) @@ -541,18 +523,19 @@ struct stmt_eval statel sr | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in let stater = stmt_eval state sr in - match statel with (meml, typesl, valsl, visitedl) -> - match stater with (memr, typesr, valsr, visitedr) -> + match statel with (meml, typesl, valsl) -> + match stater with (memr, typesr, valsr) -> if typesl != typesr || valsl != valsr then raise @@ Eval_error "choice" (* TODO: FIXME: better list union ?? *) - else (memcomb meml memr, typesl, valsl, visitedl @ visitedr) + else (memcomb meml memr, typesl, valsl) (* --- program execution --- *) let prog_eval (prog : prog) : state = match prog with (decls, s) -> let init_state = prog_init prog in + ignore @@ List.map (func_eval init_state) decls; stmt_eval init_state s let prog_eval_noret (prog : prog) : unit = @@ -627,8 +610,8 @@ struct let moded t = ((In, NOut), t) - let defgu t = VarD (t, UnitE) - let defg t e = VarD (t, e) + let defgu t = VarD t + let defg t e = VarD t let wrS p = WriteS p let rdS p = ReadS p @@ -668,40 +651,40 @@ struct [%expect {| done! |}] let%expect_test "simple var" = - prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], + prog_eval_noret ([VarD (UnitT (Rd, MayWr))], ReadS (VarP globals_min_id)); Printf.printf "done!"; [%expect {| done! |}] let%expect_test "simple var, forbidden read" = - try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + try(prog_eval_noret ([VarD (UnitT (NRd, MayWr))], ReadS (VarP globals_min_id)); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| memvmod: forbidden read |}] let%expect_test "simple vars, no read & read" = - prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE); - VarD (UnitT (Rd, MayWr), UnitE)], + prog_eval_noret ([VarD (UnitT (NRd, MayWr)); + VarD (UnitT (Rd, MayWr))], ReadS (VarP (globals_min_id + 1))); Printf.printf "done!"; [%expect {| done! |}] let%expect_test "simple var, write" = - prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + prog_eval_noret ([VarD (UnitT (NRd, MayWr))], WriteS (VarP globals_min_id)); Printf.printf "done!"; [%expect {| done! |}] let%expect_test "simple var, forbidden write" = - try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], + try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr))], WriteS (VarP globals_min_id)); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| write: write tag |}] let%expect_test "simple var, write & read" = - prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + prog_eval_noret ([VarD (UnitT (NRd, MayWr))], SeqS (WriteS (VarP globals_min_id), ReadS (VarP globals_min_id))); Printf.printf "done!"; @@ -710,7 +693,7 @@ struct (* - basic call tests *) (* let%expect_test "simple call with read" = *) - (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *) + (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr)); *) (* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *) (* CallS (VarP (globals_min_id + 1), *) (* [PathE (VarP globals_min_id)])); *) @@ -718,7 +701,7 @@ struct (* [%expect {| done! |}] *) (* let%expect_test "simple call with write" = *) - (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *) + (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr))); *) (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *) (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *) (* CallS (VarP (globals_min_id + 2), *) From ae01a435ff2d5f316fb7be2b5c0f2e42a24dbed2 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 15:59:44 +0000 Subject: [PATCH 09/10] struct: synthesizer lambdas without value fix, analyzer and model minor fixes; broken synt call tests --- model_with_structures/analyzer.ml | 148 +++++----- model_with_structures/model.typ | 4 +- model_with_structures/synthesizer.ml | 397 ++++++++++----------------- model_with_structures/tests.ml | 10 +- model_with_structures/tests_f.ml | 194 ++++++------- 5 files changed, 330 insertions(+), 423 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 6ddc6ad..8c49d32 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -438,6 +438,8 @@ struct let (mem'', id) = mem_add mem' v in (mem'', types_add types x t, vals_add vals x id) + (* --- *) + let writeval_to_cap (v_w : writeval) : write_cap = match v_w with | ZeroWV -> NeverWr @@ -468,29 +470,9 @@ struct | RefT (_, t) -> is_all_type_writable t | TupleT ts -> List.for_all is_all_type_writable ts - - (* - function evaluation *) - - let rec func_eval (state : state) (d : decl) : unit = - match d with - | FunD (ts, stmt) -> - (match state with (mem, types, vals) -> - let (state_with_args, _) = List.fold_left - (fun (st, x) (m, t) -> (addarg st x t, x + 1)) - (state, 0) ts in - (* NOTE: same x's, so can use same args for all the statements *) - match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) -> - ignore @@ List.fold_left - (fun x (_, t) -> - let id = vals_assoc x vals_after_stmt in - let v = mem_get mem_after_stmt id in - tags_check mem_after_stmt v t; x + 1) - 0 ts) - | VarD _ -> () - (* - statement evaluation *) - and stmt_eval (state : state) (s : stmt) : state = + let rec stmt_eval (state : state) (s : stmt) : state = match state with (mem, types, vals) -> match s with | SkipS -> state | CallS (f, es) -> let v = pathval mem vals f in @@ -530,6 +512,23 @@ struct (* TODO: FIXME: better list union ?? *) else (memcomb meml memr, typesl, valsl) + (* - function evaluation *) + + let rec func_eval (state : state) (d : decl) : unit = + match d with + | FunD (ts, stmt) -> + (let (state_with_args, _) = List.fold_left + (fun (st, x) (m, t) -> (addarg st x t, x + 1)) + (state, 0) ts in + match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) -> + ignore @@ List.fold_left + (fun x (_, t) -> + let id = vals_assoc x vals_after_stmt in + let v = mem_get mem_after_stmt id in + tags_check mem_after_stmt v t; x + 1) + 0 ts) + | VarD _ -> () + (* --- program execution --- *) let prog_eval (prog : prog) : state = @@ -610,8 +609,7 @@ struct let moded t = ((In, NOut), t) - let defgu t = VarD t - let defg t e = VarD t + let defg t = VarD t let wrS p = WriteS p let rdS p = ReadS p @@ -712,8 +710,8 @@ struct let%expect_test "simple call with read, dsl" = prog_eval_noret ( [ - defgu uT_r_mw; - defg (rfT uT_r_mw) rfg0E; + defg uT_r_mw; + defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], rdS @@ drf @@ v0 @@ -727,8 +725,8 @@ struct let%expect_test "simple call with write, dsl" = prog_eval_noret ( [ - defgu uT_aw; - defg (rfT uT_aw) rfg0E; + defg uT_aw; + defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], wrS @@ drf @@ v0 @@ -742,8 +740,8 @@ struct let%expect_test "simple call with read after write, dsl" = prog_eval_noret ( [ - defgu uT_aw; - defg (rfT uT_aw) rfg0E; + defg uT_aw; + defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], (wrS @@ drf @@ v0) #. @@ -758,8 +756,8 @@ struct let%expect_test "simple call with forbidden write, dsl" = try (prog_eval_noret ( [ - defgu uT_r_mw; - defg (rfT uT_r_mw) rfg0E; + defg uT_r_mw; + defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], wrS @@ drf @@ v0 @@ -775,8 +773,8 @@ struct let%expect_test "simple call with write to ref, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 @@ -790,8 +788,8 @@ struct let%expect_test "simple call with forbidden write to ref, dsl" = try (prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 @@ -807,8 +805,8 @@ struct let%expect_test "simple call with write to ref with fix, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 @@ -824,8 +822,8 @@ struct let%expect_test "call inside call, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 @@ -846,8 +844,8 @@ struct let%expect_test "call inside call, recursive, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ cpT @@ uT_aw], (callS vg2 [pE v0]) #. @@ -863,8 +861,8 @@ struct let%expect_test "call to fix after call, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 @@ -884,8 +882,8 @@ struct let%expect_test "simple call with global variable usage, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r) rfg0E; + defg uT_r_aw; + defg (rfT uT_r); FunD ( [moded @@ cpT @@ uT], (wrS @@ vg0) #. @@ -901,10 +899,10 @@ struct let%expect_test "simple call with read & write (2 args), dsl" = prog_eval_noret ( [ - defgu uT_r; - defg (rfT uT_r) rfg0E; - defgu uT_aw; - defg (rfT uT_aw) rfg2E; + defg uT_r; + defg (rfT uT_r); + defg uT_aw; + defg (rfT uT_aw); FunD ( [ moded @@ rfT @@ uT_r; @@ -922,14 +920,14 @@ struct let%expect_test "simple call with different arguments modifiers, copy, dsl" = prog_eval_noret ( [ - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg2E; - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg4E; - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg6E; + defg uT_r_aw; + defg (rfT uT_r_aw); + defg uT_r_aw; + defg (rfT uT_r_aw); + defg uT_r_aw; + defg (rfT uT_r_aw); + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [ ((NIn, NOut), cpT @@ uT); @@ -956,14 +954,14 @@ struct let%expect_test "simple call with different arguments modifiers, ref, dsl" = prog_eval_noret ( [ - defgu uT_r; - defg (rfT uT_r) rfg0E; - defgu uT_r; - defg (rfT uT_r) rfg2E; - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg4E; - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg6E; + defg uT_r; + defg (rfT uT_r); + defg uT_r; + defg (rfT uT_r); + defg uT_r_aw; + defg (rfT uT_r_aw); + defg uT_r_aw; + defg (rfT uT_r_aw); FunD ( [ ((NIn, NOut), rfT @@ uT); @@ -991,14 +989,14 @@ struct 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 *) + defg uT_r_aw; + defg (rfT uT_r_aw); (* x *) + defg uT_r_aw; + defg (rfT uT_r_aw); (* y *) + defg uT_r_aw; + defg (rfT uT_r_aw); (* z *) + defg uT_r_aw; + defg (rfT uT_r_aw); (* k *) FunD ( (* f *) [ (moded @@ rfT @@ uT_r_aw); @@ -1069,7 +1067,7 @@ struct (* [ *) (* defg userT userE; *) (* defg dataT dataE; *) - (* defgu uT_r_aw; (* time *) *) + (* defg uT_r_aw; (* time *) *) (* defg requestT requestE; *) (* FunD ( (* send *) *) (* [ *) @@ -1164,7 +1162,7 @@ struct (* defg userT userE; *) (* defg versionT versionE; *) (* defg utilsT utilsE; *) - (* defgu uT_r_aw; *) + (* defg uT_r_aw; *) (* defg requestT requestE; *) (* get_version_idF; *) (* updated_versionF; *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index bc169ac..887e5bf 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -1118,7 +1118,7 @@ $action$ - действия, совершаемые с примитивным з // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) // expect well typed program - $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$, // TODO: FIXME check (required?) + $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$, $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$, $cl types, vals, mu cr xarrowSquiggly("var" x : t)_init cl types[x <- t], vals[x <- l], mu'' cr$ @@ -1516,6 +1516,8 @@ $action$ - действия, совершаемые с примитивным з ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 2d699bc..8987412 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -147,7 +147,7 @@ struct module Decl = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's + type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't | FunD of (* 'd * 'dl * *) 'mtl * 's [@@deriving gt ~options:{ show; gmap }] type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t ] @@ -194,13 +194,12 @@ struct module Value = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw - | FunV of 'sl - | RefV of 'd - | TupleV of 'vl + type nonrec ('vm, 'vr, 'vw, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw + | FunV + | RefV of 'd + | TupleV of 'vl [@@deriving gt ~options:{ show; gmap }] type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground, - ((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t ] end @@ -237,7 +236,7 @@ struct module TypesEnv = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *) + type nonrec 'dtl t = TypesEnv of 'dtl [@@deriving gt ~options:{ show; gmap }] type nonrec ground = ((Nat.ground * Type.ground) List.ground) t ] @@ -246,27 +245,18 @@ struct module ValsEnv = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *) + type nonrec 'ddl t = ValsEnv of 'ddl [@@deriving gt ~options:{ show; gmap }] type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t ] end - module VisitedEnv = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec 'sl t = VisitedEnv of 'sl - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (Stmt.ground List.ground) t - ] - end - module StEnv = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited + type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t + type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t ] end @@ -405,87 +395,35 @@ struct let types_assoco id types tp = let open TypesEnv in ocanren { - fresh _glob_tps, tps in - types == TypesEnv (_glob_tps, tps) & + fresh tps in + types == TypesEnv tps & List.assoco id tps tp } let vals_assoco id vals v = let open ValsEnv in ocanren { - fresh _glob_vs, vs in - vals == ValsEnv (_glob_vs, vs) & + fresh vs in + vals == ValsEnv vs & List.assoco id vs v } - let types_glob_addo types x tp types' = - let open TypesEnv in - ocanren { - fresh glob_tps, tps in - types == TypesEnv (glob_tps, tps) & - types' == TypesEnv ((Std.pair x tp) :: glob_tps, - (Std.pair x tp) :: tps) - } - let types_addo types x tp types' = let open TypesEnv in ocanren { - fresh glob_tps, tps in - types == TypesEnv (glob_tps, tps) & - types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps) - } - - let vals_glob_addo vals x v vals' = - let open ValsEnv in - ocanren { - fresh glob_vs, vs in - vals == ValsEnv (glob_vs, vs) & - vals' == ValsEnv ((Std.pair x v) :: glob_vs, - (Std.pair x v) :: vs) + fresh tps in + types == TypesEnv tps & + types' == TypesEnv ((Std.pair x tp) :: tps) } let vals_addo vals x v vals' = let open ValsEnv in ocanren { - fresh glob_vs, vs in - vals == ValsEnv (glob_vs, vs) & - vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs) + fresh vs in + vals == ValsEnv vs & + vals' == ValsEnv ((Std.pair x v) :: vs) } - let visited_appendo visitedl visitedr visited' = - let open VisitedEnv in - ocanren { - fresh vsl, vsr, vs' in - visitedl == VisitedEnv vsl & - visitedr == VisitedEnv vsr & - List.appendo vsl vsr vs' & - visited' == VisitedEnv vs' - } - - let visited_checko visited stmt = - let open VisitedEnv in - ocanren { - fresh vs in - visited == VisitedEnv vs & - List.membero vs stmt - } - - let not_visited_checko visited stmt = - let open VisitedEnv in - ocanren { - fresh vs in - visited == VisitedEnv vs & - list_not_membero vs stmt - } - - let visited_addo visited stmt visited' = - let open VisitedEnv in - ocanren { - fresh vs in - visited == VisitedEnv vs & - visited' == VisitedEnv (stmt :: vs) - } - (* --- *) let mem_geto mem id v = @@ -626,51 +564,51 @@ struct mem_with_id' == Std.pair mem' (TupleV vs') } } - let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = - ocanren { - fresh mem, vs, mem', v', vs' in - Std.pair mem vs == mem_with_vs & - valcopyo mem v tp (Std.pair mem' v') & - vs' == v' :: vs & - mem_with_vs' == Std.pair mem' vs' - } - and valcopyo mem v tp mem_with_id' = - let open Type in - let open Value in - let open ReadCap in + (* let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = *) + (* ocanren { *) + (* fresh mem, vs, mem', v', vs' in *) + (* Std.pair mem vs == mem_with_vs & *) + (* valcopyo mem v tp (Std.pair mem' v') & *) + (* vs' == v' :: vs & *) + (* mem_with_vs' == Std.pair mem' vs' *) + (* } *) + (* and valcopyo mem v tp mem_with_id' = *) + (* let open Type in *) + (* let open Value in *) + (* let open ReadCap in *) (* let open CopyCap in *) - let open MemVal in - let open ReadVal in - let open WriteVal in - ocanren { - { fresh r, w in - tp == UnitT (r, w) & - { { fresh v_m, _v_r, _v_w in - r == Rd & - v == UnitV (v_m, _v_r, _v_w) & - mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } | - { r == NRd & - mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | - { fresh stmts, ts in - v == FunV stmts & - tp == FunT ts & - mem_with_id' == Std.pair mem v } | - { fresh c, tp', id in - v == RefV id & - tp == RefT (c, tp') & + (* let open MemVal in *) + (* let open ReadVal in *) + (* let open WriteVal in *) + (* ocanren { *) + (* { fresh r, w in *) + (* tp == UnitT (r, w) & *) + (* { { fresh v_m, _v_r, _v_w in *) + (* r == Rd & *) + (* v == UnitV (v_m, _v_r, _v_w) & *) + (* mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } | *) + (* { r == NRd & *) + (* mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | *) + (* { fresh stmts, ts in *) + (* v == FunV stmts & *) + (* tp == FunT ts & *) + (* mem_with_id' == Std.pair mem v } | *) + (* { 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 + (* { 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 & - list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & - mem_with_id' == Std.pair mem' (TupleV vs') } - } + (* 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 & *) + (* list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & *) + (* mem_with_id' == Std.pair mem' (TupleV vs') } *) + (* } *) (* - action rules *) @@ -820,12 +758,9 @@ struct readvalcombo u_r v_r u_r' & writevalcombo u_w v_w u_w' & u' == UnitV (u_m', u_r', u_w') } | - { fresh ustmts, vstmts, ustmts' in - u == FunV ustmts & - v == FunV vstmts & - (* TODO: swap stmts order o efficiency ? *) - List.appendo ustmts vstmts ustmts' & - u' == FunV ustmts' } | + { u == FunV & + v == FunV & + u' == FunV } | { fresh a, b in u == RefV a & v == RefV b & @@ -910,32 +845,26 @@ struct let open Value in let open Type in ocanren { - fresh mem, types, vals, visited in - st == StEnv (mem, types, vals, visited) & + fresh mem, types, vals in + st == StEnv (mem, types, vals) & { - { fresh tp, e, v, - mem_cp, v_cp, + { fresh tp, mem_bd, v_bd, mem_add, id_add, types', vals' in - d == VarD (tp, e) & - exprvalo mem vals e v & - 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) } | + d == VarD tp & + valbuildo mem tp (Pair.pair mem_bd v_bd) & + mem_addo mem_bd v_bd (Pair.pair mem_add id_add) & + types_addo types x tp types' & + vals_addo vals x id_add vals' & + st' == StEnv (mem_add, types', vals') } | { fresh tps, s, mem_add, id_add, types', vals' in d == FunD (tps, s) & - mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) & - types_glob_addo types x (FunT tps) types' & - vals_glob_addo vals x id_add vals' & - st' == StEnv (mem_add, types', vals', visited) + mem_addo mem FunV (Pair.pair mem_add id_add) & + types_addo types x (FunT tps) types' & + vals_addo vals x id_add vals' & + st' == StEnv (mem_add, types', vals') } } } @@ -948,11 +877,10 @@ struct let open StEnv in let open TypesEnv in let open ValsEnv in - let open VisitedEnv in ocanren { fresh m in empty_memo m & - st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv []) + st == StEnv (m, TypesEnv [], ValsEnv []) } (* TODO: better way ??? *) @@ -1058,9 +986,9 @@ struct v'' == UnitV (v_m''', v_r'', v_w'') & mem_with_v' == Std.pair mem v'' } } } | - { fresh ts, _stmts in + { fresh ts in tp == FunT ts & - v == FunV _stmts & + v == FunV & mem_with_v' == Std.pair mem v } | { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in tp == RefT (ctp', tp') & @@ -1086,10 +1014,10 @@ struct let open CopyCap in let open RevPath in ocanren { - fresh mem, types, vals, visited, + fresh mem, types, vals, x, id, b(* , tp' *), rp, mem_sp, b_sp, v_sp, mem_upd, v_upd in - st == StEnv (mem, types, vals, visited) & + st == StEnv (mem, types, vals) & pathvaro p x & vals_assoco x vals id & pathvalo mem vals p b & @@ -1101,11 +1029,11 @@ struct mem_seto mem_upd id v_upd mem' } - let rec argsspoile_foldero types vals visited m mem tp e mem' = + let rec argsspoile_foldero types vals m mem tp e mem' = let open StEnv in ocanren { fresh st in - st == StEnv (mem, types, vals, visited) & + st == StEnv (mem, types, vals) & argsspoileo st m tp e mem' } and argsspoileo st m tp e mem' = @@ -1114,8 +1042,8 @@ struct let open Type in let open Path in ocanren { - fresh _r, _w, mem, types, vals, visited in - st == StEnv (mem, types, vals, visited) & + fresh _r, _w, mem, types, vals in + st == StEnv (mem, types, vals) & { { e == UnitE & tp == UnitT (_r, _w) & @@ -1129,30 +1057,28 @@ struct { fresh es, tps in e == TupleE es & tp == TupleT tps & - list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'} + list_foldl2o (argsspoile_foldero types vals m) mem tps es mem'} } } (* - funciton argument addition *) - let addargo st oldvals x tp e st' = + let addargo st x tp st' = let open StEnv in ocanren { - fresh mem, types, vals, visited, v, - mem_cp, v_cp, + fresh mem, types, vals, + mem_bd, v_bd, mem_add, id_add, types', vals' in - st == StEnv (mem, types, vals, visited) & - exprvalo mem oldvals e v & - valcopyo mem v tp (Std.pair mem_cp v_cp) & - mem_addo mem_cp v_cp (Std.pair mem_add id_add) & + st == StEnv (mem, types, vals) & + valbuildo mem tp (Std.pair mem_bd v_bd) & + mem_addo mem_bd v_bd (Std.pair mem_add id_add) & types_addo types x tp types' & vals_addo vals x id_add vals' & - st' == StEnv (mem_add, types', vals', visited) + st' == StEnv (mem_add, types', vals') } - (* - function evaluation *) - (* NOTE: not needed due to performed optimization in stmt_eval ? *) + (* --- *) let writeval_to_capo v_w w' = let open WriteVal in @@ -1180,8 +1106,8 @@ struct } & writeval_to_capo v_w w } | - { fresh _stmts, _ts in - v == FunV _stmts & + { fresh _ts in + v == FunV & tp == FunT _ts } | { fresh id, _c, tp', v' in v == RefV id & @@ -1215,90 +1141,34 @@ struct (* - statement evaluation *) - let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren { - fresh st, x, m, tp, st' in - Std.pair st x == st_with_id & - Std.pair m tp == mtp & - addargo st vals x tp e st' & - st_with_id' == Std.pair st' (Nat.s x) - } - and f_tags_check_foldero mem vals x mtp x' = ocanren { - fresh m, tp, id', v' in - mtp == Std.pair m tp & - vals_assoco x vals id' & - mem_geto mem id' v' & - tags_checko mem v' tp & - x' == Nat.s x - } - and stmt_eval_func_foldero mem types vals tps visited stmt visited' = - let open StEnv in - ocanren { - { fresh visited_add, st, - st', mem', types', vals', - _x', visited'' in - not_visited_checko visited stmt & - visited_addo visited stmt visited_add & - st == StEnv (mem, types, vals, visited_add) & - stmt_evalo st stmt st' & - st' == StEnv (mem', types', vals', visited'') & - list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' & - visited' == visited'' - } | - { visited_checko visited stmt & - visited == visited' } - } - and stmt_eval_spoil_foldero types vals visited mem mtp e mem' = + let rec stmt_eval_spoil_foldero types vals mem mtp e mem' = let open StEnv in ocanren { fresh m, tp, st in Std.pair m tp == mtp & - st == StEnv (mem, types, vals, visited) & + st == StEnv (mem, types, vals) & argsspoileo st m tp e mem' } and stmt_evalo st s st' = let open StEnv in let open Stmt in - let open Value in let open Type in - (* let open WriteCap in *) - let open TypesEnv in - let open ValsEnv in let open RevPath in let open Action in ocanren { - fresh mem, types, vals, visited in - st == StEnv (mem, types, vals, visited) & + fresh mem, types, vals in + st == StEnv (mem, types, vals) & { { s == SkipS & st == st' } | - { fresh f, es, v, tp, - glob_tps, _tps, - glob_vs, _vs, - types_call, vals_call, - fstmts, tps, st_call, - state_with_args, - mem_swa, types_swa, - vals_swa, visited_swa, - _arg_id, mem_spoiled, - visited' in + { fresh f, es, tp, + _tps, _vs, tps, + mem_spoiled in s == CallS (f, es) & - pathvalo mem vals f v & pathtypeo types f tp & - types == TypesEnv (glob_tps, _tps) & - vals == ValsEnv (glob_vs, _vs) & - types_call == TypesEnv (glob_tps, glob_tps) & - vals_call == ValsEnv (glob_vs, glob_vs) & - v == FunV fstmts & tp == FunT tps & - st_call == StEnv (mem, types_call, vals_call, visited) & - list_foldl2o (stmt_addarg_foldero vals) - (Std.pair st_call 0) tps es - (Std.pair state_with_args _arg_id) & - state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) & - list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & - (* TODO: FIXME check left or right order *) - list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited') + list_foldl2o (stmt_eval_spoil_foldero types vals) mem tps es mem_spoiled & - st' == StEnv (mem_spoiled, types, vals, visited') + st' == StEnv (mem_spoiled, types, vals) } | { fresh p, tp, x, id, v, rp, mem_upd, v_upd, mem_set in @@ -1311,7 +1181,7 @@ struct pathrevo p VarRP rp & valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem_set & - st' == StEnv (mem_set, types, vals, visited) } | + st' == StEnv (mem_set, types, vals) } | { fresh p, _tp, _r, _w, x, id, v, rp, mem_upd, v_upd, mem_set in s == ReadS p & @@ -1321,7 +1191,7 @@ struct pathrevo p VarRP rp & valupdo mem v rp ReadA (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem_set & - st' == StEnv (mem_set, types, vals, visited) } | + st' == StEnv (mem_set, types, vals) } | (* { fresh p in *) (* s == ReadS p & *) (* pathvalo mem vals p ZeroV & *) @@ -1331,22 +1201,58 @@ struct stmt_evalo st sl stl & stmt_evalo stl sr st' } | { fresh sl, sr, stl, str, - meml, typesl, valsl, visitedl, - memr, typesr, valsr, visitedr, - visited', mem' in + meml, typesl, valsl, + memr, typesr, valsr, + mem' in s == ChoiceS (sl, sr) & stmt_evalo st sl stl & stmt_evalo st sr str & - stl == StEnv (meml, typesl, valsl, visitedl) & - str == StEnv (memr, typesr, valsr, visitedr) & + stl == StEnv (meml, typesl, valsl) & + str == StEnv (memr, typesr, valsr) & typesl == typesr & valsl == valsr & memcombo meml memr mem' & - visited_appendo visitedr visitedl visited' & - st' == StEnv (mem', typesl, valsl, visited') } + st' == StEnv (mem', typesl, valsl) } } } + (* - function evaluation *) + + let rec f_addarg_foldero st_with_id mtp st_with_id' = ocanren { + fresh st, x, m, tp, st' in + Std.pair st x == st_with_id & + Std.pair m tp == mtp & + addargo st x tp st' & + st_with_id' == Std.pair st' (Nat.s x) + } + and f_tags_check_foldero mem vals x mtp x' = ocanren { + fresh m, tp, id', v' in + mtp == Std.pair m tp & + vals_assoco x vals id' & + mem_geto mem id' v' & + tags_checko mem v' tp & + x' == Nat.s x + } + + (* list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & *) + and func_evalo st d = + let open StEnv in + let open Decl in + ocanren { + { fresh tps, stmt, + state_with_args, _arg_id, st_after_stmt, + mem_after_stmt, _types_after_stmt, vals_after_stmt, _x' in + d == FunD (tps, stmt) & + list_foldlo f_addarg_foldero + (Std.pair st 0) tps + (Std.pair state_with_args _arg_id) & + stmt_evalo state_with_args stmt st_after_stmt & + state_with_args == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) & + list_foldlo (f_tags_check_foldero mem_after_stmt vals_after_stmt) 0 tps _x' + } | + { fresh _tp in + d == VarD _tp } + } (* --- program execution --- *) let prog_evalo prog st' = @@ -1355,6 +1261,7 @@ struct fresh decls, s, init_st in prog == Prg (decls, s) & prog_inito prog init_st & + list_checko (func_evalo init_st) decls & stmt_evalo init_st s st' } end diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 5433e74..fe16bd6 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -5,19 +5,19 @@ open Relational (* - basic var tests *) let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); - [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []), VisitedEnv ([]))] |}] + [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([]), ValsEnv ([]))] |}] let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}] + [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] let%expect_test "simple var, forbidden read" = print_endline(prog_eval_t_simple_var_fbd_rd ()); [%expect {| [] |}] let%expect_test "simple vars, no read & read" = print_endline(prog_eval_t_simple_vars_fbd_rd_rd ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(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 (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}] + [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}] + [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] let%expect_test "simple var, forbidden write" = print_endline(prog_eval_t_simple_var_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_var_wr_rd ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}] + [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] (* - basic call tests *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 6f65938..24a39eb 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -67,7 +67,7 @@ let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg in globals_min_ido xg & - prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)], + prog == Prg ([VarD (UnitT (Rd, MayWr))], ReadS (VarP xg)) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -87,7 +87,7 @@ let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg in globals_min_ido xg & - prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + prog == Prg ([VarD (UnitT (NRd, MayWr))], ReadS (VarP xg)) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -97,8 +97,8 @@ let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q fresh prog, xg, yg in globals_min_ido xg & yg == Nat.s xg & - prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE); - VarD (UnitT (Rd, MayWr), UnitE)], + prog == Prg ([VarD (UnitT (NRd, MayWr)); + VarD (UnitT (Rd, MayWr))], ReadS (VarP yg)) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -107,7 +107,7 @@ let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg in globals_min_ido xg & - prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + prog == Prg ([VarD (UnitT (NRd, MayWr))], WriteS (VarP xg)) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -116,7 +116,7 @@ let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg in globals_min_ido xg & - prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)], + prog == Prg ([VarD (UnitT (NRd, NeverWr))], WriteS (VarP xg)) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -125,7 +125,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg in globals_min_ido xg & - prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + prog == Prg ([VarD (UnitT (NRd, MayWr))], SeqS (WriteS (VarP xg), ReadS (VarP xg))) & prog_evalo prog q }) @@ -139,7 +139,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q (* fresh prog, xg, fg, xd, fd in *) (* globals_min_ido xg & *) (* fg == Nat.s xg & *) - (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *) + (* xd == VarD (UnitT (Rd, NeverWr)) & *) (* fd == FunD ([], SkipS) & *) (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *) (* prog_evalo prog q }) *) @@ -150,7 +150,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q fresh prog, xg, fg, xd, fd in globals_min_ido xg & fg == Nat.s xg & - xd == VarD (UnitT (Rd, NeverWr), UnitE) & + xd == VarD (UnitT (Rd, NeverWr)) & fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) & prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) & prog_evalo prog q }) @@ -162,8 +162,8 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, NeverWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) & + xd == VarD (UnitT (Rd, NeverWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -176,8 +176,8 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (NRd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -190,8 +190,8 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, MayWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, MayWr)), RefE xg) & + xd == VarD (UnitT (NRd, MayWr)) & + yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], SeqS (WriteS (DerefP (VarP 0)), ReadS (DerefP (VarP 0)))) & @@ -205,8 +205,8 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, MayWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) & + xd == VarD (UnitT (Rd, MayWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -219,8 +219,8 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (NRd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -233,8 +233,8 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -248,8 +248,8 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (NRd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -265,8 +265,8 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q yg == Nat.s xg & fg == Nat.s yg & f2g == Nat.s fg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], @@ -283,8 +283,8 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & @@ -300,8 +300,8 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q yg == Nat.s xg & fg == Nat.s yg & f2g == Nat.s fg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))], @@ -318,8 +318,8 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], SeqS (WriteS (VarP xg), ReadS (DerefP (VarP 0)))) & @@ -337,10 +337,10 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q x2g == Nat.s yg & y2g == Nat.s x2g & fg == Nat.s y2g & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x2d == VarD (UnitT (Rd, AlwaysWr)) & + y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], SeqS (ReadS (DerefP (VarP 0)), @@ -375,14 +375,14 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q x4g == Nat.s y3g & y4g == Nat.s x4g & fg == Nat.s y4g & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) & - x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) & - x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x2d == VarD (UnitT (Rd, AlwaysWr)) & + y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x3d == VarD (UnitT (Rd, AlwaysWr)) & + y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x4d == VarD (UnitT (Rd, AlwaysWr)) & + y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 1)); ReadS (DerefP (VarP 3)); WriteS (DerefP (VarP 1)); @@ -434,14 +434,14 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q x4g == Nat.s y3g & y4g == Nat.s x4g & fg == Nat.s y4g & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) & - x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) & - x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) & - y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x2d == VarD (UnitT (Rd, AlwaysWr)) & + y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x3d == VarD (UnitT (Rd, AlwaysWr)) & + y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + x4d == VarD (UnitT (Rd, AlwaysWr)) & + y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 1)); ReadS (DerefP (VarP 3)); WriteS (DerefP (VarP 2)); @@ -477,8 +477,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -492,8 +492,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (r globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & @@ -506,8 +506,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -522,8 +522,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + xd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -561,14 +561,14 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q 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) & + xbd == VarD (UnitT (Rd, AlwaysWr)) & + xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + ybd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + zbd == VarD (UnitT (Rd, AlwaysWr)) & + zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + kbd == VarD (UnitT (Rd, AlwaysWr)) & + kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 0)); WriteS (DerefP (VarP 0)); ReadS (DerefP (VarP 1))] fstmts & @@ -635,14 +635,14 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r 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) & + xbd == VarD (UnitT (Rd, AlwaysWr)) & + xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + ybd == VarD (UnitT (Rd, AlwaysWr)) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + zbd == VarD (UnitT (Rd, AlwaysWr)) & + zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & + kbd == VarD (UnitT (Rd, AlwaysWr)) & + kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 0)); WriteS (DerefP (VarP 0)); ReadS (DerefP (VarP 1))] fstmts & @@ -828,10 +828,10 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q ReadS time_gp ] stmts & prog == Prg ([ - VarD (userT, userE); - VarD (dataT, dataE); - VarD (timeT, timeE); - VarD (requestT, requestE); + VarD userT; + VarD dataT; + VarD timeT; + VarD requestT; sendD ], stmts @@ -898,10 +898,10 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( ReadS time_gp ] stmts & prog == Prg ([ - VarD (userT, userE); - VarD (dataT, dataE); - VarD (timeT, timeE); - VarD (requestT, requestE); + VarD userT; + VarD dataT; + VarD timeT; + VarD requestT; sendD ], stmts @@ -1041,13 +1041,13 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q 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); + VarD user_utilsT; + VarD user_infoT; + VarD userT; + VarD versionT; + VarD utilsT; + VarD uT_r_aw; (* data *) + VarD requestT; FunD ([moded_requestT], get_version_idF); FunD ([moded_requestT], updated_versionF); FunD ([moded_requestT], sendF); @@ -1336,13 +1336,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run 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); + VarD user_utilsT; + VarD user_infoT; + VarD userT; + VarD versionT; + VarD utilsT; + VarD uT_r_aw; (* data *) + VarD requestT; (* FunD ([mrT'], get_version_idF); *) (* FunD ([mrT'], updated_versionF); *) (* FunD ([mrT'], sendF); *) From 31111947147d602b63830235a5016dd7a2f3b84f Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 20 May 2026 16:13:53 +0000 Subject: [PATCH 10/10] struct: synthesiszer fix, tests fix --- model_with_structures/synthesizer.ml | 2 +- model_with_structures/tests.ml | 30 ++++++++++++++-------------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 8987412..9c72142 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -1247,7 +1247,7 @@ struct (Std.pair st 0) tps (Std.pair state_with_args _arg_id) & stmt_evalo state_with_args stmt st_after_stmt & - state_with_args == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) & + st_after_stmt == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) & list_foldlo (f_tags_check_foldero mem_after_stmt vals_after_stmt) 0 tps _x' } | { fresh _tp in diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index fe16bd6..caecfe9 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -22,49 +22,49 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va (* - basic call tests *) let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ()); - [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(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 (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([ReadS (VarP (O))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; UnitV (ZeroMV, OneRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ()); - [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, NeverWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, NeverWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(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 (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 ([ReadS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, NeverWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple call with write" = print_endline(prog_eval_t_simple_call_wr ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (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 ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple call with read after write" = print_endline(prog_eval_t_simple_call_wr_rd ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(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 (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))), ReadS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (BotMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (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 ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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)]))] |}] let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (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 ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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)]))] |}] let%expect_test "call inside call" = print_endline(prog_eval_t_call_in_call ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), 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 (O))))))))))))), 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 ([WriteS (DerefP (VarP (O))); SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), 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)]))] |}] let%expect_test "call inside call, recursive" = print_endline(prog_eval_t_call_in_call_rec ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, 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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, 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 (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 (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 (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, 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 (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)]))] |}] let%expect_test "call to fix after call" = print_endline(prog_eval_t_fix_call_after_call ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), 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 (O))))))))))))), 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 ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), 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)]))] |}] let%expect_test "simple call with global variable usage" = print_endline(prog_eval_t_call_with_glob_usage ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (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 (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 (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 (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (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 (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)]))] |}] let%expect_test "simple call with read & write (2 args)" = print_endline(prog_eval_t_call_with_rd_wr_2_args ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (S (S (O))))); UnitV (BotMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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), 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 (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 (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 (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (O))))); UnitV (BotMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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), 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 (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)]))] |}] 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 (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); 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 (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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 (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 (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 (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 (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; RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); 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 (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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 (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 (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)]))] |}] 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 (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); 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 (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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 (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 (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 (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 (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; RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); 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 (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], 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 (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 (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)]))] |}] (* - basic synthesis tests *) @@ -83,13 +83,13 @@ let%expect_test "simple synthesis test, reference forbidden write, no read write (* - 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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; FunV; FunV; 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))]), 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)]))] |}] 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 (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (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, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); 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, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); 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 (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; 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, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); 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)]))] |}] let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog_synt_t_presentation_complex_tp ()); [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}]