mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-10 19:28:16 +00:00
struct: synt. left & right fold fix (swap), simple var synt. tests, fixes, not working (yet) call test
This commit is contained in:
ProgramSnail
parent
ee8ff429cf
commit
130079f7bd
4 changed files with 191 additions and 61 deletions
|
|
@ -519,12 +519,14 @@ struct
|
|||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var" =
|
||||
prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id));
|
||||
prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)],
|
||||
ReadS (VarP globals_min_id));
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var, no read" =
|
||||
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
|
||||
let%expect_test "simple var, forbidden read" =
|
||||
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
|
||||
ReadS (VarP globals_min_id));
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read: spoiled value |}]
|
||||
|
|
@ -537,19 +539,22 @@ struct
|
|||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var, write" =
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id));
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
|
||||
WriteS (VarP globals_min_id));
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var, no write" =
|
||||
try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id));
|
||||
let%expect_test "simple var, forbidden write" =
|
||||
try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)],
|
||||
WriteS (VarP globals_min_id));
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| write: write tag |}]
|
||||
|
||||
let%expect_test "simple var, write & read" =
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id),
|
||||
ReadS (VarP globals_min_id)));
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
|
||||
SeqS (WriteS (VarP globals_min_id),
|
||||
ReadS (VarP globals_min_id)));
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
|
|
@ -557,7 +562,7 @@ struct
|
|||
|
||||
(* let%expect_test "simple call with read" = *)
|
||||
(* 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), *)
|
||||
(* [PathE (VarP globals_min_id)])); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
|
|
@ -566,7 +571,7 @@ struct
|
|||
(* let%expect_test "simple call with write" = *)
|
||||
(* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
|
||||
(* 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), *)
|
||||
(* [PathE (VarP (globals_min_id + 1))])); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
|
|
|
|||
|
|
@ -1,3 +1,6 @@
|
|||
(* NOTE: in previous models foldl & foldr are probably spapped
|
||||
<- TODO: fix ? *)
|
||||
|
||||
module Relational =
|
||||
struct
|
||||
open GT
|
||||
|
|
@ -145,9 +148,9 @@ struct
|
|||
module Decl = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%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 }]
|
||||
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
|
||||
|
||||
|
|
@ -291,50 +294,40 @@ struct
|
|||
}
|
||||
|
||||
|
||||
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 |
|
||||
{ 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 {
|
||||
xs == [] & acc' == acc |
|
||||
{ fresh x', xs', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
f acc x' acc_upd &
|
||||
list_foldro f acc_upd xs' acc' }
|
||||
list_foldlo f acc_upd xs' acc' }
|
||||
(* TODO: inf search on swap, investigate *)
|
||||
}
|
||||
|
||||
|
||||
let rec list_foldr2o 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_foldr2o f acc_upd xs' ys' acc' }
|
||||
}
|
||||
|
||||
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' &
|
||||
list_foldl2o f acc xs' ys' acc_upd &
|
||||
f acc_upd x' y' acc' }
|
||||
f acc x' y' acc_upd &
|
||||
list_foldl2o f acc_upd xs' ys' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldr3o f acc xs ys zs acc' = ocanren {
|
||||
xs == [] & ys == [] & zs == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', z', zs', acc_upd in
|
||||
let rec list_foldr2o f acc xs ys acc' = ocanren {
|
||||
xs == [] & ys == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
zs == z' :: zs' &
|
||||
f acc x' y' z' acc_upd &
|
||||
list_foldr3o f acc_upd xs' ys' zs' acc' }
|
||||
list_foldr2o f acc xs' ys' acc_upd &
|
||||
f acc_upd x' y' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldl3o f acc xs ys zs acc' = ocanren {
|
||||
|
|
@ -343,7 +336,17 @@ struct
|
|||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
zs == z' :: zs' &
|
||||
list_foldl3o f acc xs' ys' zs' acc_upd &
|
||||
f acc x' y' z' acc_upd &
|
||||
list_foldl3o f acc_upd xs' ys' zs' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldr3o 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_foldr3o f acc xs' ys' zs' acc_upd &
|
||||
f acc_upd x' y' z' acc' }
|
||||
}
|
||||
|
||||
|
|
@ -608,24 +611,32 @@ struct
|
|||
let add_declo st x d st' =
|
||||
let open StEnv in
|
||||
let open Decl in
|
||||
let open Value in
|
||||
let open Type in
|
||||
ocanren {
|
||||
fresh mem, types, vals in
|
||||
st == StEnv (mem, types, vals) &
|
||||
{
|
||||
{ fresh tp, e, v,
|
||||
mem_with_v_cp, mem_cp, v_cp,
|
||||
mem_with_id_add, mem_add, id_add,
|
||||
mem_cp, v_cp,
|
||||
mem_add, id_add,
|
||||
types', vals' in
|
||||
d == VarD (tp, e) &
|
||||
exprvalo mem vals e v &
|
||||
valcopyo mem v tp mem_with_v_cp &
|
||||
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 &
|
||||
valcopyo mem v tp (Pair.pair mem_cp v_cp) &
|
||||
mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
|
||||
types_glob_addo types x tp types' &
|
||||
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')
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -644,7 +655,7 @@ struct
|
|||
}
|
||||
|
||||
(* TODO: better way ??? *)
|
||||
let globals_min_ido x = ocanren { x == 1000 }
|
||||
let globals_min_ido x = ocanren { x == 10 }
|
||||
|
||||
let prog_init_foldero st_with_id d st_with_id' =
|
||||
ocanren {
|
||||
|
|
@ -845,8 +856,8 @@ struct
|
|||
{ fresh f, es, v, tp,
|
||||
glob_tps, _tps,
|
||||
glob_vs, _vs,
|
||||
types', vals',
|
||||
fstmts, tps, st',
|
||||
types_call, vals_call,
|
||||
fstmts, tps, st_call,
|
||||
state_with_args, _arg_id,
|
||||
_states_evaled, mem_spoiled in
|
||||
s == CallS (f, es) &
|
||||
|
|
@ -854,13 +865,13 @@ struct
|
|||
pathtypeo types f tp &
|
||||
types == TypesEnv (glob_tps, _tps) &
|
||||
vals == ValsEnv (glob_vs, _vs) &
|
||||
types' == TypesEnv (glob_tps, glob_tps) &
|
||||
vals' == ValsEnv (glob_vs, glob_vs) &
|
||||
types_call == TypesEnv (glob_tps, glob_tps) &
|
||||
vals_call == ValsEnv (glob_vs, glob_vs) &
|
||||
v == FunV fstmts &
|
||||
tp == FunT tps &
|
||||
st' == StEnv (mem, types', vals') &
|
||||
st_call == StEnv (mem, types_call, vals_call) &
|
||||
list_foldl2o (stmt_addarg_foldero vals)
|
||||
(Std.pair st' 0) tps es
|
||||
(Std.pair st_call 0) tps es
|
||||
(Std.pair state_with_args _arg_id) &
|
||||
List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
|
||||
(* TODO: FIXME check left or right order *)
|
||||
|
|
@ -907,12 +918,9 @@ struct
|
|||
|
||||
let prog_evalo prog st' =
|
||||
let open Prg in
|
||||
let open Stmt in
|
||||
ocanren {
|
||||
fresh decls, s, init_st in
|
||||
prog == Prg (decls, s) &
|
||||
decls == [] &
|
||||
s == SkipS &
|
||||
prog_inito prog init_st &
|
||||
stmt_evalo init_st s st'
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2,8 +2,27 @@ open Tests_f
|
|||
open Synthesizer
|
||||
open Relational
|
||||
|
||||
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ());
|
||||
(* - basic var tests *)
|
||||
|
||||
let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ());
|
||||
[%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 {| [123] |}]
|
||||
|
||||
(* type tests *)
|
||||
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
|
||||
|
|
|
|||
|
|
@ -4,17 +4,115 @@ open GT
|
|||
open OCanren
|
||||
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
|
||||
|
||||
let prog_eval_t1 _ = show(answer) (Stream.take (run q
|
||||
(fun q -> let open Prg in
|
||||
let open Stmt in
|
||||
ocanren {
|
||||
(* - shortcuts *)
|
||||
|
||||
(* TODO *)
|
||||
|
||||
(* - basic var tests *)
|
||||
|
||||
let prog_eval_t_empty _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog in
|
||||
prog == Prg ([], SkipS) &
|
||||
prog_evalo prog q})
|
||||
(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 answerValue = Value.ground GT.list with show *)
|
||||
(* @type answerNat = Nat.ground GT.list with show *)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue