From db90c7da48f30a833802f23e0f41daab1ab6c316 Mon Sep 17 00:00:00 2001
From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Date: Fri, 11 Feb 2022 14:38:35 -0600
Subject: [PATCH] Add a typeToString function to the prototype (#354)

* Added Luau.Type.ToString
---
 .github/workflows/prototyping.yml   |  1 +
 prototyping/Examples.agda           |  2 +-
 prototyping/Examples/Type.agda      | 27 +++++++++++++++++++++++
 prototyping/Luau/Type.agda          | 33 +++++++++++++++++++++++++++++
 prototyping/Luau/Type/ToString.agda | 26 +++++++++++++++++++++++
 prototyping/Properties.agda         |  2 ++
 6 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 prototyping/Examples/Type.agda
 create mode 100644 prototyping/Luau/Type/ToString.agda

diff --git a/.github/workflows/prototyping.yml b/.github/workflows/prototyping.yml
index 02e021e..76c1e3c 100644
--- a/.github/workflows/prototyping.yml
+++ b/.github/workflows/prototyping.yml
@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - 'master'
+      - 'prototyping-*'
     paths:
       - '.github/workflows/**'
       - 'prototyping/**'
diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda
index fe396ef..212067b 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 0000000..859227e
--- /dev/null
+++ b/prototyping/Examples/Type.agda
@@ -0,0 +1,27 @@
+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
+
+ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)"
+ex6 = refl
+
+ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
+ex7 = refl
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 8da3a98..6e384c3 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,34 @@ 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′         | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | (S′ ∪ nil) | T′         = (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 0000000..698d6e8
--- /dev/null
+++ b/prototyping/Luau/Type/ToString.agda
@@ -0,0 +1,26 @@
+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) ++ " | " ++ (typeToStringᵁ T)
+typeToStringᵁ T = typeToString T
+
+typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
+typeToStringᴵ T = typeToString T
diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index a3c685d..b08a3a8 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