mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
2 commits
4eb3dea966
...
0be430a59b
| Author | SHA1 | Date | |
|---|---|---|---|
|
0be430a59b | ||
|
|
967d213f54 |
2 changed files with 286 additions and 160 deletions
|
|
@ -1,50 +1,212 @@
|
|||
module Functional =
|
||||
struct
|
||||
|
||||
(* --- types --- *)
|
||||
|
||||
type data = int
|
||||
type memid = int
|
||||
|
||||
(* --- syntax --- *)
|
||||
|
||||
type read_cap = Rd | NRd
|
||||
|
||||
type write_cap = AlwaysWr | MayWr | NeverWr
|
||||
type copy_cap = Cp | NCp
|
||||
type copy_cap = Cp | Rf
|
||||
|
||||
type in_cap = In | NIn
|
||||
type out_cap = Out | NOut
|
||||
|
||||
type tag = read_cap * write_cap * copy_cap * in_cap * out_cap
|
||||
type mode = in_cap * out_cap
|
||||
|
||||
type path = VarP of data | DerefP of path | AccessP of path * data
|
||||
type argtype = UnitT | RefT of tag * argtype | TupleT of argtype list | FunT of data
|
||||
type argmem = VarM of data | RefM of argmem | TupleM of argmem list | FunM
|
||||
|
||||
type stmt = Call of data * path list | CallLam of path * path list | Read of path | Write of path | Choice of stmt list * stmt list
|
||||
type body = stmt list
|
||||
type atype = UnitT of read_cap * write_cap
|
||||
| RefT of copy_cap * atype
|
||||
| TupleT of atype list
|
||||
| FunT of data (* declaration id for ease of impl (?) *)
|
||||
|
||||
type fun_decl = argtype list * body
|
||||
type prog = fun_decl list * fun_decl
|
||||
type mtype = mode * atype
|
||||
|
||||
type expr = UnitE
|
||||
| PathE of path
|
||||
(* | RefE *)
|
||||
| TupleE of expr list
|
||||
|
||||
type stmt = CallS of path * expr list
|
||||
| WriteS of path
|
||||
| ReadS of path
|
||||
| SeqS of stmt * stmt
|
||||
| ChoiceS of stmt * stmt
|
||||
|
||||
type decl = VarD of (* data * *) atype * expr
|
||||
| FunD of (* data * *) (* (data * *) mtype (* ) *) list * stmt
|
||||
|
||||
type prog = decl list * stmt
|
||||
|
||||
(* --- exceptions --- *)
|
||||
|
||||
exception Incorrect_memory_access of int
|
||||
exception Ref_rvalue_argument of int
|
||||
exception Incorrect_const_cast of int
|
||||
exception Invalid_argument_tag of int
|
||||
exception Incompatible_states
|
||||
exception Incompatible_path_and_type
|
||||
exception Incompatible_path_and_mem
|
||||
exception Incompatible_path_and_type_for_tag
|
||||
(* exception Incorrect_memory_access of int *)
|
||||
(* exception Ref_rvalue_argument of int *)
|
||||
(* exception Incorrect_const_cast of int *)
|
||||
(* exception Invalid_argument_tag of int *)
|
||||
(* exception Incompatible_states *)
|
||||
(* exception Incompatible_path_and_type *)
|
||||
(* exception Incompatible_path_and_mem *)
|
||||
(* exception Incompatible_path_and_type_for_tag *)
|
||||
exception Typing_error of string
|
||||
|
||||
(* --- static interpreter (no rec) --- *)
|
||||
(* value model & memory model *)
|
||||
|
||||
(* TODO: allow data (rvalue) in calls ?? *)
|
||||
type arg = RValue | LValue of path
|
||||
type value = UnitV | UndefV | BotV
|
||||
type deepvalue = ZeroDV
|
||||
| SmthDV
|
||||
| BotDV
|
||||
| FunDV of (* data list * *) stmt
|
||||
| RefDV of deepvalue
|
||||
| TupleDV of deepvalue list
|
||||
|
||||
type env = (int * (argmem * argtype)) list
|
||||
type value = ZeroV
|
||||
| SmthV
|
||||
| BotV
|
||||
| FunV of (* data list * *) stmt
|
||||
| RefV of memid
|
||||
| TupleV of value list
|
||||
|
||||
(* env * memory * last unused memory * visited functions *)
|
||||
type state = env * value list * int * int list
|
||||
(* TODO: any additional difference between rvalue and lvalue now ?? *)
|
||||
|
||||
(* --- *)
|
||||
|
||||
type mem = (memid * value) list * memid (* NOTE: memory and first free elem *)
|
||||
type types = (data * atype) list
|
||||
type vals = (data * memid) list
|
||||
type state = mem * types * vals
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* TODO: FIXME: use list_replace for memory instead ?? *)
|
||||
let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem)
|
||||
let mem_add (mem : mem) (v : value) : mem * memid =
|
||||
(((snd mem, v) :: fst mem, snd mem + 1), snd mem)
|
||||
let mem_set (mem : mem) (id : memid) (v : value) : mem =
|
||||
((id, v) :: fst mem, snd mem)
|
||||
|
||||
let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
|
||||
| ZeroV -> ZeroDV
|
||||
| SmthV -> SmthDV
|
||||
| BotV -> BotDV
|
||||
| FunV s -> FunDV s
|
||||
| RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
|
||||
| TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
|
||||
|
||||
let is_trivial_v (v : value) : bool =
|
||||
v == ZeroV || v == SmthV || v == BotV
|
||||
|
||||
(* --- path accessors --- *)
|
||||
|
||||
let rec pathvar (p : path) : data = match p with
|
||||
| VarP x -> x
|
||||
| DerefP p -> pathvar p
|
||||
| AccessP (p, _) -> pathvar p
|
||||
|
||||
let rec pathtype (types : types) (p : path) : atype = match p with
|
||||
| VarP x -> List.assoc x types
|
||||
| DerefP p -> (match pathtype types p with
|
||||
| RefT (_, t) -> t
|
||||
| _ -> raise @@ Typing_error "pathtype: deref")
|
||||
| AccessP (p, id) -> match pathtype types p with
|
||||
| TupleT ts -> (List.nth ts id)
|
||||
| _ -> raise @@ Typing_error "pathtype: access"
|
||||
|
||||
let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with
|
||||
| VarP x -> mem_get mem @@ List.assoc x vals
|
||||
| DerefP p -> (match pathval mem vals p with
|
||||
| RefV id -> mem_get mem id
|
||||
| _ -> raise @@ Typing_error "pathval: deref")
|
||||
| AccessP (p, id) -> match pathval mem vals p with
|
||||
| TupleV vs -> (List.nth vs id)
|
||||
| _ -> raise @@ Typing_error "pathval: access"
|
||||
|
||||
(* --- eval rules --- *)
|
||||
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
|
||||
| _ :: xs, 0 -> y :: xs
|
||||
| x :: xs, _ -> x :: list_replace xs (id - 1) y
|
||||
| [], _ -> raise Not_found
|
||||
|
||||
(* - value construction *)
|
||||
|
||||
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with
|
||||
| UnitT (Rd, w), ZeroV -> (mem, v)
|
||||
| UnitT (Rd, w), SmthV -> (mem, v)
|
||||
| UnitT (Rd, w), BotV -> (mem, v)
|
||||
| UnitT (NRd, w), ZeroV -> (mem, BotV)
|
||||
| UnitT (NRd, w), SmthV -> (mem, BotV)
|
||||
| UnitT (NRd, w), BotV -> (mem, BotV)
|
||||
| FunT _, FunV _ -> (mem, v)
|
||||
| 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
|
||||
mem, v' :: vs' in
|
||||
let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
|
||||
(mem', TupleV vs')
|
||||
| _, _ -> raise @@ Typing_error "valcopy"
|
||||
|
||||
(* - value update *)
|
||||
|
||||
let rec valupd (mem : mem) (v : value) (p : path) (b : value) : mem * value = match p, v with
|
||||
| VarP x, _ -> (mem, b)
|
||||
| DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
|
||||
(mem_set mem' id v', RefV id)
|
||||
| AccessP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p b in
|
||||
(mem', TupleV (list_replace vs id v'))
|
||||
| _, _ -> raise @@ Typing_error "valupd"
|
||||
|
||||
(* - value combination *)
|
||||
|
||||
let rec valcomb (u : value) (v : value) : value =
|
||||
if is_trivial_v u && is_trivial_v v
|
||||
then (if u == v then u else BotV)
|
||||
else match u, v with
|
||||
(* TODO: FIXME: combining semanticsfor funcitons statements *)
|
||||
| FunV s, FunV t -> if s == t then u else raise @@ Typing_error "valcomb: fun"
|
||||
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
|
||||
| TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
|
||||
| _, _ -> raise @@ Typing_error "valcomb"
|
||||
|
||||
(* TODO: func for list memory, not assoc list *)
|
||||
(* let rec memcomb (m : mem) (n : mem) : mem = *)
|
||||
(* if snd m != snd n *)
|
||||
(* then raise @@ Typing_error "memcomb" *)
|
||||
(* else (List.map2 valcomb (fst m) (fst n), snd m) *)
|
||||
|
||||
(* - call values spoil *)
|
||||
|
||||
(* TODO: check all cases *)
|
||||
let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
|
||||
(r' : read_cap) (w' : write_cap) (m : mode)
|
||||
(c : copy_cap) : bool =
|
||||
(r != Rd || v == ZeroV) &&
|
||||
(r != Rd || fst m == In) &&
|
||||
(o != Out || w == AlwaysWr) &&
|
||||
(* TODO: check *)
|
||||
((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
|
||||
is_trivial_v v
|
||||
|
||||
let rec valspoil (mem : mem) (v : value) (t : atype)
|
||||
(u : atype) (m : mode) (c : copy_cap)
|
||||
: mem * value = match t, u, v with
|
||||
| UnitT (r, w), UnitT (r', w'), _ -> (* TODO FIXME *) raise Not_found
|
||||
| FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
|
||||
| RefT (ct, t), RefT (cu, u), RefV id ->
|
||||
let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
|
||||
(mem_set mem id v', RefV id)
|
||||
| TupleT ts, TupleT us, TupleV vs -> (* TODO FIXME *) raise Not_found
|
||||
| _, _, _ -> raise @@ Typing_error "valspoil"
|
||||
|
||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||
|
||||
(* let rec argsspoil (* full spoil *) *)
|
||||
|
||||
(* --- *)
|
||||
|
||||
|
|
@ -277,12 +439,12 @@ struct
|
|||
let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
|
||||
let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
|
||||
let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
|
||||
let rwi_ref : tag = (Rd, AlwaysWr, NCp, In, NOut)
|
||||
let rmwi_ref : tag = (Rd, MayWr, NCp, In, NOut)
|
||||
let ri_ref : tag = (Rd, NeverWr, NCp, In, NOut)
|
||||
let wi_ref : tag = (NRd, AlwaysWr, NCp, In, NOut)
|
||||
let mwi_ref : tag = (NRd, MayWr, NCp, In, NOut)
|
||||
let i_ref : tag = (NRd, NeverWr, NCp, In, NOut)
|
||||
let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut)
|
||||
let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut)
|
||||
let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut)
|
||||
let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut)
|
||||
let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut)
|
||||
let i_ref : tag = (NRd, NeverWr, Rf, In, NOut)
|
||||
|
||||
(* >> tests without functions *)
|
||||
|
||||
|
|
|
|||
|
|
@ -73,7 +73,7 @@
|
|||
Prod(
|
||||
`mode`,
|
||||
{
|
||||
Or[$inTag space outTag$][]
|
||||
Or[$inTag outTag$][]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
|
|
@ -112,7 +112,7 @@
|
|||
{
|
||||
Or[$()$][value of simple type] // `Unit`
|
||||
Or[$path$][value from variable] // `Path`
|
||||
// TODO: FIXME: decide what is the result of ref expr eval
|
||||
// TODO: decide what is the result of ref expr eval
|
||||
// Or[$rf expr$][reference expr] // `Ref`
|
||||
Or[$[expr+]$][tuple expr] // `Prod`
|
||||
}
|
||||
|
|
@ -138,7 +138,7 @@
|
|||
Prod(
|
||||
`prog`,
|
||||
{
|
||||
Or[$decl stmt$][declarations and executet statement]
|
||||
Or[$decl+ space stmt$][declarations and executed statement]
|
||||
}
|
||||
),
|
||||
)
|
||||
|
|
@ -155,7 +155,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
|
||||
Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
|
||||
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -166,7 +166,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
|
||||
Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
|
||||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[value+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -225,9 +225,6 @@ $sigma : envt := X -> type, space types : envt$ - #[ типы значений
|
|||
// $d in decl, $
|
||||
$s in stmt, f in X, x in X, a in X$
|
||||
|
||||
// FIXME ??
|
||||
// $d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
|
||||
|
||||
=== Path Accessors
|
||||
|
||||
Набор частично определённых фунций для работы с путями.
|
||||
|
|
@ -373,85 +370,61 @@ $s in stmt, f in X, x in X, a in X$
|
|||
|
||||
// TODO: introduce spep env argument ??
|
||||
|
||||
=== Moded Type Correctness
|
||||
|
||||
*NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
|
||||
|
||||
#let tcorrect = $attach(tack.r, br: #[correct])$
|
||||
|
||||
// TODO: FIXME: well formatness for mode, extract
|
||||
// TODO: FIXME: check for mode, is recursion required ??
|
||||
// TODO: FIXME: check mode & access corectness in os correct
|
||||
|
||||
$ vals in envv, types in envt, space mu in mem, space m in mode,
|
||||
space c in copyTag, space r, r' in readTag, space w, w' in writeTag,
|
||||
space v in value, space t, t' in type $
|
||||
|
||||
#h(10pt)
|
||||
|
||||
// TODO: FIXME: complete rule check
|
||||
// + add part about ref -> not copy later
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit assignment tags correctness],
|
||||
|
||||
$r = Read => m = (In, \_)$,
|
||||
$m = (\_, Out) => w = AlwaysWrite$,
|
||||
// $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
|
||||
$(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
|
||||
// $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
|
||||
$v in {0, \#, bot}$,
|
||||
$r = Read => v = 0$,
|
||||
|
||||
$types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ function pointer tags correctness],
|
||||
|
||||
$types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ ref assignment tags correctness],
|
||||
|
||||
$types, vals, mu, m, c_r tcorrect v : t -> t'$,
|
||||
|
||||
// TODO: FIXME: which tag translations are correct ?? <- only assignee?
|
||||
$types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ tuple assignmenttags correctness],
|
||||
|
||||
$types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
|
||||
|
||||
$...$,
|
||||
|
||||
$types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
|
||||
|
||||
$types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... t'_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
// --- >>> ---
|
||||
// === Moded Type Correctness
|
||||
// *NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
|
||||
// #let tcorrect = $attach(tack.r, br: #[correct])$
|
||||
// $ vals in envv, types in envt, space mu in mem, space m in mode,
|
||||
// space c in copyTag, space r, r' in readTag, space w, w' in writeTag,
|
||||
// space v in value, space t, t' in type $
|
||||
// #h(10pt)
|
||||
// // TODO: FIXME: complete rule check
|
||||
// // + add part about ref -> not copy later
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit assignment tags correctness],
|
||||
// $r = Read => m = (In, \_)$,
|
||||
// $m = (\_, Out) => w = AlwaysWrite$,
|
||||
// // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
|
||||
// $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
// // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
|
||||
// $v in {0, \#, bot}$,
|
||||
// $r = Read => v = 0$,
|
||||
// $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
|
||||
// )
|
||||
// ))
|
||||
// #h(10pt)
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ function pointer tags correctness],
|
||||
// $types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
|
||||
// )
|
||||
// ))
|
||||
// #h(10pt)
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ ref assignment tags correctness],
|
||||
// $types, vals, mu, m, c_r tcorrect v : t -> t'$,
|
||||
// // TODO: FIXME: which tag translations are correct ?? <- only assignee?
|
||||
// $types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
|
||||
// )
|
||||
// ))
|
||||
// #h(10pt)
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ tuple assignmenttags correctness],
|
||||
// $types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
|
||||
// $...$,
|
||||
// $types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
|
||||
// $types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... t'_n]$,
|
||||
// )
|
||||
// ))
|
||||
// #h(10pt)
|
||||
// --- <<< ---
|
||||
|
||||
=== Value Construction
|
||||
|
||||
|
|
@ -475,7 +448,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
name: [ new trivial $not$ read value],
|
||||
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
|
||||
$cl v, mu cr xarrowSquiggly(cl not Read \, w cr)_new cl bot, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -484,7 +457,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ new funciton pointer value],
|
||||
|
||||
$cl lambda overline(t) s, mu cr xarrowSquiggly(space)_new cl lambda overline(t) s, mu cr$,
|
||||
$cl lambda overline(t) s, mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(t) s, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -494,7 +467,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
name: [ new reference ref value],
|
||||
|
||||
// TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
|
||||
// frbidden ??
|
||||
// <- forbidden ??
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||
)
|
||||
|
|
@ -579,14 +552,15 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
=== Value Combination
|
||||
|
||||
#let combine = `combine`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine trivial $0$ values],
|
||||
name: [ combine same trivial values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
|
||||
$v_1 in {0, \#, bot}$,
|
||||
$v_2 in {0, \#, bot}$,
|
||||
$v_1 = v_2$,
|
||||
$v_1 plus.o v_2 = v_1$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -595,23 +569,12 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine trivial $bot$ values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine other trivial values],
|
||||
name: [ combine different trivial values],
|
||||
|
||||
$v_1 in {0, \#, bot}$,
|
||||
$v_2 in {0, \#, bot}$,
|
||||
$v_1 != v_2$,
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
|
||||
$v_1 plus.o v_2 = \#$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -622,7 +585,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ combine lambda values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
|
||||
// TODO: FIXME: how to combine statments in the right way? should check both
|
||||
[*TODO: combining semantics for lambda values (sets?)*],
|
||||
$overline(x_1) = overline(x_2)$,
|
||||
$s_1 = s_2$,
|
||||
$lambda space overline(x_1) space s_2 plus.o lambda space overline(x_2) space s_2 = lambda$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -640,7 +607,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
// NOTE: version to use with "combine all"
|
||||
$l_1 = l_2$,
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
|
||||
$rf l_1 plus.o rf l_2 = rf l_1$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -651,28 +618,23 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ combine tuple values],
|
||||
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
|
||||
$v^1_1 plus.o v^2_1 = v'_1$,
|
||||
$...$,
|
||||
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu'_n cr$
|
||||
$v^1_n plus.o v^2_n = v'_n$,
|
||||
$[v^1_1, ... v^1_n] plus.o [v^2_1 ... v^2_n] = [v'_1, ... v'_n]$
|
||||
)
|
||||
))
|
||||
|
||||
#let dom = `dom`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine tuple values],
|
||||
name: [ combine memory],
|
||||
|
||||
$mu'_0 = []$,
|
||||
// NOTE: same labels required
|
||||
$mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
|
||||
$mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
|
||||
$dom mu_1 = dom mu_2$,
|
||||
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
|
||||
$...$,
|
||||
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
|
||||
|
||||
$cl mu_1, mu_2 cr xarrowSquiggly(space)_#[combine all] mu'_n cr$
|
||||
$mu_1 plus.o mu_2 = l -> mu_1[l] plus.o mu_2[l]$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -753,7 +715,8 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ lambda step],
|
||||
|
||||
$cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
|
||||
$overline(t) = overline(t')$,
|
||||
$cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t') \, m \, c)_spoil cl lambda, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -778,10 +741,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ tuple step],
|
||||
|
||||
$cl v_1, mu cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu cr$,
|
||||
$cl v_1, mu_0 cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu_1 cr$,
|
||||
$...$,
|
||||
$cl v_n, mu cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu cr$,
|
||||
$cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
|
||||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu_n cr$,
|
||||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu_n cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -920,8 +883,9 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
$vals, mu tval p eqmu v$,
|
||||
$types ttype p : t'$,
|
||||
// TODO: FIXME: check type compatibility for t and type for path p (?)
|
||||
[*TODO: check t ~ t' in sme way (?)*],
|
||||
// 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)_new cl v, mu' cr$,
|
||||
|
||||
|
||||
|
|
@ -1047,7 +1011,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
$types_s = types_t$,
|
||||
$vals_s = vals_t$,
|
||||
$cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
|
||||
$mu_s plus.o mu_t = mu'$,
|
||||
|
||||
// TODO changes ?? two ways ??
|
||||
$cl types, vals, mu cr
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue