st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-03-12 02:57:09 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:2ec7f963db5ff1cebe75ae652dab60a9d7136732
Branches Tags
st:main
...
compare: st:270296e7b2ed2b83e4ca3b62d6bab266e3355cd5
Branches Tags
st:main

2 commits
2ec7f963db ... 270296e7b2

Author SHA1 Message Date
ProgramSnail
270296e7b2 simplest model with mods: test fixes & mark not passed tests 2026-03-07 22:27:05 +00:00
ProgramSnail
ea03743fee syntesizer with mods: tests update (no result update, no run) 2026-03-07 21:44:55 +00:00
3 changed files with 120 additions and 109 deletions
Download patch file Download diff file Expand all files Collapse all files

56
simplest_model_with_mods/dune
View file

@ -23,36 +23,34 @@
(preprocess (preprocess
(pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test))) (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
; TODO: tmp, during change (library
; (library (name tests_mods)
; (name tests_mods) (modules tests)
; (modules tests) (flags (-rectypes))
; (flags (-rectypes)) (libraries synthesizer_mods tests_f_mods)
; (libraries synthesizer_mods tests_f_mods) (inline_tests)
; (inline_tests) (wrapped false)
; (wrapped false) (preprocess
; (preprocess (pps ppx_expect ppx_inline_test)))
; (pps ppx_expect ppx_inline_test)))
; TODO: tmp, during change (library
; (library (name tests_f_mods)
; (name tests_f_mods) (modules tests_f)
; (modules tests_f) (flags (-rectypes))
; (flags (-rectypes)) (libraries OCanren OCanren.tester synthesizer_mods)
; (libraries OCanren OCanren.tester synthesizer_mods) (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) (wrapped false)
; (wrapped false) (preprocess
; (preprocess (pps
; (pps OCanren-ppx.ppx_repr
; OCanren-ppx.ppx_repr OCanren-ppx.ppx_deriving_reify
; OCanren-ppx.ppx_deriving_reify OCanren-ppx.ppx_fresh
; OCanren-ppx.ppx_fresh GT.ppx
; GT.ppx GT.ppx_all
; GT.ppx_all OCanren-ppx.ppx_distrib
; OCanren-ppx.ppx_distrib --
; -- -pp
; -pp camlp5/pp5+gt+plugins+ocanren+dump.exe)))
; camlp5/pp5+gt+plugins+ocanren+dump.exe)))
(library (library
(name synthesizer_mods) (name synthesizer_mods)

62
simplest_model_with_mods/tests.ml
View file

@ -3,14 +3,14 @@ open Synthesizer
open Relational open Relational
(* type tests *) (* type tests *)
let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Ref] |}] let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NWr, Ref, In, NOut)] |}]
let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] 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 "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 "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, Wr, Ref, In, NOut); Tag (Rd, Wr, Val, In, NOut)], [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 "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (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 "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])] |}] let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
(* function tests *) (* function tests *)
let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
@ -19,40 +19,40 @@ let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (
let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), []); St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}] let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}] let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
let%expect_test "multiple writes eval 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 "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}] (* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *) (* FIXME *)
let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}] (* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *) (* FIXME *)
let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}] (* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *) (* FIXME *)
let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}] (* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [])] |}] *) (* FIXME *)
let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}] (* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [])] |}] *) (* FIXME *)
let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}] let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}] let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}] let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] (* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *) (* FIXME *)
let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}] let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), []); St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] (* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *)
let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] (* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *)
let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] (* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *)
let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}] (* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *)
let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}] (* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}] (* FIXME *) *)
let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}] (* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}] *) (* FIXME *)
let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] (* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] *) (* FIXME *)
let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}] (* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}] (* FIXME *) *)
let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}] (* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}] *)
let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}] (* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}] *)
let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] (* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] *)
let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] (* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] (* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
(* NOTE: inf test in current model (without additional functional interfaces and ) *) (* NOTE: inf test in current model (without additional functional interfaces and ) *)
(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *) (* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *)

111
simplest_model_with_mods/tests_f.ml
View file

@ -47,7 +47,7 @@ let st_add_arg_t _ = show(answer) (Stream.take (run q
fresh s, s', cnt in fresh s, s', cnt in
empty_stateo s & empty_stateo s &
empty_stateo s' & empty_stateo s' &
st_add_argo s s' Nat.o Val RValue q }) st_add_argo s s' Nat.o rwi_val RValue q })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
let write_eval_t1 _ = show(answer) (Stream.take (run q let write_eval_t1 _ = show(answer) (Stream.take (run q
@ -59,8 +59,8 @@ let write_eval_t1 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 0 & stmt == Write 0 &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -74,8 +74,8 @@ let write_eval_t2 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 1 & stmt == Write 1 &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -89,8 +89,8 @@ let writes_eval_t _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmts in fresh s, p, stmts in
s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmts == [Write 0; Write 1] & stmts == [Write 0; Write 1] &
eval_bodyo s p stmts q}) eval_bodyo s p stmts q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -104,8 +104,8 @@ let call_eval_t1 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 0 0], [Unit], 1, []) & s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
p == [FunDecl ([Ref], [Write 0])] & p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) & stmt == Call (0, [0]) &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -119,8 +119,8 @@ let call_eval_t2 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([Ref], [Write 0])] & p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) & stmt == Call (0, [0]) &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -134,8 +134,8 @@ let call_eval_t3 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([Ref], [Write 0])] & p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [1]) & stmt == Call (0, [1]) &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -149,8 +149,8 @@ let call_eval_t4 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [0; 1]) & stmt == Call (0, [0; 1]) &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -164,8 +164,8 @@ let call_eval_t5 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
ocanren { ocanren {
fresh s, p, stmt in fresh s, p, stmt in
s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) & s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [1; 0]) & stmt == Call (0, [1; 0]) &
eval_stmto s p stmt q}) eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -177,7 +177,7 @@ let mem_set_t1 _ = show(answer) (Stream.take (run q
let open St in let open St in
ocanren { ocanren {
fresh s in fresh s in
s == St ([Std.pair 0 0], [Bot], 1, []) & s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) &
mem_seto s 0 Unit q}) mem_seto s 0 Unit q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -188,7 +188,7 @@ let mem_set_t2 _ = show(answer) (Stream.take (run q
let open St in let open St in
ocanren { ocanren {
fresh s in fresh s in
s == St ([Std.pair 0 0], [Unit], 1, []) & s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
mem_seto s 0 Bot q}) mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -199,7 +199,7 @@ let meem_set_t3 _ = show(answer) (Stream.take (run q
let open St in let open St in
ocanren { ocanren {
fresh s in fresh s in
s == St ([Std.pair 0 1], [Unit; Unit], 2, []) & s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) &
mem_seto s 0 Bot q}) mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -210,7 +210,7 @@ let add_arg_folder_t _ = show(answer) (Stream.take (run q
fresh s, s', cnt in fresh s, s', cnt in
empty_stateo s & empty_stateo s &
empty_stateo s' & empty_stateo s' &
add_arg_foldero s (Std.pair s' Nat.o) Val RValue (Std.pair q cnt) }) add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
let foldl2_t _ = show(answer) (Stream.take (run q let foldl2_t _ = show(answer) (Stream.take (run q
@ -218,7 +218,7 @@ let foldl2_t _ = show(answer) (Stream.take (run q
let open Tag in let open Tag in
ocanren { ocanren {
fresh s, s', cnt, arg_tags, args in fresh s, s', cnt, arg_tags, args in
arg_tags == [Val] & arg_tags == [rwi_val] &
args == [RValue] & args == [RValue] &
empty_stateo s & empty_stateo s &
empty_stateo s' & empty_stateo s' &
@ -258,7 +258,7 @@ let fun_eval_t2 _ = show(answer) (Stream.take (run q
ocanren { fresh s, p, d in ocanren { fresh s, p, d in
empty_stateo s & empty_stateo s &
p == [] & p == [] &
d == FunDecl ([Val], [Write 0; Read 0]) & d == FunDecl ([wi_val], [Write 0; Read 0]) &
eval_fun_empty_argso s p d q }) eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -270,8 +270,8 @@ let fun_eval_t3 _ = show(answer) (Stream.take (run q
let open Stmt in let open Stmt in
ocanren { fresh s, p, d in ocanren { fresh s, p, d in
empty_stateo s & empty_stateo s &
p == [FunDecl ([Ref], [Write 0])] & p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([Val], [Call (0, [0]); Read 0]) & d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
eval_fun_empty_argso s p d q }) eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -283,8 +283,8 @@ let fun_eval_t4 _ = show(answer) (Stream.take (run q
let open Stmt in let open Stmt in
ocanren { fresh s, p, d in ocanren { fresh s, p, d in
empty_stateo s & empty_stateo s &
p == [FunDecl ([Ref], [Write 0])] & p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]) & d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
eval_fun_empty_argso s p d q }) eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -296,8 +296,8 @@ let fun_eval_t5 _ = show(answer) (Stream.take (run q
let open Stmt in let open Stmt in
ocanren { fresh s, p, d in ocanren { fresh s, p, d in
empty_stateo s & empty_stateo s &
p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] & p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
d == FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
eval_fun_empty_argso s p d q }) eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
@ -307,7 +307,7 @@ let prog_eval_t1 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
let open Tag in let open Tag in
let open Stmt in let open Stmt in
ocanren {eval_progo (Prog ([], FunDecl ([Val], [Write 0; Read 0]))) q}) ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *) (* prog with func eval test *)
@ -316,7 +316,8 @@ let prog_eval_t2 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
let open Tag in let open Tag in
let open Stmt 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}) ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *) (* prog with func eval test *)
@ -325,7 +326,8 @@ let prog_eval_t3 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
let open Tag in let open Tag in
let open Stmt 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}) ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *) (* prog with func eval test *)
@ -334,7 +336,8 @@ let prog_eval_t4 _ = show(answer) (Stream.take (run q
let open FunDecl in let open FunDecl in
let open Tag in let open Tag in
let open Stmt in let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) q}) ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn)))) (fun q -> q#reify (St.prj_exn))))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -344,7 +347,8 @@ let synt_t1 _ = show(answerTag) (Stream.take (run q
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St in let open St in
ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))}) ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))})
(fun q -> q#reify (Tag.prj_exn)))) (fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -354,7 +358,8 @@ let synt_t2 _ = show(answerTag) (Stream.take (run q
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St in let open St in
ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
(fun q -> q#reify (Tag.prj_exn)))) (fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -364,7 +369,8 @@ let synt_t3 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St in let open St in
ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) 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)]))) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -374,7 +380,8 @@ let synt_t4 _ = show(answerTags) (Stream.take (run q
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St 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, []))}) ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))})
(fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
(* annotation gen prog test *) (* annotation gen prog test *)
@ -384,7 +391,8 @@ let synt_t5 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St 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, []))}) ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])],
FunDecl ([wi_val; wi_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 *) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
(* annotation gen prog test *) (* annotation gen prog test *)
@ -394,7 +402,8 @@ let synt_t6 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St 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, []))}) ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])],
FunDecl ([wi_val; wi_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 *) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
(* annotation gen prog test *) (* annotation gen prog test *)
@ -404,7 +413,8 @@ let synt_t7 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St 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, []))}) ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])],
FunDecl ([wi_val; wi_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)]))) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -414,7 +424,8 @@ let synt_t8 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St 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, []))}) ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])],
FunDecl ([wi_val; wi_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)]))) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* annotation gen prog test *) (* annotation gen prog test *)
@ -424,15 +435,17 @@ let synt_t9 _ = show(answerTags) (Stream.take (run qr
let open Tag in let open Tag in
let open Stmt in let open Stmt in
let open St in let open St in
ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Read 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))}) ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Read 1])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))})
(fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* TODO: FIXME: implement memoization cuts *)
(* prog with recursive function call *) (* prog with recursive function call *)
let rec_eval_t _ = show(answer) (Stream.take (run q (* let rec_eval_t _ = show(answer) (Stream.take (run q *)
(fun q -> let open Prog in (* (fun q -> let open Prog in *)
let open FunDecl in (* let open FunDecl in *)
let open Tag in (* let open Tag in *)
let open Stmt in (* let open Stmt in *)
ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q}) (* ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
(fun q -> q#reify (St.prj_exn)))) (* (fun q -> q#reify (St.prj_exn)))) *)