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:ee8ff429cfe6baf5897e55a2d4b5961c9bc427e2
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:6620b0d0efcb5df83a246de2c91a9bec13237362
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "ee8ff429cfe6baf5897e55a2d4b5961c9bc427e2" and "6620b0d0efcb5df83a246de2c91a9bec13237362" have entirely different histories.
ee8ff429cf ... 6620b0d0ef

6 changed files with 613 additions and 998 deletions
Download patch file Download diff file Expand all files Collapse all files

417
model_with_structures/analyzer.ml
View file

@ -78,35 +78,12 @@ struct
(* --- *)
type mem = value list * memid (* NOTE: memory and first free elem *)
type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
type types = (data * atype) list
type vals = (data * memid) list
type state = mem * types * vals
(* --- *)
(* - state utils *)
let types_assoc (x : data) (types : types) : atype =
(* try ( List.assoc x (fst types) ) *)
(* with Not_found -> *)
List.assoc x (snd types)
let vals_assoc (x : data) (vals : vals) : memid =
(* try ( List.assoc x (fst vals) ) *)
(* with Not_found -> *)
List.assoc x (snd vals)
let types_glob_add (types : types) (x : data) (t : atype) =
((x, t) :: fst types, (x, t) :: snd types)
let types_add (types : types) (x : data) (t : atype) =
(fst types, (x, t) :: snd types)
let vals_glob_add (vals : vals) (x : data) (id : memid) =
((x, id) :: fst vals, (x, id) :: snd vals)
let vals_add (vals : vals) (x : data) (id : memid) =
(fst vals, (x, id) :: snd vals)
(* - utils *)
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
@ -154,7 +131,7 @@ struct
| AccessP (p, _) -> pathvar p
let rec pathtype (types : types) (p : path) : atype = match p with
| VarP x -> types_assoc x types
| VarP x -> List.assoc x types
| DerefP p -> (match pathtype types p with
| RefT (_, t) -> t
| _ -> raise @@ Typing_error "pathtype: deref")
@ -168,7 +145,7 @@ struct
Printf.printf "mem size: %i, " (List.length (fst mem));
Printf.printf "mem size stored: %i " (snd mem);
Printf.printf "\n"; *)
vals_assoc x vals)
List.assoc x vals)
| DerefP p -> (match pathval mem vals p with
| RefV id -> mem_get mem id
| _ -> raise @@ Typing_error "pathval: deref")
@ -236,7 +213,7 @@ struct
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
| UnitE -> ZeroV
| PathE p -> pathval mem vals p
| RefE x -> RefV (vals_assoc x vals)
| RefE x -> RefV (List.assoc x vals)
| TupleE es -> TupleV (List.map (exprval mem vals) es)
(* - expression typing *)
@ -244,7 +221,7 @@ struct
let rec exprtype (types : types) (e : expr) : atype = match e with
| UnitE -> UnitT (Rd, NeverWr)
| PathE p -> pathtype types p
| RefE x -> RefT (Rf, types_assoc x types)
| RefE x -> RefT (Rf, List.assoc x types)
| TupleE es -> TupleT (List.map (exprtype types) es)
(* - context initialization *)
@ -257,12 +234,12 @@ struct
| VarD (t, e) -> let v = exprval mem vals e in
let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v' in
(mem'', types_glob_add types x t, vals_glob_add vals x id)
(mem'', (x, t) :: types, (x, id) :: vals)
| 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)
(mem', (x, FunT ts) :: types, (x, id) :: vals)
let empty_mem : mem = ([], 0)
let empty_state : state = (empty_mem, ([], []), ([], []))
let empty_state : state = (empty_mem, [], [])
(* TODO: better way ??? *)
let globals_min_id : data = 1000
@ -279,14 +256,13 @@ struct
let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
(r' : read_cap) (w' : write_cap) (m : mode)
(c : copy_cap) : bool =
(* FIXME TMP *)
(* Printf.printf "%b %b %b %b %b\n" *)
(* (r != Rd || v == ZeroV) *)
(* (r != Rd || fst m == In) *)
(* (snd m != Out || w == AlwaysWr) *)
(* (* TODO: FIXME: why always write ?? *) *)
(* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
(* (is_trivial_v v); *)
(* FIXME TMP
Printf.printf "%b %b %b %b %b\n"
(r != Rd || v == ZeroV)
(r != Rd || fst m == In)
(snd m != Out || w == AlwaysWr)
(((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
(is_trivial_v v); *)
(r != Rd || v == ZeroV) &&
(r != Rd || fst m == In) &&
(snd m != Out || w == AlwaysWr) &&
@ -323,12 +299,11 @@ struct
let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
match state with (mem, types, vals) ->
let x = pathvar p in
let id = vals_assoc x vals in (* base var address *)
let b = pathval mem vals p in (* subvalue in var *)
let t' = pathtype types p in (* type of subvalue *)
let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
(* TODO: FIXME: why copy (Cp)? *)
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
let id = List.assoc x vals in
let b = pathval mem vals p in
let t' = pathtype types p in
let (mem', b') = valspoil mem b t t' m Rf in
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in
mem_set mem'' id v''
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@ -350,7 +325,7 @@ struct
(* let t' = pathtype types p in *)
let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v' in
(mem'', types_add types x t, vals_add vals x id)
(mem'', (x, t) :: types, (x, id) :: vals)
(* - function evaluation *)
(* NOTE: not needed due to performed optimization in stmt_eval *)
@ -366,8 +341,8 @@ struct
pathval mem vals f in
let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
pathtype types f in
let types' : types = (fst types, fst types) in
let vals' : vals = (fst vals, fst vals) in
let types' : types = [] in
let vals' : vals = [] in
(match v, t with
| FunV (* xs, *) fstmts (* ) *), FunT ts ->
(* TODO: memoisation of the called functions *)
@ -391,14 +366,12 @@ struct
if w == NeverWr
then raise @@ Eval_error "write: write tag"
else let x = pathvar p in
let id = vals_assoc x vals in
let id = List.assoc x vals in
let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
(mem_set mem' id v', types, vals)
| _ -> raise @@ Eval_error "write: type")
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
then raise @@ Eval_error "read: spoiled value"
else if pathval mem vals p != ZeroV
then raise @@ Eval_error "read: nontrivial value"
| ReadS p -> if pathval mem vals p != ZeroV
then raise @@ Eval_error "read"
else state
| SeqS (sl, sr) -> let statel = stmt_eval state sl in
stmt_eval statel sr
@ -426,45 +399,13 @@ struct
let ( #. ) x y = SeqS (x, y)
let v0 = VarP 0
let v1 = VarP 1
let v2 = VarP 2
let v3 = VarP 3
let v4 = VarP 4
let v5 = VarP 5
let v6 = VarP 6
let v7 = VarP 7
let v8 = VarP 8
let vg0 = VarP globals_min_id
let vg1 = VarP (globals_min_id + 1)
let vg2 = VarP (globals_min_id + 2)
let vg3 = VarP (globals_min_id + 3)
let vg4 = VarP (globals_min_id + 4)
let vg5 = VarP (globals_min_id + 5)
let vg6 = VarP (globals_min_id + 6)
let vg7 = VarP (globals_min_id + 7)
let vg8 = VarP (globals_min_id + 8)
let vx = VarP 0
let vy = VarP 1
let vz = VarP 2
let rf0E = RefE 0
let rf1E = RefE 1
let rf2E = RefE 2
let rf3E = RefE 3
let rf4E = RefE 4
let rf5E = RefE 5
let rf3E = RefE 3
let rf4E = RefE 4
let rf5E = RefE 5
let rfg0E = RefE globals_min_id
let rfg1E = RefE (globals_min_id + 1)
let rfg2E = RefE (globals_min_id + 2)
let rfg3E = RefE (globals_min_id + 3)
let rfg4E = RefE (globals_min_id + 4)
let rfg5E = RefE (globals_min_id + 5)
let rfg6E = RefE (globals_min_id + 6)
let rfg7E = RefE (globals_min_id + 7)
let rfg8E = RefE (globals_min_id + 8)
let pE p = PathE p
let vgx = VarP (globals_min_id)
let vgy = VarP (globals_min_id + 1)
let vgz = VarP (globals_min_id + 2)
let drf p = DerefP p
let access p i = AccessP (p, i)
@ -485,12 +426,7 @@ struct
let moded t = ((In, NOut), t)
let defgu t = VarD (t, UnitE)
let defg t e = VarD (t, e)
let wrS p = WriteS p
let rdS p = ReadS p
let callS f args = CallS (f, args)
let defg t = VarD (t, UnitE)
(* - utils tests *)
@ -527,7 +463,7 @@ struct
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
[%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| read: spoiled value |}]
[%expect {| read |}]
let%expect_test "simple vars, no read & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@ -555,284 +491,23 @@ struct
(* - basic call tests *)
(* let%expect_test "simple call with read" = *)
(* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
(* FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], *)
(* CallS (VarP (globals_min_id + 1), *)
(* [PathE (VarP globals_min_id)])); *)
(* Printf.printf "done!"; *)
(* [%expect {| done! |}] *)
(* let%expect_test "simple call with write" = *)
(* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
(* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *)
(* FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], *)
(* CallS (VarP (globals_min_id + 2), *)
(* [PathE (VarP (globals_min_id + 1))])); *)
(* Printf.printf "done!"; *)
(* [%expect {| done! |}] *)
let%expect_test "simple call with read, dsl" =
prog_eval_noret (
[
defgu uT_r_mw;
defg (rfT uT_r_mw) rfg0E;
FunD (
[moded @@ cpT @@ uT_r],
rdS @@ drf @@ v0
)
],
callS vg2 [pE vg1]
);
let%expect_test "simple call with read" =
prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
CallS (VarP (globals_min_id + 1),
[PathE (VarP globals_min_id)]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with write, dsl" =
prog_eval_noret (
[
defgu uT_r_mw;
defg (rfT uT_r_mw) rfg0E;
FunD (
[moded @@ cpT @@ uT_r_mw],
wrS @@ drf @@ v0
)
],
callS vg2 [pE vg1]
);
let%expect_test "simple call with write" =
prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
CallS (VarP (globals_min_id + 2),
[PathE (VarP (globals_min_id + 1))]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with read after write, dsl" =
prog_eval_noret (
[
defgu uT_r_mw;
defg (rfT uT_r_mw) rfg0E;
FunD (
[moded @@ cpT @@ uT_mw],
(wrS @@ drf @@ v0) #.
(rdS @@ drf @@ v0)
)
],
callS vg2 [pE vg1]
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with forbidden write, dsl" =
try (prog_eval_noret (
[
defgu uT_r_mw;
defg (rfT uT_r_mw) rfg0E;
FunD (
[moded @@ cpT @@ uT_r],
wrS @@ drf @@ v0
)
],
callS vg2 [pE vg1]
);
[%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}]
(* TODO: FIXME: why is condition on always write in parent ?? *)
let%expect_test "simple call with write to ref, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0
)
],
callS vg2 [pE vg1]
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with forbidden write to ref, dsl" =
try (prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0
)
],
(callS vg2 [pE vg1]) #.
(rdS @@ drf @@ vg1)
);
[%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| read: spoiled value |}]
let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0
)
],
(callS vg2 [pE vg1]) #.
(wrS @@ drf @@ vg1) #.
(rdS @@ drf @@ vg1)
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "call inside call, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0
);
FunD (
[moded @@ cpT @@ uT_aw],
(callS vg2 [pE v0]) #.
(wrS @@ drf @@ v0)
)
],
(callS vg3 [pE vg1]) #.
(rdS @@ drf @@ vg1)
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "call to fix after call, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0
);
FunD (
[((In, Out), rfT @@ uT_aw)],
wrS @@ drf @@ v0
)
],
(callS vg2 [pE vg1]) #.
(callS vg3 [pE vg1]) #.
(rdS @@ drf @@ vg1)
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with global variable usage, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
FunD (
[moded @@ cpT @@ uT_aw],
(wrS @@ vg0) #.
(rdS @@ drf @@ vg1)
)
],
(callS vg2 [pE vg1]) #.
(rdS @@ drf @@ vg1)
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with read & write (2 args), dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg2E;
FunD (
[
moded @@ rfT @@ uT_r;
moded @@ rfT @@ uT_aw;
],
(rdS @@ drf @@ v0) #.
(wrS @@ drf @@ v1)
)
],
callS vg4 [pE vg1; pE vg3]
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with different arguments modifiers, copy, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg2E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg4E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg6E;
FunD (
[
((NIn, NOut), cpT @@ uT_aw);
((In, NOut), cpT @@ uT_r_aw);
((NIn, Out), cpT @@ uT_aw);
((In, Out), cpT @@ uT_r_aw);
],
(rdS @@ drf @@ v1) #.
(rdS @@ drf @@ v3) #.
(wrS @@ drf @@ v1) #.
(wrS @@ drf @@ v2) #.
(wrS @@ drf @@ v3)
)
],
(callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
(rdS @@ drf @@ vg1) #.
(rdS @@ drf @@ vg3) #.
(rdS @@ drf @@ vg5) #.
(rdS @@ drf @@ vg7)
);
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with different arguments modifiers, ref, dsl" =
prog_eval_noret (
[
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg2E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg4E;
defgu uT_r_aw;
defg (rfT uT_r_aw) rfg6E;
FunD (
[
((NIn, NOut), rfT @@ uT);
((In, NOut), rfT @@ uT_r);
((NIn, Out), rfT @@ uT_aw);
((In, Out), rfT @@ uT_r_aw);
],
(rdS @@ drf @@ v1) #.
(rdS @@ drf @@ v3) #.
(wrS @@ drf @@ v2) #.
(wrS @@ drf @@ v3)
)
],
(callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
(rdS @@ drf @@ vg1) #.
(rdS @@ drf @@ vg3) #.
(rdS @@ drf @@ vg5) #.
(rdS @@ drf @@ vg7)
);
Printf.printf "done!";
[%expect {| done! |}]
(* TODO: recursive call test (for the future when memoization will be implemented) *)
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
(* --- tests --- *)

54
model_with_structures/dune
View file

@ -13,34 +13,34 @@
(preprocess
(pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
(library
(name tests_st)
(modules tests)
(flags (-rectypes))
(libraries synthesizer_st tests_f_st)
(inline_tests)
(wrapped false)
(preprocess
(pps ppx_expect ppx_inline_test)))
; (library
; (name tests_st)
; (modules tests)
; (flags (-rectypes))
; (libraries synthesizer_st tests_f_st)
; (inline_tests)
; (wrapped false)
; (preprocess
; (pps ppx_expect ppx_inline_test)))
(library
(name tests_f_st)
(modules tests_f)
(flags (-rectypes))
(libraries OCanren OCanren.tester synthesizer_st)
(preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
(wrapped false)
(preprocess
(pps
OCanren-ppx.ppx_repr
OCanren-ppx.ppx_deriving_reify
OCanren-ppx.ppx_fresh
GT.ppx
GT.ppx_all
OCanren-ppx.ppx_distrib
--
-pp
camlp5/pp5+gt+plugins+ocanren+dump.exe)))
; (library
; (name tests_f_st)
; (modules tests_f)
; (flags (-rectypes))
; (libraries OCanren OCanren.tester synthesizer_st)
; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
; (wrapped false)
; (preprocess
; (pps
; OCanren-ppx.ppx_repr
; OCanren-ppx.ppx_deriving_reify
; OCanren-ppx.ppx_fresh
; GT.ppx
; GT.ppx_all
; OCanren-ppx.ppx_distrib
; --
; -pp
; camlp5/pp5+gt+plugins+ocanren+dump.exe)))
(library
(name synthesizer_st)

22
model_with_structures/model.typ
View file

@ -15,8 +15,6 @@
*TODO: top-level value copy mode ??* // TODO: FIXME
*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
#h(10pt)
#let rf = $\& #h(3pt)$
@ -908,10 +906,9 @@ $s in stmt, f in X, x in X, a in X$
$l = vals[x]$,
$vals, mu texpre p eqmu b$,
$types ttype p : t'$,
// TODO: FIXME: Ref or Copy ?? in root <- Copy ??,
// <- otherwise all subsequent copy capabilities will be ref (in current impl)
// TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
// FIXME depends on parent ??
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
$cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
@ -923,7 +920,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ full spoil for ref expr],
name: [ full spoil for tuple expr],
// NOTE: x as path
$mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
@ -944,7 +941,7 @@ $s in stmt, f in X, x in X, a in X$
$...$,
$mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n])_(cl vals, types cr) mu_n$,
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
)
))
@ -982,9 +979,8 @@ $s in stmt, f in X, x in X, a in X$
rule(
name: [ new reference copy value],
// TODO: FIXME: introduce global types and vals
$types_0 = types_#[glob]$,
$vals_0 = vals_#[glob]$,
$types_0 = []$,
$vals_0 = []$,
// NOTE: dashed arrow to fill context
$cl types_0, vals_0, mu_0 cr
@ -999,7 +995,7 @@ $s in stmt, f in X, x in X, a in X$
xarrow(s)
cl types', vals', mu' cr$,
$vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
$cl vals, mu_0 cr tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
)
))
@ -1029,9 +1025,9 @@ $s in stmt, f in X, x in X, a in X$
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
// NOTE: check that all the possible bodies are possible to eval
$vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
$cl vals, mu_0 cr tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
$...$,
$vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
$cl vals, mu_0 cr tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
// NOTE: thick arrow to "spoil" context
$mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,

