From ae8e39c03a3790e4d1eac7fc8a1d5570b2090e66 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Feb 2026 16:01:42 +0000 Subject: [PATCH] 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 () = *)