From ae8e39c03a3790e4d1eac7fc8a1d5570b2090e66 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 16:01:42 +0000 Subject: [PATCH 1/6] index fix, more tests (including several params) --- lib/relational_semantic_interpreter_oc.ml | 153 +++++++++++++++++++++- 1 file changed, 149 insertions(+), 4 deletions(-) diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml index aa633cf..f50912b 100644 --- a/lib/relational_semantic_interpreter_oc.ml +++ b/lib/relational_semantic_interpreter_oc.ml @@ -204,7 +204,7 @@ struct state == St (env, mem, mem_len, assignments) & env_geto state id mem_id & inv_ido mem_len mem_id inv_mem_id & - list_replaceo mem mem_id value mem' & + list_replaceo mem inv_mem_id value mem' & assignments' == id :: assignments & state' == St (env, mem', mem_len, assignments') } @@ -385,7 +385,7 @@ struct decl == FunDecl (arg_tags, body) & state == St (env_before, mem_before, len_before, assignments_before) & state_clean == St (nil_env, mem_before, len_before, nil_assignments) & - list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & + list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *) eval_bodyo state_with_vars prog body state_evaled & st_spoil_assignmentso state_evaled state_spoiled & state_spoiled == St (_env, mem_spoiled, len, _assignments) & @@ -429,15 +429,29 @@ struct @type answer = St.ground GT.list with show @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 + + let _ = Printf.printf "inv id test: %s\n" @@ show(answerNat) (Stream.take (run q + (fun q -> ocanren { inv_ido 2 1 q }) + (fun q -> q#reify Nat.prj_exn))) + + let _ = Printf.printf "inv id test 2: %s\n" @@ show(answerNat) (Stream.take (run q + (fun q -> ocanren { inv_ido 2 0 q }) + (fun q -> q#reify Nat.prj_exn))) + + let _ = Printf.printf "inv id test 3: %s\n" @@ show(answerNat) (Stream.take (run q + (fun q -> ocanren { inv_ido 2 q 0 }) + (fun q -> q#reify Nat.prj_exn))) let _ = Printf.printf "list drop test: %s\n" @@ 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 _ = Printf.printf "list replace test: %s\n" @@ show(answerNats) (Stream.take (run q - (fun q -> ocanren { list_replaceo [1; 2; 3] 1 0 q }) + (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) let _ = Printf.printf "arg to value test: %s\n" @@ show(answerValue) (Stream.take (run q @@ -473,6 +487,36 @@ struct eval_stmto s p stmt q}) (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "call stmt eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref], [Write 0])] & + stmt == Call (0, [0]) & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + + let _ = Printf.printf "call stmt eval test 3: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref], [Write 0])] & + stmt == Call (0, [1]) & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "mem set test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Arg in let open Tag in @@ -480,10 +524,32 @@ struct let open St in ocanren { fresh s in - s == St ([Std.pair 0 0], [Unit], 1, []) & + s == St ([Std.pair 0 0], [Bot], 1, []) & mem_seto s 0 Unit q}) (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "mem set test 2: %s\n" @@ 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 0], [Unit], 1, []) & + mem_seto s 0 Bot q}) + (fun q -> q#reify (St.prj_exn)))) + + let _ = Printf.printf "mem set test 3: %s\n" @@ 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 1], [Unit; Unit], 2, []) & + mem_seto s 0 Bot q}) + (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "add arg folder test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Arg in let open Tag in @@ -556,6 +622,19 @@ struct eval_fun_empty_argso s p d q }) (fun q -> q#reify (St.prj_exn)))) + (* fun eval test *) + let _ = Printf.printf "fun eval test (wrong call 2): %s\n" @@ 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 ([Ref], [Write 0])] & + d == FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]) & + eval_fun_empty_argso s p d q }) + (fun q -> q#reify (St.prj_exn)))) + (* prog eval test *) let _ = Printf.printf "prog eval test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Prog in @@ -611,6 +690,72 @@ struct let open St in ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) (fun q -> q#reify (Tag.prj_exn)))) + + (* annotation gen prog test *) + let _ = Printf.printf "synt test 3: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + + (* TODO *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 4: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))}) + (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) + + (* TODO *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 5: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + + (* TODO *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 5' (swap call args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + + (* TODO *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 5'' (swap def args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([r; q], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + + (* TODO *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 6: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + end (* let eval_test () = *) From 77b8bdc2b9b6c459ab7e7d1f2a1d1dc862276804 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 17:32:55 +0000 Subject: [PATCH 2/6] more tests, foldr fix --- lib/relational_semantic_interpreter_oc.ml | 134 +++++++++++++++++++--- 1 file changed, 117 insertions(+), 17 deletions(-) diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml index f50912b..374de69 100644 --- a/lib/relational_semantic_interpreter_oc.ml +++ b/lib/relational_semantic_interpreter_oc.ml @@ -239,8 +239,8 @@ struct xs == [] & acc' == acc | { fresh x', xs', acc_upd in xs == x' :: xs' & - f acc x' acc' & - list_foldro f acc' xs' acc_upd } + f acc x' acc_upd & + list_foldro f acc_upd xs' acc' } (* TODO: inf search on swap, investigate *) } @@ -304,23 +304,18 @@ struct env_addo state' id mem_len_prev' state'' } } - let st_spoil_foldero mem_len state mem id mem' = + let st_spoil_foldero state id state' = let open Value in ocanren { - fresh mem_id', mem_id_inv' in - env_geto state id mem_id' & - inv_ido mem_len mem_id' mem_id_inv' & - list_replaceo mem mem_id_inv' Bot mem' + mem_seto state id Bot state' } let st_spoil_assignmentso state state' = let open St in ocanren { - fresh env, mem, mem', mem_len, assignments, nil' in - state == St (env, mem, mem_len, assignments) & - list_foldlo (st_spoil_foldero mem_len state) mem assignments mem' & - nil' == [] & - state' == St (env, mem', mem_len, nil') + fresh _env, _mem, _mem_len, assignments in + state == St (_env, _mem, _mem_len, assignments) & + list_foldlo st_spoil_foldero state assignments state' } (* --- *) @@ -472,6 +467,51 @@ struct st_add_argo s s' Nat.o Val RValue q }) (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "write stmt eval test: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & + stmt == Write 0 & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + + let _ = Printf.printf "write stmt eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & + stmt == Write 1 & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + + let _ = Printf.printf "write stmt body eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & + stmts == [Write 0; Write 1] & + eval_bodyo s p stmts q}) + (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "call stmt eval test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Arg in let open Tag in @@ -517,6 +557,36 @@ struct eval_stmto s p stmt q}) (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "call stmt eval test 4: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & + stmt == Call (0, [0; 1]) & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + + let _ = Printf.printf "call stmt eval test 5: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & + stmt == Call (0, [1; 0]) & + eval_stmto s p stmt q}) + (fun q -> q#reify (St.prj_exn)))) + let _ = Printf.printf "mem set test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Arg in let open Tag in @@ -635,6 +705,19 @@ struct eval_fun_empty_argso s p d q }) (fun q -> q#reify (St.prj_exn)))) + (* fun eval test *) + let _ = Printf.printf "fun eval test (wrong call 3): %s\n" @@ 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 ([Ref; Ref], [Write 0; Write 1])] & + d == FunDecl ([Val; 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)))) + (* prog eval test *) let _ = Printf.printf "prog eval test: %s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Prog in @@ -701,7 +784,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - (* TODO *) (* annotation gen prog test *) let _ = Printf.printf "synt test 4: %s\n" @@ show(answerTags) (Stream.take (run q (fun q -> let open Prog in @@ -712,7 +794,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))}) (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) - (* TODO *) (* annotation gen prog test *) let _ = Printf.printf "synt test 5: %s\n" @@ show(answerTags) (Stream.take (run qr (fun q r -> let open Prog in @@ -723,7 +804,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - (* TODO *) (* annotation gen prog test *) let _ = Printf.printf "synt test 5' (swap call args): %s\n" @@ show(answerTags) (Stream.take (run qr (fun q r -> let open Prog in @@ -734,7 +814,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - (* TODO *) (* annotation gen prog test *) let _ = Printf.printf "synt test 5'' (swap def args): %s\n" @@ show(answerTags) (Stream.take (run qr (fun q r -> let open Prog in @@ -745,7 +824,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([r; q], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - (* TODO *) (* annotation gen prog test *) let _ = Printf.printf "synt test 6: %s\n" @@ show(answerTags) (Stream.take (run qr (fun q r -> let open Prog in @@ -756,6 +834,28 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + (* TODO FIXME *) + (* annotation gen prog test *) + let _ = Printf.printf "synt test 6' (swap call args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + + (* annotation gen prog test *) + let _ = Printf.printf "synt test 6'' (swap def args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([r; q], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + + (* TODO: test with assymetric args order *) end (* let eval_test () = *) From 97be28ff56b6a4b65289cf349bda84cf5532dfcf Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:40:55 +0000 Subject: [PATCH 3/6] tests in the separated module --- lib/dune | 34 +- lib/relational_interpreter_oc_tests.ml | 41 +++ lib/relational_interpreter_oc_tests_f.ml | 418 ++++++++++++++++++++++ lib/relational_semantic_interpreter.ml | 28 -- lib/relational_semantic_interpreter_oc.ml | 12 - 5 files changed, 484 insertions(+), 49 deletions(-) create mode 100644 lib/relational_interpreter_oc_tests.ml create mode 100644 lib/relational_interpreter_oc_tests_f.ml diff --git a/lib/dune b/lib/dune index 42fe277..51969fe 100644 --- a/lib/dune +++ b/lib/dune @@ -10,15 +10,37 @@ (libraries OCanren OCanren.tester) (inline_tests) (wrapped false) + (preprocess + (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test))) + +(library + (name relational_interpreter_oc_tests) + (modules relational_interpreter_oc_tests) + (flags (-rectypes)) + (libraries relational_interpreter_oc_tests_f) + (inline_tests) + (wrapped false) + (preprocess + (pps ppx_expect ppx_inline_test))) + +(library + (name relational_interpreter_oc_tests_f) + (modules relational_interpreter_oc_tests_f) + (flags (-rectypes)) + (libraries OCanren OCanren.tester relational_semantic_interpreter_oc) + (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) + (wrapped false) (preprocess (pps OCanren-ppx.ppx_repr + OCanren-ppx.ppx_deriving_reify OCanren-ppx.ppx_fresh - OCanren-ppx.ppx_distrib GT.ppx GT.ppx_all - ppx_expect - ppx_inline_test))) + OCanren-ppx.ppx_distrib + -- + -pp + lib/pp5+gt+plugins+ocanren+dump.exe))) (library (name relational_semantic_interpreter) @@ -28,15 +50,12 @@ (:standard -rectypes)) (libraries OCanren OCanren.tester) (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) - ; (inline_tests) (wrapped false) (preprocess (pps OCanren-ppx.ppx_repr OCanren-ppx.ppx_deriving_reify OCanren-ppx.ppx_fresh - ppx_expect - ppx_inline_test GT.ppx GT.ppx_all OCanren-ppx.ppx_distrib @@ -52,15 +71,12 @@ (:standard -rectypes)) (libraries OCanren OCanren.tester) (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) - (inline_tests) (wrapped false) (preprocess (pps OCanren-ppx.ppx_repr OCanren-ppx.ppx_deriving_reify OCanren-ppx.ppx_fresh - ppx_expect - ppx_inline_test GT.ppx GT.ppx_all OCanren-ppx.ppx_distrib diff --git a/lib/relational_interpreter_oc_tests.ml b/lib/relational_interpreter_oc_tests.ml new file mode 100644 index 0000000..e925dbd --- /dev/null +++ b/lib/relational_interpreter_oc_tests.ml @@ -0,0 +1,41 @@ +open Relational_interpreter_oc_tests_f + +let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] +let%expect_test "some test" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] +let%expect_test "some test" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] +let%expect_test "some test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] +let%expect_test "some test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] +let%expect_test "some test" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] +let%expect_test "some test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] +let%expect_test "some test" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}] +let%expect_test "some test" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}] +let%expect_test "some test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Unit], S (S (O)), [S (O); O])] |}] +let%expect_test "some test" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}] +let%expect_test "some test" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}] +let%expect_test "some test" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}] +let%expect_test "some test" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}] +let%expect_test "some test" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}] +let%expect_test "some test" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}] +let%expect_test "some test" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}] +let%expect_test "some test" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}] +let%expect_test "some test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] +let%expect_test "some test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] +let%expect_test "some test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] +let%expect_test "some test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] +let%expect_test "some test" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] +let%expect_test "some test" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] +let%expect_test "some test" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (prog_eeal_t2 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "some test" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] +let%expect_test "some test" = print_endline (synt_t1 ()); [%expect {| [Val] |}] +let%expect_test "some test" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}] +let%expect_test "some test" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] +let%expect_test "some test" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}] +let%expect_test "some test" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}] +let%expect_test "some test" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}] +let%expect_test "some test" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] +let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] diff --git a/lib/relational_interpreter_oc_tests_f.ml b/lib/relational_interpreter_oc_tests_f.ml new file mode 100644 index 0000000..f33e1e5 --- /dev/null +++ b/lib/relational_interpreter_oc_tests_f.ml @@ -0,0 +1,418 @@ +open Relational_semantic_interpreter_oc +open Relational +open GT +open OCanren +open OCanren.Std + +@type answer = St.ground GT.list with show +@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 + +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 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 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 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 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & + p == [FunDecl ([Ref; 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 0], [Unit], 1, []) & + p == [FunDecl ([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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref; 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & + p == [FunDecl ([Ref; 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 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 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 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) 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 == [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 ([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 ([Ref], [Write 0])] & + d == FunDecl ([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 ([Ref], [Write 0])] & + d == FunDecl ([Val; 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 ([Ref; Ref], [Write 0; Write 1])] & + d == FunDecl ([Val; 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)))) + +(* 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 ([Val], [Write 0; Read 0]))) q}) + (fun q -> q#reify (St.prj_exn)))) + +(* prog with func eval test *) +let prog_eeal_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 ([Val], [Write 0; Read 0])], FunDecl ([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 ([Ref], [Write 0; Read 0])], FunDecl ([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 ([Ref], [Write 0])], FunDecl ([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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))}) + (fun q -> q#reify (Tag.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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))}) + (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) + +(* annotation gen prog test *) +let synt_t5 _ = 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + +(* annotation gen prog test *) +let synt_t6 _ = 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + +(* annotation gen prog test *) +let synt_t7 _ = 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + +(* annotation gen prog test *) +let synt_t8 _ = 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) + (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) diff --git a/lib/relational_semantic_interpreter.ml b/lib/relational_semantic_interpreter.ml index 6ab270d..6aa9dd7 100644 --- a/lib/relational_semantic_interpreter.ml +++ b/lib/relational_semantic_interpreter.ml @@ -345,32 +345,4 @@ struct (all_prog === Prog.make prog main_decl) (empty_state state) (eval_fun_empty_args state prog main_decl state') - - (* TODO: fix *) - (* let eval_prog_fwd all_prog = *) - (* Stream.hd @@ *) - (* run q (fun q -> eval_prog (inj all_prog) q) *) - (* (fun qs -> qs#reify prj_exn) *) - - (* TODO: fix *) - (* let empty_prog = (Prog.T (List.Nil, FunDecl.T (List.Nil, Body.T List.Nil))) *) - (* let empty_prog = Prog.make (Std.nil ()) (FunDecl.make (Std.nil ()) (Body.make (Std.nil ()))) *) - - (* TODO: fix *) - (* let%expect_test "empty" = *) - (* eval_prog_fwd empty_prog; *) - (* Printf.printf "done!"; *) - (* [%expect {| done! |}] *) - - let eval_test = - Stream.hd @@ - run q (fun q -> ocanren { List.assoco 0 [(0, 0)] q }) - (fun qs -> qs#reify Nat.prj_exn) - -(* ((show (GT.list) (show Nat.ground)) x *) - let%expect_test "empty" = - let x = eval_test in - Printf.printf "done! %s" ((show (Nat.ground)) x); - [%expect {| done! 0 |}] - end diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml index 374de69..b7cd1e7 100644 --- a/lib/relational_semantic_interpreter_oc.ml +++ b/lib/relational_semantic_interpreter_oc.ml @@ -834,7 +834,6 @@ struct ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - (* TODO FIXME *) (* annotation gen prog test *) let _ = Printf.printf "synt test 6' (swap call args): %s\n" @@ show(answerTags) (Stream.take (run qr (fun q r -> let open Prog in @@ -857,15 +856,4 @@ struct (* TODO: test with assymetric args order *) end - - (* let eval_test () = *) - (* Stream.hd @@ *) - (* run q (fun q -> ocanren { List.assoco 0 [(0, 0)] q }) *) - (* (fun qs -> qs#reify Nat.prj_exn) *) - - (* TODO: launch tests *) - (* let%expect_test "empty" = *) - (* let x = eval_test () in *) - (* Printf.printf "done! %s" ((show (Nat.ground)) x); *) - (* [%expect {| done! 0 |}] *) end From 98d0fe2995dcc32a9e21dcaaacfa8cc7ad191c03 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:42:13 +0000 Subject: [PATCH 4/6] remove (most of the) tests from interpreter module --- lib/relational_interpreter_oc_tests.ml | 1 + lib/relational_semantic_interpreter_oc.ml | 438 ---------------------- 2 files changed, 1 insertion(+), 438 deletions(-) diff --git a/lib/relational_interpreter_oc_tests.ml b/lib/relational_interpreter_oc_tests.ml index e925dbd..e4935ed 100644 --- a/lib/relational_interpreter_oc_tests.ml +++ b/lib/relational_interpreter_oc_tests.ml @@ -39,3 +39,4 @@ let%expect_test "some test" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref let%expect_test "some test" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}] let%expect_test "some test" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] +(* TODO: test with assymetric args order *) diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml index b7cd1e7..986bc54 100644 --- a/lib/relational_semantic_interpreter_oc.ml +++ b/lib/relational_semantic_interpreter_oc.ml @@ -418,442 +418,4 @@ struct empty_stateo state & eval_fun_empty_argso state prog main_decl state' } - - module Test = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - @type answer = St.ground GT.list with show - @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 - - let _ = Printf.printf "inv id test: %s\n" @@ show(answerNat) (Stream.take (run q - (fun q -> ocanren { inv_ido 2 1 q }) - (fun q -> q#reify Nat.prj_exn))) - - let _ = Printf.printf "inv id test 2: %s\n" @@ show(answerNat) (Stream.take (run q - (fun q -> ocanren { inv_ido 2 0 q }) - (fun q -> q#reify Nat.prj_exn))) - - let _ = Printf.printf "inv id test 3: %s\n" @@ show(answerNat) (Stream.take (run q - (fun q -> ocanren { inv_ido 2 q 0 }) - (fun q -> q#reify Nat.prj_exn))) - - let _ = Printf.printf "list drop test: %s\n" @@ 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 _ = Printf.printf "list replace test: %s\n" @@ 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 _ = Printf.printf "arg to value test: %s\n" @@ 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 _ = Printf.printf "st add arg test: %s\n" @@ 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 Val RValue q }) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "write stmt eval test: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & - p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & - stmt == Write 0 & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "write stmt eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & - p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & - stmt == Write 1 & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "write stmt body eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) & - p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & - stmts == [Write 0; Write 1] & - eval_bodyo s p stmts q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "call stmt eval test: %s\n" @@ 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 0], [Unit], 1, []) & - p == [FunDecl ([Ref], [Write 0])] & - stmt == Call (0, [0]) & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "call stmt eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & - p == [FunDecl ([Ref], [Write 0])] & - stmt == Call (0, [0]) & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "call stmt eval test 3: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & - p == [FunDecl ([Ref], [Write 0])] & - stmt == Call (0, [1]) & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "call stmt eval test 4: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & - p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & - stmt == Call (0, [0; 1]) & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "call stmt eval test 5: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) & - p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & - stmt == Call (0, [1; 0]) & - eval_stmto s p stmt q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "mem set test: %s\n" @@ 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 0], [Bot], 1, []) & - mem_seto s 0 Unit q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "mem set test 2: %s\n" @@ 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 0], [Unit], 1, []) & - mem_seto s 0 Bot q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "mem set test 3: %s\n" @@ 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 1], [Unit; Unit], 2, []) & - mem_seto s 0 Bot q}) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "add arg folder test: %s\n" @@ 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) Val RValue (Std.pair q cnt) }) - (fun q -> q#reify (St.prj_exn)))) - - let _ = Printf.printf "foldl2 test: %s\n" @@ 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 == [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 _ = Printf.printf "rvalue test: %s\n" @@ 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 _ = Printf.printf "empty state: %s\n" @@ show(answer) (Stream.take (run q - (fun q -> ocanren {empty_stateo q}) - (fun q -> q#reify (St.prj_exn)))) - - (* fun eval test *) - let _ = Printf.printf "fun eval test (empty): %s\n" @@ 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 _ = Printf.printf "fun eval tist (args): %s\n" @@ 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 ([Val], [Write 0; Read 0]) & - eval_fun_empty_argso s p d q }) - (fun q -> q#reify (St.prj_exn)))) - - (* fun eval test *) - let _ = Printf.printf "fun eval test (wrong call): %s\n" @@ 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 ([Ref], [Write 0])] & - d == FunDecl ([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 _ = Printf.printf "fun eval test (wrong call 2): %s\n" @@ 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 ([Ref], [Write 0])] & - d == FunDecl ([Val; 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 _ = Printf.printf "fun eval test (wrong call 3): %s\n" @@ 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 ([Ref; Ref], [Write 0; Write 1])] & - d == FunDecl ([Val; 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)))) - - (* prog eval test *) - let _ = Printf.printf "prog eval test: %s\n" @@ 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 ([Val], [Write 0; Read 0]))) q}) - (fun q -> q#reify (St.prj_exn)))) - - (* prog with func eval test *) - let _ = Printf.printf "prog with func eval test: %s\n" @@ 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 ([Val], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q}) - (fun q -> q#reify (St.prj_exn)))) - - (* prog with func eval test *) - let _ = Printf.printf "prog with func eval test 2: %s\n" @@ 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 ([Ref], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q}) - (fun q -> q#reify (St.prj_exn)))) - - (* prog with func eval test *) - let _ = Printf.printf "prog with func eval test 3: %s\n" @@ 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 ([Ref], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) q}) - (fun q -> q#reify (St.prj_exn)))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))}) - (fun q -> q#reify (Tag.prj_exn)))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 2: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q -> q#reify (Tag.prj_exn)))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 3: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 4: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))}) - (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 5: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 5' (swap call args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 5'' (swap def args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([r; q], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 6: %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 6' (swap call args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - - (* annotation gen prog test *) - let _ = Printf.printf "synt test 6'' (swap def args): %s\n" @@ 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 {eval_progo (Prog ([FunDecl ([r; q], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) - - (* TODO: test with assymetric args order *) - end end From 5af27283545b878f3963123aa56cc20ecb38f9ac Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:50:45 +0000 Subject: [PATCH 5/6] extract types tests --- lib/dune | 4 ++- lib/relational_interpreter_oc_tests.ml | 19 ++++++++++ lib/relational_semantic_interpreter_oc.ml | 44 +++++++++++------------ 3 files changed, 44 insertions(+), 23 deletions(-) diff --git a/lib/dune b/lib/dune index 51969fe..de65d1c 100644 --- a/lib/dune +++ b/lib/dune @@ -17,7 +17,9 @@ (name relational_interpreter_oc_tests) (modules relational_interpreter_oc_tests) (flags (-rectypes)) - (libraries relational_interpreter_oc_tests_f) + (libraries + relational_semantic_interpreter_oc + relational_interpreter_oc_tests_f) (inline_tests) (wrapped false) (preprocess diff --git a/lib/relational_interpreter_oc_tests.ml b/lib/relational_interpreter_oc_tests.ml index e4935ed..c888c92 100644 --- a/lib/relational_interpreter_oc_tests.ml +++ b/lib/relational_interpreter_oc_tests.ml @@ -1,4 +1,6 @@ open Relational_interpreter_oc_tests_f +open Relational_semantic_interpreter_oc +open Relational let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] let%expect_test "some test" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] @@ -40,3 +42,20 @@ let%expect_test "some test" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref let%expect_test "some test" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] (* TODO: test with assymetric args order *) +(* TODO: tests names *) + +let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Ref] |}] +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 ([Ref; Val], [Call (S (O), [O]); Write (S (O))])] |}] +let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Val], [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, O)], [Bot], S (O), [O])] |}] + + + + + + + diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml index 986bc54..4c8f0bd 100644 --- a/lib/relational_semantic_interpreter_oc.ml +++ b/lib/relational_semantic_interpreter_oc.ml @@ -21,8 +21,8 @@ struct module Test = struct @type answer = logic GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref}) - (fun q -> q#reify reify))) + let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref}) + (fun q -> q#reify reify))) end end @@ -38,11 +38,11 @@ struct @type answer = Nat.ground List.ground GT.list with show @type answer' = ground GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)}) - (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) + let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)}) + (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) - let _ = Printf.printf "%s\n" @@ show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q}) - (fun q -> q#reify (prj_exn)))) + let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q}) + (fun q -> q#reify (prj_exn)))) end end @@ -56,10 +56,10 @@ struct module Test = struct @type answer = ground GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Tag in - let open Stmt in - ocanren {FunDecl ([Ref; Val], [Call (1, [0]); Write 1]) == q}) - (fun q -> q#reify (prj_exn)))) + let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in + let open Stmt in + ocanren {FunDecl ([Ref; Val], [Call (1, [0]); Write 1]) == q}) + (fun q -> q#reify (prj_exn)))) end end @@ -73,11 +73,11 @@ struct module Test = struct @type answer = ground GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open FunDecl in - let open Tag in - let open Stmt in - ocanren {Prog ([], FunDecl ([Val], [Write 0; Read 0])) == q}) - (fun q -> q#reify (prj_exn)))) + let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in + let open Tag in + let open Stmt in + ocanren {Prog ([], FunDecl ([Val], [Write 0; Read 0])) == q}) + (fun q -> q#reify (prj_exn)))) end end @@ -91,8 +91,8 @@ struct module Test = struct @type answer = logic GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3}) - (fun q -> q#reify reify))) + let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3}) + (fun q -> q#reify reify))) end end @@ -106,8 +106,8 @@ struct module Test = struct @type answer = logic GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit}) - (fun q -> q#reify reify))) + let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit}) + (fun q -> q#reify reify))) end end @@ -122,9 +122,9 @@ struct module Test = struct @type answer = ground GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Value in - ocanren {St ([Std.pair 0 0], [Bot], 1, [0]) == q}) - (fun q -> q#reify (prj_exn)))) + let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in + ocanren {St ([Std.pair 0 0], [Bot], 1, [0]) == q}) + (fun q -> q#reify (prj_exn)))) end end From 9d2f508291253b5c6d37c61d9e579155521f97ae Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:56:35 +0000 Subject: [PATCH 6/6] remove old relational interpreter version (was not fixed) --- lib/dune | 44 ---- lib/relational_semantic_interpreter.ml | 348 ------------------------- 2 files changed, 392 deletions(-) delete mode 100644 lib/relational_semantic_interpreter.ml diff --git a/lib/dune b/lib/dune index de65d1c..aa69dad 100644 --- a/lib/dune +++ b/lib/dune @@ -44,27 +44,6 @@ -pp lib/pp5+gt+plugins+ocanren+dump.exe))) -(library - (name relational_semantic_interpreter) - (modules relational_semantic_interpreter) - (flags - ; (-dsource) - (:standard -rectypes)) - (libraries OCanren OCanren.tester) - (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) - (wrapped false) - (preprocess - (pps - OCanren-ppx.ppx_repr - OCanren-ppx.ppx_deriving_reify - OCanren-ppx.ppx_fresh - GT.ppx - GT.ppx_all - OCanren-ppx.ppx_distrib - -- - -pp - lib/pp5+gt+plugins+ocanren+dump.exe))) - (library (name relational_semantic_interpreter_oc) (modules relational_semantic_interpreter_oc) @@ -86,29 +65,6 @@ -pp lib/pp5+gt+plugins+ocanren+dump.exe))) -; (library -; (name test) -; (modules test) -; (flags -; (-dsource) -; (:standard -rectypes)) -; (libraries OCanren OCanren.tester) -; (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) -; (wrapped false) -; (preprocess -; (pps -; ppx_expect -; ppx_inline_test -; GT.ppx -; GT.ppx_all -; OCanren-ppx.ppx_repr -; OCanren-ppx.ppx_deriving_reify -; OCanren-ppx.ppx_fresh -; OCanren-ppx.ppx_distrib -; -- -; -pp -; lib/pp5+gt+plugins+ocanren+dump.exe))) - (rule (targets pp5+gt+plugins+ocanren+dump.exe) (action diff --git a/lib/relational_semantic_interpreter.ml b/lib/relational_semantic_interpreter.ml deleted file mode 100644 index 6aa9dd7..0000000 --- a/lib/relational_semantic_interpreter.ml +++ /dev/null @@ -1,348 +0,0 @@ -module Relational = -struct - open GT - open OCanren - open OCanren.Std - - type data_ground = Nat.ground (* with show, gmap *) - [@@deriving gt ~options:{ show; gmap }] - type data_logic = Nat.logic - [@@deriving gt ~options:{ show; gmap }] - type data_injected = Nat.injected - - module Tag = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec t = Ref | Value - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = t - ] - - let ref = inj Ref - let value = inj Value - end - - module Stmt = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (Nat.ground, Nat.ground List.ground) t - ] - - let call f args = inj (Call (f, args)) - let read id = inj (Read id) - let write id = inj (Write id) - end - - module Body = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec ('stmt, 'l) t = T of ('stmt, 'l) List.t - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (Stmt.ground, Stmt.ground List.ground) t - ] - - let make stmts = inj (T stmts) - end - - module FunDecl = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec ('l, 'b) t = T of 'l * 'b - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (Tag.ground List.ground, Body.ground) t - ] - - let make args body = inj (T (args, body)) - end - - module Prog = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec ('l, 'f) t = T of 'l * 'f - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t - ] - - let make decls main_decl = inj (T (decls, main_decl)) - end - - module Arg = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec 'd t = RValue | LValue of 'd - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = Nat.ground t - ] - - let rvalue = inj RValue - let lvalue x = inj (LValue x) - end - - module Value = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec t = Unit | Bot - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = t - ] - - let unit = inj Unit - let bot = inj Bot - end - - (* module Envr = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%distrib *) - (* type nonrec ('d, 'l) t = T of ('d * 'd, 'l) List.t *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = (Nat.ground, Nat.ground List.ground) t *) - (* ] *) - - (* let make elems = inj (T elems) *) - (* end *) - - module State = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%distrib - type nonrec ('env, 'mem, 'last_mem, 'assignments) t = T of 'env * 'mem * 'last_mem * 'assignments - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (((Nat.ground, Nat.ground) Pair.ground) List.ground, - Value.ground List.ground, Nat.ground, Nat.ground List.ground) t - ] - - let make env mem last_mem assignments = inj (T (env, mem, last_mem, assignments)) - end - - let rec list_replace xs id value ys = - conde - [ (xs === Std.nil ()) &&& (ys === Std.nil ()) (* TODO: error *) - ; fresh (x xs') (xs === List.cons x xs') (id === Nat.o) (ys === List.cons value xs) - ; fresh (x xs' id' ys') (xs === List. cons x xs') (id === Nat.s id') (ys === List.cons x ys') - (list_replace xs' id' value ys') - ] - - let rec list_assoc a xs v' = - conde - [ fresh (a' b' xs') - (xs === List.cons (a', b') xs') - (a =/= a') - (list_assoc a xs' v') - ; fresh (a' b' xs') - (xs === List.cons (a', b') xs') - (a === a') - (v' === b') - ] - (* TODO: difference from List.assoco ?? *) - - let env_get state id mem_id' = - fresh (env mem mem_len assignments) - (state === State.make env mem mem_len assignments) - (list_assoc id env mem_id') - (* (List.assoco id env mem_id') *) - - let env_add state id mem_id state' = - fresh (env env' mem mem_len assignments) - (state === State.make env mem mem_len assignments) - (state' === State.make env' mem mem_len assignments) - (env' === List.cons (id, mem_id) env) - - let inv_id mem_len id id' = - fresh (inv_id_inc) - (Nat.addo inv_id_inc id mem_len) - (Nat.addo id' (Nat.s Nat.o) inv_id_inc) - - (* --- *) - - let rec list_nth xs id x' = - conde - [ (xs === Std.nil ()) (* TODO: error *) - ; fresh (y' xs') (id === Nat.o) (List.cons y' xs' === xs) (x' === y') - ; fresh (id' y' xs') (Nat.s id' === id) (List.cons y' xs' === xs) (list_nth xs' id' x') - ] - - (* TODO: use real holes *) - let mem_get state id value' = - fresh (mem mem_len mem_id mem_id_inv _env _assignments) - (state === inj (State.T (_env, mem, mem_len, _assignments))) - (env_get state id mem_id) - (inv_id mem_len mem_id mem_id_inv) - (list_nth mem mem_id_inv value') - - let mem_set state id value state'= - fresh (env mem mem_len assignments mem_id inv_mem_id mem' assignments') - (state === State.make env mem mem_len assignments) - (env_get state id mem_id) - (inv_id mem_len mem_id inv_mem_id) - (list_replace mem mem_id value mem') - (assignments' === List.cons id assignments) - (state' === State.make env mem' mem_len assignments') - - let mem_add state value state' = - fresh (env mem mem_len mem_len' assignments mem') - (state === State.make env mem mem_len assignments) - (mem' === List.cons value mem) - (mem_len' === Nat.s mem_len) - (state' === State.make env mem mem_len' assignments) - - let mem_check state id state' = - conde - [ (mem_get state id Value.bot) &&& (state' === state) - ; (mem_get state id Value.unit) &&& (state' === state) - ] - - (* --- *) - - let rec list_foldl f acc xs acc' = - conde - [ (xs === Std.nil ()) &&& (acc' === acc) - ; fresh (x' xs' acc_upd) - (xs === List.cons x' xs') - (list_foldl f acc xs' acc_upd) - (f acc_upd x' acc') - ] - - - let rec list_foldr2 f acc xs ys acc' = - conde - [ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc) - ; fresh (x' xs' y' ys' acc_upd) - (xs === List.cons x' xs') - (ys === List.cons y' ys') - (f acc x' y' acc_upd) - (list_foldr2 f acc_upd xs' ys' acc') - ] - - let rec list_foldl2 f acc xs ys acc' = - conde - [ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc) - ; fresh (x' xs' y' ys' acc_upd) - (xs === List.cons x' xs') - (ys === List.cons y' ys') - (list_foldl2 f acc xs' ys' acc_upd) - (f acc_upd x' y' acc') - ] - - let arg_to_value state arg value' = - conde - [ (arg === Arg.rvalue) &&& (value' === Value.unit) - ; fresh (id) (arg === Arg.lvalue id) (mem_get state id value') - ] - - let arg_to_rvalue _arg value' = (value' === inj Arg.RValue) - - let st_mem_len state mem_len' = - fresh (_env _mem _assignments) (* TODO: replace with real placeholder ? *) - (state === State.make _env _mem mem_len' _assignments) - - let st_add_arg state state_before id arg_tag arg state'' = - conde - [ (arg_tag === Tag.ref) &&& (arg === Arg.rvalue) &&& (state'' === state) - (* TODO: error, TODO: allow later ?? *) - ; fresh (arg' value') - (arg_tag === Tag.ref) - (arg === Arg.lvalue arg') - (env_get state_before arg' value') - (env_add state id value' state'') - ; fresh (value' state' mem_len_dec') - (arg_tag === Tag.value) - (arg_to_value state_before arg value') - (mem_add state value' state') - (st_mem_len state (Nat.s mem_len_dec')) - (env_add state' id mem_len_dec' state'') - ] - - let st_spoil_folder mem_len state mem id mem' = - fresh (mem_id' mem_id_inv') - (env_get state id mem_id') - (inv_id mem_len mem_id' mem_id_inv') - (list_replace mem mem_id_inv' (inj Value.Bot) mem') - - let st_spoil_assignments state state' = - fresh (env mem mem' mem_len assignments nil') - (state === State.make env mem mem_len assignments) - (list_foldl (st_spoil_folder mem_len state) mem assignments mem') - (* (List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments mem') *) - (nil' === Std.nil ()) - (state' === State.make env mem' mem_len nil') - - (* --- *) - - let arg_to_lvalue arg arg' = (arg' === inj (Arg.LValue arg)) - - let rec list_drop n xs xs' = - conde - [ (xs === Std.nil ()) &&& (xs' === Std.nil ()) - ; n === Nat.o &&& (xs === xs') - ; fresh (n' y ys) (Nat.s n' === n) (xs === List.cons y ys) (list_drop n' ys xs') - ] - - let rec eval_stmt state prog stmt state' = - conde - [ fresh (f_id args f args') - (stmt === Stmt.call f_id args) - (list_nth prog f_id f) - (List.mapo arg_to_lvalue args args') - (eval_fun state prog f args' state') - ; fresh (id) (stmt === Stmt.read id) (mem_check state id state') - ; fresh (id) (stmt === Stmt.write id) (mem_set state id Value.unit state') - ] - - and eval_body_folder prog state stmt state' = eval_stmt state prog stmt state' - - and eval_body state prog body state' = - list_foldl (eval_body_folder prog) state body state' - (* (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body) *) - - and add_arg_folder state_before state_c arg_tag arg state_c' = - fresh (state id state' id') - (state_c === inj (state, id)) - (st_add_arg state state_before id arg_tag arg state') - (id' === Nat.s id) - (state_c' === inj (state', id')) - - and eval_fun state prog decl args state' = - fresh (arg_tags body - env_before mem_before len_before assignments_before - state_clean - state_with_vars _counter - state_evaled - state_spoiled - _env mem_spoiled len _assignments - mem_updated len_to_drop - nil_env nil_assignments) - (nil_env === Std.nil ()) - (nil_assignments === Std.nil ()) - (decl === FunDecl.make arg_tags body) - (state === State.make env_before mem_before len_before assignments_before) - (state_clean === State.make nil_env mem_before len_before nil_assignments) - (list_foldl2 (add_arg_folder state) (inj (state, Nat.o)) arg_tags args (inj (state_with_vars, _counter))) (* TODO: replace with real placeholder *) - (eval_body state_with_vars prog body state_evaled) - (st_spoil_assignments state_evaled state_spoiled) - (state_spoiled === State.make _env mem_spoiled len _assignments) - (Nat.addo len_to_drop len_before len) - (list_drop len_to_drop mem_spoiled mem_updated) - (state' === State.make env_before mem_updated len_before assignments_before) - - and eval_fun_empty_args state prog decl state' = - fresh (arg_tags args _hole) (* TODO: replace with real placeholder *) - (decl === FunDecl.make arg_tags _hole) - (List.mapo arg_to_rvalue arg_tags args) - (eval_fun state prog decl args state') - - (* --- *) - - let empty_state state = - fresh (nil_env nil_mem nil_assignments) - (nil_env === Std.nil ()) - (nil_assignments === Std.nil ()) - (nil_mem === Std.nil ()) - (state === State.make nil_env nil_mem Nat.o nil_assignments) - - let eval_prog all_prog state' = - fresh (prog main_decl state) - (all_prog === Prog.make prog main_decl) - (empty_state state) - (eval_fun_empty_args state prog main_decl state') -end