125
model_with_structures/synthesizer.ml
View file

@ -167,7 +167,7 @@ struct
[%%ocanren_inject
type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
[@@deriving gt ~options:{ show; gmap }]
type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
type ground = ((Nat.ground List.ground * Stmt.ground) List.ground, Nat.ground, ground List.ground) t
]
end
@ -185,7 +185,7 @@ struct
module TypesEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
type nonrec 'dtl t = TypesEnv of 'dtl
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
]
@ -194,7 +194,7 @@ struct
module ValsEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
type nonrec 'ddl t = ValsEnv of 'ddl
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
]
@ -211,58 +211,6 @@ struct
(* --- *)
(* - state utils *)
let types_assoco id types tp =
let open TypesEnv in
ocanren {
fresh _glob_tps, tps in
types == TypesEnv (_glob_tps, tps) &
List.assoco id tps tp
}
let vals_assoco id vals v =
let open ValsEnv in
ocanren {
fresh _glob_vs, vs in
vals == ValsEnv (_glob_vs, vs) &
List.assoco id vs v
}
let types_glob_addo types x tp types' =
let open TypesEnv in
ocanren {
fresh glob_tps, tps in
types == TypesEnv (glob_tps, tps) &
types' == TypesEnv ((Std.pair x tp) :: glob_tps,
(Std.pair x tp) :: tps)
}
let types_addo types x tp types' =
let open TypesEnv in
ocanren {
fresh glob_tps, tps in
types == TypesEnv (glob_tps, tps) &
types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
}
let vals_glob_addo vals x v vals' =
let open ValsEnv in
ocanren {
fresh glob_vs, vs in
vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv ((Std.pair x v) :: glob_vs,
(Std.pair x v) :: vs)
}
let vals_addo vals x v vals' =
let open ValsEnv in
ocanren {
fresh glob_vs, vs in
vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
}
(* - utils *)
let rec list_replaceo xs id value ys = ocanren {
@ -409,6 +357,22 @@ struct
{ fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
}
let types_assoco id types tp =
let open TypesEnv in
ocanren {
fresh tps in
types == TypesEnv tps &
List.assoco id tps tp
}
let vals_assoco id vals v =
let open ValsEnv in
ocanren {
fresh vs in
vals == ValsEnv vs &
List.assoco id vs v
}
let rec pathtypeo types p tp =
let open Path in
let open Type in
@ -608,23 +572,24 @@ struct
let add_declo st x d st' =
let open StEnv in
let open Decl in
let open TypesEnv in
let open ValsEnv in
ocanren {
fresh mem, types, vals in
st == StEnv (mem, types, vals) &
st == StEnv (mem, TypesEnv types, ValsEnv vals) &
{
{ fresh tp, e, v,
mem_with_v_cp, mem_cp, v_cp,
mem_with_id_add, mem_add, id_add,
types', vals' in
mem_with_id_add, mem_add, id_add in
d == VarD (tp, e) &
exprvalo mem vals e v &
exprvalo mem (ValsEnv vals) e v &
valcopyo mem v tp mem_with_v_cp &
Pair.pair mem_cp v_cp == mem_with_v_cp &
mem_addo mem_cp v_cp mem_with_id_add &
Pair.pair mem_add id_add == mem_with_id_add &
types_glob_addo types x tp types' &
vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals')
st' == StEnv (mem_add,
TypesEnv ((Pair.pair x tp) :: types),
ValsEnv ((Pair.pair x id_add) :: vals))
}
}
}
@ -640,7 +605,7 @@ struct
ocanren {
fresh m in
empty_memo m &
st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []))
st == StEnv (m, TypesEnv [], ValsEnv [])
}
(* TODO: better way ??? *)
@ -752,7 +717,7 @@ struct
vals_assoco x vals id &
pathvalo mem vals p b &
pathtypeo types p tp' &
valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) &
mem_geto mem_sp id v_sp &
valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem'
@ -794,18 +759,17 @@ struct
let addargo st oldvals x tp e st' =
let open StEnv in
let open TypesEnv in
let open ValsEnv in
ocanren {
fresh mem, types, vals, v,
mem_cp, v_cp,
mem_add, id_add,
types', vals' in
st == StEnv (mem, types, vals) &
fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in
st == StEnv (mem, TypesEnv types, ValsEnv vals) &
exprvalo mem oldvals e v &
valcopyo mem v tp (Std.pair mem_cp v_cp) &
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
types_addo types x tp types' &
vals_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals')
st' == StEnv (mem_add,
TypesEnv ((Std.pair x tp) :: types),
ValsEnv ((Std.pair x id_add) :: vals))
}
(* - function evaluation *)
@ -842,20 +806,16 @@ struct
st == StEnv (mem, types, vals) &
{
{ s == SkipS & st == st' } |
{ fresh f, es, v, tp,
glob_tps, _tps,
glob_vs, _vs,
types', vals',
{ fresh f, es, v, tp, types', vals',
fstmts, tps, st',
state_with_args, _arg_id,
_states_evaled, mem_spoiled in
_states_evaled,
mem_spoiled in
s == CallS (f, es) &
pathvalo mem vals f v &
pathtypeo types f tp &
types == TypesEnv (glob_tps, _tps) &
vals == ValsEnv (glob_vs, _vs) &
types' == TypesEnv (glob_tps, glob_tps) &
vals' == ValsEnv (glob_vs, glob_vs) &
types' == TypesEnv [] &
vals' == ValsEnv [] &
v == FunV fstmts &
tp == FunT tps &
st' == StEnv (mem, types', vals') &
@ -907,12 +867,9 @@ struct
let prog_evalo prog st' =
let open Prg in
let open Stmt in
ocanren {
fresh decls, s, init_st in
prog == Prg (decls, s) &
decls == [] &
s == SkipS &
prog_inito prog init_st &
stmt_evalo init_st s st'
}

107
model_with_structures/tests.ml
View file

@ -2,63 +2,60 @@ open Tests_f
open Synthesizer
open Relational
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ());
[%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}]
(* type tests *)
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)
(* let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}] *)
(* let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *)
(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}] *)
(* let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}] *)
(* let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}] *)
(* let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *)
let%expect_test "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])] |}]
(* function tests *)
(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *)
(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *)
(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] *)
(* let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] *)
(* let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] *)
(* let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] *)
(* let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
(* let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *)
(* let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *)
(* let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] *)
(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] *)
(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] *)
(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] *)
(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
(* let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *)
(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *)
(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}] *)
(* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
(* let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] *)
(* let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] *)
(* let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
(* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *)
(* let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] *)
(* let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] *)
(* let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] *)
(* let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] *)
(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] *)
(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] *)
(* let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] *)
(* let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] *)
(* let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] *)
(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *)
(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *)
(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] *)
(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] *)
(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] *)
(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] *)
(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
let%expect_test "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 "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]

