mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
No commits in common. "8fc0ffa805bc383c47b9c0bad35171ee24835421" and "1d65b67260643e859b17e9e73e40b73def6896cb" have entirely different histories.
8fc0ffa805
...
1d65b67260
5 changed files with 48 additions and 588 deletions
|
|
@ -200,8 +200,8 @@ struct
|
|||
| UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
|
||||
| UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
|
||||
| FunT _, FunV _ -> (mem, v)
|
||||
(* | RefT (Rf, _), RefV _ -> (mem, v) *)
|
||||
| RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
||||
| RefT (Rf, _), RefV _ -> (mem, v)
|
||||
| RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
||||
let (mem'', id'') = mem_add mem' v' in
|
||||
(mem'', RefV id'')
|
||||
| TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
|
||||
|
|
@ -570,7 +570,6 @@ struct
|
|||
let vg8 = VarP (globals_min_id + 8)
|
||||
let vg9 = VarP (globals_min_id + 9)
|
||||
let vg10 = VarP (globals_min_id + 10)
|
||||
let vg11 = VarP (globals_min_id + 11)
|
||||
|
||||
let rf0E = RefE 0
|
||||
let rf1E = RefE 1
|
||||
|
|
@ -988,117 +987,6 @@ struct
|
|||
Printf.printf "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 *)
|
||||
|
||||
(* TODO: FIXME: rw tags *)
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
|
||||
== 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
|
||||
|
||||
|
|
@ -581,26 +581,28 @@ $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(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference /* copy */ value],
|
||||
name: [ new reference ref 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$,
|
||||
|
||||
$mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
|
|||
|
|
@ -569,11 +569,11 @@ struct
|
|||
pathvalo mem vals p' v' &
|
||||
v' == RefV id &
|
||||
mem_geto mem id v } |
|
||||
{ fresh p', id', v', vs in
|
||||
p == AccessP (p', id') &
|
||||
{ fresh p', id, v', vs in
|
||||
p == AccessP (p', id) &
|
||||
pathvalo mem vals p' v' &
|
||||
v' == TupleV vs &
|
||||
list_ntho vs id' v }
|
||||
list_ntho vs id v }
|
||||
}
|
||||
|
||||
(* --- eval rules --- *)
|
||||
|
|
@ -592,7 +592,7 @@ struct
|
|||
let open Type in
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
(* let open CopyCap in *)
|
||||
let open CopyCap in
|
||||
let open MemVal in
|
||||
let open ReadVal in
|
||||
let open WriteVal in
|
||||
|
|
@ -613,13 +613,13 @@ struct
|
|||
{ fresh c, tp', id in
|
||||
v == RefV id &
|
||||
tp == RefT (c, tp') &
|
||||
(* { c == Rf & mem_with_id' == Std.pair mem v } | *)
|
||||
{ fresh v', mem_cp, v_cp, mem_add, id_add in
|
||||
(* c == Cp & *)
|
||||
mem_geto mem id v' &
|
||||
valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
|
||||
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
|
||||
mem_with_id' == (mem_add, RefV id_add) } } |
|
||||
{ { c == Rf & mem_with_id' == Std.pair mem v } |
|
||||
{ fresh v', mem_cp, v_cp, mem_add, id_add in
|
||||
c == Cp &
|
||||
mem_geto mem id v' &
|
||||
valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
|
||||
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
|
||||
mem_with_id' == (mem_add, RefV id_add) } } } |
|
||||
{ fresh vs, tps, mem', vs' in
|
||||
v == TupleV vs &
|
||||
tp == TupleT tps &
|
||||
|
|
@ -727,8 +727,8 @@ struct
|
|||
ocanren {
|
||||
{ u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
|
||||
{ u == BotMV & v == BotMV & u' == BotMV } |
|
||||
{ { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } &
|
||||
{ u =/= BotMV | { u == BotMV & v =/= BotMV } } &
|
||||
{ u =/= ZeroMV & v =/= ZeroMV &
|
||||
u =/= BotMV & v =/= BotMV &
|
||||
u' == SmthMV }
|
||||
}
|
||||
|
||||
|
|
@ -749,8 +749,8 @@ struct
|
|||
ocanren {
|
||||
{ u == OneWV & v == OneWV & u' == OneWV } |
|
||||
{ u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
|
||||
{ { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } &
|
||||
{ u =/= OneWV | { u == OneWV & v =/= OneWV } } &
|
||||
{ u =/= ZeroWV & v =/= ZeroWV &
|
||||
u =/= OneWV & v =/= OneWV &
|
||||
u' == SmthWV }
|
||||
}
|
||||
|
||||
|
|
@ -775,8 +775,7 @@ struct
|
|||
{ fresh a, b in
|
||||
u == RefV a &
|
||||
v == RefV b &
|
||||
a == b &
|
||||
u' == RefV a } |
|
||||
a == b } |
|
||||
{ fresh us, vs, us' in
|
||||
u == TupleV us &
|
||||
v == TupleV vs &
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -28,30 +28,16 @@ open StEnv
|
|||
(* - shortcuts *)
|
||||
|
||||
(* NOTE: redo with fold ?? *)
|
||||
let seq_foldero stmt_acc stmt stmt_acc' = ocanren {
|
||||
stmt_acc' == SeqS(stmt, stmt_acc)
|
||||
}
|
||||
let seqo stmts stmt' = ocanren {
|
||||
list_foldro seq_foldero SkipS stmts stmt'
|
||||
}
|
||||
(* ocanren { *)
|
||||
(* { stmts == [] & stmt' == SkipS } | *)
|
||||
(* { fresh s in *)
|
||||
(* stmts == [s] & *)
|
||||
(* stmt' == s } | *)
|
||||
(* { fresh s, s', ss, stmt_rest' in *)
|
||||
(* stmts == s :: s' :: ss & *)
|
||||
(* seqo (s' :: ss) stmt_rest' & *)
|
||||
(* stmt' == SeqS(s, stmt_rest') *)
|
||||
(* } *)
|
||||
(* } *)
|
||||
|
||||
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 rec seqo stmts stmt' = ocanren {
|
||||
{ stmts == [] & stmt' == SkipS } |
|
||||
{ fresh s in
|
||||
stmts == [s] &
|
||||
stmt' == s } |
|
||||
{ fresh s, s', ss, stmt_rest' in
|
||||
stmts == s :: s' :: ss &
|
||||
seqo (s' :: ss) stmt_rest' &
|
||||
stmt' == SeqS(s, stmt_rest')
|
||||
}
|
||||
}
|
||||
|
||||
(* - basic var tests *)
|
||||
|
|
@ -531,158 +517,7 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
|
|||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.prj_exn))))
|
||||
|
||||
(* - 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 *)
|
||||
(* - complex tests *)
|
||||
|
||||
let deref_accesso id v p' = ocanren {
|
||||
p' == DerefP (AccessP (VarP v, id))
|
||||
|
|
@ -692,256 +527,6 @@ let access_deref_accesso id_ext id_int v p' = ocanren {
|
|||
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 {
|
||||
p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
|
||||
}
|
||||
|
|
@ -1380,4 +965,4 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
|||
CallS (VarP send_allID, [PathE (VarP requestID)])
|
||||
) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue