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

Compare commits

base: st:64935b3c7e65c6c198fae814245ac77c328d61f4
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:2cc87d74dfc33eef1d6d67f030c874e0765d76f0
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "64935b3c7e65c6c198fae814245ac77c328d61f4" and "2cc87d74dfc33eef1d6d67f030c874e0765d76f0" have entirely different histories.
64935b3c7e ... 2cc87d74df

4 changed files with 700 additions and 481 deletions
Download patch file Download diff file Expand all files Collapse all files

76
model_with_structures/analyzer.ml
View file

@ -80,8 +80,7 @@ struct
type mem = value list * memid (* NOTE: memory and first free elem *) type mem = value list * memid (* NOTE: memory and first free elem *)
type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *) type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
type vals = (data * memid) list (* glob *) * (data * memid) 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
type state = mem * types * vals * visited
(* --- *) (* --- *)
@ -254,16 +253,16 @@ struct
(* TODO: check new in vars *) (* TODO: check new in vars *)
let add_decl (state : state) (x : data) (d : decl) : state = 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 | VarD (t, e) -> let v = exprval mem vals e in
let (mem', v') = valcopy mem v t in let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v' 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 | 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_mem : mem = ([], 0)
let empty_state : state = (empty_mem, ([], []), ([], []), []) let empty_state : state = (empty_mem, ([], []), ([], []))
(* TODO: better way ??? *) (* TODO: better way ??? *)
let globals_min_id : data = 1000 let globals_min_id : data = 1000
@ -322,7 +321,7 @@ struct
(* full spoil *) (* full spoil *)
let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = 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 x = pathvar p in
let id = vals_assoc x vals in (* base var address *) let id = vals_assoc x vals in (* base var address *)
let b = pathval mem vals p in (* subvalue in var *) let b = pathval mem vals p in (* subvalue in var *)
@ -333,25 +332,25 @@ struct
mem_set mem'' id v'' mem_set mem'' id v''
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = 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 | UnitE, UnitT _ -> mem
| PathE p, t -> argsspoilp state m t p | PathE p, t -> argsspoilp state m t p
| RefE x, t -> argsspoilp state m t (VarP x) | RefE x, t -> argsspoilp state m t (VarP x)
(* TODO: FIXME: check RefE case ? *) (* TODO: FIXME: check RefE case ? *)
| TupleE es, TupleT ts -> List.fold_left2 | 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 mem ts es
| _, _ -> raise @@ Typing_error "valspoile" | _, _ -> raise @@ Typing_error "valspoile"
(* - funciton argument addition *) (* - funciton argument addition *)
let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state = 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 v = exprval mem oldvals e in
(* let t' = pathtype types p in *) (* let t' = pathtype types p in *)
let (mem', v') = valcopy mem v t in let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v' 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 *) (* - function evaluation *)
(* NOTE: not needed due to performed optimization in stmt_eval *) (* NOTE: not needed due to performed optimization in stmt_eval *)
@ -360,7 +359,8 @@ struct
(* - statement evaluation *) (* - statement evaluation *)
let rec stmt_eval (state : state) (s : stmt) : state = 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 | SkipS -> state
| CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
pathval mem vals f in pathval mem vals f in
@ -370,26 +370,19 @@ struct
let vals' : vals = (fst vals, fst vals) in let vals' : vals = (fst vals, fst vals) in
(match v, t with (match v, t with
| FunV (* xs, *) fstmts (* ) *), FunT ts -> | FunV (* xs, *) fstmts (* ) *), FunT ts ->
(* TODO: memoisation of the called functions *)
let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
List.fold_left2 (* TODO: FIXME: check x's order *) List.fold_left2 (* TODO: FIXME: check x's order *)
(fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1)) (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 *) (* 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 _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *)
let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in
List.fold_left let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
(fun visited_old stmt -> List.fold_left2
if List.mem stmt visited_old (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
then stmt :: visited_old mem ts es in
else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with (mem_spoiled, types, vals)
(_, _, _, visited_after_stmt) -> visited_after_stmt)
visited_swa
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)
mem ts es in
(mem_spoiled, types, vals, visited_new))
| FunV _, _ -> raise @@ Eval_error "call: function type" | FunV _, _ -> raise @@ Eval_error "call: function type"
| _, FunT _ -> raise @@ Eval_error "call: function val" | _, FunT _ -> raise @@ Eval_error "call: function val"
| _, _ -> raise @@ Eval_error "call: function type & val") | _, _ -> raise @@ Eval_error "call: function type & val")
@ -400,7 +393,7 @@ struct
else let x = pathvar p in else let x = pathvar p in
let id = vals_assoc x vals in let id = vals_assoc x vals in
let (mem', v') = valupd mem (mem_get mem id) p ZeroV 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") | _ -> raise @@ Eval_error "write: type")
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
then raise @@ Eval_error "read: spoiled value" then raise @@ Eval_error "read: spoiled value"
@ -411,12 +404,11 @@ struct
stmt_eval statel sr stmt_eval statel sr
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
let stater = stmt_eval state sr in let stater = stmt_eval state sr in
match statel with (meml, typesl, valsl, visitedl) -> match statel with (meml, typesl, valsl) ->
match stater with (memr, typesr, valsr, visitedr) -> match stater with (memr, typesr, valsr) ->
if typesl != typesr || valsl != valsr if typesl != typesr || valsl != valsr
then raise @@ Eval_error "choice" then raise @@ Eval_error "choice"
(* TODO: FIXME: better list union ?? *) else (memcomb meml memr, typesl, valsl)
else (memcomb meml memr, typesl, valsl, visitedl @ visitedr)
(* --- program execution --- *) (* --- program execution --- *)
@ -718,24 +710,6 @@ struct
Printf.printf "done!"; Printf.printf "done!";
[%expect {| 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" = let%expect_test "call to fix after call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [

245
model_with_structures/synthesizer.ml
View file

@ -203,26 +203,69 @@ struct
] ]
end 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 module StEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ('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 }] [@@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 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 *) (* - utils *)
let rec list_replaceo xs id value ys = ocanren { let rec list_replaceo xs id value ys = ocanren {
@ -250,13 +293,6 @@ struct
list_ntho xs' id' x' } 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 { let rec list_foldro f acc xs acc' = ocanren {
xs == [] & acc' == acc | xs == [] & acc' == acc |
@ -332,92 +368,6 @@ struct
{ xs == [] & ys == [] & zs == [] } { 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 = let mem_geto mem id v =
@ -661,8 +611,8 @@ struct
let open Value in let open Value in
let open Type in let open Type in
ocanren { ocanren {
fresh mem, types, vals, visited in fresh mem, types, vals in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
{ {
{ fresh tp, e, v, { fresh tp, e, v,
mem_cp, v_cp, mem_cp, v_cp,
@ -674,7 +624,7 @@ struct
mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
types_glob_addo types x tp types' & types_glob_addo types x tp types' &
vals_glob_addo vals x id_add vals' & vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals', visited) } | st' == StEnv (mem_add, types', vals') } |
{ fresh tps, s, { fresh tps, s,
mem_add, id_add, mem_add, id_add,
types', vals' in types', vals' in
@ -682,7 +632,7 @@ struct
mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) & mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) &
types_glob_addo types x (FunT tps) types' & types_glob_addo types x (FunT tps) types' &
vals_glob_addo vals x id_add vals' & 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 StEnv in
let open TypesEnv in let open TypesEnv in
let open ValsEnv in let open ValsEnv in
let open VisitedEnv in
ocanren { ocanren {
fresh m in fresh m in
empty_memo m & empty_memo m &
st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv []) st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []))
} }
(* TODO: better way ??? *) (* TODO: better way ??? *)
@ -808,10 +757,9 @@ struct
let open StEnv in let open StEnv in
let open CopyCap in let open CopyCap in
ocanren { ocanren {
fresh mem, types, vals, visited, fresh mem, types, vals, x, id, b, tp',
x, id, b, tp',
mem_sp, b_sp, v_sp, mem_upd, v_upd in 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 & pathvaro p x &
vals_assoco x vals id & vals_assoco x vals id &
pathvalo mem vals p b & pathvalo mem vals p b &
@ -822,11 +770,11 @@ struct
mem_seto mem_upd id v_upd mem' 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 let open StEnv in
ocanren { ocanren {
fresh st in fresh st in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
argspoileo st m tp e mem' argspoileo st m tp e mem'
} }
and argspoileo st m tp e mem' = and argspoileo st m tp e mem' =
@ -835,8 +783,8 @@ struct
let open Type in let open Type in
let open Path in let open Path in
ocanren { ocanren {
fresh _r, _w, mem, types, vals, visited in fresh _r, _w, mem, types, vals in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
{ {
{ e == UnitE & { e == UnitE &
tp == UnitT (_r, _w) & tp == UnitT (_r, _w) &
@ -850,7 +798,7 @@ struct
{ fresh es, tps in { fresh es, tps in
e == TupleE es & e == TupleE es &
tp == TupleT tps & 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 addargo st oldvals x tp e st' =
let open StEnv in let open StEnv in
ocanren { ocanren {
fresh mem, types, vals, visited, v, fresh mem, types, vals, v,
mem_cp, v_cp, mem_cp, v_cp,
mem_add, id_add, mem_add, id_add,
types', vals' in types', vals' in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
exprvalo mem oldvals e v & exprvalo mem oldvals e v &
valcopyo mem v tp (Std.pair mem_cp v_cp) & valcopyo mem v tp (Std.pair mem_cp v_cp) &
mem_addo mem_cp v_cp (Std.pair mem_add id_add) & mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
types_addo types x tp types' & types_addo types x tp types' &
vals_addo vals x id_add vals' & vals_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals', visited) st' == StEnv (mem_add, types', vals')
} }
(* - function evaluation *) (* - function evaluation *)
@ -885,25 +833,12 @@ struct
addargo st vals x tp e st' & addargo st vals x tp e st' &
st_with_id' == Std.pair st' (Nat.s x) st_with_id' == Std.pair st' (Nat.s x)
} }
and stmt_eval_func_foldero mem types vals visited stmt visited' = and stmt_eval_spoil_foldero types vals mem mtp e mem' =
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' =
let open StEnv in let open StEnv in
ocanren { ocanren {
fresh m, tp, st in fresh m, tp, st in
Std.pair m tp == mtp & Std.pair m tp == mtp &
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
argspoileo st m tp e mem' argspoileo st m tp e mem'
} }
and stmt_evalo st s st' = and stmt_evalo st s st' =
@ -915,8 +850,8 @@ struct
let open TypesEnv in let open TypesEnv in
let open ValsEnv in let open ValsEnv in
ocanren { ocanren {
fresh mem, types, vals, visited in fresh mem, types, vals in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals) &
{ {
{ s == SkipS & st == st' } | { s == SkipS & st == st' } |
{ fresh f, es, v, tp, { fresh f, es, v, tp,
@ -924,11 +859,8 @@ struct
glob_vs, _vs, glob_vs, _vs,
types_call, vals_call, types_call, vals_call,
fstmts, tps, st_call, fstmts, tps, st_call,
state_with_args, state_with_args, _arg_id,
mem_swa, types_swa, _states_evaled, mem_spoiled in
vals_swa, visited_swa,
_arg_id, mem_spoiled,
visited' in
s == CallS (f, es) & s == CallS (f, es) &
pathvalo mem vals f v & pathvalo mem vals f v &
pathtypeo types f tp & pathtypeo types f tp &
@ -938,16 +870,16 @@ struct
vals_call == ValsEnv (glob_vs, glob_vs) & vals_call == ValsEnv (glob_vs, glob_vs) &
v == FunV fstmts & v == FunV fstmts &
tp == FunT tps & tp == FunT tps &
st_call == StEnv (mem, types_call, vals_call, visited) & st_call == StEnv (mem, types_call, vals_call) &
list_foldl2o (stmt_addarg_foldero vals) list_foldl2o (stmt_addarg_foldero vals)
(Std.pair st_call 0) tps es (Std.pair st_call 0) tps es
(Std.pair state_with_args _arg_id) & (Std.pair state_with_args _arg_id) &
state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) & List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' &
(* TODO: FIXME check left or right order *) (* 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 & 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, { fresh p, tp, _r, w, x, id, v,
mem_upd, v_upd, mem_set in mem_upd, v_upd, mem_set in
@ -960,7 +892,7 @@ struct
mem_geto mem id v & mem_geto mem id v &
valupdo mem v p ZeroV (Std.pair mem_upd v_upd) & valupdo mem v p ZeroV (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem_set & 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 { fresh p in
s == ReadS p & s == ReadS p &
pathvalo mem vals p ZeroV & pathvalo mem vals p ZeroV &
@ -970,19 +902,18 @@ struct
stmt_evalo st sl stl & stmt_evalo st sl stl &
stmt_evalo stl sr st' } | stmt_evalo stl sr st' } |
{ fresh sl, sr, stl, str, { fresh sl, sr, stl, str,
meml, typesl, valsl, visitedl, meml, typesl, valsl,
memr, typesr, valsr, visitedr, memr, typesr, valsr,
visited', mem' in mem' in
s == ChoiceS (sl, sr) & s == ChoiceS (sl, sr) &
stmt_evalo st sl stl & stmt_evalo st sl stl &
stmt_evalo st sr str & stmt_evalo st sr str &
stl == StEnv (meml, typesl, valsl, visitedl) & str == StEnv (memr, typesr, valsr) &
str == StEnv (memr, typesr, valsr, visitedr) & stl == StEnv (meml, typesl, valsl) &
typesl == typesr & typesl == typesr &
valsl == valsr & valsl == valsr &
memcombo meml memr mem' & memcombo meml memr mem' &
visited_appendo visitedr visitedl visited' & st' == StEnv (mem', typesl, valsl) }
st' == StEnv (mem', typesl, valsl, visited') }
} }
} }

108
model_with_structures/tests.ml
View file

@ -5,77 +5,97 @@ open Relational
(* - basic var tests *) (* - basic var tests *)
let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); 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 ()); 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 ()); let%expect_test "simple var, forbidden read" = print_endline(prog_eval_t_simple_var_fbd_rd ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple vars, no read & read" = print_endline(prog_eval_t_simple_vars_fbd_rd_rd ()); 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 ()); 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 ()); let%expect_test "simple var, forbidden write" = print_endline(prog_eval_t_simple_var_fbd_wr ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_var_wr_rd ()); 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 *) (* - basic call tests *)
let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ()); 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 ()); 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 ()); 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 ()); 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 ()); let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ()); 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 ()); let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ()); (* type tests *)
[%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)))]))] |}] (* 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 ()); (* function tests *)
[%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))))]))] |}] (* 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 ()); (* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
[%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 "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] |}]

752
model_with_structures/tests_f.ml
View file

@ -17,26 +17,12 @@ open InCap
open OutCap open OutCap
open Mode open Mode
@type answer = StEnv.ground GT.list with show @type answer = StEnv.ground GT.list with show
@type answerCpCap = CopyCap.ground GT.list with show
(* - shortcuts *) (* - shortcuts *)
(* TODO *) (* 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 *) (* - basic var tests *)
let prog_eval_t_empty _ = show(answer) (Stream.take (run q 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 let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, fg, xd, fd in fresh prog, xg, fg, xd, fd, st in
globals_min_ido xg & globals_min_ido xg &
fg == Nat.s xg & fg == Nat.s xg &
xd == VarD (UnitT (Rd, NeverWr), UnitE) & 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 let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & 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 let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
@ -241,57 +227,41 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], 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)))) & WriteS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [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_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)]),
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & 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))) & 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))) & 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)]), SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg))))) & ReadS (DerefP (VarP yg))))) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & 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), SeqS (WriteS (VarP xg),
ReadS (DerefP (VarP 0)))) & ReadS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), 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)))) (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 { (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 & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
x2g == Nat.s yg & 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) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) & 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))); fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
SeqS (ReadS (DerefP (VarP 0)), SeqS (ReadS (DerefP (VarP 0)),
WriteS (DerefP (VarP 1)))) & WriteS (DerefP (VarP 1)))) &
prog == Prg ([xd; yd; x2d; y2d; fd], prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) &
CallS (VarP fg, [PathE (VarP yg);
PathE (VarP y2g)])) &
prog_evalo prog q prog_evalo prog q
}) })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q (* TODO: add tests to test file *)
(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))))
let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q (* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
(fun q -> ocanren { (* @type answerValue = Value.ground GT.list with show *)
fresh prog, xg, yg, (* @type answerNat = Nat.ground GT.list with show *)
x2g, y2g, (* @type answerNats = (Nat.ground List.ground) GT.list with show *)
x3g, y3g, (* @type answerTag = Tag.ground GT.list with show *)
x4g, y4g, (* @type answerTags = (Tag.ground List.ground) GT.list with show *)
fg, (* @type answerCopyCap = CopyCap.ground GT.list with show *)
xd, yd, (* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *)
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))))
(* - 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 (* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
(fun q -> ocanren { (* (fun q -> ocanren { inv_ido 2 0 q }) *)
fresh prog, xg, yg, fg, xd, yd, fd, st in (* (fun q -> q#reify Nat.prj_exn))) *)
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 prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (run q (* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
(fun q -> ocanren { (* (fun q -> ocanren { inv_ido 2 q 0 }) *)
fresh prog, xg, yg, fg, xd, yd, fd, (* (fun q -> q#reify Nat.prj_exn))) *)
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 prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take (run q (* let list_drop_t _ = show(answerNats) (Stream.take (run q *)
(fun q -> ocanren { (* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *)
fresh prog, xg, yg, fg, xd, yd, fd, st in (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
globals_min_ido xg &
yg == Nat.s xg & (* let list_replace_t _ = show(answerNats) (Stream.take (run q *)
fg == Nat.s yg & (* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *)
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))], (* let arg_to_value_t _ = show(answerValue) (Stream.take (run q *)
WriteS (DerefP (VarP 0))) & (* (fun q -> let open Arg in *)
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), (* ocanren { *)
ReadS (DerefP (VarP yg)))) & (* fresh s in *)
prog_evalo prog st }) (* empty_stateo s & *)
(fun q -> q#reify (CopyCap.prj_exn)))) (* 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))))