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

struct: fixes, som more tests for analyzer

Browse source
This commit is contained in:
ProgramSnail 2026-05-06 15:01:34 +00:00
parent 6620b0d0ef
commit 5833e5949c
5 changed files with 719 additions and 540 deletions
Download patch file Download diff file Expand all files Collapse all files

866
model_with_structures/tests_f.ml
View file

@ -4,506 +4,506 @@ open GT
open OCanren
open OCanren.Std
@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
@type answerCopyCap = CopyCap.ground GT.list with show
@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show
(* @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 *)
(* @type answerCopyCap = CopyCap.ground GT.list with show *)
(* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *)
let inv_id_t _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 1 q })
(fun q -> q#reify Nat.prj_exn)))
(* let inv_id_t _ = show(answerNat) (Stream.take (run q *)
(* (fun q -> ocanren { inv_ido 2 1 q }) *)
(* (fun q -> q#reify Nat.prj_exn))) *)
let inv_id_t2 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 0 q })
(fun q -> q#reify Nat.prj_exn)))
(* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
(* (fun q -> ocanren { inv_ido 2 0 q }) *)
(* (fun q -> q#reify Nat.prj_exn))) *)
let inv_id_t3 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 q 0 })
(fun q -> q#reify Nat.prj_exn)))
(* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
(* (fun q -> ocanren { inv_ido 2 q 0 }) *)
(* (fun q -> q#reify Nat.prj_exn))) *)
let list_drop_t _ = 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 list_drop_t _ = 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 list_replace_t _ = 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 list_replace_t _ = 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 arg_to_value_t _ = 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 arg_to_value_t _ = 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 st_add_arg_t _ = 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 rwi_val RValue q })
(fun q -> q#reify (St.prj_exn))))
(* let st_add_arg_t _ = 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 rwi_val RValue q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let write_eval_t1 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 0 &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let write_eval_t1 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* stmt == Write 0 & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let write_eval_t2 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 1 &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let write_eval_t2 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* stmt == Write 1 & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let writes_eval_t _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmts == [Write 0; Write 1] &
eval_bodyo s p stmts q})
(fun q -> q#reify (St.prj_exn))))
(* let writes_eval_t _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* stmts == [Write 0; Write 1] & *)
(* eval_bodyo s p stmts q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let call_eval_t1 _ = 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 (Std.pair wi_ref 0)], [Unit], 1, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let call_eval_t1 _ = 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 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
(* p == [FunDecl ([wi_ref], [Write 0])] & *)
(* stmt == Call (0, [0]) & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let call_eval_t2 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let call_eval_t2 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
(* p == [FunDecl ([wi_ref], [Write 0])] & *)
(* stmt == Call (0, [0]) & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let call_eval_t3 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [1]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let call_eval_t3 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
(* p == [FunDecl ([wi_ref], [Write 0])] & *)
(* stmt == Call (0, [1]) & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let call_eval_t4 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [0; 1]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let call_eval_t4 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* stmt == Call (0, [0; 1]) & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let call_eval_t5 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [1; 0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
(* let call_eval_t5 _ = 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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* stmt == Call (0, [1; 0]) & *)
(* eval_stmto s p stmt q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let mem_set_t1 _ = 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 (Std.pair wi_ref 0)], [Bot], 1, []) &
mem_seto s 0 Unit q})
(fun q -> q#reify (St.prj_exn))))
(* let mem_set_t1 _ = 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 (Std.pair wi_ref 0)], [Bot], 1, []) & *)
(* mem_seto s 0 Unit q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let mem_set_t2 _ = 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 (Std.pair wi_ref 0)], [Unit], 1, []) &
mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn))))
(* let mem_set_t2 _ = 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 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
(* mem_seto s 0 Bot q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let meem_set_t3 _ = 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 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) &
mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn))))
(* let meem_set_t3 _ = 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 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) & *)
(* mem_seto s 0 Bot q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let add_arg_folder_t _ = 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) rwi_val RValue (Std.pair q cnt) })
(fun q -> q#reify (St.prj_exn))))
(* let add_arg_folder_t _ = 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) rwi_val RValue (Std.pair q cnt) }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let foldl2_t _ = 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 == [rwi_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 foldl2_t _ = 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 == [rwi_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 rvalue_t _ = 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))))
(* let rvalue_t _ = 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 empty_state_t _ = show(answer) (Stream.take (run q
(fun q -> ocanren {empty_stateo q})
(fun q -> q#reify (St.prj_exn))))
(* let empty_state_t _ = show(answer) (Stream.take (run q *)
(* (fun q -> ocanren {empty_stateo q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* fun eval test *)
let fun_eval_t1 _ = 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))))
(* let fun_eval_t1 _ = 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 fun_eval_t2 _ = 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 ([wi_val], [Write 0; Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* let fun_eval_t2 _ = 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 ([wi_val], [Write 0; Read 0]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* fun eval test *)
let fun_eval_t3 _ = 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 ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* let fun_eval_t3 _ = 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 ([wi_ref], [Write 0])] & *)
(* d == FunDecl ([wi_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 fun_eval_t4 _ = 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 ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* let fun_eval_t4 _ = 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 ([wi_ref], [Write 0])] & *)
(* d == FunDecl ([wi_val; wi_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 fun_eval_t5 _ = 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 ([wi_ref; wi_ref], [Write 0; Write 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 })
(fun q -> q#reify (St.prj_exn))))
(* let fun_eval_t5 _ = 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 ([wi_ref; wi_ref], [Write 0; Write 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 }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* fun eval test *)
let fun_eval_t6 _ = 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 ([wi_val], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0])]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* let fun_eval_t6 _ = 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 ([wi_val], [Write 0])] & *)
(* d == FunDecl ([wi_val], [Call (0, [0])]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog eval test *)
let prog_eval_t1 _ = 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 ([wi_val], [Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t1 _ = 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 ([wi_val], [Write 0; Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog with func eval test *)
let prog_eval_t2 _ = 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 ([wi_val], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t2 _ = 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 ([wi_val], [Write 0; Read 0])], *)
(* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog with func eval test *)
let prog_eval_t3 _ = 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 ([wi_ref], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t3 _ = 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 ([wi_ref], [Write 0; Read 0])], *)
(* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog with func eval test *)
let prog_eval_t4 _ = 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 ([wi_ref], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t4 _ = 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 ([wi_ref], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog with func eval test *)
let prog_eval_t5 _ = 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 ([wi_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t5 _ = 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 ([wi_val], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* prog with func eval test *)
let prog_eval_t6 _ = 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 ([ri_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let prog_eval_t6 _ = 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 ([ri_val], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
(* annotation gen prog test *)
let synt_t1 _ = 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 {i_any q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* let synt_t1 _ = 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 {i_any q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> q#reify (Tag.prj_exn)))) *)
(* annotation gen prog test *)
let synt_t2 _ = 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 {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* let synt_t2 _ = 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 {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> q#reify (Tag.prj_exn)))) *)
(* annotation gen prog test *)
let synt_t3 _ = 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 {i_any q & is_not_reado q & i_any r & is_not_reado r &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* let synt_t3 _ = 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 {i_any q & is_not_reado q & i_any r & is_not_reado r & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *)
(* annotation gen prog test *)
let synt_t4 _ = 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 {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
(* let synt_t4 _ = 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 {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *)
(* annotation gen prog test *)
let synt_t5 _ = show(answerCopyCaps) (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 {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* let synt_t5 _ = show(answerCopyCaps) (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 {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
(* annotation gen prog test *)
let synt_t6 _ = show(answerCopyCaps) (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 {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* let synt_t6 _ = show(answerCopyCaps) (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 {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
(* annotation gen prog test *)
let synt_t7 _ = show(answerCopyCaps) (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 {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
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, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* let synt_t7 _ = show(answerCopyCaps) (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 {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* 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, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
(* annotation gen prog test *)
let synt_t8 _ = show(answerCopyCaps) (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 {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
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, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* let synt_t8 _ = show(answerCopyCaps) (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 {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* 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, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
(* annotation gen prog test *)
let synt_t9 _ = show(answerCopyCaps) (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 {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
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, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* let synt_t9 _ = show(answerCopyCaps) (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 {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* 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, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
(* TODO: FIXME: implement memoization cuts *)
(* prog with recursive function call *)
let rec_eval_t _ = 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 ([wi_ref], [Write 0; Call (0, [0])])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* let rec_eval_t _ = 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 ([wi_ref], [Write 0; Call (0, [0])])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)