From 98d0fe2995dcc32a9e21dcaaacfa8cc7ad191c03 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 18:42:13 +0000 Subject: [PATCH] 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