884
model_with_structures/tests_f.ml
View file

@ -4,516 +4,506 @@ open GT
open OCanren
open OCanren.Std
@type answer = StEnv.ground GT.list with show
@type answer = St.ground GT.list with show
@type answerArgs = (Arg.ground List.ground) GT.list with show
@type answerValue = Value.ground GT.list with show
@type answerNat = Nat.ground GT.list with show
@type answerNats = (Nat.ground List.ground) GT.list with show
@type answerTag = Tag.ground GT.list with show
@type answerTags = (Tag.ground List.ground) GT.list with show
@type answerCopyCap = CopyCap.ground GT.list with show
@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show
let prog_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Prg in
let open Stmt in
let inv_id_t _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 1 q })
(fun q -> q#reify Nat.prj_exn)))
let inv_id_t2 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 0 q })
(fun q -> q#reify Nat.prj_exn)))
let inv_id_t3 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 q 0 })
(fun q -> q#reify Nat.prj_exn)))
let list_drop_t _ = show(answerNats) (Stream.take (run q
(fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let list_replace_t _ = show(answerNats) (Stream.take (run q
(fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q })
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let arg_to_value_t _ = show(answerValue) (Stream.take (run q
(fun q -> let open Arg in
ocanren {
fresh prog in
prog == Prg ([], SkipS) &
prog_evalo prog q})
(fun q -> q#reify (StEnv.prj_exn))))
fresh s in
empty_stateo s &
arg_to_valueo s RValue q })
(fun q -> q#reify (Value.prj_exn))))
(* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
(* @type answerValue = Value.ground GT.list with show *)
(* @type answerNat = Nat.ground GT.list with show *)
(* @type answerNats = (Nat.ground List.ground) GT.list with show *)
(* @type answerTag = Tag.ground GT.list with show *)
(* @type answerTags = (Tag.ground List.ground) GT.list with show *)
(* @type answerCopyCap = CopyCap.ground GT.list with show *)
(* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *)
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 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 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 inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
(* (fun q -> ocanren { inv_ido 2 0 q }) *)
(* (fun q -> q#reify Nat.prj_exn))) *)
let 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 inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
(* (fun q -> ocanren { inv_ido 2 q 0 }) *)
(* (fun q -> q#reify Nat.prj_exn))) *)
let 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 list_drop_t _ = show(answerNats) (Stream.take (run q *)
(* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *)
(* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
let 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 list_replace_t _ = show(answerNats) (Stream.take (run q *)
(* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *)
(* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
let 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 arg_to_value_t _ = show(answerValue) (Stream.take (run q *)
(* (fun q -> let open Arg in *)
(* ocanren { *)
(* fresh s in *)
(* empty_stateo s & *)
(* arg_to_valueo s RValue q }) *)
(* (fun q -> q#reify (Value.prj_exn)))) *)
let 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 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 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 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 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 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 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 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 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 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 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 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 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 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 foldl2_t _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
ocanren {
fresh s, s', cnt, arg_tags, args in
arg_tags == [rwi_val] &
args == [RValue] &
empty_stateo s &
empty_stateo s' &
list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
(fun q -> q#reify (St.prj_exn))))
(* let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q *)
(* (fun q -> let open Arg in *)
(* ocanren {fresh v in List.mapo arg_to_rvalueo v q}) *)
(* (fun q -> q#reify (List.prj_exn Arg.prj_exn)))) *)
let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q
(fun q -> let open Arg in
ocanren {fresh v in List.mapo arg_to_rvalueo v q})
(fun q -> q#reify (List.prj_exn Arg.prj_exn))))
(* empty state test *)
(* let empty_state_t _ = show(answer) (Stream.take (run q *)
(* (fun q -> ocanren {empty_stateo q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let empty_state_t _ = show(answer) (Stream.take (run q
(fun q -> ocanren {empty_stateo q})
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t1 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [] & *)
(* d == FunDecl ([], []) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [] &
d == FunDecl ([], []) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t2 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [] & *)
(* d == FunDecl ([wi_val], [Write 0; Read 0]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [] &
d == FunDecl ([wi_val], [Write 0; Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t3 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [FunDecl ([wi_ref], [Write 0])] & *)
(* d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t3 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t4 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [FunDecl ([wi_ref], [Write 0])] & *)
(* d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t4 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t5 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
(* d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t5 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
(* let fun_eval_t6 _ = show(answer) (Stream.take (run q *)
(* (fun q -> (* let open Prog in *) *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren { fresh s, p, d in *)
(* empty_stateo s & *)
(* p == [FunDecl ([wi_val], [Write 0])] & *)
(* d == FunDecl ([wi_val], [Call (0, [0])]) & *)
(* eval_fun_empty_argso s p d q }) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let fun_eval_t6 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_val], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0])]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* prog eval test *)
(* let prog_eval_t1 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
(* let prog_eval_t2 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])], *)
(* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
(* let prog_eval_t3 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])], *)
(* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t3 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
(* let prog_eval_t4 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t4 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
(* let prog_eval_t5 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t5 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
(* let prog_eval_t6 _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let prog_eval_t6 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* annotation gen prog test *)
(* let synt_t1 _ = show(answerTag) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> q#reify (Tag.prj_exn)))) *)
let synt_t1 _ = show(answerTag) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *)
(* let synt_t2 _ = show(answerTag) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> q#reify (Tag.prj_exn)))) *)
let synt_t2 _ = show(answerTag) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *)
(* let synt_t3 _ = show(answerTags) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *)
let synt_t3 _ = show(answerTags) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* annotation gen prog test *)
(* let synt_t4 _ = show(answerTags) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *)
let synt_t4 _ = show(answerTags) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
(* annotation gen prog test *)
(* let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* annotation gen prog test *)
(* let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* annotation gen prog test *)
(* let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* annotation gen prog test *)
(* let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* annotation gen prog test *)
(* let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_reado r' & is_never_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* TODO: FIXME: implement memoization cuts *)
(* prog with recursive function call *)
(* let rec_eval_t _ = show(answer) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
(* (fun q -> q#reify (St.prj_exn)))) *)
let rec_eval_t _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))