luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-24 11:26:30 -06:00
parent 9c7311c19d
commit 112cebb8b7
2 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
prototyping/Luau/RuntimeError.agda
View file

@ -15,17 +15,17 @@ data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
data RuntimeErrorᴱ H where data RuntimeErrorᴱ H where
FunctionMismatch : ∀ v w {M N} → (M ≡ val v) → (N ≡ val w) → (function ≢ valueType v) → RuntimeErrorᴱ H (M $ N) FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w)
BinopMismatch₁ : ∀ op v w {M N} → (M ≡ val v) → (N ≡ val w) → (number ≢ valueType v) → RuntimeErrorᴱ H (binexp M op N) BinopMismatch₁ : ∀ v w {op} → (number ≢ valueType v) → RuntimeErrorᴱ H (binexp (val v) op (val w))
BinopMismatch₂ : ∀ op v w {M N} → (M ≡ val v) → (N ≡ val w) → (number ≢ valueType w) → RuntimeErrorᴱ H (binexp M op N) BinopMismatch₂ : ∀ v w {op} → (number ≢ valueType w) → RuntimeErrorᴱ H (binexp (val v) op (val w))
UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x) UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)
SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a) SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N) app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N) app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end) block : ∀ {b B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N) bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N) bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)
data RuntimeErrorᴮ H where data RuntimeErrorᴮ H where
local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B) local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B) return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)

32
prototyping/Luau/RuntimeError/ToString.agda
View file

@ -1,30 +1,30 @@
{-# OPTIONS --rewriting #-} {-# OPTIONS --rewriting #-}
{-# OPTIONS --allow-unsolved-metas #-}
module Luau.RuntimeError.ToString where module Luau.RuntimeError.ToString where
open import Agda.Builtin.Float using (primShowFloat) open import Agda.Builtin.Float using (primShowFloat)
open import FFI.Data.String using (String; _++_) open import FFI.Data.String using (String; _++_)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂) open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
open import Luau.RuntimeType.ToString using (runtimeTypeToString) open import Luau.RuntimeType.ToString using (runtimeTypeToString)
open import Luau.Addr.ToString using (addrToString) open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (exprToString) open import Luau.Syntax.ToString using (exprToString)
open import Luau.Var.ToString using (varToString) open import Luau.Var.ToString using (varToString)
open import Luau.Value.ToString using (valueToString) open import Luau.Value.ToString using (valueToString)
open import Luau.Syntax using (name; _$_) open import Luau.Syntax using (var; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_)
errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String
errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String
-- errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound" errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
-- errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated" errToStringᴱ (addr a) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
-- errToStringᴱ (app₁ E) = errToStringᴱ E errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
-- errToStringᴱ (app₂ E) = errToStringᴱ E errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
-- errToStringᴱ (bin₁ E) = errToStringᴱ E errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
-- errToStringᴱ (bin₂ E) = errToStringᴱ E errToStringᴱ (binexp M op N) (BinopMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
-- errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString (name b) errToStringᴱ (binexp M op N) (BinopMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
-- errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
errToStringᴱ err = {!!} errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E
errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n in call of function " ++ varToString (name b)
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x) errToStringᴮ (local x ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n in definition of " ++ varToString (name x)
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement" errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n in return statement"