mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
Added warningToString and hooked it up to the interpreter
This commit is contained in:
ajeffrey@roblox.com
parent
5d84c8382a
commit
55f3f284a4
4 changed files with 131 additions and 84 deletions
|
|
@ -9,22 +9,33 @@ open import Agda.Builtin.Unit using (⊤)
|
|||
open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
|
||||
open import FFI.Data.Aeson using (Value; eitherDecode)
|
||||
open import FFI.Data.Either using (Left; Right)
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import FFI.Data.Text.Encoding using (encodeUtf8)
|
||||
open import FFI.System.Exit using (exitWith; ExitFailure)
|
||||
|
||||
open import Luau.Syntax using (Block)
|
||||
open import Luau.StrictMode.ToString using (warningToStringᴮ)
|
||||
open import Luau.Syntax using (Block; yes; maybe; isAnnotatedᴮ)
|
||||
open import Luau.Syntax.FromJSON using (blockFromJSON)
|
||||
open import Luau.Syntax.ToString using (blockToString)
|
||||
open import Luau.Run using (run; return; done; error)
|
||||
open import Luau.RuntimeError.ToString using (errToStringᴮ)
|
||||
open import Luau.Value.ToString using (valueToString)
|
||||
|
||||
runBlock : ∀ {a} → Block a → IO ⊤
|
||||
runBlock block with run block
|
||||
runBlock block | return V D = putStrLn (valueToString V)
|
||||
runBlock block | done D = putStrLn "nil"
|
||||
runBlock block | error E D = putStrLn (errToStringᴮ _ E)
|
||||
open import Properties.StrictMode using (wellTypedProgramsDontGoWrong)
|
||||
|
||||
runBlock′ : ∀ a → Block a → IO ⊤
|
||||
runBlock′ a block with run block
|
||||
runBlock′ a block | return V D = putStrLn (valueToString V)
|
||||
runBlock′ a block | done D = putStrLn "nil"
|
||||
runBlock′ maybe block | error E D = putStrLn (errToStringᴮ _ E)
|
||||
runBlock′ yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
|
||||
runBlock′ yes block | error E D | W = putStrLn (errToStringᴮ _ E) >> putStrLn (warningToStringᴮ _ W)
|
||||
|
||||
runBlock : Block maybe → IO ⊤
|
||||
runBlock B with isAnnotatedᴮ B
|
||||
runBlock B | nothing = runBlock′ maybe B
|
||||
runBlock B | just B′ = runBlock′ yes B′
|
||||
|
||||
runJSON : Value → IO ⊤
|
||||
runJSON value with blockFromJSON(value)
|
||||
|
|
|
|||
|
|
@ -27,13 +27,13 @@ data Warningᴱ H {Γ} where
|
|||
---------------------
|
||||
Warningᴱ H (addr {a} T)
|
||||
|
||||
UnboundVariable : ∀ x {T} {p} →
|
||||
UnboundVariable : ∀ {x T p} →
|
||||
|
||||
(Γ [ x ]ⱽ ≡ nothing) →
|
||||
------------------------
|
||||
Warningᴱ H (var {x} {T} p)
|
||||
|
||||
app₀ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
(src T ≢ U) →
|
||||
-----------------
|
||||
|
|
@ -75,7 +75,7 @@ data Warningᴱ H {Γ} where
|
|||
------------------------------
|
||||
Warningᴱ H (binexp {op} D₁ D₂)
|
||||
|
||||
function₀ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(U ≢ V) →
|
||||
-------------------------
|
||||
|
|
@ -87,7 +87,7 @@ data Warningᴱ H {Γ} where
|
|||
-------------------------
|
||||
Warningᴱ H (function {f} {U = U} D)
|
||||
|
||||
block₀ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||||
BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||||
|
||||
(T ≢ U) →
|
||||
------------------------------
|
||||
|
|
@ -107,7 +107,7 @@ data Warningᴮ H {Γ} where
|
|||
------------------
|
||||
Warningᴮ H (return D₁ D₂)
|
||||
|
||||
local₀ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(T ≢ U) →
|
||||
--------------------
|
||||
|
|
@ -125,7 +125,7 @@ data Warningᴮ H {Γ} where
|
|||
--------------------
|
||||
Warningᴮ H (local D₁ D₂)
|
||||
|
||||
function₀ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||||
FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||||
|
||||
(U ≢ V) →
|
||||
-------------------------------------
|
||||
|
|
@ -145,7 +145,7 @@ data Warningᴮ H {Γ} where
|
|||
|
||||
data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where
|
||||
|
||||
function₀ : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(U ≢ V) →
|
||||
---------------------------------
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ open import Agda.Builtin.Float using (Float)
|
|||
open import Luau.Var using (Var)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Type using (Type)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
|
||||
infixr 5 _∙_
|
||||
|
||||
|
|
@ -60,3 +61,38 @@ data Expr a where
|
|||
block_is_end : VarDec a → Block a → Expr a
|
||||
number : Float → Expr a
|
||||
binexp : Expr a → BinaryOperator → Expr a → Expr a
|
||||
|
||||
isAnnotatedᴱ : ∀ {a} → Expr a → Maybe (Expr yes)
|
||||
isAnnotatedᴮ : ∀ {a} → Block a → Maybe (Block yes)
|
||||
|
||||
isAnnotatedᴱ nil = just nil
|
||||
isAnnotatedᴱ (var x) = just (var x)
|
||||
isAnnotatedᴱ (addr a) = just (addr a)
|
||||
isAnnotatedᴱ (M $ N) with isAnnotatedᴱ M | isAnnotatedᴱ N
|
||||
isAnnotatedᴱ (M $ N) | just M′ | just N′ = just (M′ $ N′)
|
||||
isAnnotatedᴱ (M $ N) | _ | _ = nothing
|
||||
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) with isAnnotatedᴮ B
|
||||
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | just B′ = just (function f ⟨ var x ∈ T ⟩∈ U is B′ end)
|
||||
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | _ = nothing
|
||||
isAnnotatedᴱ (function _ is B end) = nothing
|
||||
isAnnotatedᴱ (block var b ∈ T is B end) with isAnnotatedᴮ B
|
||||
isAnnotatedᴱ (block var b ∈ T is B end) | just B′ = just (block var b ∈ T is B′ end)
|
||||
isAnnotatedᴱ (block var b ∈ T is B end) | _ = nothing
|
||||
isAnnotatedᴱ (block _ is B end) = nothing
|
||||
isAnnotatedᴱ (number n) = just (number n)
|
||||
isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N
|
||||
isAnnotatedᴱ (binexp M op N) | just M′ | just N′ = just (binexp M′ op N′)
|
||||
isAnnotatedᴱ (binexp M op N) | _ | _ = nothing
|
||||
|
||||
isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with isAnnotatedᴮ B | isAnnotatedᴮ C
|
||||
isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | just B′ | just C′ = just (function f ⟨ var x ∈ T ⟩∈ U is C′ end ∙ B′)
|
||||
isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | _ | _ = nothing
|
||||
isAnnotatedᴮ (function _ is C end ∙ B) = nothing
|
||||
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
|
||||
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | just M′ | just B′ = just (local var x ∈ T ← M′ ∙ B′)
|
||||
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | _ | _ = nothing
|
||||
isAnnotatedᴮ (local _ ← M ∙ B) = nothing
|
||||
isAnnotatedᴮ (return M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
|
||||
isAnnotatedᴮ (return M ∙ B) | just M′ | just B′ = just (return M′ ∙ B′)
|
||||
isAnnotatedᴮ (return M ∙ B) | _ | _ = nothing
|
||||
isAnnotatedᴮ done = just done
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ import Agda.Builtin.Equality.Rewrite
|
|||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
|
||||
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; BinopMismatch₁; BinopMismatch₂; bin₁; bin₂; block₀; block₁; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; block; addr)
|
||||
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinopMismatch₁; BinopMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr)
|
||||
open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
|
||||
open import Luau.Syntax using (Expr; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
|
||||
open import Luau.Type using (Type; strict; nil; _⇒_; bot; tgt; _≡ᵀ_; _≡ᴹᵀ_)
|
||||
|
|
@ -156,18 +156,18 @@ preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W))
|
|||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orBot (cong typeOfᴹᴼ p)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ r)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (app₀ (λ s → r (trans (trans (sym (cong src (cong orBot (cong typeOfᴹᴼ p)))) (trans s (typeOfᴱⱽ v))) (cong orBot q)))))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s → r (trans (trans (sym (cong src (cong orBot (cong typeOfᴹᴼ p)))) (trans s (typeOfᴱⱽ v))) (cong orBot q)))))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-bot v
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ v) (cong orBot q))))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
|
||||
preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl
|
||||
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) with T ≡ᵀ typeOfᴱ H ∅ (val v)
|
||||
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p
|
||||
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (block₀ p))
|
||||
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (BlockMismatch p))
|
||||
preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil
|
||||
preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p
|
||||
preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (block₀ p))
|
||||
preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (BlockMismatch p))
|
||||
preservationᴱ H (binexp M op N) (binOpEval m n) = ok refl
|
||||
preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
|
||||
preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl
|
||||
|
|
@ -178,7 +178,7 @@ preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warnin
|
|||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v)
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (local₀ (λ r → q (trans r (trans (typeOfᴱⱽ v) (cong orBot p))))))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (trans (typeOfᴱⱽ v) (cong orBot p))))))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-bot v
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (trans (typeOfᴱⱽ v) (cong orBot p))))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W))
|
||||
|
|
@ -201,36 +201,36 @@ reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y
|
|||
reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W
|
||||
reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W
|
||||
reflect-substitutionᴱ H (addr a) v x p (UnallocatedAddress r) = UnallocatedAddress r
|
||||
reflect-substitutionᴱ H (M $ N) v x p (app₀ q) = app₀ (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p))))
|
||||
reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p))))
|
||||
reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W)
|
||||
reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) | yes r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r))))
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) | no r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r))))
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r))))
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r))))
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₀ q) = block₀ (λ r → q (trans r (substitutivityᴮ H B v x p)))
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r → q (trans r (substitutivityᴮ H B v x p)))
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W)
|
||||
reflect-substitutionᴱ H (binexp M op N) x v p (BinopMismatch₁ q) = BinopMismatch₁ (λ r → q (trans (sym (substitutivityᴱ H M x v p)) r))
|
||||
reflect-substitutionᴱ H (binexp M op N) x v p (BinopMismatch₂ q) = BinopMismatch₂ (λ r → q (trans (sym (substitutivityᴱ H N x v p)) r))
|
||||
reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W)
|
||||
reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W)
|
||||
|
||||
reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable y r) = UnboundVariable y (trans (sym (⊕-lookup-miss x y _ _ p)) r)
|
||||
reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r)
|
||||
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q)
|
||||
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | ()
|
||||
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) | yes r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r))))
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) | no r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r))))
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r))))
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r))))
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₀ q) = local₀ (λ r → q (trans r (substitutivityᴱ H M v x p)))
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r → q (trans r (substitutivityᴱ H M v x p)))
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
|
||||
|
|
@ -243,12 +243,12 @@ reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ
|
|||
reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M)
|
||||
reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B)
|
||||
|
||||
reflect-weakeningᴱ H (var x) h (UnboundVariable x p) = (UnboundVariable x p)
|
||||
reflect-weakeningᴱ H (var x) h (UnboundVariable p) = (UnboundVariable p)
|
||||
reflect-weakeningᴱ H (addr a) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
|
||||
reflect-weakeningᴱ H (M $ N) h (app₀ p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h
|
||||
reflect-weakeningᴱ H (M $ N) h (app₀ p) | ok q₁ | ok q₂ = app₀ (λ r → p (trans (cong src (sym q₁)) (trans r q₂)))
|
||||
reflect-weakeningᴱ H (M $ N) h (app₀ p) | warning W | _ = app₁ W
|
||||
reflect-weakeningᴱ H (M $ N) h (app₀ p) | _ | warning W = app₂ W
|
||||
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h
|
||||
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r → p (trans (cong src (sym q₁)) (trans r q₂)))
|
||||
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W
|
||||
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W
|
||||
reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W)
|
||||
reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W)
|
||||
reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₁ p) with heap-weakeningᴱ H M h
|
||||
|
|
@ -259,72 +259,72 @@ reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₂ p) | ok q = BinopMism
|
|||
reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₂ p) | warning W = bin₂ W
|
||||
reflect-weakeningᴱ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ H M h W′)
|
||||
reflect-weakeningᴱ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ H N h W′)
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | ok q = function₀ (λ r → p (trans r q))
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | warning W = function₁ W
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W
|
||||
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W)
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) | ok q = block₀ (λ r → p (trans r q))
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) | warning W = block₁ W
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r → p (trans r q))
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | warning W = block₁ W
|
||||
reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W)
|
||||
|
||||
reflect-weakeningᴮ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ H M h W)
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) with heap-weakeningᴱ H M h
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) | ok q = local₀ (λ r → p (trans r q))
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) | warning W = local₁ W
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) with heap-weakeningᴱ H M h
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r → p (trans r q))
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | warning W = local₁ W
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W)
|
||||
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W)
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) with heap-weakeningᴮ H C h
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) | ok q = function₀ (λ r → p (trans r q))
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) | warning W = function₁ W
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | warning W = function₁ W
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W)
|
||||
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W)
|
||||
|
||||
reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) | ok q = function₀ (λ r → p (trans r q))
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) | warning W = function₁ W
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W
|
||||
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′)
|
||||
|
||||
reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M)
|
||||
reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
|
||||
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₀ p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s)
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′)))
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₀ p) | warning (expr W) | _ = expr (app₁ W)
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₀ p) | warning (heap W) | _ = heap W
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₀ p) | _ | warning W = expr (app₂ W)
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s)
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p (trans (trans (cong src (sym q)) r) q′)))
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W)
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W = expr (app₂ W)
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W)
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | ok q | ok q′ = expr (app₀ (λ r → p′ (trans (trans (cong src (sym q)) r) q′)))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | warning W | _ = expr (app₁ W)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (expr W) = expr (app₂ W)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (heap W) = heap W
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p′ (trans (trans (cong src (sym q)) r) q′)))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | warning W | _ = expr (app₁ W)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (expr W) = expr (app₂ W)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (heap W) = heap W
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) with remember (typeOfⱽ H v)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just S , r) with S ≡ᵀ T
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just T , r) | yes refl = heap (addr a p (function₀ (λ s → q (trans s (substitutivityᴮ H B v x (sym r))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just S , r) | no s = expr (app₀ (λ t → s (trans (cong orBot (sym r)) (trans (sym (typeOfᴱⱽ v)) (trans (sym t) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) with typeOf-val-not-bot v
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) | ok s = CONTRADICTION (s (trans (cong orBot (sym r)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) | warning W = expr (app₂ W)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ H B v x (sym r))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t → s (trans (cong orBot (sym r)) (trans (sym (typeOfᴱⱽ v)) (trans (sym t) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-bot v
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (trans (cong orBot (sym r)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′)))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (app₀ (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (FunctionCallMismatch (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-bot v
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W)
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) with preservationᴮ H B s
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | ok q = expr (block₀ (λ r → p (trans r q)))
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | warning (heap W) = heap W
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | warning (block W) = expr (block₁ W)
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) with preservationᴮ H B s
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | ok q = expr (BlockMismatch (λ r → p (trans r q)))
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W)
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W)
|
||||
|
|
@ -353,10 +353,10 @@ reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W
|
|||
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W)
|
||||
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) with preservationᴱ H M s
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) | ok q = block (local₀ (λ r → p (trans r q)))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) | warning (expr W) = block (local₁ W)
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) | warning (heap W) = heap W
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) with preservationᴱ H M s
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r → p (trans r q)))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W)
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with reflectᴱ H M s W′
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W)
|
||||
|
|
@ -364,7 +364,7 @@ reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (
|
|||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v)
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (local₀ (λ r → q (trans (cong orBot (sym p)) (trans (sym (typeOfᴱⱽ v)) (sym r)))))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orBot (sym p)) (trans (sym (typeOfᴱⱽ v)) (sym r)))))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-bot v
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (trans (cong orBot (sym p)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W)
|
||||
|
|
@ -378,9 +378,9 @@ reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warni
|
|||
|
||||
reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl with heap-weakeningᴮ H B (snoc defn)
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | ok r = expr (function₀ λ q → p (trans q r))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | warning W = expr (function₁ W)
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn)
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q → p (trans q r))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W)
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
|
||||
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
|
||||
|
|
@ -409,9 +409,9 @@ reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W =
|
|||
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W)
|
||||
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl with heap-weakeningᴮ H C (snoc defn)
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | ok r = block (function₀ (λ q → p (trans q r)))
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | warning W = block (function₁ W)
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn)
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q → p (trans q r)))
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W)
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′))
|
||||
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
|
||||
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′)
|
||||
|
|
@ -425,10 +425,10 @@ reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
|
|||
runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
|
||||
runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)
|
||||
|
||||
runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable x refl
|
||||
runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl
|
||||
runtimeWarningᴱ H (addr a) (SEGV p) = UnallocatedAddress p
|
||||
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-bot w
|
||||
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = app₀ (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r))))
|
||||
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = FunctionCallMismatch (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r))))
|
||||
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W
|
||||
runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
|
||||
runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue