From d37d0c857ba543ea47f0b8fce5678f7aadf5239e Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Sat, 9 Apr 2022 00:07:08 -0500 Subject: [PATCH] Prototype: Renamed any/none to unknown/never (#447) * Renamed any/none to unknown/never * Pin hackage version * Update Agda version --- .github/workflows/prototyping.yml | 10 +- prototyping/Luau/StrictMode.agda | 2 +- prototyping/Luau/Subtyping.agda | 6 +- prototyping/Luau/Type.agda | 104 +++++++-------- prototyping/Luau/Type/FromJSON.agda | 6 +- prototyping/Luau/Type/ToString.agda | 6 +- prototyping/Luau/TypeCheck.agda | 14 +- prototyping/Properties/StrictMode.agda | 62 ++++----- prototyping/Properties/Subtyping.agda | 122 +++++++++--------- prototyping/Properties/TypeCheck.agda | 20 +-- .../Tests/PrettyPrinter/smoke_test/out.txt | 6 +- 11 files changed, 181 insertions(+), 177 deletions(-) diff --git a/.github/workflows/prototyping.yml b/.github/workflows/prototyping.yml index 6bc8a81b..ff66881d 100644 --- a/.github/workflows/prototyping.yml +++ b/.github/workflows/prototyping.yml @@ -10,7 +10,9 @@ jobs: linux: strategy: matrix: - agda: [2.6.2.1] + agda: [2.6.2.2] + hackageDate: ["2022-04-07"] + hackageTime: ["23:06:28"] name: prototyping runs-on: ubuntu-latest steps: @@ -18,7 +20,7 @@ jobs: - uses: actions/cache@v2 with: path: ~/.cabal/store - key: prototyping-${{ runner.os }}-${{ matrix.agda }} + key: "prototyping-${{ runner.os }}-${{ matrix.agda }}-${{ matrix.hackageDate }}-${{ matrix.hackageTime }}" - uses: actions/cache@v2 id: luau-ast-cache with: @@ -28,12 +30,12 @@ jobs: run: sudo apt-get install -y cabal-install - name: cabal update working-directory: prototyping - run: cabal update + run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z" - name: cabal install working-directory: prototyping run: | - cabal install Agda-${{ matrix.agda }} cabal install --lib scientific vector aeson --package-env . + cabal install --allow-newer Agda-${{ matrix.agda }} - name: check targets working-directory: prototyping run: | diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 0b5fe0da..b6769f01 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -5,7 +5,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; 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; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Luau.Type using (Type; strict; nil; number; string; boolean; _⇒_; _∪_; _∩_; tgt) open import Luau.Subtyping using (_≮:_) open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda index 7d67eb43..943f459b 100644 --- a/prototyping/Luau/Subtyping.agda +++ b/prototyping/Luau/Subtyping.agda @@ -1,6 +1,6 @@ {-# OPTIONS --rewriting #-} -open import Luau.Type using (Type; Scalar; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_) +open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_) open import Properties.Equality using (_≢_) module Luau.Subtyping where @@ -29,7 +29,7 @@ data Language where left : ∀ {T U t} → Language T t → Language (T ∪ U) t right : ∀ {T U u} → Language U u → Language (T ∪ U) u _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t - any : ∀ {t} → Language any t + unknown : ∀ {t} → Language unknown t data ¬Language where @@ -42,7 +42,7 @@ data ¬Language where _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u - none : ∀ {t} → ¬Language none t + never : ∀ {t} → ¬Language never t -- Subtyping as language inclusion diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 87815ddb..30c45388 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -9,8 +9,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) data Type : Set where nil : Type _⇒_ : Type → Type → Type - none : Type - any : Type + never : Type + unknown : Type boolean : Type number : Type string : Type @@ -29,8 +29,8 @@ lhs (T ⇒ _) = T lhs (T ∪ _) = T lhs (T ∩ _) = T lhs nil = nil -lhs none = none -lhs any = any +lhs never = never +lhs unknown = unknown lhs number = number lhs boolean = boolean lhs string = string @@ -40,8 +40,8 @@ rhs (_ ⇒ T) = T rhs (_ ∪ T) = T rhs (_ ∩ T) = T rhs nil = nil -rhs none = none -rhs any = any +rhs never = never +rhs unknown = unknown rhs number = number rhs boolean = boolean rhs string = string @@ -49,16 +49,16 @@ rhs string = string _≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) nil ≡ᵀ nil = yes refl nil ≡ᵀ (S ⇒ T) = no (λ ()) -nil ≡ᵀ none = no (λ ()) -nil ≡ᵀ any = no (λ ()) +nil ≡ᵀ never = no (λ ()) +nil ≡ᵀ unknown = no (λ ()) nil ≡ᵀ number = no (λ ()) nil ≡ᵀ boolean = no (λ ()) nil ≡ᵀ (S ∪ T) = no (λ ()) nil ≡ᵀ (S ∩ T) = no (λ ()) nil ≡ᵀ string = no (λ ()) (S ⇒ T) ≡ᵀ string = no (λ ()) -none ≡ᵀ string = no (λ ()) -any ≡ᵀ string = no (λ ()) +never ≡ᵀ string = no (λ ()) +unknown ≡ᵀ string = no (λ ()) boolean ≡ᵀ string = no (λ ()) number ≡ᵀ string = no (λ ()) (S ∪ T) ≡ᵀ string = no (λ ()) @@ -68,48 +68,48 @@ number ≡ᵀ string = no (λ ()) (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) ≡ᵀ never = no (λ ()) +(S ⇒ T) ≡ᵀ unknown = 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 (λ ()) +never ≡ᵀ nil = no (λ ()) +never ≡ᵀ (U ⇒ V) = no (λ ()) +never ≡ᵀ never = yes refl +never ≡ᵀ unknown = no (λ ()) +never ≡ᵀ number = no (λ ()) +never ≡ᵀ boolean = no (λ ()) +never ≡ᵀ (U ∪ V) = no (λ ()) +never ≡ᵀ (U ∩ V) = no (λ ()) +unknown ≡ᵀ nil = no (λ ()) +unknown ≡ᵀ (U ⇒ V) = no (λ ()) +unknown ≡ᵀ never = no (λ ()) +unknown ≡ᵀ unknown = yes refl +unknown ≡ᵀ number = no (λ ()) +unknown ≡ᵀ boolean = no (λ ()) +unknown ≡ᵀ (U ∪ V) = no (λ ()) +unknown ≡ᵀ (U ∩ V) = no (λ ()) number ≡ᵀ nil = no (λ ()) number ≡ᵀ (T ⇒ U) = no (λ ()) -number ≡ᵀ none = no (λ ()) -number ≡ᵀ any = no (λ ()) +number ≡ᵀ never = no (λ ()) +number ≡ᵀ unknown = 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 ≡ᵀ never = no (λ ()) +boolean ≡ᵀ unknown = no (λ ()) boolean ≡ᵀ boolean = yes refl boolean ≡ᵀ number = no (λ ()) boolean ≡ᵀ (T ∪ U) = no (λ ()) boolean ≡ᵀ (T ∩ U) = no (λ ()) string ≡ᵀ nil = no (λ ()) string ≡ᵀ (x ⇒ x₁) = no (λ ()) -string ≡ᵀ none = no (λ ()) -string ≡ᵀ any = no (λ ()) +string ≡ᵀ never = no (λ ()) +string ≡ᵀ unknown = no (λ ()) string ≡ᵀ boolean = no (λ ()) string ≡ᵀ number = no (λ ()) string ≡ᵀ string = yes refl @@ -117,8 +117,8 @@ string ≡ᵀ (U ∪ V) = no (λ ()) string ≡ᵀ (U ∩ V) = no (λ ()) (S ∪ T) ≡ᵀ nil = no (λ ()) (S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ()) -(S ∪ T) ≡ᵀ none = no (λ ()) -(S ∪ T) ≡ᵀ any = no (λ ()) +(S ∪ T) ≡ᵀ never = no (λ ()) +(S ∪ T) ≡ᵀ unknown = no (λ ()) (S ∪ T) ≡ᵀ number = no (λ ()) (S ∪ T) ≡ᵀ boolean = no (λ ()) (S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V) @@ -128,8 +128,8 @@ string ≡ᵀ (U ∩ V) = no (λ ()) (S ∪ T) ≡ᵀ (U ∩ V) = no (λ ()) (S ∩ T) ≡ᵀ nil = no (λ ()) (S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ()) -(S ∩ T) ≡ᵀ none = no (λ ()) -(S ∩ T) ≡ᵀ any = no (λ ()) +(S ∩ T) ≡ᵀ never = no (λ ()) +(S ∩ T) ≡ᵀ unknown = no (λ ()) (S ∩ T) ≡ᵀ number = no (λ ()) (S ∩ T) ≡ᵀ boolean = no (λ ()) (S ∩ T) ≡ᵀ (U ∪ V) = no (λ ()) @@ -151,29 +151,29 @@ data Mode : Set where nonstrict : Mode src : Mode → Type → Type -src m nil = none -src m number = none -src m boolean = none -src m string = none +src m nil = never +src m number = never +src m boolean = never +src m string = never 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 +src strict never = unknown +src nonstrict never = never +src strict unknown = never +src nonstrict unknown = unknown tgt : Type → Type -tgt nil = none +tgt nil = never tgt (S ⇒ T) = T -tgt none = none -tgt any = any -tgt number = none -tgt boolean = none -tgt string = none +tgt never = never +tgt unknown = unknown +tgt number = never +tgt boolean = never +tgt string = never tgt (S ∪ T) = (tgt S) ∪ (tgt T) tgt (S ∩ T) = (tgt S) ∩ (tgt T) diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda index 2d6ba689..e3d1e8e7 100644 --- a/prototyping/Luau/Type/FromJSON.agda +++ b/prototyping/Luau/Type/FromJSON.agda @@ -2,7 +2,7 @@ module Luau.Type.FromJSON where -open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number; string) +open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; unknown; never; number; string) open import Agda.Builtin.List using (List; _∷_; []) open import Agda.Builtin.Bool using (true; false) @@ -42,7 +42,9 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing = typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil -typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right unknown -- not quite right +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "unknown") = Right unknown +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "never") = Right never typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number typeFromJSON (object o) | just (string "AstTypeReference") | just (string "string") = Right string typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type" diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index 2efe6632..a41ecec2 100644 --- a/prototyping/Luau/Type/ToString.agda +++ b/prototyping/Luau/Type/ToString.agda @@ -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; boolean; string; _∪_; _∩_; normalizeOptional) +open import Luau.Type using (Type; nil; _⇒_; never; unknown; number; boolean; string; _∪_; _∩_; normalizeOptional) {-# TERMINATING #-} typeToString : Type → String @@ -10,8 +10,8 @@ typeToStringᴵ : Type → String typeToString nil = "nil" typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T) -typeToString none = "none" -typeToString any = "any" +typeToString never = "never" +typeToString unknown = "unknown" typeToString number = "number" typeToString boolean = "boolean" typeToString string = "string" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index c22618bc..aea6507a 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -10,7 +10,7 @@ open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr 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; any; number; boolean; string; _⇒_; tgt) +open import Luau.Type using (Type; Mode; nil; unknown; number; boolean; string; _⇒_; 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) @@ -19,9 +19,9 @@ open import Properties.Product using (_×_; _,_) src : Type → Type src = Luau.Type.src m -orAny : Maybe Type → Type -orAny nothing = any -orAny (just T) = T +orUnknown : Maybe Type → Type +orUnknown nothing = unknown +orUnknown (just T) = T srcBinOp : BinaryOperator → Type srcBinOp + = number @@ -30,8 +30,8 @@ srcBinOp * = number srcBinOp / = number srcBinOp < = number srcBinOp > = number -srcBinOp == = any -srcBinOp ~= = any +srcBinOp == = unknown +srcBinOp ~= = unknown srcBinOp <= = number srcBinOp >= = number srcBinOp ·· = string @@ -89,7 +89,7 @@ data _⊢ᴱ_∈_ where var : ∀ {x T Γ} → - T ≡ orAny(Γ [ x ]ⱽ) → + T ≡ orUnknown(Γ [ x ]ⱽ) → ---------------- Γ ⊢ᴱ (var x) ∈ T diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 2ff2b153..1165fdaa 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -9,10 +9,10 @@ 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ᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr) open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) -open import Luau.Subtyping using (_≮:_; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) +open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=) -open import Luau.Type using (Type; strict; nil; number; boolean; string; _⇒_; none; any; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orAny; srcBinOp; tgtBinOp) +open import Luau.Type using (Type; strict; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) @@ -22,7 +22,7 @@ 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.Functions using (_∘_) -open import Properties.Subtyping using (any-≮:; ≡-trans-≮:; ≮:-trans-≡; none-tgt-≮:; tgt-none-≮:; src-any-≮:; any-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-none; any-≮:-scalar; scalar-≮:-none; any-≮:-none) +open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ) 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; +; -; *; /; <; >; <=; >=; ··) @@ -68,12 +68,12 @@ heap-weakeningᴱ Γ H (var x) h p = p heap-weakeningᴱ Γ H (val nil) h p = p heap-weakeningᴱ Γ H (val (addr a)) refl p = p heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p with a ≡ᴬ b -heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = any-≮: p -heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ (lookup-not-allocated q r))) p +heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = unknown-≮: p +heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ (lookup-not-allocated q r))) p heap-weakeningᴱ Γ H (val (number x)) h p = p heap-weakeningᴱ Γ H (val (bool x)) h p = p heap-weakeningᴱ Γ H (val (string x)) h p = p -heap-weakeningᴱ Γ H (M $ N) h p = none-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-none-≮: p)) +heap-weakeningᴱ Γ H (M $ N) h p = never-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-never-≮: p)) heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p heap-weakeningᴱ Γ H (binexp M op N) h p = p @@ -94,11 +94,11 @@ substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p substitutivityᴱ H (val w) v x p = Left p substitutivityᴱ H (binexp M op N) v x p = Left p -substitutivityᴱ H (M $ N) v x p = mapL none-tgt-≮: (substitutivityᴱ H M v x (tgt-none-≮: p)) +substitutivityᴱ H (M $ N) v x p = mapL never-tgt-≮: (substitutivityᴱ H M v x (tgt-never-≮: p)) substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q) -substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orAny (sym (⊕-lookup-miss x y _ _ p))) q) +substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orUnknown (sym (⊕-lookup-miss x y _ _ p))) q) substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p @@ -125,9 +125,9 @@ binOpPreservation H (·· v w) = refl reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M)) reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B)) -reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR none-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-none-≮: p)) -reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (none-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-none-≮: p))) -reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orAny (cong typeOfᴹᴼ q))) p) +reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR never-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-never-≮: p)) +reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (never-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-never-≮: p))) +reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orUnknown (cong typeOfᴹᴼ q))) p) reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p)) @@ -152,8 +152,8 @@ reflect-substitutionᴱ H (var y) v x W = reflect-substitutionᴱ-whenever H v x reflect-substitutionᴱ H (val (addr a)) v x (UnallocatedAddress r) = Left (UnallocatedAddress r) reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with substitutivityᴱ H N v x p reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Right W = Right (Right W) -reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-any-≮: q) -reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ any-src-≮: q) r) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-unknown-≮: q) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ unknown-src-≮: q) r) reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Right W = Right (Right W) reflect-substitutionᴱ H (M $ N) v x (app₁ W) = mapL app₁ (reflect-substitutionᴱ H M v x W) reflect-substitutionᴱ H (M $ N) v x (app₂ W) = mapL app₂ (reflect-substitutionᴱ H N v x W) @@ -187,7 +187,7 @@ reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (t 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) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (any-src-≮: p (heap-weakeningᴱ Γ H M h (src-any-≮: p)))) +reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (unknown-src-≮: p (heap-weakeningᴱ Γ H M h (src-unknown-≮: p)))) 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) = BinOpMismatch₁ (heap-weakeningᴱ Γ H M h p) @@ -214,19 +214,19 @@ reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (fu reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H)) reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H)) -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ any-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-any-≮: p)) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ unknown-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-unknown-≮: p)) reflectᴱ H (M $ N) (app₁ s) (app₁ W′) = mapL app₁ (reflectᴱ H M s W′) reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = Left (app₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′)) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (any-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-any-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (unknown-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-unknown-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q) reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = Left (app₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′)) reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) = mapL app₂ (reflectᴱ H N s W′) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with substitutivityᴮ H B v x q reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Left r = Right (addr a p (FunctionDefnMismatch r)) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orAny (cong typeOfᴹᴼ (sym p))))))) +reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orUnknown (cong typeOfᴹᴼ (sym p))))))) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with reflect-substitutionᴮ _ B v x W′ reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Left W = Right (addr a p (function₁ W)) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Left W) = Left (app₂ W) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orAny (cong typeOfᴹᴼ (sym p)))))) +reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orUnknown (cong typeOfᴹᴼ (sym p)))))) reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (reflect-subtypingᴮ H B s p)) reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) = mapL block₁ (reflectᴮ H B s W′) reflectᴱ H (block var b ∈ T is B end) (return v) W′ = Left (block₁ (return W′)) @@ -283,8 +283,8 @@ reflect* H B (step s t) W = cond (reflectᴮ H B s) (reflectᴴᴮ H B s) (refle isntNumber : ∀ H v → (valueType v ≢ number) → (typeOfᴱ H ∅ (val v) ≮: number) isntNumber H nil p = scalar-≢-impl-≮: nil number (λ ()) isntNumber H (addr a) p with remember (H [ a ]ᴴ) -isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar number) -isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar number) +isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar number) +isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar number) isntNumber H (number x) p = CONTRADICTION (p refl) isntNumber H (bool x) p = scalar-≢-impl-≮: boolean number (λ ()) isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ()) @@ -292,8 +292,8 @@ isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ()) isntString : ∀ H v → (valueType v ≢ string) → (typeOfᴱ H ∅ (val v) ≮: string) isntString H nil p = scalar-≢-impl-≮: nil string (λ ()) isntString H (addr a) p with remember (H [ a ]ᴴ) -isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar string) -isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar string) +isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar string) +isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar string) isntString H (number x) p = scalar-≢-impl-≮: number string (λ ()) isntString H (bool x) p = scalar-≢-impl-≮: boolean string (λ ()) isntString H (string x) p = CONTRADICTION (p refl) @@ -305,14 +305,14 @@ isntFunction H (number x) p = scalar-≮:-function number isntFunction H (bool x) p = scalar-≮:-function boolean isntFunction H (string x) p = scalar-≮:-function string -isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: none) -isntEmpty H nil = scalar-≮:-none nil +isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: never) +isntEmpty H nil = scalar-≮:-never nil isntEmpty H (addr a) with remember (H [ a ]ᴴ) -isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) function-≮:-none -isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) any-≮:-none -isntEmpty H (number x) = scalar-≮:-none number -isntEmpty H (bool x) = scalar-≮:-none boolean -isntEmpty H (string x) = scalar-≮:-none string +isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) function-≮:-never +isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) unknown-≮:-never +isntEmpty H (number x) = scalar-≮:-never number +isntEmpty H (bool x) = scalar-≮:-never boolean +isntEmpty H (string x) = scalar-≮:-never string runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → (typeOfᴱ H ∅ (val v) ≮: srcBinOp op) runtimeBinOpWarning H v (+ p) = isntNumber H v p @@ -330,7 +330,7 @@ runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheck runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (any-src-≮: (isntEmpty H w) (isntFunction H v p)) +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (unknown-src-≮: (isntEmpty H w) (isntFunction H v p)) 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) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 0a20f244..cc6bb5c1 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -4,8 +4,8 @@ module Properties.Subtyping where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond) -open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_) -open import Luau.Type using (Type; Scalar; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_) +open import Luau.Type using (Type; Scalar; strict; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; tgt) open import Properties.Contradiction using (CONTRADICTION; ¬) open import Properties.Equality using (_≢_) open import Properties.Functions using (_∘_) @@ -47,8 +47,8 @@ dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s) dec-language (T₁ ⇒ T₂) function = Right function dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t) dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t)) -dec-language none t = Left none -dec-language any t = Right any +dec-language never t = Left never +dec-language unknown t = Right unknown dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t) dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t) @@ -60,7 +60,7 @@ language-comp t (left p) (q₁ , q₂) = language-comp t p q₁ language-comp t (right p) (q₁ , q₂) = language-comp t p q₂ language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function -language-comp (scalar s) none (scalar ()) +language-comp (scalar s) never (scalar ()) language-comp function (scalar-function ()) function language-comp (function-ok t) (scalar-function-ok ()) (function-ok q) language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q @@ -104,11 +104,11 @@ function-≮:-scalar s = witness function function (scalar-function s) scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T)) scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s) -any-≮:-scalar : ∀ {U} → (Scalar U) → (any ≮: U) -any-≮:-scalar s = witness (function-ok (scalar s)) any (scalar-function-ok s) +unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U) +unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s) -scalar-≮:-none : ∀ {U} → (Scalar U) → (U ≮: none) -scalar-≮:-none s = witness (scalar s) (scalar s) none +scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never) +scalar-≮:-never s = witness (scalar s) (scalar s) never scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U) scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p) @@ -117,8 +117,8 @@ scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-s tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t) tgt-function-ok {T = nil} (scalar ()) tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p -tgt-function-ok {T = none} (scalar ()) -tgt-function-ok {T = any} p = any +tgt-function-ok {T = never} (scalar ()) +tgt-function-ok {T = unknown} p = unknown tgt-function-ok {T = boolean} (scalar ()) tgt-function-ok {T = number} (scalar ()) tgt-function-ok {T = string} (scalar ()) @@ -131,7 +131,7 @@ function-ok-tgt (function-ok p) = p function-ok-tgt (left p) = left (function-ok-tgt p) function-ok-tgt (right p) = right (function-ok-tgt p) function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂) -function-ok-tgt any = any +function-ok-tgt unknown = unknown skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) @@ -142,22 +142,22 @@ skalar-scalar boolean = right (right (right (scalar boolean))) skalar-scalar string = right (left (scalar string)) skalar-scalar nil = right (right (left (scalar nil))) -tgt-none-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (none ⇒ U))) -tgt-none-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) +tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U))) +tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) -none-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (none ⇒ U))) → (tgt T ≮: U) -none-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) -none-tgt-≮: (witness function p (q₁ , scalar-function ())) -none-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ -none-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) +never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U) +never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) +never-tgt-≮: (witness function p (q₁ , scalar-function ())) +never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ +never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) -- Properties of src function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t) -function-err-src {T = nil} none = scalar-function-err nil +function-err-src {T = nil} never = scalar-function-err nil function-err-src {T = T₁ ⇒ T₂} p = function-err p -function-err-src {T = none} (scalar-scalar number () p) -function-err-src {T = none} (scalar-function-ok ()) -function-err-src {T = any} none = any +function-err-src {T = never} (scalar-scalar number () p) +function-err-src {T = never} (scalar-function-ok ()) +function-err-src {T = unknown} never = unknown function-err-src {T = boolean} p = scalar-function-err boolean function-err-src {T = number} p = scalar-function-err number function-err-src {T = string} p = scalar-function-err string @@ -168,8 +168,8 @@ function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , fun ¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t) ¬function-err-src {T = nil} (scalar ()) ¬function-err-src {T = T₁ ⇒ T₂} p = function-err p -¬function-err-src {T = none} any = none -¬function-err-src {T = any} (scalar ()) +¬function-err-src {T = never} unknown = never +¬function-err-src {T = unknown} (scalar ()) ¬function-err-src {T = boolean} (scalar ()) ¬function-err-src {T = number} (scalar ()) ¬function-err-src {T = string} (scalar ()) @@ -178,53 +178,53 @@ function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , fun ¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p) src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t) -src-¬function-err {T = nil} p = none +src-¬function-err {T = nil} p = never src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p -src-¬function-err {T = none} (scalar-function-err ()) -src-¬function-err {T = any} p = none -src-¬function-err {T = boolean} p = none -src-¬function-err {T = number} p = none -src-¬function-err {T = string} p = none +src-¬function-err {T = never} (scalar-function-err ()) +src-¬function-err {T = unknown} p = never +src-¬function-err {T = boolean} p = never +src-¬function-err {T = number} p = never +src-¬function-err {T = string} p = never src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p) src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p) src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂) src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t) -src-¬scalar number (scalar number) = none -src-¬scalar boolean (scalar boolean) = none -src-¬scalar string (scalar string) = none -src-¬scalar nil (scalar nil) = none +src-¬scalar number (scalar number) = never +src-¬scalar boolean (scalar boolean) = never +src-¬scalar string (scalar string) = never +src-¬scalar nil (scalar nil) = never src-¬scalar s (left p) = left (src-¬scalar s p) src-¬scalar s (right p) = right (src-¬scalar s p) src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂) -src-¬scalar s any = none +src-¬scalar s unknown = never -src-any-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ any)) -src-any-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) +src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown)) +src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) -any-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ any)) → (U ≮: src T) -any-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) -any-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) -any-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) -any-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) +unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T) +unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) +unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) +unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) +unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) --- Properties of any and none -any-≮: : ∀ {T U} → (T ≮: U) → (any ≮: U) -any-≮: (witness t p q) = witness t any q +-- Properties of unknown and never +unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U) +unknown-≮: (witness t p q) = witness t unknown q -none-≮: : ∀ {T U} → (T ≮: U) → (T ≮: none) -none-≮: (witness t p q) = witness t p none +never-≮: : ∀ {T U} → (T ≮: U) → (T ≮: never) +never-≮: (witness t p q) = witness t p never -any-≮:-none : (any ≮: none) -any-≮:-none = witness (scalar nil) any none +unknown-≮:-never : (unknown ≮: never) +unknown-≮:-never = witness (scalar nil) unknown never -function-≮:-none : ∀ {T U} → ((T ⇒ U) ≮: none) -function-≮:-none = witness function function none +function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never) +function-≮:-never = witness function function never -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf) -- defines a "set-theoretic" model (sec 2.5) -- Unfortunately we don't quite have this property, due to uninhabited types, --- for example (none -> T) is equivalent to (none -> U) +-- for example (never -> T) is equivalent to (never -> U) -- when types are interpreted as sets of syntactic values. _⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set @@ -258,7 +258,7 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → -- We don't quite have that this is a set-theoretic model -- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited - -- in particular it's not true when T₁ is none, or T₂ is any. + -- in particular it's not true when T₁ is never, or T₂ is unknown. ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ → -- This is the "only if" part of being a set-theoretic model @@ -285,11 +285,11 @@ not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ -- A counterexample when the argument type is empty. -set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language none) ⊗ Comp(Language number)) → Q ⊆ Comp((Language none) ⊗ Comp(Language string))) +set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string))) set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p) set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p) -set-theoretic-counterexample-two : (none ⇒ number) ≮: (none ⇒ string) +set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string) set-theoretic-counterexample-two = witness (function-ok (scalar number)) (function-ok (scalar number)) (function-ok (scalar-scalar number string (λ ()))) @@ -298,14 +298,14 @@ set-theoretic-counterexample-two = witness -- The reason why this is connected to overloaded functions is that currently we have that the type of -- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U), -- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V) --- and tgt(none => T) should be any. For example +-- and tgt(never => T) should be unknown. For example -- -- tgt((number => string) & (string => bool))(number) -- is tgt(number => string)(number) & tgt(string => bool)(number) --- is tgt(number => string)(number) & tgt(string => bool)(number&any) --- is tgt(number => string)(number) & tgt(string&number => bool)(any) --- is tgt(number => string)(number) & tgt(none => bool)(any) --- is string & any +-- is tgt(number => string)(number) & tgt(string => bool)(number&unknown) +-- is tgt(number => string)(number) & tgt(string&number => bool)(unknown) +-- is tgt(number => string)(number) & tgt(never => bool)(unknown) +-- is string & unknown -- is string -- -- there's some discussion of this in the Gentle Introduction paper. diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index ead0c097..a5916a13 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -8,9 +8,9 @@ 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; string; app; function; block; binexp; done; return; local; nothing; orAny; tgtBinOp) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp) open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; 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; string; _⇒_; tgt) +open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; tgt) open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType) open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) @@ -42,8 +42,8 @@ typeOfⱽ H (string x) = just string typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type -typeOfᴱ H Γ (var x) = orAny(Γ [ x ]ⱽ) -typeOfᴱ H Γ (val v) = orAny(typeOfⱽ H v) +typeOfᴱ H Γ (var x) = orUnknown(Γ [ x ]ⱽ) +typeOfᴱ H Γ (val v) = orUnknown(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 @@ -54,7 +54,7 @@ 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 Γ v → (never ≢ 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) @@ -64,17 +64,17 @@ mustBeFunction H Γ (string x) p = CONTRADICTION (p refl) mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number) mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ) -mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orUnknown (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 orAny (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p mustBeNumber H Γ (addr a) p | nothing , q | () mustBeNumber H Γ (number n) p = refl mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string) mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ) -mustBeString H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (just O , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | () -mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p mustBeString H Γ (addr a) p | (nothing , q) | () mustBeString H Γ (string x) p = refl @@ -83,7 +83,7 @@ typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) typeCheckᴱ H Γ (var x) = var refl typeCheckᴱ H Γ (val nil) = nil -typeCheckᴱ H Γ (val (addr a)) = addr (orAny (typeOfᴹᴼ (H [ a ]ᴴ))) +typeCheckᴱ H Γ (val (addr a)) = addr (orUnknown (typeOfᴹᴼ (H [ a ]ᴴ))) typeCheckᴱ H Γ (val (number n)) = number typeCheckᴱ H Γ (val (bool b)) = bool typeCheckᴱ H Γ (val (string x)) = string diff --git a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt index 34e0c4fe..ca95cae9 100644 --- a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt +++ b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt @@ -10,10 +10,10 @@ local function comp(f) end local id2 = comp(id)(id) local nil2 = id2(nil) -local a : any = nil +local a : unknown = nil local b : nil = nil local c : (nil) -> nil = nil -local d : (any & nil) = nil -local e : any? = nil +local d : (unknown & nil) = nil +local e : unknown? = nil local f : number = 123.0 return id2(nil2)