path types

[intsuc]

• NBT paths to world-objects as const-references
• An NBT path is a constructor for path types
  • Variables x
  • Paths ~x
• Trace *x yields the const-string (NBT path)

Typing

Γ | const ⊢ τ : tag
Γ | world ⊢ α : type τ
---------------------------------
Γ | const ⊢ path α : type end_tag


------------------------------------
Γ, world x : α | const ⊢ ~x : path α


Γ | const ⊢ e : path α
-----------------------
Γ | const ⊢ *e : string

Examples

test def f :=
  let x := 0;
  # *(~x) = "int[-1]"
  let y := 1;
  # *(~x) = "int[-2]"
  # *(~y) = "int[-1]"

  let xs := [0];
  # *(~xs) = "list[-1]"
  let ys := [1];
  # *(~xs) = "list[-2]"
  # *(~ys) = "list[-1]"
  # *(~xs.[0]) = "list[-2][0]"
  # *(~ys.[0]) = "list[-1][0]"

  true;

export const def size(self : path byte_array) : code int := `(
  let _ as end := /"data modify storage mcx: int append value 0";
  /"execute store result storage mcx: int[-1] int 1 run data get storage mcx: ${*self}";
)

test def use_size :=
  let x := [byte; 0b, 1b, 2b];
  let y := { k: [byte; 3b, 4b, 5b] };
  let z := [byte; 6b, 7b, 8b];
  let a := $size(~z);
  let b := $size(~y.k);
  let c := $size(~x);
  true;

# data modify storage mcx: byte_array append value [B;0b,1b,2b]
# data modify storage mcx: compound append value {k:[B;3b,4b,5b]}
# data modify storage mcx: byte_array append value [B;]
# data modify storage mcx: byte_array append value [B;6b,7b,8b]
# data modify storage mcx: int append value 0
# execute store result storage mcx: int[-1] int 1 run data get storage mcx: byte_array[-1]
# data modify storage mcx: int append value 0
# execute store result storage mcx: int[-1] int 1 run data get storage mcx: compound[-1].k
# data modify storage mcx: int append value 0
# execute store result storage mcx: int[-1] int 1 run data get storage mcx: byte_array[-2]
# data modify storage mcx: byte append value 1b
#
# data remove storage mcx: int[-1]
# data remove storage mcx: int[-1]
# data remove storage mcx: int[-1]
# data remove storage mcx: byte_array[-1]
# data remove storage mcx: compound[-1]
# data remove storage mcx: byte_array[-1]

Problems

• path::to_string is not a normal function because it requires the context information
  • Add system to track variable offsets?
  • Trace *x as primitive
• Need to maintain stack indices at elaborate phase?
• Traces are an effect by themselves:

  let x := 0;
  let a := *(~x) # "int[-1]"
  let y := 1;
  let b := *(~x) # "int[-2]"
  
  # conv a         b            => ?
  # conv *(~x)     *(~x)        => ok?
  # conv "int[-1]" "int[-2]"    => no

• Capture the environment, implicitly or explicitly?

  let x := 0;
  let a := *(~{} x)  # "int[-1]"
  let y := 1;
  let b := *(~{y} x) # "int[-2]"
  let z := 2;
  let c := *(~{z} y) # "int[-2]"
  
  # conv a         b            => ?
  # conv *(~{} x)  *(~{y} x)    => ?
  # conv "int[-1]" "int[-2]"    => no
  
  # conv b         c            => ?
  # conv *(~{y} x) *(~{z} y)    => ?
  # conv "int[-2]" "int[-2]"    => ok