st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-03-11 18:47:08 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

remove (most of the) tests from interpreter module

Browse source
This commit is contained in:
ProgramSnail 2026-02-15 18:42:13 +00:00
parent 97be28ff56
commit 98d0fe2995
2 changed files with 1 additions and 438 deletions
Download patch file Download diff file Expand all files Collapse all files

1
lib/relational_interpreter_oc_tests.ml
View file

@ -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_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_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
(* TODO: test with assymetric args order *)

438
lib/relational_semantic_interpreter_oc.ml
View file

@ -418,442 +418,4 @@ struct
empty_stateo state & empty_stateo state &
eval_fun_empty_argso state prog main_decl 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 end