Add a typeToString function to the prototype

.github/workflows/prototyping.yml

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - 'master'
+      - 'prototyping-*'
     paths:
       - '.github/workflows/**'
       - 'prototyping/**'

prototyping/Examples.agda

@@ -4,4 +4,4 @@ module Examples where
 import Examples.Syntax
 import Examples.OpSem
 import Examples.Run
-
+import Examples.Type

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

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
+

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

prototyping/Properties.agda

@@ -1,3 +1,5 @@
 module Properties where
 
 import Properties.Dec
+import Properties.Step
+import Properties.Remember