From 120207bb671eb9efbdfdee68569925b3a854b981 Mon Sep 17 00:00:00 2001
From: "ajeffrey@roblox.com" <ajeffrey@roblox.com>
Date: Thu, 10 Feb 2022 17:03:10 -0600
Subject: [PATCH] Added Luau.Type.ToString

---
 prototyping/Examples.agda           |  2 +-
 prototyping/Examples/Type.agda      | 21 +++++++++++++++++++
 prototyping/Luau/Type.agda          | 31 +++++++++++++++++++++++++++++
 prototyping/Luau/Type/ToString.agda | 28 ++++++++++++++++++++++++++
 prototyping/Properties.agda         |  2 ++
 5 files changed, 83 insertions(+), 1 deletion(-)
 create mode 100644 prototyping/Examples/Type.agda
 create mode 100644 prototyping/Luau/Type/ToString.agda

diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda
index fe396eff..212067b7 100644
--- a/prototyping/Examples.agda
+++ b/prototyping/Examples.agda
@@ -4,4 +4,4 @@ module Examples where
 import Examples.Syntax
 import Examples.OpSem
 import Examples.Run
-
+import Examples.Type
diff --git a/prototyping/Examples/Type.agda b/prototyping/Examples/Type.agda
new file mode 100644
index 00000000..5d35e8c1
--- /dev/null
+++ b/prototyping/Examples/Type.agda
@@ -0,0 +1,21 @@
+module Examples.Type where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.String using (_++_)
+open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
+open import Luau.Type.ToString using (typeToString)
+
+ex1 : typeToString(nil) ≡ "nil"
+ex1 = refl
+
+ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
+ex2 = refl
+
+ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
+ex3 = refl
+
+ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
+ex4 = refl
+
+ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
+ex5 = refl
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 8da3a985..60de2d1b 100644
--- a/prototyping/Luau/Type.agda
+++ b/prototyping/Luau/Type.agda
@@ -1,5 +1,7 @@
 module Luau.Type where
 
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
 data Type : Set where
   nil : Type
   _⇒_ : Type → Type → Type
@@ -8,3 +10,32 @@ data Type : Set where
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
+src : Type → Type
+src nil = none
+src (S ⇒ T) = S
+src none = none
+src any = any
+src (S ∪ T) = (src S) ∪ (src T)
+src (S ∩ T) = (src S) ∩ (src T)
+
+tgt : Type → Type
+tgt nil = none
+tgt (S ⇒ T) = T
+tgt none = none
+tgt any = any
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+
+optional : Type → Type
+optional nil = nil
+optional (T ∪ nil) = (T ∪ nil)
+optional T = (T ∪ nil)
+
+normalizeOptional : Type → Type
+normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
+normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | S′ | nil = optional S′
+normalizeOptional (S ∪ T) | nil | T′ = optional T′
+normalizeOptional (S ∪ T) | S′ | T′ = S′ ∪ T′
+normalizeOptional T = T
+
diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda
new file mode 100644
index 00000000..7533a3d7
--- /dev/null
+++ b/prototyping/Luau/Type/ToString.agda
@@ -0,0 +1,28 @@
+module Luau.Type.ToString where
+
+open import FFI.Data.String using (String; _++_)
+open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
+
+{-# TERMINATING #-}
+typeToString : Type → String
+typeToStringᵁ : Type → String
+typeToStringᴵ : Type → String
+
+typeToString nil = "nil"
+typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
+typeToString none = "none"
+typeToString any = "any"
+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′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")"
+typeToString (S ∪ T) | T′ = typeToString T′
+typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")"
+
+typeToStringᵁ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
+typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T)
+typeToStringᵁ T = typeToString T
+
+typeToStringᴵ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
+typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
+typeToStringᴵ T = typeToString T
diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index a3c685d1..b08a3a81 100644
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@@ -1,3 +1,5 @@
 module Properties where
 
 import Properties.Dec
+import Properties.Step
+import Properties.Remember