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

extract types tests

Browse source
This commit is contained in:
ProgramSnail 2026-02-15 18:50:45 +00:00
parent 98d0fe2995
commit 5af2728354
3 changed files with 44 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

4
lib/dune
View file

@ -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

19
lib/relational_interpreter_oc_tests.ml
View file

@ -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])] |}]

44
lib/relational_semantic_interpreter_oc.ml
View file

@ -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