mirror of
https://github.com/luau-lang/luau.git
synced 2024-11-15 14:25:44 +08:00
Prototyping strict mode (#399)
* First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi>
This commit is contained in:
Alan Jeffrey
GitHub
parent
d277cc2c3b
commit
c5477d522d
2
prototyping/.gitignore
vendored
2
prototyping/.gitignore
vendored
@ -2,10 +2,8 @@
|
||||
*.agdai
|
||||
Main
|
||||
MAlonzo
|
||||
Examples
|
||||
PrettyPrinter
|
||||
Interpreter
|
||||
Properties
|
||||
!Tests/Interpreter
|
||||
!Tests/PrettyPrinter
|
||||
.ghc.*
|
||||
|
||||
8
prototyping/Everything.agda
Normal file
8
prototyping/Everything.agda
Normal file
@ -0,0 +1,8 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Everything where
|
||||
|
||||
import Examples
|
||||
import Properties
|
||||
import PrettyPrinter
|
||||
import Interpreter
|
||||
@ -1,8 +1,10 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Examples.OpSem where
|
||||
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
|
||||
open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end)
|
||||
open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)
|
||||
open import Luau.Heap using (∅)
|
||||
|
||||
ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
|
||||
ex1 = subst
|
||||
ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅
|
||||
ex1 = subst nil
|
||||
|
||||
@ -4,22 +4,17 @@ module Examples.Run where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; true; false)
|
||||
open import Luau.Value using (nil; number; bool)
|
||||
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool)
|
||||
open import Luau.Run using (run; return)
|
||||
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
|
||||
|
||||
import Agda.Builtin.Equality.Rewrite
|
||||
{-# REWRITE lookup-next next-emp lookup-next-emp #-}
|
||||
|
||||
ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
|
||||
ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ val nil) ∙ done) ≡ return nil _)
|
||||
ex1 = refl
|
||||
|
||||
ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
|
||||
ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (val (number 123.0)) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 123.0) _)
|
||||
ex2 = refl
|
||||
|
||||
ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _)
|
||||
ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) + (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 3.0) _)
|
||||
ex3 = refl
|
||||
|
||||
ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) < (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool true) _)
|
||||
ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) < (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _)
|
||||
ex4 = refl
|
||||
|
||||
@ -2,7 +2,7 @@ module Examples.Syntax where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.String using (_++_)
|
||||
open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
|
||||
open import Luau.Syntax using (var; _$_; return; val; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
|
||||
open import Luau.Syntax.ToString using (exprToString; blockToString)
|
||||
|
||||
ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
|
||||
@ -11,7 +11,7 @@ ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙
|
||||
"end"
|
||||
ex1 = refl
|
||||
|
||||
ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡
|
||||
ex2 : blockToString(local var "x" ← (val nil) ∙ return (var "x") ∙ done) ≡
|
||||
"local x = nil\n" ++
|
||||
"return x"
|
||||
ex2 = refl
|
||||
|
||||
@ -25,3 +25,4 @@ ex6 = refl
|
||||
|
||||
ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
|
||||
ex7 = refl
|
||||
|
||||
|
||||
@ -1,15 +1,21 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module FFI.Data.Aeson where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Equality.Rewrite using ()
|
||||
open import Agda.Builtin.Bool using (Bool)
|
||||
open import Agda.Builtin.String using (String)
|
||||
|
||||
open import FFI.Data.ByteString using (ByteString)
|
||||
open import FFI.Data.HaskellString using (HaskellString; pack)
|
||||
open import FFI.Data.Maybe using (Maybe)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import FFI.Data.Either using (Either; mapLeft)
|
||||
open import FFI.Data.Scientific using (Scientific)
|
||||
open import FFI.Data.Vector using (Vector)
|
||||
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
{-# FOREIGN GHC import qualified Data.Aeson #-}
|
||||
{-# FOREIGN GHC import qualified Data.Aeson.Key #-}
|
||||
{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}
|
||||
@ -19,14 +25,35 @@ postulate
|
||||
Key : Set
|
||||
fromString : String → Key
|
||||
toString : Key → String
|
||||
empty : ∀ {A} → KeyMap A
|
||||
singleton : ∀ {A} → Key → A → (KeyMap A)
|
||||
insert : ∀ {A} → Key → A → (KeyMap A) → (KeyMap A)
|
||||
delete : ∀ {A} → Key → (KeyMap A) → (KeyMap A)
|
||||
unionWith : ∀ {A} → (A → A → A) → (KeyMap A) → (KeyMap A) → (KeyMap A)
|
||||
lookup : ∀ {A} → Key -> KeyMap A -> Maybe A
|
||||
{-# POLARITY KeyMap ++ #-}
|
||||
{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
|
||||
{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
|
||||
{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
|
||||
{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
|
||||
{-# COMPILE GHC empty = \_ -> Data.Aeson.KeyMap.empty #-}
|
||||
{-# COMPILE GHC singleton = \_ -> Data.Aeson.KeyMap.singleton #-}
|
||||
{-# COMPILE GHC insert = \_ -> Data.Aeson.KeyMap.insert #-}
|
||||
{-# COMPILE GHC delete = \_ -> Data.Aeson.KeyMap.delete #-}
|
||||
{-# COMPILE GHC unionWith = \_ -> Data.Aeson.KeyMap.unionWith #-}
|
||||
{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}
|
||||
|
||||
postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m) ≡ just v)
|
||||
postulate lookup-empty : ∀ {A} k → (lookup {A} k empty ≡ nothing)
|
||||
postulate lookup-insert-not : ∀ {A} j k v (m : KeyMap A) → (j ≢ k) → (lookup k m ≡ lookup k (insert j v m))
|
||||
postulate singleton-insert-empty : ∀ {A} k (v : A) → (singleton k v ≡ insert k v empty)
|
||||
postulate insert-swap : ∀ {A} j k (v w : A) m → (j ≢ k) → insert j v (insert k w m) ≡ insert k w (insert j v m)
|
||||
postulate insert-over : ∀ {A} j k (v w : A) m → (j ≡ k) → insert j v (insert k w m) ≡ insert j v m
|
||||
postulate to-from : ∀ k → toString(fromString k) ≡ k
|
||||
postulate from-to : ∀ k → fromString(toString k) ≡ k
|
||||
|
||||
{-# REWRITE lookup-insert lookup-empty singleton-insert-empty #-}
|
||||
|
||||
data Value : Set where
|
||||
object : KeyMap Value → Value
|
||||
array : Vector Value → Value
|
||||
|
||||
@ -1,8 +1,14 @@
|
||||
module FFI.Data.Maybe where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
|
||||
{-# FOREIGN GHC import qualified Data.Maybe #-}
|
||||
|
||||
data Maybe (A : Set) : Set where
|
||||
nothing : Maybe A
|
||||
just : A → Maybe A
|
||||
{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}
|
||||
|
||||
just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y)
|
||||
just-inv refl = refl
|
||||
|
||||
|
||||
@ -1,11 +1,15 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module FFI.Data.Vector where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Equality.Rewrite using ()
|
||||
open import Agda.Builtin.Int using (Int; pos; negsuc)
|
||||
open import Agda.Builtin.Nat using (Nat)
|
||||
open import Agda.Builtin.Bool using (Bool; false; true)
|
||||
open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
{-# FOREIGN GHC import qualified Data.Vector #-}
|
||||
|
||||
@ -30,8 +34,13 @@ postulate
|
||||
{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}
|
||||
|
||||
postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0)
|
||||
postulate lookup-empty : ∀ {A} n → (lookup (empty {A}) n ≡ nothing)
|
||||
postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x)
|
||||
postulate lookup-length : ∀ {A} (v : Vector A) → (lookup v (length v) ≡ nothing)
|
||||
postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x)
|
||||
postulate lookup-snoc-not : ∀ {A n} (x : A) (v : Vector A) → (n ≢ length v) → (lookup v n ≡ lookup (snoc v x) n)
|
||||
|
||||
{-# REWRITE length-empty lookup-snoc lookup-length lookup-snoc-empty lookup-empty #-}
|
||||
|
||||
head : ∀ {A} → (Vector A) → (Maybe A)
|
||||
head vec with null vec
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Interpreter where
|
||||
|
||||
open import Agda.Builtin.IO using (IO)
|
||||
@ -7,31 +9,41 @@ 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.Syntax.ToString using (blockToString; valueToString)
|
||||
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 ("\nRAN WITH RESULT: " ++ valueToString V)
|
||||
runBlock′ a block | done D = putStrLn ("\nRAN")
|
||||
runBlock′ maybe block | error E D = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E)
|
||||
runBlock′ yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
|
||||
runBlock′ yes block | error E D | W = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E ++ "\n\nTYPE ERROR:\n" ++ warningToStringᴮ _ W)
|
||||
|
||||
runBlock : Block maybe → IO ⊤
|
||||
runBlock B with isAnnotatedᴮ B
|
||||
runBlock B | nothing = putStrLn ("UNANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ maybe B
|
||||
runBlock B | just B′ = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ yes B′
|
||||
|
||||
runJSON : Value → IO ⊤
|
||||
runJSON value with blockFromJSON(value)
|
||||
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runJSON value | (Left err) = putStrLn ("LUAU ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runJSON value | (Right block) = runBlock block
|
||||
|
||||
runString : String → IO ⊤
|
||||
runString txt with eitherDecode (encodeUtf8 txt)
|
||||
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runString txt | (Left err) = putStrLn ("JSON ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runString txt | (Right value) = runJSON value
|
||||
|
||||
main : IO ⊤
|
||||
|
||||
@ -5,13 +5,14 @@ open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Nat using (Nat; _==_)
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Agda.Builtin.TrustMe using (primTrustMe)
|
||||
open import Properties.Dec using (Dec; yes; no; ⊥)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
Addr : Set
|
||||
Addr = Nat
|
||||
|
||||
_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b)
|
||||
a ≡ᴬ b with a == b
|
||||
a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥
|
||||
a ≡ᴬ b | false = no p where postulate p : (a ≢ b)
|
||||
a ≡ᴬ b | true = yes primTrustMe
|
||||
|
||||
|
||||
@ -1,32 +1,39 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.Heap where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (Maybe; just)
|
||||
open import FFI.Data.Vector using (Vector; length; snoc; empty)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import FFI.Data.Vector using (Vector; length; snoc; empty; lookup-snoc-not)
|
||||
open import Luau.Addr using (Addr; _≡ᴬ_)
|
||||
open import Luau.Var using (Var)
|
||||
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)
|
||||
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end)
|
||||
open import Properties.Equality using (_≢_; trans)
|
||||
open import Properties.Remember using (remember; _,_)
|
||||
open import Properties.Dec using (yes; no)
|
||||
|
||||
data HeapValue (a : Annotated) : Set where
|
||||
function_is_end : FunDec a → Block a → HeapValue a
|
||||
-- Heap-allocated objects
|
||||
data Object (a : Annotated) : Set where
|
||||
|
||||
function_is_end : FunDec a → Block a → Object a
|
||||
|
||||
Heap : Annotated → Set
|
||||
Heap a = Vector (HeapValue a)
|
||||
Heap a = Vector (Object a)
|
||||
|
||||
data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where
|
||||
data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → Object a → Set where
|
||||
|
||||
defn : ∀ {H val} →
|
||||
|
||||
-----------------------------------
|
||||
(snoc H val) ≡ H ⊕ (length H) ↦ val
|
||||
|
||||
_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a)
|
||||
_[_] : ∀ {a} → Heap a → Addr → Maybe (Object a)
|
||||
_[_] = FFI.Data.Vector.lookup
|
||||
|
||||
∅ : ∀ {a} → Heap a
|
||||
∅ = empty
|
||||
|
||||
data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
|
||||
data AllocResult a (H : Heap a) (V : Object a) : Set where
|
||||
ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V
|
||||
|
||||
alloc : ∀ {a} H V → AllocResult a H V
|
||||
@ -35,15 +42,8 @@ alloc H V = ok (length H) (snoc H V) defn
|
||||
next : ∀ {a} → Heap a → Addr
|
||||
next = length
|
||||
|
||||
allocated : ∀ {a} → Heap a → HeapValue a → Heap a
|
||||
allocated : ∀ {a} → Heap a → Object a → Heap a
|
||||
allocated = snoc
|
||||
|
||||
-- next-emp : (length ∅ ≡ 0)
|
||||
next-emp = FFI.Data.Vector.length-empty
|
||||
|
||||
-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
|
||||
lookup-next = FFI.Data.Vector.lookup-snoc
|
||||
|
||||
-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
|
||||
lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty
|
||||
|
||||
lookup-not-allocated : ∀ {a} {H H′ : Heap a} {b c O} → (H′ ≡ H ⊕ b ↦ O) → (c ≢ b) → (H [ c ] ≡ H′ [ c ])
|
||||
lookup-not-allocated {H = H} {O = O} defn p = lookup-snoc-not O H p
|
||||
|
||||
@ -1,66 +1,53 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.OpSem where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import Utility.Bool using (not; _or_; _and_)
|
||||
open import Agda.Builtin.Nat using (_==_)
|
||||
open import FFI.Data.Maybe using (just)
|
||||
open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
|
||||
open import Luau.Substitution using (_[_/_]ᴮ)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; number)
|
||||
open import Luau.Value using (addr; val; number; Value; bool)
|
||||
open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; number; bool)
|
||||
open import Luau.RuntimeType using (RuntimeType; valueType)
|
||||
open import Properties.Product using (_×_; _,_)
|
||||
|
||||
evalNumOp : Float → BinaryOperator → Float → Value
|
||||
evalNumOp x + y = number (primFloatPlus x y)
|
||||
evalNumOp x - y = number (primFloatMinus x y)
|
||||
evalNumOp x * y = number (primFloatTimes x y)
|
||||
evalNumOp x / y = number (primFloatDiv x y)
|
||||
evalNumOp x < y = bool (primFloatLess x y)
|
||||
evalNumOp x > y = bool (primFloatLess y x)
|
||||
evalNumOp x ≡ y = bool (primFloatEquality x y)
|
||||
evalNumOp x ≅ y = bool (primFloatInequality x y)
|
||||
evalNumOp x ≤ y = bool ((primFloatLess x y) or (primFloatEquality x y))
|
||||
evalNumOp x ≥ y = bool ((primFloatLess y x) or (primFloatEquality x y))
|
||||
evalEqOp : Value → Value → Bool
|
||||
evalEqOp Value.nil Value.nil = true
|
||||
evalEqOp (addr x) (addr y) = (x ==ᴬ y)
|
||||
evalEqOp (number x) (number y) = primFloatEquality x y
|
||||
evalEqOp (bool true) (bool y) = y
|
||||
evalEqOp (bool false) (bool y) = not y
|
||||
evalEqOp _ _ = false
|
||||
|
||||
evalEqOp : Value → Value → Value
|
||||
evalEqOp Value.nil Value.nil = bool true
|
||||
evalEqOp (addr x) (addr y) = bool (x == y)
|
||||
evalEqOp (number x) (number y) = bool (primFloatEquality x y)
|
||||
evalEqOp (bool true) (bool y) = bool y
|
||||
evalEqOp (bool false) (bool y) = bool (not y)
|
||||
evalEqOp _ _ = bool false
|
||||
evalNeqOp : Value → Value → Bool
|
||||
evalNeqOp (number x) (number y) = primFloatInequality x y
|
||||
evalNeqOp x y = not (evalEqOp x y)
|
||||
|
||||
evalNeqOp : Value → Value → Value
|
||||
evalNeqOp Value.nil Value.nil = bool false
|
||||
evalNeqOp (addr x) (addr y) = bool (not (x == y))
|
||||
evalNeqOp (number x) (number y) = bool (primFloatInequality x y)
|
||||
evalNeqOp (bool true) (bool y) = bool (not y)
|
||||
evalNeqOp (bool false) (bool y) = bool y
|
||||
evalNeqOp _ _ = bool true
|
||||
|
||||
coerceToBool : Value → Bool
|
||||
coerceToBool Value.nil = false
|
||||
coerceToBool (addr x) = true
|
||||
coerceToBool (number x) = true
|
||||
coerceToBool (bool x) = x
|
||||
data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
|
||||
+ : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)
|
||||
- : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n)
|
||||
/ : ∀ m n → (number m) ⟦ / ⟧ (number n) ⟶ number (primFloatTimes m n)
|
||||
* : ∀ m n → (number m) ⟦ * ⟧ (number n) ⟶ number (primFloatDiv m n)
|
||||
< : ∀ m n → (number m) ⟦ < ⟧ (number n) ⟶ bool (primFloatLess m n)
|
||||
> : ∀ m n → (number m) ⟦ > ⟧ (number n) ⟶ bool (primFloatLess n m)
|
||||
<= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n))
|
||||
>= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
|
||||
== : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
|
||||
~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
|
||||
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
|
||||
|
||||
data _⊢_⟶ᴱ_⊣_ where
|
||||
|
||||
nil : ∀ {H} →
|
||||
|
||||
-------------------
|
||||
H ⊢ nil ⟶ᴱ nil ⊣ H
|
||||
|
||||
function : ∀ {H H′ a F B} →
|
||||
function : ∀ a {H H′ F B} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function F is B end) →
|
||||
-------------------------------------------
|
||||
H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
|
||||
H ⊢ (function F is B end) ⟶ᴱ val(addr a) ⊣ H′
|
||||
|
||||
app₁ : ∀ {H H′ M M′ N} →
|
||||
|
||||
@ -68,17 +55,18 @@ data _⊢_⟶ᴱ_⊣_ where
|
||||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
|
||||
|
||||
app₂ : ∀ {H H′ V N N′} →
|
||||
app₂ : ∀ v {H H′ N N′} →
|
||||
|
||||
H ⊢ N ⟶ᴱ N′ ⊣ H′ →
|
||||
-----------------------------
|
||||
H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′
|
||||
H ⊢ (val v $ N) ⟶ᴱ (val v $ N′) ⊣ H′
|
||||
|
||||
beta : ∀ {H a F B V} →
|
||||
beta : ∀ O v {H a F B} →
|
||||
|
||||
H [ a ] ≡ just(function F is B end) →
|
||||
(O ≡ function F is B end) →
|
||||
H [ a ] ≡ just(O) →
|
||||
-----------------------------------------------------------------------------
|
||||
H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H
|
||||
H ⊢ (val (addr a) $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H
|
||||
|
||||
block : ∀ {H H′ B B′ b} →
|
||||
|
||||
@ -86,44 +74,34 @@ data _⊢_⟶ᴱ_⊣_ where
|
||||
----------------------------------------------------
|
||||
H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′
|
||||
|
||||
return : ∀ {H V B b} →
|
||||
return : ∀ v {H B b} →
|
||||
|
||||
--------------------------------------------------------
|
||||
H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H
|
||||
H ⊢ (block b is return (val v) ∙ B end) ⟶ᴱ val v ⊣ H
|
||||
|
||||
done : ∀ {H b} →
|
||||
|
||||
---------------------------------
|
||||
H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
|
||||
--------------------------------------------
|
||||
H ⊢ (block b is done end) ⟶ᴱ (val nil) ⊣ H
|
||||
|
||||
binOpEquality :
|
||||
∀ {H x y} →
|
||||
---------------------------------------------------------------------------
|
||||
H ⊢ (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H
|
||||
binOp₀ : ∀ {H op v₁ v₂ w} →
|
||||
|
||||
binOpInequality :
|
||||
∀ {H x y} →
|
||||
----------------------------------------------------------------------------
|
||||
H ⊢ (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H
|
||||
v₁ ⟦ op ⟧ v₂ ⟶ w →
|
||||
--------------------------------------------------
|
||||
H ⊢ (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) ⊣ H
|
||||
|
||||
binOpNumbers :
|
||||
∀ {H x op y} →
|
||||
-----------------------------------------------------------------------
|
||||
H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H
|
||||
binOp₁ : ∀ {H H′ x x′ op y} →
|
||||
|
||||
binOp₁ :
|
||||
∀ {H H′ x x′ op y} →
|
||||
H ⊢ x ⟶ᴱ x′ ⊣ H′ →
|
||||
---------------------------------------------
|
||||
H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′
|
||||
|
||||
binOp₂ :
|
||||
∀ {H H′ x op y y′} →
|
||||
binOp₂ : ∀ {H H′ x op y y′} →
|
||||
|
||||
H ⊢ y ⟶ᴱ y′ ⊣ H′ →
|
||||
---------------------------------------------
|
||||
H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′
|
||||
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ where
|
||||
|
||||
local : ∀ {H H′ x M M′ B} →
|
||||
@ -132,16 +110,16 @@ data _⊢_⟶ᴮ_⊣_ where
|
||||
-------------------------------------------------
|
||||
H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′
|
||||
|
||||
subst : ∀ {H x v B} →
|
||||
subst : ∀ v {H x B} →
|
||||
|
||||
------------------------------------------------------
|
||||
H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H
|
||||
|
||||
function : ∀ {H H′ a F B C} →
|
||||
function : ∀ a {H H′ F B C} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function F is C end) →
|
||||
--------------------------------------------------------------
|
||||
H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′
|
||||
H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) ⊣ H′
|
||||
|
||||
return : ∀ {H H′ M M′ B} →
|
||||
|
||||
|
||||
@ -1,15 +1,16 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.Run where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Luau.Heap using (Heap; ∅)
|
||||
open import Luau.Syntax using (Block; return; _∙_; done)
|
||||
open import Luau.Syntax using (Block; val; return; _∙_; done)
|
||||
open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
|
||||
open import Luau.Value using (val)
|
||||
open import Properties.Step using (stepᴮ; step; return; done; error)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ)
|
||||
|
||||
data RunResult {a} (H : Heap a) (B : Block a) : Set where
|
||||
return : ∀ V {B′ H′} → (H ⊢ B ⟶* (return (val V) ∙ B′) ⊣ H′) → RunResult H B
|
||||
return : ∀ v {B′ H′} → (H ⊢ B ⟶* (return (val v) ∙ B′) ⊣ H′) → RunResult H B
|
||||
done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B
|
||||
error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B
|
||||
|
||||
|
||||
@ -1,27 +1,40 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.RuntimeError where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Luau.Heap using (Heap; _[_])
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import FFI.Data.String using (String)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp)
|
||||
open import Luau.RuntimeType using (RuntimeType; valueType)
|
||||
open import Luau.Value using (val)
|
||||
open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp; +; -; *; /; <; >; <=; >=)
|
||||
open import Luau.RuntimeType using (RuntimeType; valueType; function; number)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
data BinOpError : BinaryOperator → RuntimeType → Set where
|
||||
+ : ∀ {t} → (t ≢ number) → BinOpError + t
|
||||
- : ∀ {t} → (t ≢ number) → BinOpError - t
|
||||
* : ∀ {t} → (t ≢ number) → BinOpError * t
|
||||
/ : ∀ {t} → (t ≢ number) → BinOpError / t
|
||||
< : ∀ {t} → (t ≢ number) → BinOpError < t
|
||||
> : ∀ {t} → (t ≢ number) → BinOpError > t
|
||||
<= : ∀ {t} → (t ≢ number) → BinOpError <= t
|
||||
>= : ∀ {t} → (t ≢ number) → BinOpError >= t
|
||||
|
||||
data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
|
||||
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
|
||||
|
||||
data RuntimeErrorᴱ H where
|
||||
TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v)
|
||||
UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
|
||||
SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
|
||||
FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w)
|
||||
BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
|
||||
BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
|
||||
UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)
|
||||
SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (val (addr a))
|
||||
app₁ : ∀ {M N} → RuntimeErrorᴱ H M → 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 N → RuntimeErrorᴱ H (binexp M op N)
|
||||
|
||||
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)
|
||||
|
||||
@ -1,27 +1,29 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.RuntimeError.ToString where
|
||||
|
||||
open import Agda.Builtin.Float using (primShowFloat)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; 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.Addr.ToString using (addrToString)
|
||||
open import Luau.Syntax.ToString using (exprToString)
|
||||
open import Luau.Syntax.ToString using (valueToString; exprToString)
|
||||
open import Luau.Var.ToString using (varToString)
|
||||
open import Luau.Value.ToString using (valueToString)
|
||||
open import Luau.Syntax using (name; _$_)
|
||||
open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_)
|
||||
|
||||
errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
|
||||
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ᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
|
||||
errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
|
||||
errToStringᴱ (app₁ E) = errToStringᴱ E
|
||||
errToStringᴱ (app₂ E) = errToStringᴱ E
|
||||
errToStringᴱ (bin₁ E) = errToStringᴱ E
|
||||
errToStringᴱ (bin₂ E) = errToStringᴱ E
|
||||
errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b
|
||||
errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t
|
||||
|
||||
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x)
|
||||
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement"
|
||||
errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
|
||||
errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
|
||||
errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
|
||||
errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
|
||||
errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
|
||||
errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
|
||||
errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
|
||||
errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
|
||||
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 ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n in definition of " ++ varToString (name x)
|
||||
errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n in return statement"
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
module Luau.RuntimeType where
|
||||
|
||||
open import Luau.Value using (Value; nil; addr; number; bool)
|
||||
open import Luau.Syntax using (Value; nil; addr; number; bool)
|
||||
|
||||
data RuntimeType : Set where
|
||||
function : RuntimeType
|
||||
@ -10,6 +10,6 @@ data RuntimeType : Set where
|
||||
|
||||
valueType : Value → RuntimeType
|
||||
valueType nil = nil
|
||||
valueType (addr x) = function
|
||||
valueType (number x) = number
|
||||
valueType (bool _) = boolean
|
||||
valueType (addr a) = function
|
||||
valueType (number n) = number
|
||||
valueType (bool b) = boolean
|
||||
|
||||
205
prototyping/Luau/StrictMode.agda
Normal file
205
prototyping/Luau/StrictMode.agda
Normal file
@ -0,0 +1,205 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.StrictMode where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=)
|
||||
open import Luau.Type using (Type; strict; nil; number; _⇒_; tgt)
|
||||
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
|
||||
open import Properties.Equality using (_≢_)
|
||||
open import Properties.TypeCheck(strict) using (typeCheckᴮ)
|
||||
open import Properties.Product using (_,_)
|
||||
|
||||
src : Type → Type
|
||||
src = Luau.Type.src strict
|
||||
|
||||
data BinOpWarning : BinaryOperator → Type → Set where
|
||||
+ : ∀ {T} → (T ≢ number) → BinOpWarning + T
|
||||
- : ∀ {T} → (T ≢ number) → BinOpWarning - T
|
||||
* : ∀ {T} → (T ≢ number) → BinOpWarning * T
|
||||
/ : ∀ {T} → (T ≢ number) → BinOpWarning / T
|
||||
< : ∀ {T} → (T ≢ number) → BinOpWarning < T
|
||||
> : ∀ {T} → (T ≢ number) → BinOpWarning > T
|
||||
<= : ∀ {T} → (T ≢ number) → BinOpWarning <= T
|
||||
>= : ∀ {T} → (T ≢ number) → BinOpWarning >= T
|
||||
|
||||
data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
|
||||
data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set
|
||||
|
||||
data Warningᴱ H {Γ} where
|
||||
|
||||
UnallocatedAddress : ∀ {a T} →
|
||||
|
||||
(H [ a ]ᴴ ≡ nothing) →
|
||||
---------------------
|
||||
Warningᴱ H (addr {a} T)
|
||||
|
||||
UnboundVariable : ∀ {x T p} →
|
||||
|
||||
(Γ [ x ]ⱽ ≡ nothing) →
|
||||
------------------------
|
||||
Warningᴱ H (var {x} {T} p)
|
||||
|
||||
FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
(src T ≢ U) →
|
||||
-----------------
|
||||
Warningᴱ H (app D₁ D₂)
|
||||
|
||||
app₁ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
Warningᴱ H D₁ →
|
||||
-----------------
|
||||
Warningᴱ H (app D₁ D₂)
|
||||
|
||||
app₂ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
Warningᴱ H D₂ →
|
||||
-----------------
|
||||
Warningᴱ H (app D₁ D₂)
|
||||
|
||||
BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
BinOpWarning op T →
|
||||
------------------------------
|
||||
Warningᴱ H (binexp {op} D₁ D₂)
|
||||
|
||||
BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
BinOpWarning op U →
|
||||
------------------------------
|
||||
Warningᴱ H (binexp {op} D₁ D₂)
|
||||
|
||||
bin₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
Warningᴱ H D₁ →
|
||||
------------------------------
|
||||
Warningᴱ H (binexp {op} D₁ D₂)
|
||||
|
||||
bin₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||||
|
||||
Warningᴱ H D₂ →
|
||||
------------------------------
|
||||
Warningᴱ H (binexp {op} D₁ D₂)
|
||||
|
||||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(U ≢ V) →
|
||||
-------------------------
|
||||
Warningᴱ H (function {f} {U = U} D)
|
||||
|
||||
function₁ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
Warningᴮ H D →
|
||||
-------------------------
|
||||
Warningᴱ H (function {f} {U = U} D)
|
||||
|
||||
BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||||
|
||||
(T ≢ U) →
|
||||
------------------------------
|
||||
Warningᴱ H (block {b} {T = T} D)
|
||||
|
||||
block₁ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||||
|
||||
Warningᴮ H D →
|
||||
------------------------------
|
||||
Warningᴱ H (block {b} {T = T} D)
|
||||
|
||||
data Warningᴮ H {Γ} where
|
||||
|
||||
return : ∀ {M B T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴮ B ∈ U} →
|
||||
|
||||
Warningᴱ H D₁ →
|
||||
------------------
|
||||
Warningᴮ H (return D₁ D₂)
|
||||
|
||||
LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(T ≢ U) →
|
||||
--------------------
|
||||
Warningᴮ H (local D₁ D₂)
|
||||
|
||||
local₁ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
Warningᴱ H D₁ →
|
||||
--------------------
|
||||
Warningᴮ H (local D₁ D₂)
|
||||
|
||||
local₂ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
Warningᴮ H D₂ →
|
||||
--------------------
|
||||
Warningᴮ H (local D₁ D₂)
|
||||
|
||||
FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||||
|
||||
(U ≢ V) →
|
||||
-------------------------------------
|
||||
Warningᴮ H (function D₁ D₂)
|
||||
|
||||
function₁ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||||
|
||||
Warningᴮ H D₁ →
|
||||
--------------------
|
||||
Warningᴮ H (function D₁ D₂)
|
||||
|
||||
function₂ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||||
|
||||
Warningᴮ H D₂ →
|
||||
--------------------
|
||||
Warningᴮ H (function D₁ D₂)
|
||||
|
||||
data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where
|
||||
|
||||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
(U ≢ V) →
|
||||
---------------------------------
|
||||
Warningᴼ H (function {f} {U = U} D)
|
||||
|
||||
function₁ : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
|
||||
|
||||
Warningᴮ H D →
|
||||
---------------------------------
|
||||
Warningᴼ H (function {f} {U = U} D)
|
||||
|
||||
data Warningᴴ H (D : ⊢ᴴ H) : Set where
|
||||
|
||||
addr : ∀ a {O} →
|
||||
|
||||
(p : H [ a ]ᴴ ≡ O) →
|
||||
Warningᴼ H (D a p) →
|
||||
---------------
|
||||
Warningᴴ H D
|
||||
|
||||
data Warningᴴᴱ H {Γ M T} : (Γ ⊢ᴴᴱ H ▷ M ∈ T) → Set where
|
||||
|
||||
heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →
|
||||
|
||||
Warningᴴ H D₁ →
|
||||
-----------------
|
||||
Warningᴴᴱ H (D₁ , D₂)
|
||||
|
||||
expr : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →
|
||||
|
||||
Warningᴱ H D₂ →
|
||||
---------------------
|
||||
Warningᴴᴱ H (D₁ , D₂)
|
||||
|
||||
data Warningᴴᴮ H {Γ B T} : (Γ ⊢ᴴᴮ H ▷ B ∈ T) → Set where
|
||||
|
||||
heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →
|
||||
|
||||
Warningᴴ H D₁ →
|
||||
-----------------
|
||||
Warningᴴᴮ H (D₁ , D₂)
|
||||
|
||||
block : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →
|
||||
|
||||
Warningᴮ H D₂ →
|
||||
---------------------
|
||||
Warningᴴᴮ H (D₁ , D₂)
|
||||
39
prototyping/Luau/StrictMode/ToString.agda
Normal file
39
prototyping/Luau/StrictMode/ToString.agda
Normal file
@ -0,0 +1,39 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.StrictMode.ToString where
|
||||
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
|
||||
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
|
||||
open import Luau.Type using (strict)
|
||||
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Var.ToString using (varToString)
|
||||
open import Luau.Type.ToString using (typeToString)
|
||||
open import Luau.Syntax.ToString using (binOpToString)
|
||||
|
||||
warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String
|
||||
warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String
|
||||
|
||||
warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
|
||||
warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a
|
||||
warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U
|
||||
warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
|
||||
warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
|
||||
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
|
||||
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n in function expression " ++ varToString f
|
||||
warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) = "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U
|
||||
warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n in block " ++ varToString b
|
||||
warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T
|
||||
warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U
|
||||
warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
|
||||
warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W
|
||||
|
||||
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
|
||||
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n in function declaration " ++ varToString f
|
||||
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W
|
||||
warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) = "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U
|
||||
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n in local variable declaration " ++ varToString x
|
||||
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W
|
||||
warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n in return statement"
|
||||
|
||||
@ -1,7 +1,6 @@
|
||||
module Luau.Substitution where
|
||||
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
|
||||
open import Luau.Value using (Value; val)
|
||||
open import Luau.Syntax using (Value; Expr; Stat; Block; val; nil; bool; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
|
||||
open import Luau.Var using (Var; _≡ⱽ_)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
|
||||
@ -10,18 +9,14 @@ _[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
|
||||
var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a
|
||||
_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
|
||||
|
||||
nil [ v / x ]ᴱ = nil
|
||||
true [ v / x ]ᴱ = true
|
||||
false [ v / x ]ᴱ = false
|
||||
val w [ v / x ]ᴱ = val w
|
||||
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
|
||||
addr a [ v / x ]ᴱ = addr a
|
||||
(number y) [ v / x ]ᴱ = number y
|
||||
(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
|
||||
function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
|
||||
block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
|
||||
(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)
|
||||
|
||||
(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
|
||||
(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name(fun F)))
|
||||
(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))
|
||||
(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
|
||||
done [ v / x ]ᴮ = done
|
||||
|
||||
@ -1,11 +1,12 @@
|
||||
module Luau.Syntax where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import Agda.Builtin.Float using (Float)
|
||||
open import Properties.Dec using (⊥)
|
||||
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 _∙_
|
||||
|
||||
@ -25,9 +26,9 @@ data FunDec : Annotated → Set where
|
||||
_⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
|
||||
_⟨_⟩ : Var → VarDec maybe → FunDec maybe
|
||||
|
||||
fun : ∀ {a} → FunDec a → Var
|
||||
fun (f ⟨ x ⟩∈ T) = f
|
||||
fun (f ⟨ x ⟩) = f
|
||||
fun : ∀ {a} → FunDec a → VarDec a
|
||||
fun (f ⟨ x ⟩∈ T) = (var f ∈ T)
|
||||
fun (f ⟨ x ⟩) = (var f)
|
||||
|
||||
arg : ∀ {a} → FunDec a → VarDec a
|
||||
arg (f ⟨ x ⟩∈ T) = x
|
||||
@ -40,10 +41,16 @@ data BinaryOperator : Set where
|
||||
/ : BinaryOperator
|
||||
< : BinaryOperator
|
||||
> : BinaryOperator
|
||||
≡ : BinaryOperator
|
||||
≅ : BinaryOperator
|
||||
≤ : BinaryOperator
|
||||
≥ : BinaryOperator
|
||||
== : BinaryOperator
|
||||
~= : BinaryOperator
|
||||
<= : BinaryOperator
|
||||
>= : BinaryOperator
|
||||
|
||||
data Value : Set where
|
||||
nil : Value
|
||||
addr : Addr → Value
|
||||
number : Float → Value
|
||||
bool : Bool → Value
|
||||
|
||||
data Block (a : Annotated) : Set
|
||||
data Stat (a : Annotated) : Set
|
||||
@ -59,13 +66,42 @@ data Stat a where
|
||||
return : Expr a → Stat a
|
||||
|
||||
data Expr a where
|
||||
nil : Expr a
|
||||
true : Expr a
|
||||
false : Expr a
|
||||
var : Var → Expr a
|
||||
addr : Addr → Expr a
|
||||
val : Value → Expr a
|
||||
_$_ : Expr a → Expr a → Expr a
|
||||
function_is_end : FunDec a → Block a → Expr a
|
||||
block_is_end : Var → Block a → Expr a
|
||||
number : Float → Expr a
|
||||
block_is_end : VarDec a → Block a → 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ᴱ (var x) = just (var x)
|
||||
isAnnotatedᴱ (val v) = just (val v)
|
||||
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ᴱ (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
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.Syntax.FromJSON where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /; ≡; ≅; <; >; ≤; ≥)
|
||||
open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=)
|
||||
open import Luau.Type.FromJSON using (typeFromJSON)
|
||||
|
||||
open import Agda.Builtin.List using (List; _∷_; [])
|
||||
@ -26,6 +28,8 @@ vars = fromString "vars"
|
||||
op = fromString "op"
|
||||
left = fromString "left"
|
||||
right = fromString "right"
|
||||
returnAnnotation = fromString "returnAnnotation"
|
||||
types = fromString "types"
|
||||
|
||||
data Lookup : Set where
|
||||
_,_ : String → Value → Lookup
|
||||
@ -49,22 +53,22 @@ blockFromJSON : Value → Either String (Block maybe)
|
||||
blockFromArray : Array → Either String (Block maybe)
|
||||
|
||||
binOpFromJSON (string s) = binOpFromString s
|
||||
binOpFromJSON val = Left "Binary operator not a string"
|
||||
binOpFromJSON _ = Left "Binary operator not a string"
|
||||
|
||||
binOpFromString "Add" = Right +
|
||||
binOpFromString "Sub" = Right -
|
||||
binOpFromString "Mul" = Right *
|
||||
binOpFromString "Div" = Right /
|
||||
binOpFromString "CompareEq" = Right ≡
|
||||
binOpFromString "CompareNe" = Right ≅
|
||||
binOpFromString "CompareEq" = Right ==
|
||||
binOpFromString "CompareNe" = Right ~=
|
||||
binOpFromString "CompareLt" = Right <
|
||||
binOpFromString "CompareLe" = Right ≤
|
||||
binOpFromString "CompareLe" = Right <=
|
||||
binOpFromString "CompareGt" = Right >
|
||||
binOpFromString "CompareGe" = Right ≥
|
||||
binOpFromString "CompareGe" = Right >=
|
||||
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
|
||||
|
||||
varDecFromJSON (object arg) = varDecFromObject arg
|
||||
varDecFromJSON val = Left "VarDec not an object"
|
||||
varDecFromJSON _ = Left "VarDec not an object"
|
||||
|
||||
varDecFromObject obj with lookup name obj | lookup type obj
|
||||
varDecFromObject obj | just (string name) | nothing = Right (var name)
|
||||
@ -76,7 +80,7 @@ varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string"
|
||||
varDecFromObject obj | nothing | _ = Left "AstLocal missing name"
|
||||
|
||||
exprFromJSON (object obj) = exprFromObject obj
|
||||
exprFromJSON val = Left "AstExpr not an object"
|
||||
exprFromJSON _ = Left "AstExpr not an object"
|
||||
|
||||
exprFromObject obj with lookup type obj
|
||||
exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj
|
||||
@ -89,29 +93,37 @@ exprFromObject obj | just (string "AstExprCall") | just value | just (array arr)
|
||||
exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array")
|
||||
exprFromObject obj | just (string "AstExprCall") | nothing | _ = Left ("AstExprCall missing func")
|
||||
exprFromObject obj | just (string "AstExprCall") | _ | nothing = Left ("AstExprCall missing args")
|
||||
exprFromObject obj | just (string "AstExprConstantNil") = Right nil
|
||||
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue with head arr | blockFromJSON blockValue
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
|
||||
exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
|
||||
exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
|
||||
exprFromObject obj | just (string "AstExprConstantNil") = Right (val nil)
|
||||
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj | lookup returnAnnotation obj
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn with head arr | blockFromJSON blockValue
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B with varDecFromJSON argValue
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg with lookup types rtnObj
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) with head rtnTypes
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType with typeFromJSON rtnType
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Right T = Right (function "" ⟨ arg ⟩∈ T is B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | nothing = Right (function "" ⟨ arg ⟩ is B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just _ = Left "returnAnnotation types not an array"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | nothing = Left "returnAnnotation missing types"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just _ | just argValue | Right B | Right arg = Left "returnAnnotation not an object"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | nothing | Right B = Left "Unsupported AstExprFunction empty args"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | _ | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ | rtn = Left "AstExprFunction args not an array"
|
||||
exprFromObject obj | just (string "AstExprFunction") | nothing | _ | rtn = Left "AstExprFunction missing args"
|
||||
exprFromObject obj | just (string "AstExprFunction") | _ | nothing | rtn = Left "AstExprFunction missing body"
|
||||
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
|
||||
exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
|
||||
exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
|
||||
exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
|
||||
exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
|
||||
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
|
||||
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (val (number (toFloat x)))
|
||||
exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
|
||||
exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
|
||||
exprFromObject obj | just (string "AstExprConstantBool") with lookup value obj
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool b) = Right (val (bool b))
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool missing value"
|
||||
exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
|
||||
@ -147,6 +159,7 @@ statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLo
|
||||
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩ is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩ is B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩∈ T is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩∈ T is B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
|
||||
|
||||
@ -1,7 +1,8 @@
|
||||
module Luau.Syntax.ToString where
|
||||
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import Agda.Builtin.Float using (primShowFloat)
|
||||
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; binexp; true; false)
|
||||
open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; binexp)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Type.ToString using (typeToString)
|
||||
@ -24,19 +25,24 @@ binOpToString * = "*"
|
||||
binOpToString / = "/"
|
||||
binOpToString < = "<"
|
||||
binOpToString > = ">"
|
||||
binOpToString ≡ = "=="
|
||||
binOpToString ≅ = "~="
|
||||
binOpToString ≤ = "<="
|
||||
binOpToString ≥ = ">="
|
||||
binOpToString == = "=="
|
||||
binOpToString ~= = "~="
|
||||
binOpToString <= = "<="
|
||||
binOpToString >= = ">="
|
||||
|
||||
valueToString : Value → String
|
||||
valueToString nil = "nil"
|
||||
valueToString (addr a) = addrToString a
|
||||
valueToString (number x) = primShowFloat x
|
||||
valueToString (bool false) = "false"
|
||||
valueToString (bool true) = "true"
|
||||
|
||||
exprToString′ : ∀ {a} → String → Expr a → String
|
||||
statToString′ : ∀ {a} → String → Stat a → String
|
||||
blockToString′ : ∀ {a} → String → Block a → String
|
||||
|
||||
exprToString′ lb nil =
|
||||
"nil"
|
||||
exprToString′ lb (addr a) =
|
||||
addrToString(a)
|
||||
exprToString′ lb (val v) =
|
||||
valueToString(v)
|
||||
exprToString′ lb (var x) =
|
||||
varToString(x)
|
||||
exprToString′ lb (M $ N) =
|
||||
@ -46,13 +52,10 @@ exprToString′ lb (function F is B end) =
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end"
|
||||
exprToString′ lb (block b is B end) =
|
||||
"(" ++ b ++ "()" ++ lb ++
|
||||
"(" ++ varDecToString b ++ "()" ++ lb ++
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end)()"
|
||||
exprToString′ lb (number x) = primShowFloat x
|
||||
exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
|
||||
exprToString′ lb true = "true"
|
||||
exprToString′ lb false = "false"
|
||||
|
||||
statToString′ lb (function F is B end) =
|
||||
"local " ++ funDecToString F ++ lb ++
|
||||
|
||||
@ -1,5 +1,9 @@
|
||||
module Luau.Type where
|
||||
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing; just-inv)
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
open import Properties.Equality using (cong)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
|
||||
data Type : Set where
|
||||
@ -7,18 +11,132 @@ data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
none : Type
|
||||
any : Type
|
||||
boolean : Type
|
||||
number : Type
|
||||
_∪_ : Type → Type → Type
|
||||
_∩_ : Type → Type → Type
|
||||
|
||||
src : Type → Type
|
||||
src nil = none
|
||||
src (S ⇒ T) = S
|
||||
src none = none
|
||||
src any = any
|
||||
src number = none
|
||||
src (S ∪ T) = (src S) ∪ (src T)
|
||||
src (S ∩ T) = (src S) ∩ (src T)
|
||||
lhs : Type → Type
|
||||
lhs (T ⇒ _) = T
|
||||
lhs (T ∪ _) = T
|
||||
lhs (T ∩ _) = T
|
||||
lhs nil = nil
|
||||
lhs none = none
|
||||
lhs any = any
|
||||
lhs number = number
|
||||
lhs boolean = boolean
|
||||
|
||||
rhs : Type → Type
|
||||
rhs (_ ⇒ T) = T
|
||||
rhs (_ ∪ T) = T
|
||||
rhs (_ ∩ T) = T
|
||||
rhs nil = nil
|
||||
rhs none = none
|
||||
rhs any = any
|
||||
rhs number = number
|
||||
rhs boolean = boolean
|
||||
|
||||
_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
|
||||
nil ≡ᵀ nil = yes refl
|
||||
nil ≡ᵀ (S ⇒ T) = no (λ ())
|
||||
nil ≡ᵀ none = no (λ ())
|
||||
nil ≡ᵀ any = no (λ ())
|
||||
nil ≡ᵀ number = no (λ ())
|
||||
nil ≡ᵀ boolean = no (λ ())
|
||||
nil ≡ᵀ (S ∪ T) = no (λ ())
|
||||
nil ≡ᵀ (S ∩ T) = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ nil = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
|
||||
(S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
|
||||
(S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q))
|
||||
(S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q))
|
||||
(S ⇒ T) ≡ᵀ none = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ any = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ number = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ boolean = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ())
|
||||
none ≡ᵀ nil = no (λ ())
|
||||
none ≡ᵀ (U ⇒ V) = no (λ ())
|
||||
none ≡ᵀ none = yes refl
|
||||
none ≡ᵀ any = no (λ ())
|
||||
none ≡ᵀ number = no (λ ())
|
||||
none ≡ᵀ boolean = no (λ ())
|
||||
none ≡ᵀ (U ∪ V) = no (λ ())
|
||||
none ≡ᵀ (U ∩ V) = no (λ ())
|
||||
any ≡ᵀ nil = no (λ ())
|
||||
any ≡ᵀ (U ⇒ V) = no (λ ())
|
||||
any ≡ᵀ none = no (λ ())
|
||||
any ≡ᵀ any = yes refl
|
||||
any ≡ᵀ number = no (λ ())
|
||||
any ≡ᵀ boolean = no (λ ())
|
||||
any ≡ᵀ (U ∪ V) = no (λ ())
|
||||
any ≡ᵀ (U ∩ V) = no (λ ())
|
||||
number ≡ᵀ nil = no (λ ())
|
||||
number ≡ᵀ (T ⇒ U) = no (λ ())
|
||||
number ≡ᵀ none = no (λ ())
|
||||
number ≡ᵀ any = no (λ ())
|
||||
number ≡ᵀ number = yes refl
|
||||
number ≡ᵀ boolean = no (λ ())
|
||||
number ≡ᵀ (T ∪ U) = no (λ ())
|
||||
number ≡ᵀ (T ∩ U) = no (λ ())
|
||||
boolean ≡ᵀ nil = no (λ ())
|
||||
boolean ≡ᵀ (T ⇒ U) = no (λ ())
|
||||
boolean ≡ᵀ none = no (λ ())
|
||||
boolean ≡ᵀ any = no (λ ())
|
||||
boolean ≡ᵀ boolean = yes refl
|
||||
boolean ≡ᵀ number = no (λ ())
|
||||
boolean ≡ᵀ (T ∪ U) = no (λ ())
|
||||
boolean ≡ᵀ (T ∩ U) = no (λ ())
|
||||
(S ∪ T) ≡ᵀ nil = no (λ ())
|
||||
(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
|
||||
(S ∪ T) ≡ᵀ none = no (λ ())
|
||||
(S ∪ T) ≡ᵀ any = no (λ ())
|
||||
(S ∪ T) ≡ᵀ number = no (λ ())
|
||||
(S ∪ T) ≡ᵀ boolean = no (λ ())
|
||||
(S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
|
||||
(S ∪ T) ≡ᵀ (S ∪ T) | yes refl | yes refl = yes refl
|
||||
(S ∪ T) ≡ᵀ (U ∪ V) | _ | no p = no (λ q → p (cong rhs q))
|
||||
(S ∪ T) ≡ᵀ (U ∪ V) | no p | _ = no (λ q → p (cong lhs q))
|
||||
(S ∪ T) ≡ᵀ (U ∩ V) = no (λ ())
|
||||
(S ∩ T) ≡ᵀ nil = no (λ ())
|
||||
(S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ())
|
||||
(S ∩ T) ≡ᵀ none = no (λ ())
|
||||
(S ∩ T) ≡ᵀ any = no (λ ())
|
||||
(S ∩ T) ≡ᵀ number = no (λ ())
|
||||
(S ∩ T) ≡ᵀ boolean = no (λ ())
|
||||
(S ∩ T) ≡ᵀ (U ∪ V) = no (λ ())
|
||||
(S ∩ T) ≡ᵀ (U ∩ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
|
||||
(S ∩ T) ≡ᵀ (U ∩ V) | yes refl | yes refl = yes refl
|
||||
(S ∩ T) ≡ᵀ (U ∩ V) | _ | no p = no (λ q → p (cong rhs q))
|
||||
(S ∩ T) ≡ᵀ (U ∩ V) | no p | _ = no (λ q → p (cong lhs q))
|
||||
|
||||
_≡ᴹᵀ_ : ∀ (T U : Maybe Type) → Dec(T ≡ U)
|
||||
nothing ≡ᴹᵀ nothing = yes refl
|
||||
nothing ≡ᴹᵀ just U = no (λ ())
|
||||
just T ≡ᴹᵀ nothing = no (λ ())
|
||||
just T ≡ᴹᵀ just U with T ≡ᵀ U
|
||||
(just T ≡ᴹᵀ just T) | yes refl = yes refl
|
||||
(just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))
|
||||
|
||||
data Mode : Set where
|
||||
strict : Mode
|
||||
nonstrict : Mode
|
||||
|
||||
src : Mode → Type → Type
|
||||
src m nil = none
|
||||
src m number = none
|
||||
src m boolean = none
|
||||
src m (S ⇒ T) = S
|
||||
-- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant
|
||||
src strict (S ∪ T) = (src strict S) ∩ (src strict T)
|
||||
src nonstrict (S ∪ T) = (src nonstrict S) ∪ (src nonstrict T)
|
||||
src strict (S ∩ T) = (src strict S) ∪ (src strict T)
|
||||
src nonstrict (S ∩ T) = (src nonstrict S) ∩ (src nonstrict T)
|
||||
src strict none = any
|
||||
src nonstrict none = none
|
||||
src strict any = none
|
||||
src nonstrict any = any
|
||||
|
||||
tgt : Type → Type
|
||||
tgt nil = none
|
||||
@ -26,6 +144,7 @@ tgt (S ⇒ T) = T
|
||||
tgt none = none
|
||||
tgt any = any
|
||||
tgt number = none
|
||||
tgt boolean = none
|
||||
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
|
||||
tgt (S ∩ T) = (tgt S) ∩ (tgt T)
|
||||
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.Type.FromJSON where
|
||||
|
||||
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
module Luau.Type.ToString where
|
||||
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)
|
||||
open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; _∪_; _∩_; normalizeOptional)
|
||||
|
||||
{-# TERMINATING #-}
|
||||
typeToString : Type → String
|
||||
@ -13,6 +13,7 @@ typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
|
||||
typeToString none = "none"
|
||||
typeToString any = "any"
|
||||
typeToString number = "number"
|
||||
typeToString boolean = "boolean"
|
||||
typeToString (S ∪ T) with normalizeOptional(S ∪ T)
|
||||
typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
|
||||
typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
|
||||
|
||||
143
prototyping/Luau/TypeCheck.agda
Normal file
143
prototyping/Luau/TypeCheck.agda
Normal file
@ -0,0 +1,143 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
open import Luau.Type using (Mode)
|
||||
|
||||
module Luau.TypeCheck (m : Mode) where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (Maybe; just)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=)
|
||||
open import Luau.Var using (Var)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Luau.Type using (Type; Mode; nil; none; number; boolean; _⇒_; tgt)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import FFI.Data.Vector using (Vector)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Properties.Product using (_×_; _,_)
|
||||
|
||||
src : Type → Type
|
||||
src = Luau.Type.src m
|
||||
|
||||
orNone : Maybe Type → Type
|
||||
orNone nothing = none
|
||||
orNone (just T) = T
|
||||
|
||||
tgtBinOp : BinaryOperator → Type
|
||||
tgtBinOp + = number
|
||||
tgtBinOp - = number
|
||||
tgtBinOp * = number
|
||||
tgtBinOp / = number
|
||||
tgtBinOp < = boolean
|
||||
tgtBinOp > = boolean
|
||||
tgtBinOp == = boolean
|
||||
tgtBinOp ~= = boolean
|
||||
tgtBinOp <= = boolean
|
||||
tgtBinOp >= = boolean
|
||||
|
||||
data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
|
||||
data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set
|
||||
|
||||
data _⊢ᴮ_∈_ where
|
||||
|
||||
done : ∀ {Γ} →
|
||||
|
||||
---------------
|
||||
Γ ⊢ᴮ done ∈ nil
|
||||
|
||||
return : ∀ {M B T U Γ} →
|
||||
|
||||
Γ ⊢ᴱ M ∈ T →
|
||||
Γ ⊢ᴮ B ∈ U →
|
||||
---------------------
|
||||
Γ ⊢ᴮ return M ∙ B ∈ T
|
||||
|
||||
local : ∀ {x M B T U V Γ} →
|
||||
|
||||
Γ ⊢ᴱ M ∈ U →
|
||||
(Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
|
||||
--------------------------------
|
||||
Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V
|
||||
|
||||
function : ∀ {f x B C T U V W Γ} →
|
||||
|
||||
(Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V →
|
||||
(Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W →
|
||||
-------------------------------------------------
|
||||
Γ ⊢ᴮ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W
|
||||
|
||||
data _⊢ᴱ_∈_ where
|
||||
|
||||
nil : ∀ {Γ} →
|
||||
|
||||
--------------------
|
||||
Γ ⊢ᴱ (val nil) ∈ nil
|
||||
|
||||
var : ∀ {x T Γ} →
|
||||
|
||||
T ≡ orNone(Γ [ x ]ⱽ) →
|
||||
----------------
|
||||
Γ ⊢ᴱ (var x) ∈ T
|
||||
|
||||
addr : ∀ {a Γ} T →
|
||||
|
||||
-----------------
|
||||
Γ ⊢ᴱ val(addr a) ∈ T
|
||||
|
||||
number : ∀ {n Γ} →
|
||||
|
||||
---------------------------
|
||||
Γ ⊢ᴱ val(number n) ∈ number
|
||||
|
||||
bool : ∀ {b Γ} →
|
||||
|
||||
--------------------------
|
||||
Γ ⊢ᴱ val(bool b) ∈ boolean
|
||||
|
||||
app : ∀ {M N T U Γ} →
|
||||
|
||||
Γ ⊢ᴱ M ∈ T →
|
||||
Γ ⊢ᴱ N ∈ U →
|
||||
----------------------
|
||||
Γ ⊢ᴱ (M $ N) ∈ (tgt T)
|
||||
|
||||
function : ∀ {f x B T U V Γ} →
|
||||
|
||||
(Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
|
||||
-----------------------------------------------------
|
||||
Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U)
|
||||
|
||||
block : ∀ {b B T U Γ} →
|
||||
|
||||
Γ ⊢ᴮ B ∈ U →
|
||||
------------------------------------
|
||||
Γ ⊢ᴱ (block var b ∈ T is B end) ∈ T
|
||||
|
||||
binexp : ∀ {op Γ M N T U} →
|
||||
|
||||
Γ ⊢ᴱ M ∈ T →
|
||||
Γ ⊢ᴱ N ∈ U →
|
||||
----------------------------------
|
||||
Γ ⊢ᴱ (binexp M op N) ∈ tgtBinOp op
|
||||
|
||||
data ⊢ᴼ_ : Maybe(Object yes) → Set where
|
||||
|
||||
nothing :
|
||||
|
||||
---------
|
||||
⊢ᴼ nothing
|
||||
|
||||
function : ∀ {f x T U V B} →
|
||||
|
||||
(x ↦ T) ⊢ᴮ B ∈ V →
|
||||
----------------------------------------------
|
||||
⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end)
|
||||
|
||||
⊢ᴴ_ : Heap yes → Set
|
||||
⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O)
|
||||
|
||||
_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set
|
||||
(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T)
|
||||
|
||||
_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set
|
||||
(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T)
|
||||
@ -1,20 +0,0 @@
|
||||
module Luau.Value where
|
||||
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import Agda.Builtin.Float using (Float)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false)
|
||||
open import Luau.Var using (Var)
|
||||
|
||||
data Value : Set where
|
||||
nil : Value
|
||||
addr : Addr → Value
|
||||
number : Float → Value
|
||||
bool : Bool → Value
|
||||
|
||||
val : ∀ {a} → Value → Expr a
|
||||
val nil = nil
|
||||
val (addr a) = addr a
|
||||
val (number x) = number x
|
||||
val (bool false) = false
|
||||
val (bool true) = true
|
||||
@ -1,14 +0,0 @@
|
||||
module Luau.Value.ToString where
|
||||
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Agda.Builtin.Float using (primShowFloat)
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import Luau.Value using (Value; nil; addr; number; bool)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
|
||||
valueToString : Value → String
|
||||
valueToString nil = "nil"
|
||||
valueToString (addr a) = addrToString a
|
||||
valueToString (number x) = primShowFloat x
|
||||
valueToString (bool false) = "false"
|
||||
valueToString (bool true) = "true"
|
||||
@ -4,13 +4,13 @@ open import Agda.Builtin.Bool using (true; false)
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.String using (String; primStringEquality)
|
||||
open import Agda.Builtin.TrustMe using (primTrustMe)
|
||||
open import Properties.Dec using (Dec; yes; no; ⊥)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
Var : Set
|
||||
Var = String
|
||||
|
||||
_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
|
||||
a ≡ⱽ b with primStringEquality a b
|
||||
a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥
|
||||
a ≡ⱽ b | false = no p where postulate p : (a ≢ b)
|
||||
a ≡ⱽ b | true = yes primTrustMe
|
||||
|
||||
|
||||
43
prototyping/Luau/VarCtxt.agda
Normal file
43
prototyping/Luau/VarCtxt.agda
Normal file
@ -0,0 +1,43 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.VarCtxt where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Luau.Type using (Type; _∪_; _∩_)
|
||||
open import Luau.Var using (Var)
|
||||
open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from; insert-swap; insert-over)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Properties.Equality using (_≢_; cong; sym; trans)
|
||||
|
||||
VarCtxt : Set
|
||||
VarCtxt = KeyMap Type
|
||||
|
||||
∅ : VarCtxt
|
||||
∅ = empty
|
||||
|
||||
_⋒_ : VarCtxt → VarCtxt → VarCtxt
|
||||
_⋒_ = unionWith _∩_
|
||||
|
||||
_⋓_ : VarCtxt → VarCtxt → VarCtxt
|
||||
_⋓_ = unionWith _∪_
|
||||
|
||||
_[_] : VarCtxt → Var → Maybe Type
|
||||
Γ [ x ] = lookup (fromString x) Γ
|
||||
|
||||
_⊝_ : VarCtxt → Var → VarCtxt
|
||||
Γ ⊝ x = delete (fromString x) Γ
|
||||
|
||||
_↦_ : Var → Type → VarCtxt
|
||||
x ↦ T = singleton (fromString x) T
|
||||
|
||||
_⊕_↦_ : VarCtxt → Var → Type → VarCtxt
|
||||
Γ ⊕ x ↦ T = insert (fromString x) T Γ
|
||||
|
||||
⊕-over : ∀ {Γ x y T U} → (x ≡ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ (Γ ⊕ y ↦ U)
|
||||
⊕-over p = insert-over _ _ _ _ _ (cong fromString (sym p))
|
||||
|
||||
⊕-swap : ∀ {Γ x y T U} → (x ≢ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ ((Γ ⊕ y ↦ U) ⊕ x ↦ T)
|
||||
⊕-swap p = insert-swap _ _ _ _ _ (λ q → p (trans (sym (to-from _)) (trans (cong toString (sym q) ) (to-from _))) )
|
||||
|
||||
⊕-lookup-miss : ∀ x y T Γ → (x ≢ y) → (Γ [ y ] ≡ (Γ ⊕ x ↦ T) [ y ])
|
||||
⊕-lookup-miss x y T Γ p = lookup-insert-not (fromString x) (fromString y) T Γ λ q → p (trans (sym (to-from x)) (trans (cong toString q) (to-from y)))
|
||||
@ -1,3 +1,5 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module PrettyPrinter where
|
||||
|
||||
open import Agda.Builtin.IO using (IO)
|
||||
|
||||
@ -1,7 +1,11 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Properties where
|
||||
|
||||
import Properties.Contradiction
|
||||
import Properties.Dec
|
||||
import Properties.Equality
|
||||
import Properties.Step
|
||||
import Properties.Remember
|
||||
import Properties.Step
|
||||
import Properties.StrictMode
|
||||
import Properties.TypeCheck
|
||||
|
||||
@ -1,8 +1,7 @@
|
||||
module Properties.Dec where
|
||||
|
||||
data ⊥ : Set where
|
||||
open import Properties.Contradiction using (¬)
|
||||
|
||||
data Dec(A : Set) : Set where
|
||||
yes : A → Dec A
|
||||
no : (A → ⊥) → Dec A
|
||||
|
||||
no : ¬ A → Dec A
|
||||
|
||||
14
prototyping/Properties/Product.agda
Normal file
14
prototyping/Properties/Product.agda
Normal file
@ -0,0 +1,14 @@
|
||||
module Properties.Product where
|
||||
|
||||
infixr 5 _×_ _,_
|
||||
|
||||
record Σ {A : Set} (B : A → Set) : Set where
|
||||
|
||||
constructor _,_
|
||||
field fst : A
|
||||
field snd : B fst
|
||||
|
||||
open Σ public
|
||||
|
||||
_×_ : Set → Set → Set
|
||||
A × B = Σ (λ (a : A) → B)
|
||||
@ -1,24 +1,91 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Properties.Step where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
|
||||
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess)
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; true; false; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; ≅)
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
|
||||
open import Luau.RuntimeType using (function; number)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=)
|
||||
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp; evalNeqOp)
|
||||
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=)
|
||||
open import Luau.RuntimeType using (valueType; function; number)
|
||||
open import Luau.Substitution using (_[_/_]ᴮ)
|
||||
open import Luau.Value using (nil; addr; val; number; bool)
|
||||
open import Properties.Remember using (remember; _,_)
|
||||
open import Utility.Bool using (not; _or_)
|
||||
|
||||
data BinOpStepResult v op w : Set where
|
||||
step : ∀ x → (v ⟦ op ⟧ w ⟶ x) → BinOpStepResult v op w
|
||||
error₁ : BinOpError op (valueType(v)) → BinOpStepResult v op w
|
||||
error₂ : BinOpError op (valueType(w)) → BinOpStepResult v op w
|
||||
|
||||
binOpStep : ∀ v op w → BinOpStepResult v op w
|
||||
binOpStep nil + w = error₁ (+ (λ ()))
|
||||
binOpStep (addr a) + w = error₁ (+ (λ ()))
|
||||
binOpStep (number m) + nil = error₂ (+ (λ ()))
|
||||
binOpStep (number m) + (addr a) = error₂ (+ (λ ()))
|
||||
binOpStep (number m) + (number n) = step (number (primFloatPlus m n)) (+ m n)
|
||||
binOpStep (number m) + (bool b) = error₂ (+ (λ ()))
|
||||
binOpStep (bool b) + w = error₁ (+ (λ ()))
|
||||
binOpStep nil - w = error₁ (- (λ ()))
|
||||
binOpStep (addr a) - w = error₁ (- (λ ()))
|
||||
binOpStep (number x) - nil = error₂ (- (λ ()))
|
||||
binOpStep (number x) - (addr a) = error₂ (- (λ ()))
|
||||
binOpStep (number x) - (number n) = step (number (primFloatMinus x n)) (- x n)
|
||||
binOpStep (number x) - (bool b) = error₂ (- (λ ()))
|
||||
binOpStep (bool b) - w = error₁ (- (λ ()))
|
||||
binOpStep nil * w = error₁ (* (λ ()))
|
||||
binOpStep (addr a) * w = error₁ (* (λ ()))
|
||||
binOpStep (number m) * nil = error₂ (* (λ ()))
|
||||
binOpStep (number m) * (addr a) = error₂ (* (λ ()))
|
||||
binOpStep (number m) * (number n) = step (number (primFloatDiv m n)) (* m n)
|
||||
binOpStep (number m) * (bool b) = error₂ (* (λ ()))
|
||||
binOpStep (bool b) * w = error₁ (* (λ ()))
|
||||
binOpStep nil / w = error₁ (/ (λ ()))
|
||||
binOpStep (addr a) / w = error₁ (/ (λ ()))
|
||||
binOpStep (number m) / nil = error₂ (/ (λ ()))
|
||||
binOpStep (number m) / (addr a) = error₂ (/ (λ ()))
|
||||
binOpStep (number m) / (number n) = step (number (primFloatTimes m n)) (/ m n)
|
||||
binOpStep (number m) / (bool b) = error₂ (/ (λ ()))
|
||||
binOpStep (bool b) / w = error₁ (/ (λ ()))
|
||||
binOpStep nil < w = error₁ (< (λ ()))
|
||||
binOpStep (addr a) < w = error₁ (< (λ ()))
|
||||
binOpStep (number m) < nil = error₂ (< (λ ()))
|
||||
binOpStep (number m) < (addr a) = error₂ (< (λ ()))
|
||||
binOpStep (number m) < (number n) = step (bool (primFloatLess m n)) (< m n)
|
||||
binOpStep (number m) < (bool b) = error₂ (< (λ ()))
|
||||
binOpStep (bool b) < w = error₁ (< (λ ()))
|
||||
binOpStep nil > w = error₁ (> (λ ()))
|
||||
binOpStep (addr a) > w = error₁ (> (λ ()))
|
||||
binOpStep (number m) > nil = error₂ (> (λ ()))
|
||||
binOpStep (number m) > (addr a) = error₂ (> (λ ()))
|
||||
binOpStep (number m) > (number n) = step (bool (primFloatLess n m)) (> m n)
|
||||
binOpStep (number m) > (bool b) = error₂ (> (λ ()))
|
||||
binOpStep (bool b) > w = error₁ (> (λ ()))
|
||||
binOpStep v == w = step (bool (evalEqOp v w)) (== v w)
|
||||
binOpStep v ~= w = step (bool (evalNeqOp v w)) (~= v w)
|
||||
binOpStep nil <= w = error₁ (<= (λ ()))
|
||||
binOpStep (addr a) <= w = error₁ (<= (λ ()))
|
||||
binOpStep (number m) <= nil = error₂ (<= (λ ()))
|
||||
binOpStep (number m) <= (addr a) = error₂ (<= (λ ()))
|
||||
binOpStep (number m) <= (number n) = step (bool (primFloatLess m n or primFloatEquality m n)) (<= m n)
|
||||
binOpStep (number m) <= (bool b) = error₂ (<= (λ ()))
|
||||
binOpStep (bool b) <= w = error₁ (<= (λ ()))
|
||||
binOpStep nil >= w = error₁ (>= (λ ()))
|
||||
binOpStep (addr a) >= w = error₁ (>= (λ ()))
|
||||
binOpStep (number m) >= nil = error₂ (>= (λ ()))
|
||||
binOpStep (number m) >= (addr a) = error₂ (>= (λ ()))
|
||||
binOpStep (number m) >= (number n) = step (bool (primFloatLess n m or primFloatEquality m n)) (>= m n)
|
||||
binOpStep (number m) >= (bool b) = error₂ (>= (λ ()))
|
||||
binOpStep (bool b) >= w = error₁ (>= (λ ()))
|
||||
|
||||
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
|
||||
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
|
||||
|
||||
data StepResultᴮ H B where
|
||||
step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
|
||||
return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B
|
||||
return : ∀ v {B′} → (B ≡ (return (val v) ∙ B′)) → StepResultᴮ H B
|
||||
done : (B ≡ done) → StepResultᴮ H B
|
||||
error : (RuntimeErrorᴮ H B) → StepResultᴮ H B
|
||||
|
||||
@ -30,54 +97,44 @@ data StepResultᴱ H M where
|
||||
stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
|
||||
stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
|
||||
|
||||
stepᴱ H nil = value nil refl
|
||||
stepᴱ H (var x) = error (UnboundVariable x)
|
||||
stepᴱ H (addr a) = value (addr a) refl
|
||||
stepᴱ H (number x) = value (number x) refl
|
||||
stepᴱ H (true) = value (bool true) refl
|
||||
stepᴱ H (false) = value (bool false) refl
|
||||
stepᴱ H (val v) = value v refl
|
||||
stepᴱ H (var x) = error UnboundVariable
|
||||
stepᴱ H (M $ N) with stepᴱ H M
|
||||
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
|
||||
stepᴱ H (_ $ N) | value V refl with stepᴱ H N
|
||||
stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s)
|
||||
stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
|
||||
stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
|
||||
stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ()))
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (nothing , p) = error (app₁ (SEGV a p))
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
|
||||
stepᴱ H (_ $ N) | value v refl with stepᴱ H N
|
||||
stepᴱ H (_ $ N) | value v refl | step H′ N′ s = step H′ (val v $ N′) (app₂ v s)
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ])
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV p))
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p)
|
||||
stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ()))
|
||||
stepᴱ H (_ $ _) | value (number m) refl | value w refl = error (FunctionMismatch (number m) w (λ ()))
|
||||
stepᴱ H (_ $ _) | value (bool b) refl | value w refl = error (FunctionMismatch (bool b) w (λ ()))
|
||||
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
|
||||
stepᴱ H (M $ N) | error E = error (app₁ E)
|
||||
stepᴱ H (block b is B end) with stepᴮ H B
|
||||
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
|
||||
stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
|
||||
stepᴱ H (block b is done end) | done refl = step H nil done
|
||||
stepᴱ H (block b is B end) | error E = error (block b E)
|
||||
stepᴱ H (block b is (return _ ∙ B′) end) | return v refl = step H (val v) (return v)
|
||||
stepᴱ H (block b is done end) | done refl = step H (val nil) done
|
||||
stepᴱ H (block b is B end) | error E = error (block E)
|
||||
stepᴱ H (function F is C end) with alloc H (function F is C end)
|
||||
stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
|
||||
stepᴱ H (binexp x op y) with stepᴱ H x
|
||||
stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y
|
||||
-- Have to use explicit form for ≡ here because it's a heavily overloaded symbol
|
||||
stepᴱ H (binexp x Luau.Syntax.≡ y) | value x′ refl | value y′ refl = step H (val (evalEqOp x′ y′)) binOpEquality
|
||||
stepᴱ H (binexp x ≅ y) | value x′ refl | value y′ refl = step H (val (evalNeqOp x′ y′)) binOpInequality
|
||||
stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (val (evalNumOp x′ op y′)) binOpNumbers
|
||||
stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s)
|
||||
stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E)
|
||||
stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ()))
|
||||
stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
|
||||
stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
|
||||
stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
|
||||
stepᴱ H (binexp x op y) | value (bool x′) refl | _ = error (bin₁ (TypeMismatch number (bool x′) λ()))
|
||||
stepᴱ H (binexp x op y) | _ | value (bool y′) refl = error (bin₂ (TypeMismatch number (bool y′) λ()))
|
||||
stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s)
|
||||
stepᴱ H (binexp x op y) | error E = error (bin₁ E)
|
||||
stepᴱ H function F is C end | ok a H′ p = step H′ (val (addr a)) (function a p)
|
||||
stepᴱ H (binexp M op N) with stepᴱ H M
|
||||
stepᴱ H (binexp M op N) | step H′ M′ s = step H′ (binexp M′ op N) (binOp₁ s)
|
||||
stepᴱ H (binexp M op N) | error E = error (bin₁ E)
|
||||
stepᴱ H (binexp M op N) | value v refl with stepᴱ H N
|
||||
stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s)
|
||||
stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E)
|
||||
stepᴱ H (binexp M op N) | value v refl | value w refl with binOpStep v op w
|
||||
stepᴱ H (binexp M op N) | value v refl | value w refl | step x p = step H (val x) (binOp₀ p)
|
||||
stepᴱ H (binexp M op N) | value v refl | value w refl | error₁ E = error (BinOpMismatch₁ v w E)
|
||||
stepᴱ H (binexp M op N) | value v refl | value w refl | error₂ E = error (BinOpMismatch₂ v w E)
|
||||
|
||||
stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
|
||||
stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
|
||||
stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / name (fun F) ]ᴮ) (function a p)
|
||||
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
|
||||
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
|
||||
stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
|
||||
stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
|
||||
stepᴮ H (local x ← _ ∙ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v)
|
||||
stepᴮ H (local x ← M ∙ B) | error E = error (local E)
|
||||
stepᴮ H (return M ∙ B) with stepᴱ H M
|
||||
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
|
||||
stepᴮ H (return _ ∙ B) | value V refl = return V refl
|
||||
|
||||
470
prototyping/Properties/StrictMode.agda
Normal file
470
prototyping/Properties/StrictMode.agda
Normal file
@ -0,0 +1,470 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Properties.StrictMode where
|
||||
|
||||
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; FunctionCallMismatch; app₁; app₂; BinOpWarning; 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; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
|
||||
open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
|
||||
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
|
||||
open import Luau.Var using (_≡ⱽ_)
|
||||
open import Luau.Addr using (_≡ᴬ_)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅)
|
||||
open import Properties.Remember using (remember; _,_)
|
||||
open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
open import Properties.Contradiction using (CONTRADICTION)
|
||||
open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber)
|
||||
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=)
|
||||
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=)
|
||||
open import Luau.RuntimeType using (valueType)
|
||||
|
||||
src = Luau.Type.src strict
|
||||
|
||||
data _⊑_ (H : Heap yes) : Heap yes → Set where
|
||||
refl : (H ⊑ H)
|
||||
snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′)
|
||||
|
||||
rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′)
|
||||
rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′)
|
||||
|
||||
rednᴱ⊑ (function a p) = snoc p
|
||||
rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
|
||||
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
|
||||
rednᴱ⊑ (beta O v p q) = refl
|
||||
rednᴱ⊑ (block s) = rednᴮ⊑ s
|
||||
rednᴱ⊑ (return v) = refl
|
||||
rednᴱ⊑ done = refl
|
||||
rednᴱ⊑ (binOp₀ p) = refl
|
||||
rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
|
||||
rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s
|
||||
|
||||
rednᴮ⊑ (local s) = rednᴱ⊑ s
|
||||
rednᴮ⊑ (subst v) = refl
|
||||
rednᴮ⊑ (function a p) = snoc p
|
||||
rednᴮ⊑ (return s) = rednᴱ⊑ s
|
||||
|
||||
data LookupResult (H : Heap yes) a V : Set where
|
||||
just : (H [ a ]ᴴ ≡ just V) → LookupResult H a V
|
||||
nothing : (H [ a ]ᴴ ≡ nothing) → LookupResult H a V
|
||||
|
||||
lookup-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ nothing)
|
||||
lookup-⊑-nothing {H} a refl p = p
|
||||
lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
|
||||
lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
|
||||
lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p
|
||||
|
||||
data OrWarningᴱ {Γ M T} (H : Heap yes) (D : Γ ⊢ᴱ M ∈ T) A : Set where
|
||||
ok : A → OrWarningᴱ H D A
|
||||
warning : Warningᴱ H D → OrWarningᴱ H D A
|
||||
|
||||
data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B ∈ T) A : Set where
|
||||
ok : A → OrWarningᴮ H D A
|
||||
warning : Warningᴮ H D → OrWarningᴮ H D A
|
||||
|
||||
data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H ▷ M ∈ T) A : Set where
|
||||
ok : A → OrWarningᴴᴱ H D A
|
||||
warning : Warningᴴᴱ H D → OrWarningᴴᴱ H D A
|
||||
|
||||
data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H ▷ B ∈ T) A : Set where
|
||||
ok : A → OrWarningᴴᴮ H D A
|
||||
warning : Warningᴴᴮ H D → OrWarningᴴᴮ H D A
|
||||
|
||||
heap-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M)
|
||||
heap-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B)
|
||||
|
||||
heap-weakeningᴱ H (var x) h = ok refl
|
||||
heap-weakeningᴱ H (val nil) h = ok refl
|
||||
heap-weakeningᴱ H (val (addr a)) refl = ok refl
|
||||
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} defn) with a ≡ᴬ b
|
||||
heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl)
|
||||
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
|
||||
heap-weakeningᴱ H (val (number n)) h = ok refl
|
||||
heap-weakeningᴱ H (val (bool b)) h = ok refl
|
||||
heap-weakeningᴱ H (binexp M op N) h = ok refl
|
||||
heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
|
||||
heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
|
||||
heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W)
|
||||
heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl
|
||||
heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl
|
||||
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h
|
||||
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p
|
||||
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W)
|
||||
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h
|
||||
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p
|
||||
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W)
|
||||
heap-weakeningᴮ H (return M ∙ B) h with heap-weakeningᴱ H M h
|
||||
heap-weakeningᴮ H (return M ∙ B) h | ok p = ok p
|
||||
heap-weakeningᴮ H (return M ∙ B) h | warning W = warning (return W)
|
||||
heap-weakeningᴮ H (done) h = ok refl
|
||||
|
||||
none-not-obj : ∀ O → none ≢ typeOfᴼ O
|
||||
none-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) ()
|
||||
|
||||
typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (none ≢ typeOfᴱ H Γ (val v))
|
||||
typeOf-val-not-none nil = ok (λ ())
|
||||
typeOf-val-not-none (number n) = ok (λ ())
|
||||
typeOf-val-not-none (bool b) = ok (λ ())
|
||||
typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
|
||||
typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
|
||||
typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)
|
||||
|
||||
substitutivityᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ))
|
||||
substitutivityᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p)))
|
||||
substitutivityᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p)))
|
||||
substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ))
|
||||
substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p)))
|
||||
substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p)))
|
||||
|
||||
substitutivityᴱ H (var y) v x p with x ≡ⱽ y
|
||||
substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p
|
||||
substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p
|
||||
substitutivityᴱ H (val w) v x p = refl
|
||||
substitutivityᴱ H (binexp M op N) v x p = refl
|
||||
substitutivityᴱ H (M $ N) v x p = cong tgt (substitutivityᴱ H M v x p)
|
||||
substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = refl
|
||||
substitutivityᴱ H (block var b ∈ T is B end) v x p = refl
|
||||
substitutivityᴱ-whenever-yes H v x x refl q = cong orNone q
|
||||
substitutivityᴱ-whenever-no H v x y p q = cong orNone ( sym (⊕-lookup-miss x y _ _ p))
|
||||
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f
|
||||
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q)
|
||||
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q)
|
||||
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y
|
||||
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q)
|
||||
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x y q p (⊕-swap q)
|
||||
substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p
|
||||
substitutivityᴮ H done v x p = refl
|
||||
substitutivityᴮ-unless-yes H B v x x refl q refl = refl
|
||||
substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q
|
||||
|
||||
binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x))
|
||||
binOpPreservation H (+ m n) = refl
|
||||
binOpPreservation H (- m n) = refl
|
||||
binOpPreservation H (/ m n) = refl
|
||||
binOpPreservation H (* m n) = refl
|
||||
binOpPreservation H (< m n) = refl
|
||||
binOpPreservation H (> m n) = refl
|
||||
binOpPreservation H (<= m n) = refl
|
||||
binOpPreservation H (>= m n) = refl
|
||||
binOpPreservation H (== v w) = refl
|
||||
binOpPreservation H (~= v w) = refl
|
||||
|
||||
preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
|
||||
preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)
|
||||
|
||||
preservationᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = ok refl
|
||||
preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s
|
||||
preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p)
|
||||
preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W))
|
||||
preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W)
|
||||
preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s)
|
||||
preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q)
|
||||
preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W))
|
||||
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
|
||||
preservationᴱ H (val (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 (val (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 orNone (cong typeOfᴹᴼ p)))
|
||||
preservationᴱ H (val (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 (val (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 orNone (cong typeOfᴹᴼ p)))) s) (cong orNone q)))))
|
||||
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-none v
|
||||
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (cong orNone q)))
|
||||
preservationᴱ H (val (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 (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 (BlockMismatch p))
|
||||
preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s)
|
||||
preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
|
||||
preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl
|
||||
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s)
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W))
|
||||
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 (LocalVarMismatch (λ r → q (trans r (cong orNone p)))))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-none v
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orNone p)))
|
||||
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W))
|
||||
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H B (snoc defn)
|
||||
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl))
|
||||
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W))
|
||||
preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s
|
||||
preservationᴮ H (return M ∙ B) (return s) | ok p = ok p
|
||||
preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W))
|
||||
preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W)
|
||||
|
||||
reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)
|
||||
reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))
|
||||
reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))
|
||||
reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
|
||||
reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)
|
||||
reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)
|
||||
|
||||
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 (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r
|
||||
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 (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 (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₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q)
|
||||
reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q)
|
||||
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 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 (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 (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)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
|
||||
reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W)
|
||||
|
||||
reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W
|
||||
reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W
|
||||
|
||||
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 p) = (UnboundVariable p)
|
||||
reflect-weakeningᴱ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
|
||||
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
|
||||
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)
|
||||
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W
|
||||
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h
|
||||
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)
|
||||
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 (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 (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 (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 (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 (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) (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) (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 (val (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 (val (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 (val (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 (val (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 orNone (sym r)) (trans (sym t) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-none v
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (cong orNone (sym r)))
|
||||
reflectᴱ H (val (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 (val (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 (val (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 (val (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 (val (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 orNone (sym q)) (trans (sym s) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-none v
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (cong orNone (sym q)))
|
||||
reflectᴱ H (val (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) (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)
|
||||
reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′))
|
||||
reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
|
||||
reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) with preservationᴱ H M s
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p)))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M 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 (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s)
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W)
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W)
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
|
||||
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) (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)
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′))
|
||||
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 (LocalVarMismatch (λ r → q (trans (cong orNone (sym p)) (sym r))))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-none v
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orNone (sym p)))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W)
|
||||
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W′)))
|
||||
reflectᴮ H (return M ∙ B) (return s) (return W′) with reflectᴱ H M s W′
|
||||
reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W
|
||||
reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return 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 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 (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′)
|
||||
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W)
|
||||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′)
|
||||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W)
|
||||
reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′
|
||||
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′)
|
||||
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W)
|
||||
reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′
|
||||
reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W′) = heap W′
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W)
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′)
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W)
|
||||
|
||||
reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′
|
||||
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′)
|
||||
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | 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 (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′)
|
||||
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | expr W = block (return W)
|
||||
|
||||
reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
|
||||
reflect* H B refl W = W
|
||||
reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
|
||||
|
||||
runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → BinOpWarning op (orNone (typeOfⱽ H v))
|
||||
runtimeBinOpWarning H v (+ p) = + (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (- p) = - (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (* p) = * (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (/ p) = / (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q))
|
||||
runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q))
|
||||
|
||||
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 refl
|
||||
runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p
|
||||
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-none w
|
||||
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)
|
||||
runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err)
|
||||
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₁ v w p) = BinOpMismatch₁ (runtimeBinOpWarning H v p)
|
||||
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₂ v w p) = BinOpMismatch₂ (runtimeBinOpWarning H w p)
|
||||
runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err)
|
||||
runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err)
|
||||
|
||||
runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err)
|
||||
runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)
|
||||
|
||||
wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)
|
||||
wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H′ B′ err))
|
||||
wellTypedProgramsDontGoWrong H′ B B′ t err | heap (addr a refl ())
|
||||
wellTypedProgramsDontGoWrong H′ B B′ t err | block W = W
|
||||
103
prototyping/Properties/TypeCheck.agda
Normal file
103
prototyping/Properties/TypeCheck.agda
Normal file
@ -0,0 +1,103 @@
|
||||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
open import Luau.Type using (Mode)
|
||||
|
||||
module Properties.TypeCheck (m : Mode) where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import FFI.Data.Either using (Either)
|
||||
open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
|
||||
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
|
||||
open import Luau.Type using (Type; nil; any; none; number; boolean; _⇒_; tgt)
|
||||
open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Var using (Var; _≡ⱽ_)
|
||||
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Properties.Contradiction using (CONTRADICTION)
|
||||
open import Properties.Dec using (yes; no)
|
||||
open import Properties.Equality using (_≢_; sym; trans; cong)
|
||||
open import Properties.Product using (_×_; _,_)
|
||||
open import Properties.Remember using (Remember; remember; _,_)
|
||||
|
||||
src : Type → Type
|
||||
src = Luau.Type.src m
|
||||
|
||||
typeOfᴼ : Object yes → Type
|
||||
typeOfᴼ (function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T)
|
||||
|
||||
typeOfᴹᴼ : Maybe(Object yes) → Maybe Type
|
||||
typeOfᴹᴼ nothing = nothing
|
||||
typeOfᴹᴼ (just O) = just (typeOfᴼ O)
|
||||
|
||||
typeOfⱽ : Heap yes → Value → Maybe Type
|
||||
typeOfⱽ H nil = just nil
|
||||
typeOfⱽ H (bool b) = just boolean
|
||||
typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ)
|
||||
typeOfⱽ H (number n) = just number
|
||||
|
||||
typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
|
||||
typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
|
||||
|
||||
typeOfᴱ H Γ (var x) = orNone(Γ [ x ]ⱽ)
|
||||
typeOfᴱ H Γ (val v) = orNone(typeOfⱽ H v)
|
||||
typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M)
|
||||
typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T
|
||||
typeOfᴱ H Γ (block var b ∈ T is B end) = T
|
||||
typeOfᴱ H Γ (binexp M op N) = tgtBinOp op
|
||||
|
||||
typeOfᴮ H Γ (function f ⟨ var x ∈ S ⟩∈ T is C end ∙ B) = typeOfᴮ H (Γ ⊕ f ↦ (S ⇒ T)) B
|
||||
typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B
|
||||
typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M
|
||||
typeOfᴮ H Γ done = nil
|
||||
|
||||
mustBeFunction : ∀ H Γ v → (none ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v))
|
||||
mustBeFunction H Γ nil p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (addr a) p = refl
|
||||
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
|
||||
|
||||
mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
|
||||
mustBeNumber H Γ nil ()
|
||||
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
|
||||
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
|
||||
mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
|
||||
mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
|
||||
mustBeNumber H Γ (addr a) p | nothing , q | ()
|
||||
mustBeNumber H Γ (number n) p = refl
|
||||
mustBeNumber H Γ (bool true) ()
|
||||
mustBeNumber H Γ (bool false) ()
|
||||
|
||||
typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
|
||||
typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))
|
||||
|
||||
typeCheckᴱ H Γ (var x) = var refl
|
||||
typeCheckᴱ H Γ (val nil) = nil
|
||||
typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
|
||||
typeCheckᴱ H Γ (val (number n)) = number
|
||||
typeCheckᴱ H Γ (val (bool b)) = bool
|
||||
typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
|
||||
typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
|
||||
typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B)
|
||||
typeCheckᴱ H Γ (binexp M op N) = binexp (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
|
||||
|
||||
typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B)
|
||||
typeCheckᴮ H Γ (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
|
||||
typeCheckᴮ H Γ (return M ∙ B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B)
|
||||
typeCheckᴮ H Γ done = done
|
||||
|
||||
typeCheckᴼ : ∀ H O → (⊢ᴼ O)
|
||||
typeCheckᴼ H nothing = nothing
|
||||
typeCheckᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (x ↦ T) B)
|
||||
|
||||
typeCheckᴴ : ∀ H → (⊢ᴴ H)
|
||||
typeCheckᴴ H a {O} p = typeCheckᴼ H (O)
|
||||
|
||||
typeCheckᴴᴱ : ∀ H Γ M → (Γ ⊢ᴴᴱ H ▷ M ∈ typeOfᴱ H Γ M)
|
||||
typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)
|
||||
|
||||
typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M)
|
||||
typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)
|
||||
@ -1 +1,4 @@
|
||||
false
|
||||
ANNOTATED PROGRAM:
|
||||
return true == false
|
||||
|
||||
RAN WITH RESULT: false
|
||||
|
||||
@ -1 +1,4 @@
|
||||
true
|
||||
ANNOTATED PROGRAM:
|
||||
return 1.0 == 1.0
|
||||
|
||||
RAN WITH RESULT: true
|
||||
|
||||
@ -1 +1,4 @@
|
||||
1.0
|
||||
ANNOTATED PROGRAM:
|
||||
return 1.0 + 2.0 - 2.0 * 2.0 / 2.0
|
||||
|
||||
RAN WITH RESULT: 1.0
|
||||
|
||||
@ -1 +1,7 @@
|
||||
nil
|
||||
UNANNOTATED PROGRAM:
|
||||
local function foo(x)
|
||||
return nil
|
||||
end
|
||||
return foo(nil)
|
||||
|
||||
RAN WITH RESULT: nil
|
||||
|
||||
Loading…
Reference in New Issue
Block a user