From 9f6fc4a56b79895f692f7b8b73fd89e98c95b592 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 24 Feb 2022 11:34:11 -0600 Subject: [PATCH] WIP --- prototyping/Examples/Type.agda | 4 +--- prototyping/Luau/Type/ToString.agda | 3 ++- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/prototyping/Examples/Type.agda b/prototyping/Examples/Type.agda index 1c5b2478..3fdd37d5 100644 --- a/prototyping/Examples/Type.agda +++ b/prototyping/Examples/Type.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} - module Examples.Type where open import Agda.Builtin.Equality using (_≡_; refl) @@ -26,5 +24,5 @@ ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil ex6 = refl ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?" -ex7 = {!!} +ex7 = refl diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index cc55f00a..a864b84c 100644 --- a/prototyping/Luau/Type/ToString.agda +++ b/prototyping/Luau/Type/ToString.agda @@ -15,12 +15,13 @@ typeToString top = "top" typeToString number = "number" typeToString (S ∪ T) with normalizeOptional(S ∪ T) typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?" -typeToString (S ∪ T) | (S′ ∪ nil) = "(" ++ typeToString S′ ++ "?" +typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?" typeToString (S ∪ T) | (S′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")" typeToString (S ∪ T) | T′ = typeToString T′ typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")" typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T) typeToStringᵁ T = typeToString T + typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T) typeToStringᴵ T = typeToString T