verona-op-sem

# Questions about the rules

## Syntax

* `σ[ι↦(ρ, τ)]` means objectID l to object of type τ in region ρ, right?

## Freeze

Destroy a region and freeze all objects that were in it.
x ∉ σ
ι = σ(y)
iso(σ, ι)
--- [freeze]
σ, x = freeze y; e* → σ[σ(v).regions→∅]\{y}[x↦v], acquire x; e*

* What is v?

## Catch
Test and set the success flag.
x ∉ σ₁
σ₂ = (σ.frames, σ.objects, σ.fields, σ.regions, true)
--- [catch]
σ₁, x = catch; e* → σ₂[x↦σ₁.except], e*

* σ₁ has except but also success, while state has only one boolean.
* Should we have two?
* It does not seem enough to just set the boolean to true.
  Is there a except value store in the state to which we make x point? 

## Return

σ₂ = ((ϕ*; ϕ₁[ϕ₂.ret↦σ₁(x*)]), σ₁.objects, σ₁.fields, σ₁.except)
(ϕ₁.regions ≠ ϕ₂.regions) ⇒ iso(σ₂, ϕ₂(x)) ∨ imm(σ₂, ϕ₂(x))
ιs = σ₁.objects(ϕ₂.regions) if ϕ₁.regions ≠ ϕ₂.regions
     ∅ otherwise

* Do I understand correctly by if the regions are not the same, we remove the objects
  that belong to ϕ₂?

## Functions vs. Lambdas

* Are they the same?

## Setting up regions in new frame

newframe(σ, ρ*, x*, y, z*, e*) =
  ((ϕ*; ϕ₁\{y, z*}; ϕ₂), σ.objects, σ.fields, σ.regions, σ.except), λ.expr
  if λ ∈ Function
  where
    λ = σ(y),
    σ.frames = (ϕ*; ϕ₁),
    ϕ₂ = ((ϕ₁.regions; ρ*), [λ.args↦σ(z*)], x*, e*)

* We must remove y and `z*` from the current frame?

## Unpin

I don't really get it

## Continuation and Ret from Frame

* When are rests added?
* When are continuations added?