From 967d213f545fe8167b69d787cc27f5c67441fbc2 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 28 Apr 2026 11:17:15 +0000 Subject: [PATCH 1/2] structures: grammar fixes --- model_with_structures/model.typ | 203 +++++++++++++------------------- 1 file changed, 81 insertions(+), 122 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 1221071..8d41d7c 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -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` } @@ -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,7 @@ $ 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$ + $lambda plus.o lambda = lambda$ ) )) @@ -640,7 +603,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 +614,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]$ ) )) @@ -920,8 +878,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 +1006,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 From 0be430a59b3dc4d0553a719b8c4c8cf04daed556 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 28 Apr 2026 14:37:54 +0000 Subject: [PATCH 2/2] structures: semantics fixes, part of analyzer --- model_with_structures/analyzer.ml | 224 +++++++++++++++++++++++++----- model_with_structures/model.typ | 21 +-- 2 files changed, 206 insertions(+), 39 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 0779a8a..1b5740e 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -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 *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 8d41d7c..3449afc 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -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` } @@ -585,7 +585,11 @@ $s in stmt, f in X, x in X, a in X$ rule( name: [ combine lambda values], - $lambda plus.o lambda = lambda$ + // 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$ ) )) @@ -711,7 +715,8 @@ $s in stmt, f in X, x in X, a in X$ 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$, ) )) @@ -736,10 +741,10 @@ $s in stmt, f in X, x in X, a in X$ 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$, ) ))