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

Compare commits

base: st:68f2569922986334894d303b68b9b93d6db6db31
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:ee8ff429cfe6baf5897e55a2d4b5961c9bc427e2
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "68f2569922986334894d303b68b9b93d6db6db31" and "ee8ff429cfe6baf5897e55a2d4b5961c9bc427e2" have entirely different histories.
68f2569922 ... ee8ff429cf

4 changed files with 68 additions and 202 deletions
Download patch file Download diff file Expand all files Collapse all files

23
model_with_structures/analyzer.ml
View file

@ -519,14 +519,12 @@ struct
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var" = let%expect_test "simple var" =
prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id));
ReadS (VarP globals_min_id));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, forbidden read" = let%expect_test "simple var, no read" =
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
ReadS (VarP globals_min_id));
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| read: spoiled value |}] [%expect {| read: spoiled value |}]
@ -539,21 +537,18 @@ struct
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, write" = let%expect_test "simple var, write" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id));
WriteS (VarP globals_min_id));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, forbidden write" = let%expect_test "simple var, no write" =
try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id));
WriteS (VarP globals_min_id));
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}] [%expect {| write: write tag |}]
let%expect_test "simple var, write & read" = let%expect_test "simple var, write & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id),
SeqS (WriteS (VarP globals_min_id),
ReadS (VarP globals_min_id))); ReadS (VarP globals_min_id)));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -562,7 +557,7 @@ struct
(* let%expect_test "simple call with read" = *) (* let%expect_test "simple call with read" = *)
(* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *) (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
(* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *) (* FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], *)
(* CallS (VarP (globals_min_id + 1), *) (* CallS (VarP (globals_min_id + 1), *)
(* [PathE (VarP globals_min_id)])); *) (* [PathE (VarP globals_min_id)])); *)
(* Printf.printf "done!"; *) (* Printf.printf "done!"; *)
@ -571,7 +566,7 @@ struct
(* let%expect_test "simple call with write" = *) (* let%expect_test "simple call with write" = *)
(* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *) (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
(* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *) (* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *)
(* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *) (* FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], *)
(* CallS (VarP (globals_min_id + 2), *) (* CallS (VarP (globals_min_id + 2), *)
(* [PathE (VarP (globals_min_id + 1))])); *) (* [PathE (VarP (globals_min_id + 1))])); *)
(* Printf.printf "done!"; *) (* Printf.printf "done!"; *)

116
model_with_structures/synthesizer.ml
View file

