From 97be28ff56b6a4b65289cf349bda84cf5532dfcf Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:40:55 +0000 Subject: [PATCH] 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