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. "fac507bebf28e5dd9e48fda6a59756b9ba8b6282" and "eff48a1c6e993a9d2bfa2b07453a90504a32820b" have entirely different histories.
fac507bebf
...
eff48a1c6e
4 changed files with 22 additions and 144 deletions
|
|
@ -195,19 +195,6 @@ struct
|
|||
|
||||
(* - value construction *)
|
||||
|
||||
let rec valbuild (mem : mem) (t : atype) : mem * value =
|
||||
match t with
|
||||
| UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
|
||||
| UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
|
||||
| FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported"
|
||||
| RefT (_, t) -> let (mem', v') = valbuild mem t in
|
||||
let (mem'', id'') = mem_add mem' v' in
|
||||
(mem'', RefV id'')
|
||||
| TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in
|
||||
(mem', v' :: vs') in
|
||||
let mem', vs' = List.fold_right folder ts (mem, []) in
|
||||
(mem', TupleV vs')
|
||||
|
||||
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
|
||||
match t, v with
|
||||
| UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
|
||||
|
|
@ -217,10 +204,10 @@ struct
|
|||
| RefT (_, 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 v t (mem, vs') -> 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
|
||||
(mem', v' :: vs') in
|
||||
let mem', vs' = List.fold_right2 folder vs ts (mem, []) in
|
||||
(mem', TupleV vs')
|
||||
let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
|
||||
(mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
|
||||
| _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
|
||||
|
||||
(* - action rules *)
|
||||
|
|
|
|||
|
|
@ -540,69 +540,9 @@ $action$ - действия, совершаемые с примитивным з
|
|||
|
||||
=== Value Construction
|
||||
|
||||
#let build = `build`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ build trivial read value],
|
||||
|
||||
$mu xarrowSquiggly(cl Read \, w cr)_build
|
||||
cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ build trivial $not$ read value],
|
||||
|
||||
$mu xarrowSquiggly(cl not Read \, w cr)_build
|
||||
cl cdl bot, 0_r, 0_w cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
// TODO: function pointer type ??
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ build reference value],
|
||||
|
||||
$mu xarrowSquiggly(t)_build cl v, mu_v cr$,
|
||||
|
||||
$mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
|
||||
|
||||
$mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ build tuple value],
|
||||
|
||||
$mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
|
||||
$...$,
|
||||
$mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
|
||||
|
||||
$mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
// ---
|
||||
|
||||
// TODO: FIXME:add ref / copy modes correctness check ??
|
||||
|
||||
// #let copy = `copy`
|
||||
#let new = `new`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
|
|
@ -611,26 +551,22 @@ $action$ - действия, совершаемые с примитивным з
|
|||
|
||||
$v_m in {0, ?, bot}$,
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl Read \, w cr)_copy
|
||||
cl cdl v_m, 0_r, 0_w cdr, mu cr$,
|
||||
xarrowSquiggly(cl Read \, w cr)_new
|
||||
cl cdl v_m, 0, 0 cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ new trivial read $top$ value],
|
||||
|
||||
// $cl cdl top, v_r, v_w cdr, mu cr
|
||||
// xarrowSquiggly(cl Read \, w cr)_copy
|
||||
// xarrowSquiggly(cl Read \, w cr)_new
|
||||
// cl cdl 0, 0, 0 cdr, mu cr$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
|
|
@ -638,61 +574,53 @@ $action$ - действия, совершаемые с примитивным з
|
|||
|
||||
$v_m in {0, ?, bot/*, top */}$,
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl not Read \, w cr)_copy
|
||||
cl cdl bot, 0_r, 0_w cdr, mu cr$,
|
||||
xarrowSquiggly(cl not Read \, w cr)_new
|
||||
cl cdl bot, 0, 0 cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new funciton pointer value],
|
||||
|
||||
$cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$,
|
||||
$cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ new reference ref value],
|
||||
|
||||
// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$,
|
||||
// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
// #h(10pt)
|
||||
|
||||
// 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],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(t)_copy 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$,
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new tuple value],
|
||||
|
||||
$cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$,
|
||||
$cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
|
||||
$...$,
|
||||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$,
|
||||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
|
||||
|
||||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$,
|
||||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -1139,7 +1067,7 @@ $action$ - действия, совершаемые с примитивным з
|
|||
// expect well typed program
|
||||
|
||||
$vals, mu texpre e eqmu v$,
|
||||
$cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?)
|
||||
$cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?)
|
||||
$mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
|
||||
|
||||
$cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
|
||||
|
|
@ -1426,7 +1354,7 @@ $action$ - действия, совершаемые с примитивным з
|
|||
// TODO: check type compatibility for t and type for path p (?)
|
||||
// [*TODO: check t ~ t' in sme way (?)*],
|
||||
// <- programs considired to be well-typed
|
||||
$cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$,
|
||||
$cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
|
||||
$mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
|
||||
|
||||
// TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
|
||||
|
|
|
|||
|
|
@ -588,44 +588,6 @@ struct
|
|||
|
||||
(* - value construction *)
|
||||
|
||||
let rec valbuild_foldero mem_with_vs tp mem_with_vs' =
|
||||
ocanren {
|
||||
fresh mem, vs, mem', v', vs' in
|
||||
Std.pair mem vs == mem_with_vs &
|
||||
valbuildo mem tp (Std.pair mem' v') &
|
||||
vs' == v' :: vs &
|
||||
mem_with_vs' == Std.pair mem' vs'
|
||||
}
|
||||
and valbuildo mem tp mem_with_id' =
|
||||
let open Type in
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
(* let open CopyCap in *)
|
||||
let open MemVal in
|
||||
let open ReadVal in
|
||||
let open WriteVal in
|
||||
ocanren {
|
||||
{ fresh r, w in
|
||||
tp == UnitT (r, w) &
|
||||
{ { r == Rd &
|
||||
mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } |
|
||||
{ r == NRd &
|
||||
mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
|
||||
(* { fresh ts in *)
|
||||
(* tp == FunT ts & *)
|
||||
(* ??? } | *)
|
||||
{ fresh c, tp' in
|
||||
tp == RefT (c, tp') &
|
||||
{ fresh mem_cp, v_cp, mem_add, id_add in
|
||||
valbuildo mem 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 tps, mem', vs' in
|
||||
tp == TupleT tps &
|
||||
list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') &
|
||||
mem_with_id' == Std.pair mem' (TupleV vs') }
|
||||
}
|
||||
|
||||
let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
|
||||
ocanren {
|
||||
fresh mem, vs, mem', v', vs' in
|
||||
|
|
@ -644,6 +606,7 @@ struct
|
|||
let open WriteVal in
|
||||
ocanren {
|
||||
{ fresh r, w in
|
||||
is_trivial_vo v &
|
||||
tp == UnitT (r, w) &
|
||||
{ { fresh v_m, _v_r, _v_w in
|
||||
r == Rd &
|
||||
|
|
|
|||
|
|
@ -1018,8 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
|
|||
ReadS sb_access3]
|
||||
sendFBranch &
|
||||
seqo [ChoiceS (sendFBranch, SkipS);
|
||||
WriteS (VarP 0);
|
||||
ReadS (VarP 0)]
|
||||
WriteS (VarP 0));
|
||||
ReadS (VarP 0))]
|
||||
sendF &
|
||||
|
||||
fresh sa_access0, sa_access1, sa_access2, sa_access3 in
|
||||
|
|
@ -1027,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
|
|||
access_deref_accesso 1 1 0 sa_access1 &
|
||||
access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
|
||||
access_deref_accesso 0 1 0 sa_access3 &
|
||||
seqo [WriteS (VarP 0);
|
||||
seqo [WriteS (VarP 0));
|
||||
CallS (VarP sendID, [PathE (VarP 0)]);
|
||||
CallS (VarP get_version_idID, [PathE (VarP 0)]);
|
||||
CallS (VarP updated_versionID, [PathE (VarP 0)]);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue