mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
No commits in common. "64935b3c7e65c6c198fae814245ac77c328d61f4" and "2cc87d74dfc33eef1d6d67f030c874e0765d76f0" have entirely different histories.
64935b3c7e
...
2cc87d74df
4 changed files with 700 additions and 481 deletions
|
|
@ -80,8 +80,7 @@ struct
|
|||
type mem = value list * memid (* NOTE: memory and first free elem *)
|
||||
type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
|
||||
type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
|
||||
type visited = stmt list (* TODO: FIXME: optimize, use ids *)
|
||||
type state = mem * types * vals * visited
|
||||
type state = mem * types * vals
|
||||
|
||||
(* --- *)
|
||||
|
||||
|
|
@ -254,16 +253,16 @@ struct
|
|||
|
||||
(* TODO: check new in vars *)
|
||||
let add_decl (state : state) (x : data) (d : decl) : state =
|
||||
match state with (mem, types, vals, visited) -> match d with
|
||||
match state with (mem, types, vals) -> match d with
|
||||
| VarD (t, e) -> let v = exprval mem vals e in
|
||||
let (mem', v') = valcopy mem v t in
|
||||
let (mem'', id) = mem_add mem' v' in
|
||||
(mem'', types_glob_add types x t, vals_glob_add vals x id, visited)
|
||||
(mem'', types_glob_add types x t, vals_glob_add vals x id)
|
||||
| FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in
|
||||
(mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited)
|
||||
(mem', types_glob_add types x (FunT ts), vals_glob_add vals x id)
|
||||
|
||||
let empty_mem : mem = ([], 0)
|
||||
let empty_state : state = (empty_mem, ([], []), ([], []), [])
|
||||
let empty_state : state = (empty_mem, ([], []), ([], []))
|
||||
|
||||
(* TODO: better way ??? *)
|
||||
let globals_min_id : data = 1000
|
||||
|
|
@ -322,7 +321,7 @@ struct
|
|||
(* full spoil *)
|
||||
|
||||
let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
|
||||
match state with (mem, types, vals, visited) ->
|
||||
match state with (mem, types, vals) ->
|
||||
let x = pathvar p in
|
||||
let id = vals_assoc x vals in (* base var address *)
|
||||
let b = pathval mem vals p in (* subvalue in var *)
|
||||
|
|
@ -333,25 +332,25 @@ struct
|
|||
mem_set mem'' id v''
|
||||
|
||||
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
|
||||
match state with (mem, types, vals, visited) -> match e, t with
|
||||
match state with (mem, types, vals) -> match e, t with
|
||||
| UnitE, UnitT _ -> mem
|
||||
| PathE p, t -> argsspoilp state m t p
|
||||
| RefE x, t -> argsspoilp state m t (VarP x)
|
||||
(* TODO: FIXME: check RefE case ? *)
|
||||
| TupleE es, TupleT ts -> List.fold_left2
|
||||
(fun mem' t' e' -> argsspoile (mem', types, vals, visited) m t' e')
|
||||
(fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
|
||||
mem ts es
|
||||
| _, _ -> raise @@ Typing_error "valspoile"
|
||||
|
||||
(* - funciton argument addition *)
|
||||
|
||||
let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
|
||||
match state with (mem, types, vals, visited) ->
|
||||
match state with (mem, types, vals) ->
|
||||
let v = exprval mem oldvals e in
|
||||
(* let t' = pathtype types p in *)
|
||||
let (mem', v') = valcopy mem v t in
|
||||
let (mem'', id) = mem_add mem' v' in
|
||||
(mem'', types_add types x t, vals_add vals x id, visited)
|
||||
(mem'', types_add types x t, vals_add vals x id)
|
||||
|
||||
(* - function evaluation *)
|
||||
(* NOTE: not needed due to performed optimization in stmt_eval *)
|
||||
|
|
@ -360,7 +359,8 @@ struct
|
|||
(* - statement evaluation *)
|
||||
|
||||
let rec stmt_eval (state : state) (s : stmt) : state =
|
||||
match state with (mem, types, vals, visited) -> match s with
|
||||
match state with (mem, types, vals) -> match s with
|
||||
(* TODO: FIXME: Add memoization *)
|
||||
| SkipS -> state
|
||||
| CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
|
||||
pathval mem vals f in
|
||||
|
|
@ -370,26 +370,19 @@ struct
|
|||
let vals' : vals = (fst vals, fst vals) in
|
||||
(match v, t with
|
||||
| FunV (* xs, *) fstmts (* ) *), FunT ts ->
|
||||
(* TODO: memoisation of the called functions *)
|
||||
let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
|
||||
List.fold_left2 (* TODO: FIXME: check x's order *)
|
||||
(fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
|
||||
((mem, types', vals', visited), 0) ts es in
|
||||
((mem, types', vals'), 0) ts es in
|
||||
(* NOTE: same x's, so can use same args for all the statements *)
|
||||
(match state_with_args with (mem_swa, types_swa, vals_swa, visited_swa) ->
|
||||
let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *)
|
||||
List.fold_left
|
||||
(fun visited_old stmt ->
|
||||
if List.mem stmt visited_old
|
||||
then stmt :: visited_old
|
||||
else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
|
||||
(_, _, _, visited_after_stmt) -> visited_after_stmt)
|
||||
visited_swa
|
||||
fstmts in
|
||||
let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *)
|
||||
List.map (stmt_eval state_with_args) fstmts in
|
||||
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
|
||||
List.fold_left2
|
||||
(fun mem (m, t) e -> argsspoile (mem, types, vals, (* NOTE: not important *) visited_new) m t e)
|
||||
(fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
|
||||
mem ts es in
|
||||
(mem_spoiled, types, vals, visited_new))
|
||||
(mem_spoiled, types, vals)
|
||||
| FunV _, _ -> raise @@ Eval_error "call: function type"
|
||||
| _, FunT _ -> raise @@ Eval_error "call: function val"
|
||||
| _, _ -> raise @@ Eval_error "call: function type & val")
|
||||
|
|
@ -400,7 +393,7 @@ struct
|
|||
else let x = pathvar p in
|
||||
let id = vals_assoc x vals in
|
||||
let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
|
||||
(mem_set mem' id v', types, vals, visited)
|
||||
(mem_set mem' id v', types, vals)
|
||||
| _ -> raise @@ Eval_error "write: type")
|
||||
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
|
||||
then raise @@ Eval_error "read: spoiled value"
|
||||
|
|
@ -411,12 +404,11 @@ struct
|
|||
stmt_eval statel sr
|
||||
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
let stater = stmt_eval state sr in
|
||||
match statel with (meml, typesl, valsl, visitedl) ->
|
||||
match stater with (memr, typesr, valsr, visitedr) ->
|
||||
match statel with (meml, typesl, valsl) ->
|
||||
match stater with (memr, typesr, valsr) ->
|
||||
if typesl != typesr || valsl != valsr
|
||||
then raise @@ Eval_error "choice"
|
||||
(* TODO: FIXME: better list union ?? *)
|
||||
else (memcomb meml memr, typesl, valsl, visitedl @ visitedr)
|
||||
else (memcomb meml memr, typesl, valsl)
|
||||
|
||||
(* --- program execution --- *)
|
||||
|
||||
|
|
@ -718,24 +710,6 @@ struct
|
|||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* NOTE: memoization used *)
|
||||
let%expect_test "call inside call, recursive, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_aw],
|
||||
(callS vg2 [pE v0]) #.
|
||||
(wrS @@ drf @@ v0)
|
||||
)
|
||||
],
|
||||
(callS vg2 [pE vg1]) #.
|
||||
(rdS @@ drf @@ vg1)
|
||||
);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "call to fix after call, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
|
|
|
|||
|
|
@ -203,26 +203,69 @@ struct
|
|||
]
|
||||
end
|
||||
|
||||
module VisitedEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec 'sl t = VisitedEnv of 'sl
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = (Stmt.ground List.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
module StEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited
|
||||
type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t
|
||||
type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* - state utils *)
|
||||
|
||||
let types_assoco id types tp =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh _glob_tps, tps in
|
||||
types == TypesEnv (_glob_tps, tps) &
|
||||
List.assoco id tps tp
|
||||
}
|
||||
|
||||
let vals_assoco id vals v =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh _glob_vs, vs in
|
||||
vals == ValsEnv (_glob_vs, vs) &
|
||||
List.assoco id vs v
|
||||
}
|
||||
|
||||
let types_glob_addo types x tp types' =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh glob_tps, tps in
|
||||
types == TypesEnv (glob_tps, tps) &
|
||||
types' == TypesEnv ((Std.pair x tp) :: glob_tps,
|
||||
(Std.pair x tp) :: tps)
|
||||
}
|
||||
|
||||
let types_addo types x tp types' =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh glob_tps, tps in
|
||||
types == TypesEnv (glob_tps, tps) &
|
||||
types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
|
||||
}
|
||||
|
||||
let vals_glob_addo vals x v vals' =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh glob_vs, vs in
|
||||
vals == ValsEnv (glob_vs, vs) &
|
||||
vals' == ValsEnv ((Std.pair x v) :: glob_vs,
|
||||
(Std.pair x v) :: vs)
|
||||
}
|
||||
|
||||
let vals_addo vals x v vals' =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh glob_vs, vs in
|
||||
vals == ValsEnv (glob_vs, vs) &
|
||||
vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
|
||||
}
|
||||
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replaceo xs id value ys = ocanren {
|
||||
|
|
@ -250,13 +293,6 @@ struct
|
|||
list_ntho xs' id' x' }
|
||||
}
|
||||
|
||||
let rec list_not_membero xs x = ocanren {
|
||||
xs == [] |
|
||||
{ fresh x', xs' in
|
||||
xs == x' :: xs' &
|
||||
x' =/= x &
|
||||
list_not_membero xs' x }
|
||||
}
|
||||
|
||||
let rec list_foldro f acc xs acc' = ocanren {
|
||||
xs == [] & acc' == acc |
|
||||
|
|
@ -332,92 +368,6 @@ struct
|
|||
{ xs == [] & ys == [] & zs == [] }
|
||||
}
|
||||
|
||||
(* - state utils *)
|
||||
|
||||
let types_assoco id types tp =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh _glob_tps, tps in
|
||||
types == TypesEnv (_glob_tps, tps) &
|
||||
List.assoco id tps tp
|
||||
}
|
||||
|
||||
let vals_assoco id vals v =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh _glob_vs, vs in
|
||||
vals == ValsEnv (_glob_vs, vs) &
|
||||
List.assoco id vs v
|
||||
}
|
||||
|
||||
let types_glob_addo types x tp types' =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh glob_tps, tps in
|
||||
types == TypesEnv (glob_tps, tps) &
|
||||
types' == TypesEnv ((Std.pair x tp) :: glob_tps,
|
||||
(Std.pair x tp) :: tps)
|
||||
}
|
||||
|
||||
let types_addo types x tp types' =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh glob_tps, tps in
|
||||
types == TypesEnv (glob_tps, tps) &
|
||||
types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
|
||||
}
|
||||
|
||||
let vals_glob_addo vals x v vals' =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh glob_vs, vs in
|
||||
vals == ValsEnv (glob_vs, vs) &
|
||||
vals' == ValsEnv ((Std.pair x v) :: glob_vs,
|
||||
(Std.pair x v) :: vs)
|
||||
}
|
||||
|
||||
let vals_addo vals x v vals' =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh glob_vs, vs in
|
||||
vals == ValsEnv (glob_vs, vs) &
|
||||
vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
|
||||
}
|
||||
|
||||
let visited_appendo visitedl visitedr visited' =
|
||||
let open VisitedEnv in
|
||||
ocanren {
|
||||
fresh vsl, vsr, vs' in
|
||||
visitedl == VisitedEnv vsl &
|
||||
visitedr == VisitedEnv vsr &
|
||||
List.appendo vsl vsr vs' &
|
||||
visited' == VisitedEnv vs'
|
||||
}
|
||||
|
||||
let visited_checko visited stmt =
|
||||
let open VisitedEnv in
|
||||
ocanren {
|
||||
fresh vs in
|
||||
visited == VisitedEnv vs &
|
||||
List.membero vs stmt
|
||||
}
|
||||
|
||||
let not_visited_checko visited stmt =
|
||||
let open VisitedEnv in
|
||||
ocanren {
|
||||
fresh vs in
|
||||
visited == VisitedEnv vs &
|
||||
list_not_membero vs stmt
|
||||
}
|
||||
|
||||
let visited_addo visited stmt visited' =
|
||||
let open VisitedEnv in
|
||||
ocanren {
|
||||
fresh vs in
|
||||
visited == VisitedEnv vs &
|
||||
visited' == VisitedEnv (stmt :: vs)
|
||||
}
|
||||
|
||||
(* --- *)
|
||||
|
||||
let mem_geto mem id v =
|
||||
|
|
@ -661,8 +611,8 @@ struct
|
|||
let open Value in
|
||||
let open Type in
|
||||
ocanren {
|
||||
fresh mem, types, vals, visited in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
fresh mem, types, vals in
|
||||
st == StEnv (mem, types, vals) &
|
||||
{
|
||||
{ fresh tp, e, v,
|
||||
mem_cp, v_cp,
|
||||
|
|
@ -674,7 +624,7 @@ struct
|
|||
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', visited) } |
|
||||
st' == StEnv (mem_add, types', vals') } |
|
||||
{ fresh tps, s,
|
||||
mem_add, id_add,
|
||||
types', vals' in
|
||||
|
|
@ -682,7 +632,7 @@ struct
|
|||
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', visited)
|
||||
st' == StEnv (mem_add, types', vals')
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -695,11 +645,10 @@ struct
|
|||
let open StEnv in
|
||||
let open TypesEnv in
|
||||
let open ValsEnv in
|
||||
let open VisitedEnv in
|
||||
ocanren {
|
||||
fresh m in
|
||||
empty_memo m &
|
||||
st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv [])
|
||||
st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []))
|
||||
}
|
||||
|
||||
(* TODO: better way ??? *)
|
||||
|
|
@ -808,10 +757,9 @@ struct
|
|||
let open StEnv in
|
||||
let open CopyCap in
|
||||
ocanren {
|
||||
fresh mem, types, vals, visited,
|
||||
x, id, b, tp',
|
||||
fresh mem, types, vals, x, id, b, tp',
|
||||
mem_sp, b_sp, v_sp, mem_upd, v_upd in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
st == StEnv (mem, types, vals) &
|
||||
pathvaro p x &
|
||||
vals_assoco x vals id &
|
||||
pathvalo mem vals p b &
|
||||
|
|
@ -822,11 +770,11 @@ struct
|
|||
mem_seto mem_upd id v_upd mem'
|
||||
}
|
||||
|
||||
let rec argspoile_foldero types vals visited m mem tp e mem' =
|
||||
let rec argspoile_foldero types vals m mem tp e mem' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
fresh st in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
st == StEnv (mem, types, vals) &
|
||||
argspoileo st m tp e mem'
|
||||
}
|
||||
and argspoileo st m tp e mem' =
|
||||
|
|
@ -835,8 +783,8 @@ struct
|
|||
let open Type in
|
||||
let open Path in
|
||||
ocanren {
|
||||
fresh _r, _w, mem, types, vals, visited in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
fresh _r, _w, mem, types, vals in
|
||||
st == StEnv (mem, types, vals) &
|
||||
{
|
||||
{ e == UnitE &
|
||||
tp == UnitT (_r, _w) &
|
||||
|
|
@ -850,7 +798,7 @@ struct
|
|||
{ fresh es, tps in
|
||||
e == TupleE es &
|
||||
tp == TupleT tps &
|
||||
list_foldl2o (argspoile_foldero types vals visited m) mem tps es mem'}
|
||||
list_foldl2o (argspoile_foldero types vals m) mem tps es mem'}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -859,17 +807,17 @@ struct
|
|||
let addargo st oldvals x tp e st' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
fresh mem, types, vals, visited, v,
|
||||
fresh mem, types, vals, v,
|
||||
mem_cp, v_cp,
|
||||
mem_add, id_add,
|
||||
types', vals' in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
st == StEnv (mem, types, vals) &
|
||||
exprvalo mem oldvals e v &
|
||||
valcopyo mem v tp (Std.pair mem_cp v_cp) &
|
||||
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
|
||||
types_addo types x tp types' &
|
||||
vals_addo vals x id_add vals' &
|
||||
st' == StEnv (mem_add, types', vals', visited)
|
||||
st' == StEnv (mem_add, types', vals')
|
||||
}
|
||||
|
||||
(* - function evaluation *)
|
||||
|
|
@ -885,25 +833,12 @@ struct
|
|||
addargo st vals x tp e st' &
|
||||
st_with_id' == Std.pair st' (Nat.s x)
|
||||
}
|
||||
and stmt_eval_func_foldero mem types vals visited stmt visited' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
{ fresh visited_add, st,
|
||||
st', mem', types', vals' in
|
||||
not_visited_checko visited stmt &
|
||||
visited_addo visited stmt visited_add &
|
||||
st == StEnv (mem, types, vals, visited_add) &
|
||||
stmt_evalo st stmt st' &
|
||||
st' == StEnv (mem', types', vals', visited') } |
|
||||
{ visited_checko visited stmt &
|
||||
visited == visited' }
|
||||
}
|
||||
and stmt_eval_spoil_foldero types vals visited mem mtp e mem' =
|
||||
and stmt_eval_spoil_foldero types vals mem mtp e mem' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
fresh m, tp, st in
|
||||
Std.pair m tp == mtp &
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
st == StEnv (mem, types, vals) &
|
||||
argspoileo st m tp e mem'
|
||||
}
|
||||
and stmt_evalo st s st' =
|
||||
|
|
@ -915,8 +850,8 @@ struct
|
|||
let open TypesEnv in
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh mem, types, vals, visited in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
fresh mem, types, vals in
|
||||
st == StEnv (mem, types, vals) &
|
||||
{
|
||||
{ s == SkipS & st == st' } |
|
||||
{ fresh f, es, v, tp,
|
||||
|
|
@ -924,11 +859,8 @@ struct
|
|||
glob_vs, _vs,
|
||||
types_call, vals_call,
|
||||
fstmts, tps, st_call,
|
||||
state_with_args,
|
||||
mem_swa, types_swa,
|
||||
vals_swa, visited_swa,
|
||||
_arg_id, mem_spoiled,
|
||||
visited' in
|
||||
state_with_args, _arg_id,
|
||||
_states_evaled, mem_spoiled in
|
||||
s == CallS (f, es) &
|
||||
pathvalo mem vals f v &
|
||||
pathtypeo types f tp &
|
||||
|
|
@ -938,16 +870,16 @@ struct
|
|||
vals_call == ValsEnv (glob_vs, glob_vs) &
|
||||
v == FunV fstmts &
|
||||
tp == FunT tps &
|
||||
st_call == StEnv (mem, types_call, vals_call, visited) &
|
||||
st_call == StEnv (mem, types_call, vals_call) &
|
||||
list_foldl2o (stmt_addarg_foldero vals)
|
||||
(Std.pair st_call 0) tps es
|
||||
(Std.pair state_with_args _arg_id) &
|
||||
state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) &
|
||||
list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' &
|
||||
List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
|
||||
(* TODO: FIXME check left or right order *)
|
||||
list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
|
||||
list_foldl2o (stmt_eval_spoil_foldero types vals)
|
||||
mem tps es mem_spoiled &
|
||||
st' == StEnv (mem_spoiled, types, vals, visited')
|
||||
(* st' == state_with_args *)
|
||||
st' == StEnv (mem_spoiled, types, vals)
|
||||
} |
|
||||
{ fresh p, tp, _r, w, x, id, v,
|
||||
mem_upd, v_upd, mem_set in
|
||||
|
|
@ -960,7 +892,7 @@ struct
|
|||
mem_geto mem id v &
|
||||
valupdo mem v p ZeroV (Std.pair mem_upd v_upd) &
|
||||
mem_seto mem_upd id v_upd mem_set &
|
||||
st' == StEnv (mem_set, types, vals, visited) } |
|
||||
st' == StEnv (mem_set, types, vals) } |
|
||||
{ fresh p in
|
||||
s == ReadS p &
|
||||
pathvalo mem vals p ZeroV &
|
||||
|
|
@ -970,19 +902,18 @@ struct
|
|||
stmt_evalo st sl stl &
|
||||
stmt_evalo stl sr st' } |
|
||||
{ fresh sl, sr, stl, str,
|
||||
meml, typesl, valsl, visitedl,
|
||||
memr, typesr, valsr, visitedr,
|
||||
visited', mem' in
|
||||
meml, typesl, valsl,
|
||||
memr, typesr, valsr,
|
||||
mem' in
|
||||
s == ChoiceS (sl, sr) &
|
||||
stmt_evalo st sl stl &
|
||||
stmt_evalo st sr str &
|
||||
stl == StEnv (meml, typesl, valsl, visitedl) &
|
||||
str == StEnv (memr, typesr, valsr, visitedr) &
|
||||
str == StEnv (memr, typesr, valsr) &
|
||||
stl == StEnv (meml, typesl, valsl) &
|
||||
typesl == typesr &
|
||||
valsl == valsr &
|
||||
memcombo meml memr mem' &
|
||||
visited_appendo visitedr visitedl visited' &
|
||||
st' == StEnv (mem', typesl, valsl, visited') }
|
||||
st' == StEnv (mem', typesl, valsl) }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -5,77 +5,97 @@ open Relational
|
|||
(* - basic var tests *)
|
||||
|
||||
let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ());
|
||||
[%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []), VisitedEnv ([]))] |}]
|
||||
[%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)]), VisitedEnv ([]))] |}]
|
||||
[%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)]), VisitedEnv ([]))] |}]
|
||||
[%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)]), VisitedEnv ([]))] |}]
|
||||
[%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)]), VisitedEnv ([]))] |}]
|
||||
[%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)]), VisitedEnv ([ReadS (VarP (O))]))] |}]
|
||||
[%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)]))] |}]
|
||||
|
||||
let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([ReadS (DerefP (VarP (O)))]))] |}]
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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 call with write" = print_endline(prog_eval_t_simple_call_wr ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}]
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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 call with read after write" = print_endline(prog_eval_t_simple_call_wr_rd ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]))] |}]
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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 call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ());
|
||||
[%expect {| [] |}]
|
||||
|
||||
let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}]
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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 call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ());
|
||||
[%expect {| [] |}]
|
||||
|
||||
let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}]
|
||||
(* type tests *)
|
||||
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, 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 (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 ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *)
|
||||
(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, 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 "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, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *)
|
||||
|
||||
let%expect_test "call inside call" = print_endline(prog_eval_t_call_in_call ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([WriteS (DerefP (VarP (O))); SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}]
|
||||
(* function tests *)
|
||||
(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *)
|
||||
(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *)
|
||||
(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [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 "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, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
|
||||
(* let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] *)
|
||||
(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] *)
|
||||
(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] *)
|
||||
(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] *)
|
||||
(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
|
||||
(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
|
||||
(* let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *)
|
||||
(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *)
|
||||
(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, 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, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
|
||||
(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
|
||||
(* 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 "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 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 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] *)
|
||||
(* let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] *)
|
||||
(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
|
||||
(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] *)
|
||||
(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] *)
|
||||
(* let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] *)
|
||||
(* let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] *)
|
||||
(* let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] *)
|
||||
(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *)
|
||||
(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *)
|
||||
(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
|
||||
(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
|
||||
(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] *)
|
||||
(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] *)
|
||||
(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] *)
|
||||
(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] *)
|
||||
(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
|
||||
|
||||
let%expect_test "call inside call, recursive" = print_endline(prog_eval_t_call_in_call_rec ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}]
|
||||
(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
|
||||
|
||||
let%expect_test "call to fix after call" = print_endline(prog_eval_t_fix_call_after_call ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}]
|
||||
|
||||
let%expect_test "simple call with global variable usage" = print_endline(prog_eval_t_call_with_glob_usage ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]))] |}]
|
||||
|
||||
let%expect_test "simple call with read & write (2 args)" = print_endline(prog_eval_t_call_with_rd_wr_2_args ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (O))); BotV; RefV (O); ZeroV], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}]
|
||||
|
||||
let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]))] |}]
|
||||
|
||||
let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ());
|
||||
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]))] |}]
|
||||
|
||||
(* - basic synthesis tests *)
|
||||
|
||||
let%expect_test "simple synthesis test" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr ());
|
||||
[%expect {| [Rf; Cp] |}]
|
||||
|
||||
let%expect_test "simple synthesis test, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr' ());
|
||||
[%expect {| [Rf; Rf; Rf; Rf; Cp; Cp; Cp; Cp] |}]
|
||||
|
||||
let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ());
|
||||
[%expect {| [Cp] |}]
|
||||
|
||||
let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ());
|
||||
[%expect {| [Cp; Cp; Cp; Cp] |}]
|
||||
|
|
|
|||
|
|
@ -18,25 +18,11 @@ open OutCap
|
|||
open Mode
|
||||
|
||||
@type answer = StEnv.ground GT.list with show
|
||||
@type answerCpCap = CopyCap.ground GT.list with show
|
||||
|
||||
(* - shortcuts *)
|
||||
(* - shortcuts *)
|
||||
|
||||
(* TODO *)
|
||||
|
||||
(* NOTE: redo with fold ?? *)
|
||||
let rec seqo stmts stmt' = ocanren {
|
||||
{ stmts == [] & stmt' == SkipS } |
|
||||
{ fresh s in
|
||||
stmts == [s] &
|
||||
stmt' == s } |
|
||||
{ fresh s, s', ss, stmt_rest' in
|
||||
stmts == s :: s' :: ss &
|
||||
seqo (s' :: ss) stmt_rest' &
|
||||
stmt' == SeqS(s, stmt_rest')
|
||||
}
|
||||
}
|
||||
|
||||
(* - basic var tests *)
|
||||
|
||||
let prog_eval_t_empty _ = show(answer) (Stream.take (run q
|
||||
|
|
@ -118,7 +104,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, fg, xd, fd in
|
||||
fresh prog, xg, fg, xd, fd, st in
|
||||
globals_min_ido xg &
|
||||
fg == Nat.s xg &
|
||||
xd == VarD (UnitT (Rd, NeverWr), UnitE) &
|
||||
|
|
@ -129,7 +115,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -143,7 +129,7 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -157,7 +143,7 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -172,7 +158,7 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -186,7 +172,7 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -200,7 +186,7 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -215,7 +201,7 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -231,7 +217,7 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in
|
||||
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
|
|
@ -241,43 +227,27 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
|
|||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
SeqS (CallS (VarP fg, [PathE (VarP 0)]),
|
||||
SeqS (CallS (VarP f2g, [PathE (VarP 0)]),
|
||||
WriteS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg)))) &
|
||||
prog_evalo prog q })
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
SeqS (CallS (VarP fg, [PathE (VarP 0)]),
|
||||
WriteS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg)))) &
|
||||
prog_evalo prog q })
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in
|
||||
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
f2g == Nat.s fg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg))))) &
|
||||
prog_evalo prog q })
|
||||
|
|
@ -285,13 +255,13 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
|
|||
|
||||
let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd in
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
SeqS (WriteS (VarP xg),
|
||||
ReadS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
|
|
@ -300,9 +270,9 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
|
|||
})
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
|
||||
let prog_eval_t_call_with_rd_wr_2_args_ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd in
|
||||
fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
x2g == Nat.s yg &
|
||||
|
|
@ -311,193 +281,517 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
|
|||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
|
||||
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
|
||||
(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
SeqS (ReadS (DerefP (VarP 0)),
|
||||
WriteS (DerefP (VarP 1)))) &
|
||||
prog == Prg ([xd; yd; x2d; y2d; fd],
|
||||
CallS (VarP fg, [PathE (VarP yg);
|
||||
PathE (VarP y2g)])) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) &
|
||||
prog_evalo prog q
|
||||
})
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg,
|
||||
x2g, y2g,
|
||||
x3g, y3g,
|
||||
x4g, y4g,
|
||||
fg,
|
||||
xd, yd,
|
||||
x2d, y2d,
|
||||
x3d, y3d,
|
||||
x4d, y4d,
|
||||
fd,
|
||||
fstmts,
|
||||
stmts in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
x2g == Nat.s yg &
|
||||
y2g == Nat.s x2g &
|
||||
x3g == Nat.s y2g &
|
||||
y3g == Nat.s x3g &
|
||||
x4g == Nat.s y3g &
|
||||
y4g == Nat.s x4g &
|
||||
fg == Nat.s y4g &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
|
||||
x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
|
||||
x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
|
||||
seqo [ReadS (DerefP (VarP 1));
|
||||
ReadS (DerefP (VarP 3));
|
||||
WriteS (DerefP (VarP 1));
|
||||
WriteS (DerefP (VarP 2));
|
||||
WriteS (DerefP (VarP 3))] fstmts &
|
||||
fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)));
|
||||
(Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
fstmts) &
|
||||
seqo [CallS (VarP fg, [PathE (VarP yg);
|
||||
PathE (VarP y2g);
|
||||
PathE (VarP y3g);
|
||||
PathE (VarP y4g)]);
|
||||
ReadS (DerefP (VarP yg));
|
||||
ReadS (DerefP (VarP y2g));
|
||||
ReadS (DerefP (VarP y3g));
|
||||
ReadS (DerefP (VarP y4g))] stmts &
|
||||
prog == Prg ([xd; yd;
|
||||
x2d; y2d;
|
||||
x3d; y3d;
|
||||
x4d; y4d;
|
||||
fd],
|
||||
stmts) &
|
||||
prog_evalo prog q
|
||||
})
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
(* TODO: add tests to test file *)
|
||||
|
||||
let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg,
|
||||
x2g, y2g,
|
||||
x3g, y3g,
|
||||
x4g, y4g,
|
||||
fg,
|
||||
xd, yd,
|
||||
x2d, y2d,
|
||||
x3d, y3d,
|
||||
x4d, y4d,
|
||||
fd,
|
||||
fstmts,
|
||||
stmts in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
x2g == Nat.s yg &
|
||||
y2g == Nat.s x2g &
|
||||
x3g == Nat.s y2g &
|
||||
y3g == Nat.s x3g &
|
||||
x4g == Nat.s y3g &
|
||||
y4g == Nat.s x4g &
|
||||
fg == Nat.s y4g &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
|
||||
x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
|
||||
x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
|
||||
seqo [ReadS (DerefP (VarP 1));
|
||||
ReadS (DerefP (VarP 3));
|
||||
WriteS (DerefP (VarP 2));
|
||||
WriteS (DerefP (VarP 3))] fstmts &
|
||||
fd == FunD ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr)));
|
||||
(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
|
||||
(Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
fstmts) &
|
||||
seqo [CallS (VarP fg, [PathE (VarP yg);
|
||||
PathE (VarP y2g);
|
||||
PathE (VarP y3g);
|
||||
PathE (VarP y4g)]);
|
||||
ReadS (DerefP (VarP yg));
|
||||
ReadS (DerefP (VarP y2g));
|
||||
ReadS (DerefP (VarP y3g));
|
||||
ReadS (DerefP (VarP y4g))] stmts &
|
||||
prog == Prg ([xd; yd;
|
||||
x2d; y2d;
|
||||
x3d; y3d;
|
||||
x4d; y4d;
|
||||
fd],
|
||||
stmts) &
|
||||
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 *)
|
||||
(* @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 *)
|
||||
|
||||
(* - basic synthesis tests *)
|
||||
(* 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 prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.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 prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd,
|
||||
st, rd_cap, wr_cap in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.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 prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd, st in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg)))) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.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 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 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 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_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_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 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 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 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)))) *)
|
||||
|
||||
(* 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)]))) *)
|
||||
|
||||
(* 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] *) *)
|
||||
|
||||
(* 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 *) *)
|
||||
|
||||
(* 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 *) *)
|
||||
|
||||
(* 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)]))) *)
|
||||
|
||||
(* 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)]))) *)
|
||||
|
||||
(* 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)]))) *)
|
||||
|
||||
(* 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 prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, yg, fg, xd, yd, fd,
|
||||
st, rd_cap, wr_cap in
|
||||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg)))) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.prj_exn))))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue