From ac76424b6dfb7cbe62d05f1a4303066bef7771e8 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 25 Feb 2022 14:47:01 -0600 Subject: [PATCH] WIP --- prototyping/Examples/OpSem.agda | 5 +- prototyping/Examples/Run.agda | 11 +- prototyping/Examples/Syntax.agda | 4 +- prototyping/Interpreter.agda | 3 +- prototyping/Luau/OpSem.agda | 87 ++++------ prototyping/Luau/Run.agda | 5 +- prototyping/Luau/RuntimeError.agda | 19 ++- prototyping/Luau/RuntimeError/ToString.agda | 13 +- prototyping/Luau/RuntimeType.agda | 8 +- prototyping/Luau/StrictMode.agda | 20 ++- prototyping/Luau/StrictMode/ToString.agda | 10 +- prototyping/Luau/Substitution.agda | 9 +- prototyping/Luau/Syntax.agda | 19 ++- prototyping/Luau/Syntax/FromJSON.agda | 15 +- prototyping/Luau/Syntax/ToString.agda | 27 ++-- prototyping/Luau/TypeCheck.agda | 40 +++-- prototyping/Luau/Value.agda | 19 --- prototyping/Luau/Value/ToString.agda | 13 -- prototyping/Properties/Product.agda | 2 + prototyping/Properties/Step.agda | 108 ++++++++++--- prototyping/Properties/StrictMode.agda | 169 +++++++++++--------- prototyping/Properties/TypeCheck.agda | 35 ++-- 22 files changed, 335 insertions(+), 306 deletions(-) diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index 17d655eb..c3f74ec1 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -3,9 +3,8 @@ 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 (∅) -open import Luau.Value using (nil) -ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅ +ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅ ex1 = subst nil diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index daf627a5..545ecf51 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -4,18 +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) -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 diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda index 4ffcf4c5..e2793023 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -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 diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index bcaaee2d..cb62c707 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -17,10 +17,9 @@ open import FFI.System.Exit using (exitWith; ExitFailure) 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) open import Properties.StrictMode using (wellTypedProgramsDontGoWrong) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index e3f3aa6f..96002aff 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -7,47 +7,33 @@ open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; prim open import Agda.Builtin.Bool using (Bool; true; false) open import Utility.Bool using (not; _or_; _and_) open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_) -open import FFI.Data.Maybe using (just) +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 → 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 → 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 +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 +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 (not (evalEqOp v w)) + data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set @@ -57,7 +43,7 @@ data _⊢_⟶ᴱ_⊣_ where 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} → @@ -76,7 +62,7 @@ data _⊢_⟶ᴱ_⊣_ where (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} → @@ -91,24 +77,15 @@ data _⊢_⟶ᴱ_⊣_ where done : ∀ {H b} → - --------------------------------- - H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H - - binOpEquality : - ∀ {H x y} → - --------------------------------------------------------------------------- - H ⊢ (binexp (val x) == (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H - - binOpInequality : - ∀ {H x y} → - ---------------------------------------------------------------------------- - H ⊢ (binexp (val x) ~= (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H - - binOpNumbers : - ∀ {H x op y} → - ----------------------------------------------------------------------- - H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H + -------------------------------------------- + H ⊢ (block b is done end) ⟶ᴱ (val nil) ⊣ H + binOp₀ : ∀ {H op v₁ v₂ w} → + + v₁ ⟦ op ⟧ v₂ ⟶ w → + -------------------------------------------------- + H ⊢ (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) ⊣ H + binOp₁ : ∀ {H H′ x x′ op y} → H ⊢ x ⟶ᴱ x′ ⊣ H′ → diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda index fc60a1a4..bcd75578 100644 --- a/prototyping/Luau/Run.agda +++ b/prototyping/Luau/Run.agda @@ -4,14 +4,13 @@ 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 diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 8c052e72..4440d2b7 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -6,20 +6,29 @@ 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.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 Luau.Value using (val) 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 FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w) - BinopMismatch₁ : ∀ v w {op} → (number ≢ valueType v) → RuntimeErrorᴱ H (binexp (val v) op (val w)) - BinopMismatch₂ : ∀ v w {op} → (number ≢ valueType w) → RuntimeErrorᴱ H (binexp (val v) op (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 (addr a) + 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) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index e3522a24..6a6ed3e2 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -4,24 +4,23 @@ 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; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; 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 (var; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_) +open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_) errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound" -errToStringᴱ (addr a) (SEGV p) = "address " ++ addrToString a ++ " is unallocated" +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) (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) diff --git a/prototyping/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda index 375fc540..f6b8b4a4 100644 --- a/prototyping/Luau/RuntimeType.agda +++ b/prototyping/Luau/RuntimeType.agda @@ -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 diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 55221bba..44991043 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -4,7 +4,7 @@ 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; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name) +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; bot; top; nil; number; _⇒_; tgt) open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) @@ -16,6 +16,16 @@ 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 @@ -51,15 +61,15 @@ data Warningᴱ H {Γ} where ----------------- Warningᴱ H (app D₁ D₂) - BinopMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → + BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → - (T ≢ number) → + BinOpWarning op T → ------------------------------ Warningᴱ H (binexp {op} D₁ D₂) - BinopMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → + BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → - (U ≢ number) → + BinOpWarning op U → ------------------------------ Warningᴱ H (binexp {op} D₁ D₂) diff --git a/prototyping/Luau/StrictMode/ToString.agda b/prototyping/Luau/StrictMode/ToString.agda index 0630aeec..ca55888c 100644 --- a/prototyping/Luau/StrictMode/ToString.agda +++ b/prototyping/Luau/StrictMode/ToString.agda @@ -3,8 +3,8 @@ 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; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name) +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) @@ -16,7 +16,7 @@ warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x -warningToStringᴱ (addr a) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a +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 @@ -24,8 +24,8 @@ warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnM 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 ++ " not number" -warningToStringᴱ (binexp M op N) (BinopMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U ++ " not number" +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 diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index abf2ee7f..883cc638 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -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,12 +9,8 @@ _[_/_]ᴮ : ∀ {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 diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index b1320efb..8be0830f 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -1,6 +1,7 @@ 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 Luau.Var using (Var) open import Luau.Addr using (Addr) @@ -45,6 +46,12 @@ data BinaryOperator : Set where <= : 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 data Expr (a : Annotated) : Set @@ -59,25 +66,18 @@ 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 : VarDec a → Block a → Expr a - number : Float → Expr a binexp : Expr a → BinaryOperator → Expr a → Expr a isAnnotatedᴱ : ∀ {a} → Expr a → Maybe (Expr yes) isAnnotatedᴮ : ∀ {a} → Block a → Maybe (Block yes) -isAnnotatedᴱ nil = just nil isAnnotatedᴱ (var x) = just (var x) -isAnnotatedᴱ (addr a) = just (addr a) -isAnnotatedᴱ true = just true -isAnnotatedᴱ false = just false +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 @@ -89,7 +89,6 @@ isAnnotatedᴱ (block var b ∈ T is B end) with isAnnotatedᴮ B isAnnotatedᴱ (block var b ∈ T is B end) | just B′ = just (block var b ∈ T is B′ end) isAnnotatedᴱ (block var b ∈ T is B end) | _ = nothing isAnnotatedᴱ (block _ is B end) = nothing -isAnnotatedᴱ (number n) = just (number n) isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N isAnnotatedᴱ (binexp M op N) | just M′ | just N′ = just (binexp M′ op N′) isAnnotatedᴱ (binexp M op N) | _ | _ = nothing diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 41c0c1c9..a727a5b0 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -2,7 +2,7 @@ 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; _∷_; []) @@ -53,7 +53,7 @@ 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 - @@ -68,7 +68,7 @@ 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) @@ -80,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 @@ -93,7 +93,7 @@ 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 "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 @@ -119,12 +119,11 @@ exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right 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 diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 70ef672d..60ec471d 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -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) = @@ -49,10 +55,7 @@ exprToString′ lb (block b is B end) = "(" ++ 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 ++ diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index 39d0420f..d4725f13 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -6,11 +6,10 @@ 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; yes; nil; addr; number; true; false; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name) +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.Value using (addr; val) open import Luau.Type using (Type; Mode; nil; bot; top; number; boolean; _⇒_; tgt) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import FFI.Data.Vector using (Vector) @@ -24,6 +23,18 @@ orBot : Maybe Type → Type orBot nothing = bot orBot (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 @@ -59,8 +70,8 @@ data _⊢ᴱ_∈_ where nil : ∀ {Γ} → - -------------- - Γ ⊢ᴱ nil ∈ nil + -------------------- + Γ ⊢ᴱ (val nil) ∈ nil var : ∀ {x T Γ} → @@ -71,22 +82,17 @@ data _⊢ᴱ_∈_ where addr : ∀ {a Γ} T → ----------------- - Γ ⊢ᴱ (addr a) ∈ T + Γ ⊢ᴱ val(addr a) ∈ T number : ∀ {n Γ} → - ------------------------ - Γ ⊢ᴱ (number n) ∈ number + --------------------------- + Γ ⊢ᴱ val(number n) ∈ number - true : ∀ {Γ} → + bool : ∀ {b Γ} → - ------------------- - Γ ⊢ᴱ true ∈ boolean - - false : ∀ {Γ} → - - ------------------- - Γ ⊢ᴱ false ∈ boolean + -------------------------- + Γ ⊢ᴱ val(bool b) ∈ boolean app : ∀ {M N T U Γ} → @@ -111,8 +117,8 @@ data _⊢ᴱ_∈_ where Γ ⊢ᴱ M ∈ T → Γ ⊢ᴱ N ∈ U → - ---------------------------- - Γ ⊢ᴱ (binexp M op N) ∈ number + ---------------------------------- + Γ ⊢ᴱ (binexp M op N) ∈ tgtBinOp op data ⊢ᴼ_ : Maybe(Object yes) → Set where diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda index ed51abd7..2c35fa0a 100644 --- a/prototyping/Luau/Value.agda +++ b/prototyping/Luau/Value.agda @@ -1,20 +1 @@ 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 diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda index 3421d4cd..e5a8d5a0 100644 --- a/prototyping/Luau/Value/ToString.agda +++ b/prototyping/Luau/Value/ToString.agda @@ -1,14 +1 @@ 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" diff --git a/prototyping/Properties/Product.agda b/prototyping/Properties/Product.agda index 2118d577..0d41c817 100644 --- a/prototyping/Properties/Product.agda +++ b/prototyping/Properties/Product.agda @@ -1,5 +1,7 @@ module Properties.Product where +infixr 5 _×_ _,_ + record Σ {A : Set} (B : A → Set) : Set where constructor _,_ diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 545e84c7..608912b8 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -3,24 +3,89 @@ 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ᴮ; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; 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) +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 (not (evalEqOp 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 @@ -32,12 +97,8 @@ 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 (val v) = value v refl stepᴱ H (var x) = error UnboundVariable -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 (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 @@ -46,32 +107,27 @@ 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 x) refl | value w refl = error (FunctionMismatch (number x) 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 v) -stepᴱ H (block b is done end) | done refl = step H nil done +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 a p) +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 == N) | value v refl | value w refl = step H (val (evalEqOp v w)) binOpEquality -stepᴱ H (binexp M ~= N) | value v refl | value w refl = step H (val (evalNeqOp v w)) binOpInequality -stepᴱ H (binexp M op N) | value (number m) refl | value (number n) refl = step H (val (evalNumOp m op n)) binOpNumbers -stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ nil w λ ()) -stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ (addr a) w λ ()) -stepᴱ H (binexp M op N) | value (bool b) refl | value w refl = error (BinopMismatch₁ (bool b) w λ ()) -stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ v nil (λ ())) -stepᴱ H (binexp M op N) | value v refl | value (addr a) refl = error (BinopMismatch₂ v (addr a) (λ ())) -stepᴱ H (binexp M op N) | value v refl | value (bool b) refl = error (BinopMismatch₂ v (bool b) (λ ())) -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 | 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 / name (fun F) ]ᴮ) (function a p) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index ba4d47fb..adea8ea1 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -6,12 +6,11 @@ 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₂; BinopMismatch₁; BinopMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr) +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; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name) +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; _⇒_; bot; tgt; _≡ᵀ_; _≡ᴹᵀ_) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orBot) -open import Luau.Value using (val; nil; addr; number) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orBot; tgtBinOp) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) @@ -20,9 +19,10 @@ 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ᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber) -open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₁; binOp₂; binOpEval; refl; step) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return) +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 @@ -40,7 +40,7 @@ rednᴱ⊑ (beta O v p q) = refl rednᴱ⊑ (block s) = rednᴮ⊑ s rednᴱ⊑ (return v) = refl rednᴱ⊑ done = refl -rednᴱ⊑ (binOpEval m n) = refl +rednᴱ⊑ (binOp₀ p) = refl rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s @@ -78,13 +78,14 @@ data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H ▷ B ∈ T) A : Set where 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 (nil) h = ok refl heap-weakeningᴱ H (var x) h = ok refl -heap-weakeningᴱ H (addr a) refl = ok refl -heap-weakeningᴱ H (addr a) (snoc {a = b} defn) with a ≡ᴬ b -heap-weakeningᴱ H (addr a) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl) -heap-weakeningᴱ H (addr a) (snoc {a = b} p) | no q = ok (cong orBot (cong typeOfᴹᴼ (lookup-not-allocated p q))) -heap-weakeningᴱ H (number n) 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 orBot (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) @@ -108,6 +109,7 @@ bot-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () typeOf-val-not-bot : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (bot ≢ typeOfᴱ H Γ (val v)) typeOf-val-not-bot nil = ok (λ ()) typeOf-val-not-bot (number n) = ok (λ ()) +typeOf-val-not-bot (bool b) = ok (λ ()) typeOf-val-not-bot {H = H} (addr a) with remember (H [ a ]ᴴ) typeOf-val-not-bot {H = H} (addr a) | (just O , p) = ok (λ q → bot-not-obj O (trans q (cong orBot (cong typeOfᴹᴼ p)))) typeOf-val-not-bot {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p) @@ -119,17 +121,15 @@ substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeO 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 nil v x p = refl 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 (addr a) v x p = refl -substitutivityᴱ H (number n) v x p = refl +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 = trans (cong orBot q) (sym (typeOfᴱⱽ v)) +substitutivityᴱ-whenever-yes H v x x refl q = cong orBot q substitutivityᴱ-whenever-no H v x y p q = cong orBot ( 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) @@ -142,6 +142,18 @@ 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′) @@ -153,14 +165,14 @@ 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 (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orBot (cong typeOfᴹᴼ p))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s → r (trans (trans (sym (cong src (cong orBot (cong typeOfᴹᴼ p)))) (trans s (typeOfᴱⱽ v))) (cong orBot q))))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-bot v -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ v) (cong orBot q)))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W)) +preservationᴱ H (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 orBot (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 orBot (cong typeOfᴹᴼ p)))) s) (cong orBot 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-bot 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 orBot 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 @@ -168,7 +180,7 @@ preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no 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) (binOpEval m n) = ok refl +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 @@ -178,9 +190,9 @@ preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warnin preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p)) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (trans (typeOfᴱⱽ v) (cong orBot p)))))) +preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (cong orBot p))))) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-bot v -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (trans (typeOfᴱⱽ v) (cong orBot p)))) +preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orBot 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)) @@ -200,7 +212,7 @@ reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W -reflect-substitutionᴱ H (addr a) v x p (UnallocatedAddress r) = UnallocatedAddress r +reflect-substitutionᴱ H (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) @@ -212,8 +224,8 @@ reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p ( 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₁ (λ r → q (trans (sym (substitutivityᴱ H M x v p)) r)) -reflect-substitutionᴱ H (binexp M op N) x v p (BinopMismatch₂ q) = BinopMismatch₂ (λ r → q (trans (sym (substitutivityᴱ H N x v p)) r)) +reflect-substitutionᴱ H (binexp M op N) x v p (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) @@ -244,19 +256,19 @@ reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (t 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 (addr a) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h 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₁ (λ r → p (trans (sym q) r)) -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₂ (λ r → p (trans (sym q) r)) -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 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 @@ -307,20 +319,20 @@ reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakenin reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′ reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ H B v x (sym r)))))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t → s (trans (cong orBot (sym r)) (trans (sym (typeOfᴱⱽ v)) (trans (sym t) (cong src (cong orBot (cong typeOfᴹᴼ p)))))))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-bot v -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (trans (cong orBot (sym r)) (sym (typeOfᴱⱽ v)))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (FunctionCallMismatch (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p)))))))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-bot v -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v)))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W) +reflectᴱ H (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 orBot (sym r)) (trans (sym t) (cong src (cong orBot (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-bot 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 orBot (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 orBot (sym q)) (trans (sym s) (cong src (cong orBot (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-bot 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 orBot (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 @@ -330,24 +342,25 @@ reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = h 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₁ s) (BinopMismatch₁ p) with preservationᴱ H M s -reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₁ p) | ok q = expr (BinopMismatch₁ (λ r → p (trans (sym q) r))) -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₂ (λ r → p (trans (sym q) r))) -reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₂ p) | warning W = expr (bin₂ W) +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₁ (λ r → p (trans (sym q) r))) -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₂ (λ r → p (trans (sym q) r))) -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 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 @@ -364,9 +377,9 @@ reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block ( reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v) reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′)) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orBot (sym p)) (trans (sym (typeOfᴱⱽ v)) (sym r))))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orBot (sym p)) (sym r)))) reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-bot v -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (trans (cong orBot (sym p)) (sym (typeOfᴱⱽ v)))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orBot (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′ @@ -395,7 +408,7 @@ reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = he 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) (binOpEval m n) (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) @@ -422,19 +435,29 @@ reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴ 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 (orBot (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 (addr a) (SEGV p) = UnallocatedAddress p +runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-bot w runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = 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₁ (λ q → p (mustBeNumber H ∅ v (sym q))) -runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = BinopMismatch₂ (λ q → p (mustBeNumber H ∅ w (sym q))) +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) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 7b7ee63d..746ce3ec 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -8,14 +8,13 @@ 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; true; false; app; function; block; binexp; done; return; local; nothing; orBot) -open import Luau.Syntax using (Block; Expr; yes; nil; var; addr; number; true; false; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orBot; 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; top; bot; 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.Value using (Value; nil; addr; number; bool; val) 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) @@ -42,29 +41,18 @@ typeOfⱽ H (number n) = just number typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type -typeOfᴱ H Γ nil = nil typeOfᴱ H Γ (var x) = orBot(Γ [ x ]ⱽ) -typeOfᴱ H Γ (addr a) = orBot(typeOfᴹᴼ (H [ a ]ᴴ)) -typeOfᴱ H Γ (number n) = number -typeOfᴱ H Γ true = boolean -typeOfᴱ H Γ false = boolean +typeOfᴱ H Γ (val v) = orBot(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) = number +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 -typeOfᴱⱽ : ∀ {H Γ} v → (typeOfᴱ H Γ (val v) ≡ orBot(typeOfⱽ H v)) -typeOfᴱⱽ nil = refl -typeOfᴱⱽ (bool true) = refl -typeOfᴱⱽ (bool false) = refl -typeOfᴱⱽ (addr a) = refl -typeOfᴱⱽ (number n) = refl - mustBeFunction : ∀ H Γ v → (bot ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v)) mustBeFunction H Γ nil p = CONTRADICTION (p refl) mustBeFunction H Γ (addr a) p = refl @@ -72,12 +60,12 @@ 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 → (number ≡ typeOfᴱ H Γ (val v)) → (number ≡ valueType(v)) +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 p (cong orBot (cong typeOfᴹᴼ q)) +mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orBot (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 p (cong orBot (cong typeOfᴹᴼ q)) +mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orBot (cong typeOfᴹᴼ (sym q))) p mustBeNumber H Γ (addr a) p | nothing , q | () mustBeNumber H Γ (number n) p = refl mustBeNumber H Γ (bool true) () @@ -86,12 +74,11 @@ mustBeNumber H Γ (bool false) () typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M)) typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) -typeCheckᴱ H Γ nil = nil typeCheckᴱ H Γ (var x) = var refl -typeCheckᴱ H Γ (addr a) = addr (orBot (typeOfᴹᴼ (H [ a ]ᴴ))) -typeCheckᴱ H Γ (number n) = number -typeCheckᴱ H Γ true = true -typeCheckᴱ H Γ false = false +typeCheckᴱ H Γ (val nil) = nil +typeCheckᴱ H Γ (val (addr a)) = addr (orBot (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)