@ -1,6 +1,3 @@
(* NOTE: in previous models foldl & foldr are probably spapped
<- TODO: fix ? *)
module Relational = module Relational =
struct struct
open GT open GT
@ -148,9 +145,9 @@ struct
module Decl = struct module Decl = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's type nonrec ((* 'd, *) 't, 'e, 'dl, 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * *) 'dl * 'mtl * 's
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t type ground = ((* Nat.ground, *) Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
] ]
end end
@ -294,50 +291,40 @@ struct
} }
let rec list_foldro f acc xs acc' = ocanren {
xs == [] & acc' == acc |
{ fresh x', xs', acc_upd in
xs == x' :: xs' &
list_foldro f acc xs' acc_upd &
f acc_upd x' acc' }
}
let rec list_foldlo f acc xs acc' = ocanren { let rec list_foldlo f acc xs acc' = ocanren {
xs == [] & acc' == acc |
{ fresh x', xs', acc_upd in
xs == x' :: xs' &
list_foldlo f acc xs' acc_upd &
f acc_upd x' acc' }
}
let rec list_foldro f acc xs acc' = ocanren {
xs == [] & acc' == acc | xs == [] & acc' == acc |
{ fresh x', xs', acc_upd in { fresh x', xs', acc_upd in
xs == x' :: xs' & xs == x' :: xs' &
f acc x' acc_upd & f acc x' acc_upd &
list_foldlo f acc_upd xs' acc' } list_foldro f acc_upd xs' acc' }
(* TODO: inf search on swap, investigate *) (* TODO: inf search on swap, investigate *)
} }
let rec list_foldl2o f acc xs ys acc' = ocanren {
xs == [] & ys == [] & acc' == acc |
{ fresh x', xs', y', ys', acc_upd in
xs == x' :: xs' &
ys == y' :: ys' &
f acc x' y' acc_upd &
list_foldl2o f acc_upd xs' ys' acc' }
}
let rec list_foldr2o f acc xs ys acc' = ocanren { let rec list_foldr2o f acc xs ys acc' = ocanren {
xs == [] & ys == [] & acc' == acc | xs == [] & ys == [] & acc' == acc |
{ fresh x', xs', y', ys', acc_upd in { fresh x', xs', y', ys', acc_upd in
xs == x' :: xs' & xs == x' :: xs' &
ys == y' :: ys' & ys == y' :: ys' &
list_foldr2o f acc xs' ys' acc_upd & f acc x' y' acc_upd &
f acc_upd x' y' acc' } list_foldr2o f acc_upd xs' ys' acc' }
} }
let rec list_foldl3o f acc xs ys zs acc' = ocanren { let rec list_foldl2o f acc xs ys acc' = ocanren {
xs == [] & ys == [] & zs == [] & acc' == acc | xs == [] & ys == [] & acc' == acc |
{ fresh x', xs', y', ys', z', zs', acc_upd in { fresh x', xs', y', ys', acc_upd in
xs == x' :: xs' & xs == x' :: xs' &
ys == y' :: ys' & ys == y' :: ys' &
zs == z' :: zs' & list_foldl2o f acc xs' ys' acc_upd &
f acc x' y' z' acc_upd & f acc_upd x' y' acc' }
list_foldl3o f acc_upd xs' ys' zs' acc' }
} }
let rec list_foldr3o f acc xs ys zs acc' = ocanren { let rec list_foldr3o f acc xs ys zs acc' = ocanren {
@ -346,7 +333,17 @@ struct
xs == x' :: xs' & xs == x' :: xs' &
ys == y' :: ys' & ys == y' :: ys' &
zs == z' :: zs' & zs == z' :: zs' &
list_foldr3o f acc xs' ys' zs' acc_upd & f acc x' y' z' acc_upd &
list_foldr3o f acc_upd xs' ys' zs' acc' }
}
let rec list_foldl3o f acc xs ys zs acc' = ocanren {
xs == [] & ys == [] & zs == [] & acc' == acc |
{ fresh x', xs', y', ys', z', zs', acc_upd in
xs == x' :: xs' &
ys == y' :: ys' &
zs == z' :: zs' &
list_foldl3o f acc xs' ys' zs' acc_upd &
f acc_upd x' y' z' acc' } f acc_upd x' y' z' acc' }
} }
@ -611,30 +608,22 @@ struct
let add_declo st x d st' = let add_declo st x d st' =
let open StEnv in let open StEnv in
let open Decl in let open Decl in
let open Value in
let open Type in
ocanren { ocanren {
fresh mem, types, vals in fresh mem, types, vals in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals) &
{ {
{ fresh tp, e, v, { fresh tp, e, v,
mem_cp, v_cp, mem_with_v_cp, mem_cp, v_cp,
mem_add, id_add, mem_with_id_add, mem_add, id_add,
types', vals' in types', vals' in
d == VarD (tp, e) & d == VarD (tp, e) &
exprvalo mem vals e v & exprvalo mem vals e v &
valcopyo mem v tp (Pair.pair mem_cp v_cp) & valcopyo mem v tp mem_with_v_cp &
mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & Pair.pair mem_cp v_cp == mem_with_v_cp &
mem_addo mem_cp v_cp mem_with_id_add &
Pair.pair mem_add id_add == mem_with_id_add &
types_glob_addo types x tp types' & types_glob_addo types x tp types' &
vals_glob_addo vals x id_add vals' & vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals') } |
{ fresh tps, s,
mem_add, id_add,
types', vals' in
d == FunD (tps, s) &
mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) &
types_glob_addo types x (FunT tps) types' &
vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals') st' == StEnv (mem_add, types', vals')
} }
} }
@ -655,7 +644,7 @@ struct
} }
(* TODO: better way ??? *) (* TODO: better way ??? *)
let globals_min_ido x = ocanren { x == 10 } let globals_min_ido x = ocanren { x == 1000 }
let prog_init_foldero st_with_id d st_with_id' = let prog_init_foldero st_with_id d st_with_id' =
ocanren { ocanren {
@ -686,12 +675,12 @@ struct
let open Mode in let open Mode in
let open CopyCap in let open CopyCap in
ocanren { ocanren {
{ r == NRd | r == Rd & v == ZeroV } & { r == NRd | v == ZeroV } &
{ r == NRd | r == Rd & is_ino m } & { r == NRd | is_ino m } &
{ is_not_outo m | is_outo m & w == AlwaysWr } & { is_not_outo m | w == AlwaysWr } &
{ w == NeverWr | { w == NeverWr |
w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp | { is_not_outo m & c == Cp } |
w =/= NeverWr & w' == AlwaysWr } & w' == AlwaysWr } &
is_trivial_vo v is_trivial_vo v
} }
@ -721,12 +710,8 @@ struct
{ is_outo m & { is_outo m &
w == AlwaysWr & w == AlwaysWr &
mem_with_v' == Std.pair mem ZeroV } | mem_with_v' == Std.pair mem ZeroV } |
{ { is_outo m | { { is_outo m | c == Cp | w == NeverWr } &
is_not_outo m & c == Cp | { is_not_outo m | w == MayWr | w == NeverWr } &
is_not_outo m & c == Rf & w == NeverWr } &
{ is_not_outo m |
is_outo m & w == MayWr |
is_outo m & w == NeverWr } &
mem_with_v' == Std.pair mem v } mem_with_v' == Std.pair mem v }
} } | } } |
{ fresh ts, us, _stmts in { fresh ts, us, _stmts in
@ -860,8 +845,8 @@ struct
{ fresh f, es, v, tp, { fresh f, es, v, tp,
glob_tps, _tps, glob_tps, _tps,
glob_vs, _vs, glob_vs, _vs,
types_call, vals_call, types', vals',
fstmts, tps, st_call, fstmts, tps, st',
state_with_args, _arg_id, state_with_args, _arg_id,
_states_evaled, mem_spoiled in _states_evaled, mem_spoiled in
s == CallS (f, es) & s == CallS (f, es) &
@ -869,13 +854,13 @@ struct
pathtypeo types f tp & pathtypeo types f tp &
types == TypesEnv (glob_tps, _tps) & types == TypesEnv (glob_tps, _tps) &
vals == ValsEnv (glob_vs, _vs) & vals == ValsEnv (glob_vs, _vs) &
types_call == TypesEnv (glob_tps, glob_tps) & types' == TypesEnv (glob_tps, glob_tps) &
vals_call == ValsEnv (glob_vs, glob_vs) & vals' == ValsEnv (glob_vs, glob_vs) &
v == FunV fstmts & v == FunV fstmts &
tp == FunT tps & tp == FunT tps &
st_call == StEnv (mem, types_call, vals_call) & st' == StEnv (mem, types', vals') &
list_foldl2o (stmt_addarg_foldero vals) list_foldl2o (stmt_addarg_foldero vals)
(Std.pair st_call 0) tps es (Std.pair st' 0) tps es
(Std.pair state_with_args _arg_id) & (Std.pair state_with_args _arg_id) &
List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
(* TODO: FIXME check left or right order *) (* TODO: FIXME check left or right order *)
@ -922,9 +907,12 @@ struct
let prog_evalo prog st' = let prog_evalo prog st' =
let open Prg in let open Prg in
let open Stmt in
ocanren { ocanren {
fresh decls, s, init_st in fresh decls, s, init_st in
prog == Prg (decls, s) & prog == Prg (decls, s) &
decls == [] &
s == SkipS &
prog_inito prog init_st & prog_inito prog init_st &
stmt_evalo init_st s st' stmt_evalo init_st s st'
} }

21
model_with_structures/tests.ml
View file

@ -2,27 +2,8 @@ open Tests_f
open Synthesizer open Synthesizer
open Relational open Relational
(* - basic var tests *) let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ());
let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ());
[%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}] [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}]
let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ());
[%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
let%expect_test "simple var, forbidden read" = print_endline(prog_eval_t_simple_var_fbd_rd ());
[%expect {| [] |}]
let%expect_test "simple vars, no read & read" = print_endline(prog_eval_t_simple_vars_fbd_rd_rd ());
[%expect {| [StEnv (MemEnv ([ZeroV; BotV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ());
[%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
let%expect_test "simple var, forbidden write" = print_endline(prog_eval_t_simple_var_fbd_wr ());
[%expect {| [] |}]
let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_var_wr_rd ());
[%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
(* - basic call tests *)
let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ());
[%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); ZeroV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
(* type tests *) (* type tests *)
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)

106
model_with_structures/tests_f.ml
View file

@ -4,115 +4,17 @@ open GT
open OCanren open OCanren
open OCanren.Std open OCanren.Std
open Prg
open Stmt
open Decl
open Type
open Expr
open Path
open ReadCap
open WriteCap
open InCap
open OutCap
open Mode
@type answer = StEnv.ground GT.list with show @type answer = StEnv.ground GT.list with show
(* - shortcuts *) let prog_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Prg in
(* TODO *) let open Stmt in
ocanren {
(* - basic var tests *)
let prog_eval_t_empty _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog in fresh prog in
prog == Prg ([], SkipS) & prog == Prg ([], SkipS) &
prog_evalo prog q}) prog_evalo prog q})
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg in
globals_min_ido xg &
prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP xg)) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
(* NOTE: does not work well for tests :( *)
(* let prog_eval_t2_simple_var_ans _ = show(answer) (Stream.take (run q *)
(* (fun q -> ocanren { *)
(* fresh xg in *)
(* globals_min_ido xg & *)
(* q == StEnv (MemEnv ([ZeroV], 1), *)
(* TypesEnv ([(xg, UnitT (Rd, MayWr))], *)
(* [(xg, UnitT (Rd, MayWr))]), *)
(* ValsEnv ([(xg, 0)], [(xg, 0)])) }) *)
(* (fun q -> q#reify (StEnv.prj_exn)))) *)
let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg in
globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
ReadS (VarP xg)) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg, yg in
globals_min_ido xg &
yg == Nat.s xg &
prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE);
VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP yg)) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg in
globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
WriteS (VarP xg)) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg in
globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)],
WriteS (VarP xg)) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg in
globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
SeqS (WriteS (VarP xg),
ReadS (VarP xg))) &
prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn))))
(* - basic call tests *)
let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren {
fresh prog, xg, fg, xd, fd, st in
globals_min_ido xg &
fg == Nat.s xg &
xd == VarD (UnitT (Rd, NeverWr), UnitE) &
fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) &
prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) &
prog_evalo prog q
})
(fun q -> q#reify (StEnv.prj_exn))))
(* @type answerArgs = (Arg.ground List.ground) GT.list with show *) (* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
(* @type answerValue = Value.ground GT.list with show *) (* @type answerValue = Value.ground GT.list with show *)
(* @type answerNat = Nat.ground GT.list with show *) (* @type answerNat = Nat.ground GT.list with show *)