From 10cea0133871a572ccec41b298ef0557d9e6a367 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 14:35:21 +0000 Subject: [PATCH 1/6] struct: synt. tests fixes, simple forward tests done --- model_with_structures/tests.ml | 21 +++++++++++++++++++++ model_with_structures/tests_f.ml | 22 ++++++++++++---------- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 416a361..e2ec909 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -42,6 +42,27 @@ let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simp 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 (O); ZeroV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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 "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 (O); ZeroV], 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 (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + +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 (O); ZeroV], 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 (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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + +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 (O); ZeroV], 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, 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 (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 (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 (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 "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 (O); ZeroV; RefV (O); BotV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + +(* TODO: dif. ref modifiers tests ? *) + +(* TODO: synthesis tests ? *) + (* type tests *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) (* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index ad1e3b8..889e146 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -227,9 +227,9 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], - SeqS (CallS (VarP f2g, [PathE (VarP 0)]), + SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), + prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -243,13 +243,13 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q f2g == Nat.s fg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), 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 (Rd, AlwaysWr)))], + f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - SeqS (CallS (VarP f2g, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg))))) & + prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + SeqS (CallS (VarP f2g, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg))))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) @@ -261,7 +261,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q fg == Nat.s yg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], SeqS (WriteS (VarP xg), ReadS (DerefP (VarP 0)))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -270,7 +270,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q }) (fun q -> q#reify (StEnv.prj_exn)))) -let prog_eval_t_call_with_rd_wr_2_args_ = show(answer) (Stream.take (run q +let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd, st in globals_min_ido xg & @@ -286,7 +286,9 @@ let prog_eval_t_call_with_rd_wr_2_args_ = show(answer) (Stream.take (run q (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], SeqS (ReadS (DerefP (VarP 0)), WriteS (DerefP (VarP 1)))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) & + prog == Prg ([xd; yd; x2d; y2d; fd], + CallS (VarP fg, [PathE (VarP yg); + PathE (VarP y2g)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) From a7711733641951c43a3d43bca4daf5fcb97481f4 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 15:22:11 +0000 Subject: [PATCH 2/6] struct: synt. argument modes tests --- model_with_structures/tests.ml | 8 +- model_with_structures/tests_f.ml | 156 ++++++++++++++++++++++++++++--- 2 files changed, 149 insertions(+), 15 deletions(-) diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index e2ec909..4d2fff9 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -57,7 +57,13 @@ let%expect_test "simple call with global variable usage" = print_endline(prog_ev [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (O); ZeroV], 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, 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 (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 (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 (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 "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 (O); ZeroV; RefV (O); BotV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (O))); BotV; RefV (O); ZeroV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + +let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ()); + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + +let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ()); + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] (* TODO: dif. ref modifiers tests ? *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 889e146..c4d53df 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -23,6 +23,19 @@ open Mode (* TODO *) +(* NOTE: redo with fold ?? *) +let rec seqo stmts stmt' = ocanren { + { stmts == [] & stmt' == SkipS } | + { fresh s in + stmts == [s] & + stmt' == s } | + { fresh s, s', ss, stmt_rest' in + stmts == s :: s' :: ss & + seqo (s' :: ss) stmt_rest' & + stmt' == SeqS(s, stmt_rest') + } + } + (* - basic var tests *) let prog_eval_t_empty _ = show(answer) (Stream.take (run q @@ -104,7 +117,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, fg, xd, fd, st in + fresh prog, xg, fg, xd, fd in globals_min_ido xg & fg == Nat.s xg & xd == VarD (UnitT (Rd, NeverWr), UnitE) & @@ -115,7 +128,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -129,7 +142,7 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -143,7 +156,7 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -158,7 +171,7 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -172,7 +185,7 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -186,7 +199,7 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -201,7 +214,7 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -217,7 +230,7 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in + fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -236,7 +249,7 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in + fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -255,7 +268,7 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd, st in + fresh prog, xg, yg, fg, xd, yd, fd in globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & @@ -272,7 +285,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd, st in + fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd in globals_min_ido xg & yg == Nat.s xg & x2g == Nat.s yg & @@ -281,7 +294,7 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q 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 xg) & + y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], SeqS (ReadS (DerefP (VarP 0)), @@ -293,7 +306,122 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q }) (fun q -> q#reify (StEnv.prj_exn)))) -(* TODO: add tests to test file *) +let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, + x2g, y2g, + x3g, y3g, + x4g, y4g, + fg, + xd, yd, + x2d, y2d, + x3d, y3d, + x4d, y4d, + fd, + fstmts, + stmts in + globals_min_ido xg & + yg == Nat.s xg & + x2g == Nat.s yg & + y2g == Nat.s x2g & + x3g == Nat.s y2g & + y3g == Nat.s x3g & + 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) & + seqo [ReadS (DerefP (VarP 1)); + ReadS (DerefP (VarP 3)); + WriteS (DerefP (VarP 1)); + WriteS (DerefP (VarP 2)); + WriteS (DerefP (VarP 3))] fstmts & + fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr))); + (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); + (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); + (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))], + fstmts) & + seqo [CallS (VarP fg, [PathE (VarP yg); + PathE (VarP y2g); + PathE (VarP y3g); + PathE (VarP y4g)]); + ReadS (DerefP (VarP yg)); + ReadS (DerefP (VarP y2g)); + ReadS (DerefP (VarP y3g)); + ReadS (DerefP (VarP y4g))] stmts & + prog == Prg ([xd; yd; + x2d; y2d; + x3d; y3d; + x4d; y4d; + fd], + stmts) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, + x2g, y2g, + x3g, y3g, + x4g, y4g, + fg, + xd, yd, + x2d, y2d, + x3d, y3d, + x4d, y4d, + fd, + fstmts, + stmts in + globals_min_ido xg & + yg == Nat.s xg & + x2g == Nat.s yg & + y2g == Nat.s x2g & + x3g == Nat.s y2g & + y3g == Nat.s x3g & + 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) & + seqo [ReadS (DerefP (VarP 1)); + ReadS (DerefP (VarP 3)); + WriteS (DerefP (VarP 2)); + WriteS (DerefP (VarP 3))] fstmts & + fd == FunD ([(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)))], + fstmts) & + seqo [CallS (VarP fg, [PathE (VarP yg); + PathE (VarP y2g); + PathE (VarP y3g); + PathE (VarP y4g)]); + ReadS (DerefP (VarP yg)); + ReadS (DerefP (VarP y2g)); + ReadS (DerefP (VarP y3g)); + ReadS (DerefP (VarP y4g))] stmts & + prog == Prg ([xd; yd; + x2d; y2d; + x3d; y3d; + x4d; y4d; + fd], + stmts) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) (* @type answerArgs = (Arg.ground List.ground) GT.list with show *) (* @type answerValue = Value.ground GT.list with show *) From e79b7fa7bc45a003244e692085cac29a1382f539 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 15:48:28 +0000 Subject: [PATCH 3/6] struct: synthesizer simple synthesis tests --- model_with_structures/tests.ml | 68 +---- model_with_structures/tests_f.ml | 451 ++++--------------------------- 2 files changed, 70 insertions(+), 449 deletions(-) diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 4d2fff9..2f947e2 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -42,8 +42,6 @@ let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simp 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 (O); ZeroV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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)]))] |}] @@ -65,64 +63,18 @@ let%expect_test "simple call with different arguments modifiers, copy" = print_e let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ()); [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] -(* TODO: dif. ref modifiers tests ? *) +(* - basic synthesis tests *) -(* TODO: synthesis tests ? *) +let%expect_test "simple synthesis test" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr ()); + [%expect {| [Rf; Cp] |}] -(* type tests *) -(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) -(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *) -(* let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}] *) -(* let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *) -(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}] *) -(* let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}] *) -(* let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}] *) -(* let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *) +let%expect_test "simple synthesis test, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr' ()); + [%expect {| [Rf; Rf; Rf; Rf; Cp; Cp; Cp; Cp] |}] -(* function tests *) -(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *) -(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *) -(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] *) -(* let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] *) -(* let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] *) -(* let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] *) -(* let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *) -(* let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *) -(* let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *) -(* let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] *) -(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] *) -(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] *) -(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] *) -(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *) -(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *) -(* let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *) -(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *) -(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}] *) -(* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *) -(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *) -(* let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] *) -(* let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] *) -(* let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *) -(* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *) -(* let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] *) -(* let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] *) -(* let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] *) -(* let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] *) -(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *) -(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] *) -(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] *) -(* let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] *) -(* let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] *) -(* let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] *) -(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *) -(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *) -(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *) -(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *) -(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] *) -(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] *) -(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] *) -(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] *) -(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *) +let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ()); + [%expect {| [Cp] |}] -(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *) +let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ()); + [%expect {| [Cp; Cp; Cp; Cp] |}] +(* TODO *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index c4d53df..5307742 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -17,9 +17,10 @@ open InCap open OutCap open Mode -@type answer = StEnv.ground GT.list with show +@type answer = StEnv.ground GT.list with show +@type answerCpCap = CopyCap.ground GT.list with show - (* - shortcuts *) +(* - shortcuts *) (* TODO *) @@ -423,387 +424,67 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q }) (fun q -> q#reify (StEnv.prj_exn)))) -(* @type answerArgs = (Arg.ground List.ground) GT.list with show *) -(* @type answerValue = Value.ground GT.list with show *) -(* @type answerNat = Nat.ground GT.list with show *) -(* @type answerNats = (Nat.ground List.ground) GT.list with show *) -(* @type answerTag = Tag.ground GT.list with show *) -(* @type answerTags = (Tag.ground List.ground) GT.list with show *) -(* @type answerCopyCap = CopyCap.ground GT.list with show *) -(* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *) +(* - basic synthesis tests *) -(* let inv_id_t _ = show(answerNat) (Stream.take (run q *) - (* (fun q -> ocanren { inv_ido 2 1 q }) *) - (* (fun q -> q#reify Nat.prj_exn))) *) +let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, st in + 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) & + fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))], + WriteS (DerefP (VarP 0))) & + prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog_evalo prog st }) + (fun q -> q#reify (CopyCap.prj_exn)))) -(* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *) - (* (fun q -> ocanren { inv_ido 2 0 q }) *) - (* (fun q -> q#reify Nat.prj_exn))) *) +let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, + st, rd_cap, wr_cap in + 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) & + 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)])) & + prog_evalo prog st }) + (fun q -> q#reify (CopyCap.prj_exn)))) -(* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *) - (* (fun q -> ocanren { inv_ido 2 q 0 }) *) - (* (fun q -> q#reify Nat.prj_exn))) *) +let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, st in + 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) & + fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))], + WriteS (DerefP (VarP 0))) & + prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & + prog_evalo prog st }) + (fun q -> q#reify (CopyCap.prj_exn)))) -(* let list_drop_t _ = show(answerNats) (Stream.take (run q *) - (* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *) - (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *) - -(* let list_replace_t _ = show(answerNats) (Stream.take (run q *) - (* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *) - (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *) - -(* let arg_to_value_t _ = show(answerValue) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* ocanren { *) - (* fresh s in *) - (* empty_stateo s & *) - (* arg_to_valueo s RValue q }) *) - (* (fun q -> q#reify (Value.prj_exn)))) *) - -(* let st_add_arg_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* ocanren { *) - (* fresh s, s', cnt in *) - (* empty_stateo s & *) - (* empty_stateo s' & *) - (* st_add_argo s s' Nat.o rwi_val RValue q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let write_eval_t1 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* stmt == Write 0 & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let write_eval_t2 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* stmt == Write 1 & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let writes_eval_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmts in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* stmts == [Write 0; Write 1] & *) - (* eval_bodyo s p stmts q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let call_eval_t1 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *) - (* p == [FunDecl ([wi_ref], [Write 0])] & *) - (* stmt == Call (0, [0]) & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let call_eval_t2 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *) - (* p == [FunDecl ([wi_ref], [Write 0])] & *) - (* stmt == Call (0, [0]) & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let call_eval_t3 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *) - (* p == [FunDecl ([wi_ref], [Write 0])] & *) - (* stmt == Call (0, [1]) & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let call_eval_t4 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* stmt == Call (0, [0; 1]) & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let call_eval_t5 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* let open Stmt in *) - (* let open FunDecl in *) - (* ocanren { *) - (* fresh s, p, stmt in *) - (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* stmt == Call (0, [1; 0]) & *) - (* eval_stmto s p stmt q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let mem_set_t1 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* ocanren { *) - (* fresh s in *) - (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) & *) - (* mem_seto s 0 Unit q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let mem_set_t2 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* ocanren { *) - (* fresh s in *) - (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *) - (* mem_seto s 0 Bot q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let meem_set_t3 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* let open Value in *) - (* let open St in *) - (* ocanren { *) - (* fresh s in *) - (* s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) & *) - (* mem_seto s 0 Bot q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let add_arg_folder_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* ocanren { *) - (* fresh s, s', cnt in *) - (* empty_stateo s & *) - (* empty_stateo s' & *) - (* add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* let foldl2_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Arg in *) - (* let open Tag in *) - (* ocanren { *) - (* fresh s, s', cnt, arg_tags, args in *) - (* arg_tags == [rwi_val] & *) - (* args == [RValue] & *) - (* empty_stateo s & *) - (* empty_stateo s' & *) - (* list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - - -(* let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q *) - (* (fun q -> let open Arg in *) - (* ocanren {fresh v in List.mapo arg_to_rvalueo v q}) *) - (* (fun q -> q#reify (List.prj_exn Arg.prj_exn)))) *) - -(* empty state test *) -(* let empty_state_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> ocanren {empty_stateo q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t1 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [] & *) - (* d == FunDecl ([], []) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t2 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [] & *) - (* d == FunDecl ([wi_val], [Write 0; Read 0]) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t3 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [FunDecl ([wi_ref], [Write 0])] & *) - (* d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t4 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [FunDecl ([wi_ref], [Write 0])] & *) - (* d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t5 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *) - (* d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* fun eval test *) -(* let fun_eval_t6 _ = show(answer) (Stream.take (run q *) - (* (fun q -> (* let open Prog in *) *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren { fresh s, p, d in *) - (* empty_stateo s & *) - (* p == [FunDecl ([wi_val], [Write 0])] & *) - (* d == FunDecl ([wi_val], [Call (0, [0])]) & *) - (* eval_fun_empty_argso s p d q }) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog eval test *) -(* let prog_eval_t1 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog with func eval test *) -(* let prog_eval_t2 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])], *) - (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog with func eval test *) -(* let prog_eval_t3 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])], *) - (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog with func eval test *) -(* let prog_eval_t4 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog with func eval test *) -(* let prog_eval_t5 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* prog with func eval test *) -(* let prog_eval_t6 _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - -(* annotation gen prog test *) -(* let synt_t1 _ = show(answerTag) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {i_any q & *) - (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) *) - (* (fun q -> q#reify (Tag.prj_exn)))) *) +let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, + st, rd_cap, wr_cap in + 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) & + 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)]), + ReadS (DerefP (VarP yg)))) & + prog_evalo prog st }) + (fun q -> q#reify (CopyCap.prj_exn)))) (* annotation gen prog test *) (* let synt_t2 _ = show(answerTag) (Stream.take (run q *) @@ -913,15 +594,3 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *) (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *) (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *) - -(* TODO: FIXME: implement memoization cuts *) -(* prog with recursive function call *) -(* let rec_eval_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) - From 1a61fb01ee2e8f53dc07a6467d6e7151acb122da Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 15:49:07 +0000 Subject: [PATCH 4/6] struct: remove commented tests from prev iteration --- model_with_structures/tests.ml | 2 - model_with_structures/tests_f.ml | 109 ------------------------------- 2 files changed, 111 deletions(-) diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 2f947e2..232daef 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -76,5 +76,3 @@ let%expect_test "simple synthesis test, reference forbidden write" = print_endli let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ()); [%expect {| [Cp; Cp; Cp; Cp] |}] - -(* TODO *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 5307742..80e009c 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -485,112 +485,3 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak ReadS (DerefP (VarP yg)))) & prog_evalo prog st }) (fun q -> q#reify (CopyCap.prj_exn)))) - -(* annotation gen prog test *) -(* let synt_t2 _ = show(answerTag) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {i_any q & is_not_reado q & *) - (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *) - (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *) - (* (fun q -> q#reify (Tag.prj_exn)))) *) - -(* annotation gen prog test *) -(* let synt_t3 _ = show(answerTags) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & *) - (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *) - (* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *) - -(* annotation gen prog test *) -(* let synt_t4 _ = show(answerTags) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {i_any q & is_not_reado q & *) - (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *) - (* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *) - -(* annotation gen prog test *) -(* let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {fresh q', r' in *) - (* i_any q' & is_not_reado q' & *) - (* i_any r' & is_not_reado r' & is_never_writeo r' & *) - (* eq_copyo q' q & eq_copyo r' r & *) - (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *) - -(* annotation gen prog test *) -(* let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {fresh q', r' in *) - (* i_any q' & is_not_reado q' & *) - (* i_any r' & is_not_reado r' & is_never_writeo r' & *) - (* eq_copyo q' q & eq_copyo r' r & *) - (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *) - -(* annotation gen prog test *) -(* let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {fresh q', r' in *) - (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *) - (* eq_copyo q' q & eq_copyo r' r & *) - (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *) - -(* annotation gen prog test *) -(* let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {fresh q', r' in *) - (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *) - (* eq_copyo q' q & eq_copyo r' r & *) - (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *) - -(* annotation gen prog test *) -(* let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr *) - (* (fun q r -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* let open St in *) - (* ocanren {fresh q', r' in *) - (* i_any q' & is_not_reado q' & *) - (* i_any r' & is_reado r' & is_never_writeo r' & *) - (* eq_copyo q' q & eq_copyo r' r & *) - (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *) - (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *) - (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *) From 810b655ba81ca4843e81d491f01e385e16e82aed Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 16:34:47 +0000 Subject: [PATCH 5/6] struct: analyzer memoization (store list of stmts for now) --- model_with_structures/analyzer.ml | 76 +++++++++++++++++++++---------- 1 file changed, 51 insertions(+), 25 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 039f8e5..bf190f4 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -80,7 +80,8 @@ 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 state = mem * types * vals + type visited = stmt list (* TODO: FIXME: optimize, use ids *) + type state = mem * types * vals * visited (* --- *) @@ -253,16 +254,16 @@ struct (* TODO: check new in vars *) let add_decl (state : state) (x : data) (d : decl) : state = - match state with (mem, types, vals) -> match d with + 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) + (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) + (mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited) 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 @@ -321,7 +322,7 @@ struct (* full spoil *) let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = - match state with (mem, types, vals) -> + match state with (mem, types, vals, visited) -> 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 *) @@ -332,25 +333,25 @@ struct mem_set mem'' id v'' let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = - match state with (mem, types, vals) -> match e, t with + match state with (mem, types, vals, visited) -> 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) m t' e') + (fun mem' t' e' -> argsspoile (mem', types, vals, visited) 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) -> + 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) + (mem'', types_add types x t, vals_add vals x id, visited) (* - function evaluation *) (* NOTE: not needed due to performed optimization in stmt_eval *) @@ -359,8 +360,7 @@ struct (* - statement evaluation *) let rec stmt_eval (state : state) (s : stmt) : state = - match state with (mem, types, vals) -> match s with - (* TODO: FIXME: Add memoization *) + match state with (mem, types, vals, visited) -> match s with | SkipS -> state | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in @@ -370,19 +370,26 @@ struct let vals' : vals = (fst vals, fst vals) in (match v, t with | FunV (* xs, *) fstmts (* ) *), FunT ts -> - (* TODO: memoisation of the called functions *) 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'), 0) ts es in + ((mem, types', vals', visited), 0) ts es in (* NOTE: same x's, so can use same args for all the statements *) - let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) - List.map (stmt_eval state_with_args) 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) m t e) - mem ts es in - (mem_spoiled, types, vals) + (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 + (_, _, _, visited_after_stmt) -> 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) + mem ts es in + (mem_spoiled, types, vals, visited_new)) | FunV _, _ -> raise @@ Eval_error "call: function type" | _, FunT _ -> raise @@ Eval_error "call: function val" | _, _ -> raise @@ Eval_error "call: function type & val") @@ -393,7 +400,7 @@ struct else let x = pathvar p in let id = vals_assoc x vals in let (mem', v') = valupd mem (mem_get mem id) p ZeroV in - (mem_set mem' id v', types, vals) + (mem_set mem' id v', types, vals, visited) | _ -> raise @@ Eval_error "write: type") | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV then raise @@ Eval_error "read: spoiled value" @@ -404,11 +411,12 @@ 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) -> - match stater with (memr, typesr, valsr) -> + match statel with (meml, typesl, valsl, visitedl) -> + match stater with (memr, typesr, valsr, visitedr) -> if typesl != typesr || valsl != valsr then raise @@ Eval_error "choice" - else (memcomb meml memr, typesl, valsl) + (* TODO: FIXME: better list union ?? *) + else (memcomb meml memr, typesl, valsl, visitedl @ visitedr) (* --- program execution --- *) @@ -710,6 +718,24 @@ struct Printf.printf "done!"; [%expect {| done! |}] + (* NOTE: memoization used *) + let%expect_test "call inside call, recursive, dsl" = + prog_eval_noret ( + [ + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg0E; + FunD ( + [moded @@ cpT @@ uT_aw], + (callS vg2 [pE v0]) #. + (wrS @@ drf @@ v0) + ) + ], + (callS vg2 [pE vg1]) #. + (rdS @@ drf @@ vg1) + ); + Printf.printf "done!"; + [%expect {| done! |}] + let%expect_test "call to fix after call, dsl" = prog_eval_noret ( [ From 64935b3c7e65c6c198fae814245ac77c328d61f4 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 9 May 2026 17:29:54 +0000 Subject: [PATCH 6/6] struct: synt. memoization (+ rec function test), fixes --- model_with_structures/synthesizer.ml | 245 +++++++++++++++++---------- model_with_structures/tests.ml | 37 ++-- model_with_structures/tests_f.ml | 16 ++ 3 files changed, 193 insertions(+), 105 deletions(-) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index e34ddc2..c26b2b7 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -203,69 +203,26 @@ struct ] 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) t = StEnv of 'mem * 'types * 'vals + type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t + type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t ] end (* --- *) - (* - state utils *) - - let types_assoco id types tp = - let open TypesEnv in - ocanren { - fresh _glob_tps, tps in - types == TypesEnv (_glob_tps, 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) & - 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) - } - - 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) - } - (* - utils *) let rec list_replaceo xs id value ys = ocanren { @@ -293,6 +250,13 @@ struct list_ntho xs' id' x' } } + let rec list_not_membero xs x = ocanren { + xs == [] | + { fresh x', xs' in + xs == x' :: xs' & + x' =/= x & + list_not_membero xs' x } + } let rec list_foldro f acc xs acc' = ocanren { xs == [] & acc' == acc | @@ -368,6 +332,92 @@ struct { xs == [] & ys == [] & zs == [] } } + (* - state utils *) + + let types_assoco id types tp = + let open TypesEnv in + ocanren { + fresh _glob_tps, tps in + types == TypesEnv (_glob_tps, 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) & + 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) + } + + 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) + } + + 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 = @@ -611,8 +661,8 @@ struct let open Value in let open Type in ocanren { - fresh mem, types, vals in - st == StEnv (mem, types, vals) & + fresh mem, types, vals, visited in + st == StEnv (mem, types, vals, visited) & { { fresh tp, e, v, mem_cp, v_cp, @@ -624,7 +674,7 @@ struct mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & types_glob_addo types x tp types' & vals_glob_addo vals x id_add vals' & - st' == StEnv (mem_add, types', vals') } | + st' == StEnv (mem_add, types', vals', visited) } | { fresh tps, s, mem_add, id_add, types', vals' in @@ -632,7 +682,7 @@ struct 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') + st' == StEnv (mem_add, types', vals', visited) } } } @@ -645,10 +695,11 @@ 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 ([], [])) + st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv []) } (* TODO: better way ??? *) @@ -757,9 +808,10 @@ struct let open StEnv in let open CopyCap in ocanren { - fresh mem, types, vals, x, id, b, tp', + fresh mem, types, vals, visited, + x, id, b, tp', mem_sp, b_sp, v_sp, mem_upd, v_upd in - st == StEnv (mem, types, vals) & + st == StEnv (mem, types, vals, visited) & pathvaro p x & vals_assoco x vals id & pathvalo mem vals p b & @@ -770,11 +822,11 @@ struct mem_seto mem_upd id v_upd mem' } - let rec argspoile_foldero types vals m mem tp e mem' = + let rec argspoile_foldero types vals visited m mem tp e mem' = let open StEnv in ocanren { fresh st in - st == StEnv (mem, types, vals) & + st == StEnv (mem, types, vals, visited) & argspoileo st m tp e mem' } and argspoileo st m tp e mem' = @@ -783,8 +835,8 @@ struct let open Type in let open Path in ocanren { - fresh _r, _w, mem, types, vals in - st == StEnv (mem, types, vals) & + fresh _r, _w, mem, types, vals, visited in + st == StEnv (mem, types, vals, visited) & { { e == UnitE & tp == UnitT (_r, _w) & @@ -798,7 +850,7 @@ struct { fresh es, tps in e == TupleE es & tp == TupleT tps & - list_foldl2o (argspoile_foldero types vals m) mem tps es mem'} + list_foldl2o (argspoile_foldero types vals visited m) mem tps es mem'} } } @@ -807,17 +859,17 @@ struct let addargo st oldvals x tp e st' = let open StEnv in ocanren { - fresh mem, types, vals, v, + fresh mem, types, vals, visited, v, mem_cp, v_cp, mem_add, id_add, types', vals' in - st == StEnv (mem, types, vals) & + 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) & types_addo types x tp types' & vals_addo vals x id_add vals' & - st' == StEnv (mem_add, types', vals') + st' == StEnv (mem_add, types', vals', visited) } (* - function evaluation *) @@ -833,12 +885,25 @@ struct addargo st vals x tp e st' & st_with_id' == Std.pair st' (Nat.s x) } - and stmt_eval_spoil_foldero types vals mem mtp e mem' = + and stmt_eval_func_foldero mem types vals visited stmt visited' = + let open StEnv in + ocanren { + { fresh visited_add, st, + st', mem', types', vals' 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') } | + { visited_checko visited stmt & + visited == visited' } + } + and stmt_eval_spoil_foldero types vals visited mem mtp e mem' = let open StEnv in ocanren { fresh m, tp, st in Std.pair m tp == mtp & - st == StEnv (mem, types, vals) & + st == StEnv (mem, types, vals, visited) & argspoileo st m tp e mem' } and stmt_evalo st s st' = @@ -850,8 +915,8 @@ struct let open TypesEnv in let open ValsEnv in ocanren { - fresh mem, types, vals in - st == StEnv (mem, types, vals) & + fresh mem, types, vals, visited in + st == StEnv (mem, types, vals, visited) & { { s == SkipS & st == st' } | { fresh f, es, v, tp, @@ -859,8 +924,11 @@ struct glob_vs, _vs, types_call, vals_call, fstmts, tps, st_call, - state_with_args, _arg_id, - _states_evaled, mem_spoiled in + state_with_args, + mem_swa, types_swa, + vals_swa, visited_swa, + _arg_id, mem_spoiled, + visited' in s == CallS (f, es) & pathvalo mem vals f v & pathtypeo types f tp & @@ -870,16 +938,16 @@ struct vals_call == ValsEnv (glob_vs, glob_vs) & v == FunV fstmts & tp == FunT tps & - st_call == StEnv (mem, types_call, vals_call) & + 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) & - List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & + state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) & + list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' & (* TODO: FIXME check left or right order *) - list_foldl2o (stmt_eval_spoil_foldero types vals) - mem tps es mem_spoiled & - (* st' == state_with_args *) - st' == StEnv (mem_spoiled, types, vals) + list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited') + mem tps es mem_spoiled & + st' == StEnv (mem_spoiled, types, vals, visited') } | { fresh p, tp, _r, w, x, id, v, mem_upd, v_upd, mem_set in @@ -892,7 +960,7 @@ struct mem_geto mem id v & valupdo mem v p ZeroV (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem_set & - st' == StEnv (mem_set, types, vals) } | + st' == StEnv (mem_set, types, vals, visited) } | { fresh p in s == ReadS p & pathvalo mem vals p ZeroV & @@ -902,18 +970,19 @@ struct stmt_evalo st sl stl & stmt_evalo stl sr st' } | { fresh sl, sr, stl, str, - meml, typesl, valsl, - memr, typesr, valsr, - mem' in + meml, typesl, valsl, visitedl, + memr, typesr, valsr, visitedr, + visited', mem' in s == ChoiceS (sl, sr) & stmt_evalo st sl stl & stmt_evalo st sr str & - str == StEnv (memr, typesr, valsr) & - stl == StEnv (meml, typesl, valsl) & + stl == StEnv (meml, typesl, valsl, visitedl) & + str == StEnv (memr, typesr, valsr, visitedr) & typesl == typesr & valsl == valsr & memcombo meml memr mem' & - st' == StEnv (mem', typesl, valsl) } + visited_appendo visitedr visitedl visited' & + st' == StEnv (mem', typesl, valsl, visited') } } } diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 232daef..85ff5ad 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -5,63 +5,66 @@ open Relational (* - basic var tests *) let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); - [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}] + [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []), VisitedEnv ([]))] |}] let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ()); - [%expect {| [StEnv (MemEnv ([ZeroV], 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)]))] |}] + [%expect {| [StEnv (MemEnv ([ZeroV], 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 ([]))] |}] 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 ([ZeroV; BotV], 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)]))] |}] + [%expect {| [StEnv (MemEnv ([ZeroV; BotV], 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 ([]))] |}] let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ()); - [%expect {| [StEnv (MemEnv ([ZeroV], 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)]))] |}] + [%expect {| [StEnv (MemEnv ([ZeroV], 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 ([]))] |}] 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 ([ZeroV], 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)]))] |}] + [%expect {| [StEnv (MemEnv ([ZeroV], 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 ([]))] |}] (* - 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))]); ZeroV], 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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); ZeroV], 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))]))] |}] 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 (O); ZeroV], 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, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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 (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 ([ReadS (DerefP (VarP (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 (O); ZeroV], 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, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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 (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 ([WriteS (DerefP (VarP (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 (O); BotV], 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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (O); BotV], 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 (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 (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 (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (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 (O); BotV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); BotV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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 ([WriteS (DerefP (VarP (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 (O); ZeroV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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 (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 (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (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 (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 ([WriteS (DerefP (VarP (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 (O); ZeroV], 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 (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%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 (O); ZeroV], 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 (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, 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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([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))))]))] |}] + +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 (O); ZeroV], 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, 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 (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 (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 (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 (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (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 (O); ZeroV], 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 (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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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 (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 (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (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 (O); ZeroV], 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, 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 (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 (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 (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (O); ZeroV], 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, 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 (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 (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 (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 (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (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 (O))); BotV; RefV (O); ZeroV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (O))); BotV; RefV (O); ZeroV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}] let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]))] |}] let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]))] |}] (* - basic synthesis tests *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 80e009c..1452cf4 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -244,6 +244,22 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd in + 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) & + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], + SeqS (CallS (VarP fg, [PathE (VarP 0)]), + WriteS (DerefP (VarP 0)))) & + prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn))))