mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
2 commits
1d65b67260
...
8fc0ffa805
| Author | SHA1 | Date | |
|---|---|---|---|
|
8fc0ffa805 | ||
|
|
0ef7ebdad2 |
5 changed files with 588 additions and 48 deletions
|
|
@ -200,8 +200,8 @@ struct
|
||||||
| UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
|
| UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
|
||||||
| UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
|
| UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
|
||||||
| FunT _, FunV _ -> (mem, v)
|
| FunT _, FunV _ -> (mem, v)
|
||||||
| RefT (Rf, _), RefV _ -> (mem, v)
|
(* | RefT (Rf, _), RefV _ -> (mem, v) *)
|
||||||
| RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
| RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
||||||
let (mem'', id'') = mem_add mem' v' in
|
let (mem'', id'') = mem_add mem' v' in
|
||||||
(mem'', RefV id'')
|
(mem'', RefV id'')
|
||||||
| TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
|
| TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
|
||||||
|
|
@ -570,6 +570,7 @@ struct
|
||||||
let vg8 = VarP (globals_min_id + 8)
|
let vg8 = VarP (globals_min_id + 8)
|
||||||
let vg9 = VarP (globals_min_id + 9)
|
let vg9 = VarP (globals_min_id + 9)
|
||||||
let vg10 = VarP (globals_min_id + 10)
|
let vg10 = VarP (globals_min_id + 10)
|
||||||
|
let vg11 = VarP (globals_min_id + 11)
|
||||||
|
|
||||||
let rf0E = RefE 0
|
let rf0E = RefE 0
|
||||||
let rf1E = RefE 1
|
let rf1E = RefE 1
|
||||||
|
|
@ -987,6 +988,117 @@ struct
|
||||||
Printf.printf "done!";
|
Printf.printf "done!";
|
||||||
[%expect {| done! |}]
|
[%expect {| done! |}]
|
||||||
|
|
||||||
|
(* - tests for presentation *)
|
||||||
|
|
||||||
|
let%expect_test "presentation test 1 (simple types), dsl" =
|
||||||
|
prog_eval_noret (
|
||||||
|
[
|
||||||
|
defgu uT_r_aw;
|
||||||
|
defg (rfT uT_r_aw) rfg0E; (* x *)
|
||||||
|
defgu uT_r_aw;
|
||||||
|
defg (rfT uT_r_aw) rfg2E; (* y *)
|
||||||
|
defgu uT_r_aw;
|
||||||
|
defg (rfT uT_r_aw) rfg4E; (* z *)
|
||||||
|
defgu uT_r_aw;
|
||||||
|
defg (rfT uT_r_aw) rfg6E; (* k *)
|
||||||
|
FunD ( (* f *)
|
||||||
|
[
|
||||||
|
(moded @@ rfT @@ uT_r_aw);
|
||||||
|
(moded @@ rfT @@ uT_r);
|
||||||
|
],
|
||||||
|
(rdS @@ drf @@ v0) #.
|
||||||
|
(wrS @@ drf @@ v0) #.
|
||||||
|
(rdS @@ drf @@ v1)
|
||||||
|
);
|
||||||
|
FunD ( (* w *)
|
||||||
|
[
|
||||||
|
(moded @@ cpT @@ uT_mw);
|
||||||
|
],
|
||||||
|
(wrS @@ drf @@ v0) |. skp
|
||||||
|
);
|
||||||
|
FunD ( (* g *)
|
||||||
|
[
|
||||||
|
(moded @@ rfT @@ uT_aw);
|
||||||
|
(moded @@ cpT @@ uT_r_mw);
|
||||||
|
],
|
||||||
|
(wrS @@ drf @@ v0) #.
|
||||||
|
((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #.
|
||||||
|
(rdS @@ drf @@ v0) #.
|
||||||
|
(rdS @@ drf @@ v1)
|
||||||
|
);
|
||||||
|
FunD ( (* r *)
|
||||||
|
[
|
||||||
|
(moded @@ rfT @@ uT_r);
|
||||||
|
],
|
||||||
|
(rdS @@ drf @@ v0)
|
||||||
|
)
|
||||||
|
],
|
||||||
|
let xV = vg1 in
|
||||||
|
let yV = vg3 in
|
||||||
|
let zV = vg5 in
|
||||||
|
let kV = vg7 in
|
||||||
|
let fF = vg8 in
|
||||||
|
let wF = vg9 in
|
||||||
|
let gF = vg10 in
|
||||||
|
let rF = vg11 in
|
||||||
|
(callS wF [pE xV]) #.
|
||||||
|
(callS rF [pE xV]) #.
|
||||||
|
(callS fF [pE xV; pE yV]) #.
|
||||||
|
(callS rF [pE yV]) #.
|
||||||
|
(callS gF [pE zV; pE kV]) #.
|
||||||
|
(wrS @@ drf @@ zV) #.
|
||||||
|
(callS wF [pE zV]) #.
|
||||||
|
(callS fF [pE yV; pE zV]) #.
|
||||||
|
(callS rF [pE kV])
|
||||||
|
);
|
||||||
|
Printf.printf "done!";
|
||||||
|
[%expect {| done! |}]
|
||||||
|
|
||||||
|
(* TODO tags, access *)
|
||||||
|
(* let%expect_test "presentation test 2 (complex types), dsl" = *)
|
||||||
|
(* prog_eval_noret ( *)
|
||||||
|
(* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
|
||||||
|
(* let dataT = TupleT [uT_r_aw; uT_r_aw] in *)
|
||||||
|
(* let requestT = TupleT [cpT userT; *)
|
||||||
|
(* cpT dataT; *)
|
||||||
|
(* cpT dataT] in *)
|
||||||
|
(* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
|
||||||
|
(* cpT dataT; *)
|
||||||
|
(* cpT dataT] in *)
|
||||||
|
(* let userE = TupleE [UnitE; UnitE; UnitE] in *)
|
||||||
|
(* let dataE = TupleE [UnitE; UnitE] in *)
|
||||||
|
(* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
|
||||||
|
(* [ *)
|
||||||
|
(* defg userT userE; *)
|
||||||
|
(* defg dataT dataE; *)
|
||||||
|
(* defgu uT_r_aw; (* time *) *)
|
||||||
|
(* defg requestT requestE; *)
|
||||||
|
(* FunD ( (* send *) *)
|
||||||
|
(* [ *)
|
||||||
|
(* (moded @@ requestArgsT) *)
|
||||||
|
(* ], *)
|
||||||
|
(* ( *)
|
||||||
|
(* ( (* TODO access *) *)
|
||||||
|
(* (rdS @@ drf @@ v0) #. *)
|
||||||
|
(* (wrS @@ drf @@ v0) #. *)
|
||||||
|
(* (rdS @@ drf @@ v0) #. *)
|
||||||
|
(* (wrS @@ drf @@ v0) *)
|
||||||
|
(* ) |. *)
|
||||||
|
(* skp) #. *)
|
||||||
|
(* TODO access *)
|
||||||
|
(* (wrS @@ drf @@ v0) #. *)
|
||||||
|
(* (rdS @@ drf @@ v1) *)
|
||||||
|
(* ); *)
|
||||||
|
(* ], *)
|
||||||
|
(* (callS vg4 [pE vg3]) #. *)
|
||||||
|
(* TODO access *)
|
||||||
|
(* (wrS @@ drf @@ vg3) #. *)
|
||||||
|
(* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *)
|
||||||
|
(* (rdS @@ drf @@ vg3) *)
|
||||||
|
(* ); *)
|
||||||
|
(* Printf.printf "done!"; *)
|
||||||
|
(* [%expect {| done! |}] *)
|
||||||
|
|
||||||
(* - complex tests *)
|
(* - complex tests *)
|
||||||
|
|
||||||
(* TODO: FIXME: rw tags *)
|
(* TODO: FIXME: rw tags *)
|
||||||
|
|
|
||||||
|
|
@ -13,7 +13,7 @@
|
||||||
|
|
||||||
== Syntax
|
== Syntax
|
||||||
|
|
||||||
*TODO: top-level value copy mode ??* // TODO: FIXME
|
// *TODO: top-level value copy mode ??* // TODO: FIXME
|
||||||
|
|
||||||
*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
|
*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
|
||||||
|
|
||||||
|
|
@ -581,28 +581,26 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
// #align(center, prooftree(
|
||||||
|
// vertical-spacing: 4pt,
|
||||||
|
// rule(
|
||||||
|
// name: [ new reference ref value],
|
||||||
|
|
||||||
|
// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||||
|
// )
|
||||||
|
// ))
|
||||||
|
|
||||||
|
// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
|
||||||
#align(center, prooftree(
|
#align(center, prooftree(
|
||||||
vertical-spacing: 4pt,
|
vertical-spacing: 4pt,
|
||||||
rule(
|
rule(
|
||||||
name: [ new reference ref value],
|
name: [ new reference /* copy */ value],
|
||||||
|
|
||||||
// TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
|
|
||||||
// <- forbidden ??
|
|
||||||
|
|
||||||
$cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
|
||||||
)
|
|
||||||
))
|
|
||||||
|
|
||||||
#align(center, prooftree(
|
|
||||||
vertical-spacing: 4pt,
|
|
||||||
rule(
|
|
||||||
name: [ new reference copy value],
|
|
||||||
|
|
||||||
$cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
|
$cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
|
||||||
|
|
||||||
$mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
$mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||||||
|
|
||||||
$cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
|
$cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -569,11 +569,11 @@ struct
|
||||||
pathvalo mem vals p' v' &
|
pathvalo mem vals p' v' &
|
||||||
v' == RefV id &
|
v' == RefV id &
|
||||||
mem_geto mem id v } |
|
mem_geto mem id v } |
|
||||||
{ fresh p', id, v', vs in
|
{ fresh p', id', v', vs in
|
||||||
p == AccessP (p', id) &
|
p == AccessP (p', id') &
|
||||||
pathvalo mem vals p' v' &
|
pathvalo mem vals p' v' &
|
||||||
v' == TupleV vs &
|
v' == TupleV vs &
|
||||||
list_ntho vs id v }
|
list_ntho vs id' v }
|
||||||
}
|
}
|
||||||
|
|
||||||
(* --- eval rules --- *)
|
(* --- eval rules --- *)
|
||||||
|
|
@ -592,7 +592,7 @@ struct
|
||||||
let open Type in
|
let open Type in
|
||||||
let open Value in
|
let open Value in
|
||||||
let open ReadCap in
|
let open ReadCap in
|
||||||
let open CopyCap in
|
(* let open CopyCap in *)
|
||||||
let open MemVal in
|
let open MemVal in
|
||||||
let open ReadVal in
|
let open ReadVal in
|
||||||
let open WriteVal in
|
let open WriteVal in
|
||||||
|
|
@ -613,13 +613,13 @@ struct
|
||||||
{ fresh c, tp', id in
|
{ fresh c, tp', id in
|
||||||
v == RefV id &
|
v == RefV id &
|
||||||
tp == RefT (c, tp') &
|
tp == RefT (c, tp') &
|
||||||
{ { c == Rf & mem_with_id' == Std.pair mem v } |
|
(* { c == Rf & mem_with_id' == Std.pair mem v } | *)
|
||||||
{ fresh v', mem_cp, v_cp, mem_add, id_add in
|
{ fresh v', mem_cp, v_cp, mem_add, id_add in
|
||||||
c == Cp &
|
(* c == Cp & *)
|
||||||
mem_geto mem id v' &
|
mem_geto mem id 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) &
|
||||||
mem_with_id' == (mem_add, RefV id_add) } } } |
|
mem_with_id' == (mem_add, RefV id_add) } } |
|
||||||
{ fresh vs, tps, mem', vs' in
|
{ fresh vs, tps, mem', vs' in
|
||||||
v == TupleV vs &
|
v == TupleV vs &
|
||||||
tp == TupleT tps &
|
tp == TupleT tps &
|
||||||
|
|
@ -727,8 +727,8 @@ struct
|
||||||
ocanren {
|
ocanren {
|
||||||
{ u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
|
{ u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
|
||||||
{ u == BotMV & v == BotMV & u' == BotMV } |
|
{ u == BotMV & v == BotMV & u' == BotMV } |
|
||||||
{ u =/= ZeroMV & v =/= ZeroMV &
|
{ { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } &
|
||||||
u =/= BotMV & v =/= BotMV &
|
{ u =/= BotMV | { u == BotMV & v =/= BotMV } } &
|
||||||
u' == SmthMV }
|
u' == SmthMV }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -749,8 +749,8 @@ struct
|
||||||
ocanren {
|
ocanren {
|
||||||
{ u == OneWV & v == OneWV & u' == OneWV } |
|
{ u == OneWV & v == OneWV & u' == OneWV } |
|
||||||
{ u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
|
{ u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
|
||||||
{ u =/= ZeroWV & v =/= ZeroWV &
|
{ { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } &
|
||||||
u =/= OneWV & v =/= OneWV &
|
{ u =/= OneWV | { u == OneWV & v =/= OneWV } } &
|
||||||
u' == SmthWV }
|
u' == SmthWV }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -775,7 +775,8 @@ struct
|
||||||
{ fresh a, b in
|
{ fresh a, b in
|
||||||
u == RefV a &
|
u == RefV a &
|
||||||
v == RefV b &
|
v == RefV b &
|
||||||
a == b } |
|
a == b &
|
||||||
|
u' == RefV a } |
|
||||||
{ fresh us, vs, us' in
|
{ fresh us, vs, us' in
|
||||||
u == TupleV us &
|
u == TupleV us &
|
||||||
v == TupleV vs &
|
v == TupleV vs &
|
||||||
|
|
|
||||||
File diff suppressed because one or more lines are too long
|
|
@ -28,16 +28,30 @@ open StEnv
|
||||||
(* - shortcuts *)
|
(* - shortcuts *)
|
||||||
|
|
||||||
(* NOTE: redo with fold ?? *)
|
(* NOTE: redo with fold ?? *)
|
||||||
let rec seqo stmts stmt' = ocanren {
|
let seq_foldero stmt_acc stmt stmt_acc' = ocanren {
|
||||||
{ stmts == [] & stmt' == SkipS } |
|
stmt_acc' == SeqS(stmt, stmt_acc)
|
||||||
{ fresh s in
|
}
|
||||||
stmts == [s] &
|
let seqo stmts stmt' = ocanren {
|
||||||
stmt' == s } |
|
list_foldro seq_foldero SkipS stmts stmt'
|
||||||
{ fresh s, s', ss, stmt_rest' in
|
}
|
||||||
stmts == s :: s' :: ss &
|
(* ocanren { *)
|
||||||
seqo (s' :: ss) stmt_rest' &
|
(* { stmts == [] & stmt' == SkipS } | *)
|
||||||
stmt' == SeqS(s, stmt_rest')
|
(* { 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') *)
|
||||||
|
(* } *)
|
||||||
|
(* } *)
|
||||||
|
|
||||||
|
let deref_accesso id v p' = ocanren {
|
||||||
|
p' == DerefP (AccessP (VarP v, id))
|
||||||
|
}
|
||||||
|
|
||||||
|
let access_deref_accesso id_ext id_int v p' = ocanren {
|
||||||
|
p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
|
||||||
}
|
}
|
||||||
|
|
||||||
(* - basic var tests *)
|
(* - basic var tests *)
|
||||||
|
|
@ -517,7 +531,158 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
|
||||||
prog_evalo prog st })
|
prog_evalo prog st })
|
||||||
(fun q -> q#reify (CopyCap.prj_exn))))
|
(fun q -> q#reify (CopyCap.prj_exn))))
|
||||||
|
|
||||||
(* - complex tests *)
|
(* - presentation tests *)
|
||||||
|
|
||||||
|
(* simple types *)
|
||||||
|
|
||||||
|
let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
|
||||||
|
(fun q -> ocanren {
|
||||||
|
fresh prog, xbg, xg,
|
||||||
|
ybg, yg,
|
||||||
|
zbg, zg,
|
||||||
|
kbg, kg,
|
||||||
|
fg, wg, gg, rg,
|
||||||
|
xbd, xd,
|
||||||
|
ybd, yd,
|
||||||
|
zbd, zd,
|
||||||
|
kbd, kd,
|
||||||
|
fd, wd, gd, rd,
|
||||||
|
fstmts, gstmts,
|
||||||
|
stmts in
|
||||||
|
globals_min_ido xbg &
|
||||||
|
xg == Nat.s xbg &
|
||||||
|
ybg == Nat.s xg &
|
||||||
|
yg == Nat.s ybg &
|
||||||
|
zbg == Nat.s yg &
|
||||||
|
zg == Nat.s zbg &
|
||||||
|
kbg == Nat.s zg &
|
||||||
|
kg == Nat.s kbg &
|
||||||
|
fg == Nat.s kg &
|
||||||
|
wg == Nat.s fg &
|
||||||
|
gg == Nat.s wg &
|
||||||
|
rg == Nat.s gg &
|
||||||
|
xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
|
||||||
|
ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
|
||||||
|
zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
|
||||||
|
kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
|
||||||
|
seqo [ReadS (DerefP (VarP 0));
|
||||||
|
WriteS (DerefP (VarP 0));
|
||||||
|
ReadS (DerefP (VarP 1))] fstmts &
|
||||||
|
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)));
|
||||||
|
(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
|
||||||
|
fstmts) &
|
||||||
|
wd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))],
|
||||||
|
ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
|
||||||
|
seqo [WriteS (DerefP (VarP 0));
|
||||||
|
ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
|
||||||
|
ReadS (DerefP (VarP 0));
|
||||||
|
ReadS (DerefP (VarP 1))] gstmts &
|
||||||
|
gd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)));
|
||||||
|
(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
|
||||||
|
gstmts) &
|
||||||
|
rd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
|
||||||
|
ReadS (DerefP (VarP 0))) &
|
||||||
|
seqo [
|
||||||
|
CallS (VarP wg, [PathE (VarP xg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP xg)]);
|
||||||
|
CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP yg)]);
|
||||||
|
CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
|
||||||
|
CallS (VarP wg, [PathE (VarP zg)]);
|
||||||
|
WriteS (DerefP (VarP zg));
|
||||||
|
CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP kg)])
|
||||||
|
] stmts &
|
||||||
|
prog == Prg ([xbd; xd;
|
||||||
|
ybd; yd;
|
||||||
|
zbd; zd;
|
||||||
|
kbd; kd;
|
||||||
|
fd; wd; gd; rd],
|
||||||
|
stmts) &
|
||||||
|
prog_evalo prog q
|
||||||
|
})
|
||||||
|
(fun q -> q#reify (StEnv.prj_exn))))
|
||||||
|
|
||||||
|
let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q
|
||||||
|
(fun q -> ocanren {
|
||||||
|
fresh prog, xbg, xg,
|
||||||
|
ybg, yg,
|
||||||
|
zbg, zg,
|
||||||
|
kbg, kg,
|
||||||
|
fg, wg, gg, rg,
|
||||||
|
xbd, xd,
|
||||||
|
ybd, yd,
|
||||||
|
zbd, zd,
|
||||||
|
kbd, kd,
|
||||||
|
fd, wd, gd, rd,
|
||||||
|
fstmts, gstmts,
|
||||||
|
stmts,
|
||||||
|
c_fx, c_fy, c_wx, c_gx, c_gy, c_rx,
|
||||||
|
st in
|
||||||
|
globals_min_ido xbg &
|
||||||
|
xg == Nat.s xbg &
|
||||||
|
ybg == Nat.s xg &
|
||||||
|
yg == Nat.s ybg &
|
||||||
|
zbg == Nat.s yg &
|
||||||
|
zg == Nat.s zbg &
|
||||||
|
kbg == Nat.s zg &
|
||||||
|
kg == Nat.s kbg &
|
||||||
|
fg == Nat.s kg &
|
||||||
|
wg == Nat.s fg &
|
||||||
|
gg == Nat.s wg &
|
||||||
|
rg == Nat.s gg &
|
||||||
|
xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
|
||||||
|
ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
|
||||||
|
zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
|
||||||
|
kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||||
|
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
|
||||||
|
seqo [ReadS (DerefP (VarP 0));
|
||||||
|
WriteS (DerefP (VarP 0));
|
||||||
|
ReadS (DerefP (VarP 1))] fstmts &
|
||||||
|
fd == FunD ([(Mode (In, NOut), RefT (c_fx, UnitT (Rd, AlwaysWr)));
|
||||||
|
(Mode (In, NOut), RefT (c_fy, UnitT (Rd, NeverWr)))],
|
||||||
|
fstmts) &
|
||||||
|
wd == FunD ([(Mode (In, NOut), RefT (c_wx, UnitT (NRd, MayWr)))],
|
||||||
|
ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
|
||||||
|
seqo [WriteS (DerefP (VarP 0));
|
||||||
|
ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
|
||||||
|
ReadS (DerefP (VarP 0));
|
||||||
|
ReadS (DerefP (VarP 1))] gstmts &
|
||||||
|
gd == FunD ([(Mode (In, NOut), RefT (c_gx, UnitT (NRd, AlwaysWr)));
|
||||||
|
(Mode (In, NOut), RefT (c_gy, UnitT (Rd, MayWr)))],
|
||||||
|
gstmts) &
|
||||||
|
rd == FunD ([(Mode (In, NOut), RefT (c_rx, UnitT (Rd, NeverWr)))],
|
||||||
|
ReadS (DerefP (VarP 0))) &
|
||||||
|
seqo [
|
||||||
|
CallS (VarP wg, [PathE (VarP xg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP xg)]);
|
||||||
|
CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP yg)]);
|
||||||
|
CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
|
||||||
|
CallS (VarP wg, [PathE (VarP zg)]);
|
||||||
|
WriteS (DerefP (VarP zg));
|
||||||
|
CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
|
||||||
|
CallS (VarP rg, [PathE (VarP kg)])
|
||||||
|
] stmts &
|
||||||
|
prog == Prg ([xbd; xd;
|
||||||
|
ybd; yd;
|
||||||
|
zbd; zd;
|
||||||
|
kbd; kd;
|
||||||
|
fd; wd; gd; rd],
|
||||||
|
stmts) &
|
||||||
|
prog_evalo prog st &
|
||||||
|
q == [c_fx; c_fy; c_wx; c_gx; c_gy; c_rx]
|
||||||
|
})
|
||||||
|
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||||
|
|
||||||
|
(* complex type *)
|
||||||
|
|
||||||
let deref_accesso id v p' = ocanren {
|
let deref_accesso id v p' = ocanren {
|
||||||
p' == DerefP (AccessP (VarP v, id))
|
p' == DerefP (AccessP (VarP v, id))
|
||||||
|
|
@ -527,6 +692,256 @@ let access_deref_accesso id_ext id_int v p' = ocanren {
|
||||||
p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
|
p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
(* --- *)
|
||||||
|
|
||||||
|
let p_rw_unitTo tp = ocanren {
|
||||||
|
(* fresh r, w in *)
|
||||||
|
tp == UnitT (Rd, AlwaysWr)
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_rw_userTo tp = ocanren {
|
||||||
|
fresh x, y, z in
|
||||||
|
p_rw_unitTo x &
|
||||||
|
p_rw_unitTo y &
|
||||||
|
p_rw_unitTo z &
|
||||||
|
tp == TupleT [x; y; z]
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_rw_dataTo tp = ocanren {
|
||||||
|
fresh x, y in
|
||||||
|
p_rw_unitTo x &
|
||||||
|
p_rw_unitTo y &
|
||||||
|
tp == TupleT [x; y]
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_rw_timeTo tp = ocanren {
|
||||||
|
p_rw_unitTo tp
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_rw_requestTo cu cd ct tp = ocanren {
|
||||||
|
fresh userT, dataT, timeT in
|
||||||
|
p_rw_userTo userT &
|
||||||
|
p_rw_dataTo dataT &
|
||||||
|
p_rw_timeTo timeT &
|
||||||
|
tp == TupleT [RefT (cu, userT);
|
||||||
|
RefT (cd, dataT);
|
||||||
|
RefT (ct, timeT)]
|
||||||
|
}
|
||||||
|
|
||||||
|
(* --- *)
|
||||||
|
|
||||||
|
let p_any_unitTo tp = ocanren {
|
||||||
|
fresh r, w in
|
||||||
|
tp == UnitT (r, w)
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_any_userTo tp = ocanren {
|
||||||
|
fresh x, y, z in
|
||||||
|
p_any_unitTo x &
|
||||||
|
p_any_unitTo y &
|
||||||
|
p_any_unitTo z &
|
||||||
|
tp == TupleT [x; y; z]
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_any_dataTo tp = ocanren {
|
||||||
|
fresh x, y in
|
||||||
|
p_any_unitTo x &
|
||||||
|
p_any_unitTo y &
|
||||||
|
tp == TupleT [x; y]
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_any_timeTo tp = ocanren {
|
||||||
|
p_any_unitTo tp
|
||||||
|
}
|
||||||
|
|
||||||
|
let p_any_requestTo cu cd ct tp = ocanren {
|
||||||
|
fresh userT, dataT, timeT in
|
||||||
|
p_any_userTo userT &
|
||||||
|
p_any_dataTo dataT &
|
||||||
|
p_any_timeTo timeT &
|
||||||
|
tp == TupleT [RefT (cu, userT);
|
||||||
|
RefT (cd, dataT);
|
||||||
|
RefT (ct, timeT)]
|
||||||
|
}
|
||||||
|
|
||||||
|
(* --- *)
|
||||||
|
|
||||||
|
let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
|
||||||
|
(fun q -> ocanren {
|
||||||
|
fresh prog,
|
||||||
|
userT, dataT, timeT, requestT,
|
||||||
|
requestArgsT,
|
||||||
|
userE, dataE, timeE, requestE,
|
||||||
|
userVID, dataVID, timeVID, requestVID,
|
||||||
|
sendFID, sendD, sendBranchStmts, sendStmts,
|
||||||
|
stmts in
|
||||||
|
globals_min_ido userVID &
|
||||||
|
dataVID == Nat.s userVID &
|
||||||
|
timeVID == Nat.s dataVID &
|
||||||
|
requestVID == Nat.s timeVID &
|
||||||
|
sendFID == Nat.s requestVID &
|
||||||
|
|
||||||
|
p_rw_userTo userT &
|
||||||
|
p_rw_dataTo dataT &
|
||||||
|
p_rw_timeTo timeT &
|
||||||
|
p_rw_requestTo Cp Cp Cp requestT &
|
||||||
|
p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *)
|
||||||
|
|
||||||
|
userE == TupleE [UnitE; UnitE; UnitE] &
|
||||||
|
dataE == TupleE [UnitE; UnitE] &
|
||||||
|
timeE == UnitE &
|
||||||
|
requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
|
||||||
|
|
||||||
|
fresh data_p0, data_p1, time_p,
|
||||||
|
user_id_p, user_name_p, user_surname_p in
|
||||||
|
access_deref_accesso 0 1 0 data_p0 &
|
||||||
|
access_deref_accesso 1 1 0 data_p1 &
|
||||||
|
deref_accesso 2 0 time_p &
|
||||||
|
access_deref_accesso 0 0 0 user_id_p &
|
||||||
|
access_deref_accesso 1 0 0 user_name_p &
|
||||||
|
access_deref_accesso 2 0 0 user_surname_p &
|
||||||
|
seqo [ReadS data_p0;
|
||||||
|
ReadS data_p1;
|
||||||
|
WriteS data_p0;
|
||||||
|
WriteS data_p1;
|
||||||
|
|
||||||
|
ReadS user_name_p;
|
||||||
|
WriteS user_name_p] sendBranchStmts &
|
||||||
|
seqo [sendBranchStmts; (* TMP *)
|
||||||
|
(* TODO: FIXME *)
|
||||||
|
(* ChoiceS (sendBranchStmts, SkipS); *)
|
||||||
|
WriteS time_p;
|
||||||
|
|
||||||
|
ReadS data_p0;
|
||||||
|
ReadS data_p1;
|
||||||
|
ReadS time_p;
|
||||||
|
ReadS user_id_p;
|
||||||
|
ReadS user_name_p;
|
||||||
|
ReadS user_surname_p] sendStmts &
|
||||||
|
(* sendStmts == SkipS & *)
|
||||||
|
sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
|
||||||
|
|
||||||
|
fresh time_gp, user_name_gp, user_surname_gp in
|
||||||
|
deref_accesso 2 requestVID time_gp &
|
||||||
|
access_deref_accesso 1 0 requestVID user_name_gp &
|
||||||
|
access_deref_accesso 2 0 requestVID user_surname_gp &
|
||||||
|
seqo [
|
||||||
|
CallS (VarP sendFID, [PathE (VarP requestVID)]);
|
||||||
|
WriteS time_gp;
|
||||||
|
(* TODO: FIXME *)
|
||||||
|
(* ChoiceS (ReadS user_name_gp, *)
|
||||||
|
(* ReadS user_surname_gp); *)
|
||||||
|
ReadS user_name_gp; (* TMP *)
|
||||||
|
ReadS user_surname_gp; (* TMP *)
|
||||||
|
ReadS time_gp
|
||||||
|
] stmts &
|
||||||
|
prog == Prg ([
|
||||||
|
VarD (userT, userE);
|
||||||
|
VarD (dataT, dataE);
|
||||||
|
VarD (timeT, timeE);
|
||||||
|
VarD (requestT, requestE);
|
||||||
|
sendD
|
||||||
|
],
|
||||||
|
stmts
|
||||||
|
) &
|
||||||
|
prog_evalo prog q
|
||||||
|
})
|
||||||
|
(fun q -> q#reify (StEnv.prj_exn))))
|
||||||
|
|
||||||
|
let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (run q
|
||||||
|
(fun q -> ocanren {
|
||||||
|
fresh prog,
|
||||||
|
userT, dataT, timeT, requestT,
|
||||||
|
requestArgsT,
|
||||||
|
userE, dataE, timeE, requestE,
|
||||||
|
userVID, dataVID, timeVID, requestVID,
|
||||||
|
sendFID, sendD, sendBranchStmts, sendStmts,
|
||||||
|
stmts,
|
||||||
|
st, c_u, c_d, c_t in
|
||||||
|
globals_min_ido userVID &
|
||||||
|
dataVID == Nat.s userVID &
|
||||||
|
timeVID == Nat.s dataVID &
|
||||||
|
requestVID == Nat.s timeVID &
|
||||||
|
sendFID == Nat.s requestVID &
|
||||||
|
|
||||||
|
p_rw_userTo userT &
|
||||||
|
p_rw_dataTo dataT &
|
||||||
|
p_rw_timeTo timeT &
|
||||||
|
p_rw_requestTo Cp Cp Cp requestT &
|
||||||
|
p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *)
|
||||||
|
|
||||||
|
userE == TupleE [UnitE; UnitE; UnitE] &
|
||||||
|
dataE == TupleE [UnitE; UnitE] &
|
||||||
|
timeE == UnitE &
|
||||||
|
requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
|
||||||
|
|
||||||
|
fresh data_p0, data_p1, time_p,
|
||||||
|
user_id_p, user_name_p, user_surname_p in
|
||||||
|
access_deref_accesso 0 1 0 data_p0 &
|
||||||
|
access_deref_accesso 1 1 0 data_p1 &
|
||||||
|
deref_accesso 2 0 time_p &
|
||||||
|
access_deref_accesso 0 0 0 user_id_p &
|
||||||
|
access_deref_accesso 1 0 0 user_name_p &
|
||||||
|
access_deref_accesso 2 0 0 user_surname_p &
|
||||||
|
seqo [ReadS data_p0;
|
||||||
|
ReadS data_p1;
|
||||||
|
WriteS data_p0;
|
||||||
|
WriteS data_p1;
|
||||||
|
|
||||||
|
ReadS user_name_p;
|
||||||
|
WriteS user_name_p] sendBranchStmts &
|
||||||
|
seqo [sendBranchStmts; (* TMP *)
|
||||||
|
(* TODO: FIXME *)
|
||||||
|
(* ChoiceS (sendBranchStmts, SkipS); *)
|
||||||
|
WriteS time_p;
|
||||||
|
|
||||||
|
ReadS data_p0;
|
||||||
|
ReadS data_p1;
|
||||||
|
ReadS time_p;
|
||||||
|
ReadS user_id_p;
|
||||||
|
ReadS user_name_p;
|
||||||
|
ReadS user_surname_p] sendStmts &
|
||||||
|
(* sendStmts == SkipS & *)
|
||||||
|
sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
|
||||||
|
|
||||||
|
fresh time_gp, user_name_gp, user_surname_gp in
|
||||||
|
deref_accesso 2 requestVID time_gp &
|
||||||
|
access_deref_accesso 1 0 requestVID user_name_gp &
|
||||||
|
access_deref_accesso 2 0 requestVID user_surname_gp &
|
||||||
|
seqo [
|
||||||
|
CallS (VarP sendFID, [PathE (VarP requestVID)]);
|
||||||
|
WriteS time_gp;
|
||||||
|
(* TODO: FIXME *)
|
||||||
|
(* ChoiceS (ReadS user_name_gp, *)
|
||||||
|
(* ReadS user_surname_gp); *)
|
||||||
|
ReadS user_name_gp; (* TMP *)
|
||||||
|
ReadS user_surname_gp; (* TMP *)
|
||||||
|
ReadS time_gp
|
||||||
|
] stmts &
|
||||||
|
prog == Prg ([
|
||||||
|
VarD (userT, userE);
|
||||||
|
VarD (dataT, dataE);
|
||||||
|
VarD (timeT, timeE);
|
||||||
|
VarD (requestT, requestE);
|
||||||
|
sendD
|
||||||
|
],
|
||||||
|
stmts
|
||||||
|
) &
|
||||||
|
prog_evalo prog st &
|
||||||
|
q == [c_u; c_d; c_t]
|
||||||
|
})
|
||||||
|
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||||
|
|
||||||
|
(* - complex tests *)
|
||||||
|
|
||||||
|
(* let deref_accesso id v p' = ocanren { *)
|
||||||
|
(* p' == DerefP (AccessP (VarP v, id)) *)
|
||||||
|
(* } *)
|
||||||
|
|
||||||
|
(* let access_deref_accesso id_ext id_int v p' = ocanren { *)
|
||||||
|
(* p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) *)
|
||||||
|
(* } *)
|
||||||
|
|
||||||
let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren {
|
let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren {
|
||||||
p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
|
p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
|
||||||
}
|
}
|
||||||
|
|
@ -965,4 +1380,4 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
||||||
CallS (VarP send_allID, [PathE (VarP requestID)])
|
CallS (VarP send_allID, [PathE (VarP requestID)])
|
||||||
) &
|
) &
|
||||||
prog_evalo prog st })
|
prog_evalo prog st })
|
||||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)
|
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue