From 74f0dc953839179aae071dda1ddb924295bc6061 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 2 Jan 2023 15:43:24 +0000
Subject: Add more program structure to type universes.

---
 src/Obs/NormalForm.idr | 107 +++++++++++++++++++++++++------------------------
 1 file changed, 55 insertions(+), 52 deletions(-)

(limited to 'src/Obs/NormalForm.idr')

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index a756728..d660111 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -1,10 +1,9 @@
 module Obs.NormalForm
 
 import Data.List.Elem
-import Data.So
 
-import Obs.Sort
 import Obs.Substitution
+import Obs.Universe
 
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
@@ -13,29 +12,33 @@ import Text.PrettyPrint.Prettyprinter
 
 -- Definition ------------------------------------------------------------------
 
-data NormalForm  : Sorted.Family Bool
+data NormalForm  : Sorted.Family Relevance
 
 public export
-data Constructor : Unsorted.Family Bool where
-  Sort : (s : Sort) -> Constructor ctx
-  Pi : (s, s' : Sort)
+TypeNormalForm : Unsorted.Family Relevance
+TypeNormalForm = NormalForm Relevant
+
+public export
+data Constructor : Unsorted.Family Relevance where
+  Universe : (s : Universe) -> Constructor ctx
+  Pi : (s, s' : Universe)
     -> (var : String)
-    -> (a : NormalForm True ctx)
-    -> (b : NormalForm True (isSet s :: ctx))
+    -> (a : TypeNormalForm ctx)
+    -> (b : TypeNormalForm (relevance s :: ctx))
     -> Constructor ctx
-  Lambda : (s : Sort)
+  Lambda : (s : Universe)
     -> (var : String)
-    -> NormalForm True (isSet s :: ctx)
+    -> NormalForm Relevant (relevance s :: ctx)
     -> Constructor ctx
-  Sigma : (s, s' : Sort)
+  Sigma : (s, s' : Universe)
     -> (var : String)
-    -> (a : NormalForm True ctx)
-    -> (b : NormalForm True (isSet s :: ctx))
+    -> (a : TypeNormalForm ctx)
+    -> (b : TypeNormalForm (relevance s :: ctx))
     -> Constructor ctx
-  Pair : (s, s' : Sort)
-    -> (prf : So (isSet (max s s')))
-    -> NormalForm (isSet s) ctx
-    -> NormalForm (isSet s') ctx
+  Pair : (s, s' : Universe)
+    -> (prf : IsRelevant (max s s'))
+    -> NormalForm (relevance s) ctx
+    -> NormalForm (relevance s') ctx
     -> Constructor ctx
   Bool : Constructor ctx
   True : Constructor ctx
@@ -44,61 +47,61 @@ data Constructor : Unsorted.Family Bool where
   Bottom : Constructor ctx
 
 public export
-data Neutral : Unsorted.Family Bool where
+data Neutral : Unsorted.Family Relevance where
   Var : (var : String)
-    -> (sort : Sort)
-    -> (prf : So (isSet sort))
-    -> (i : Elem True ctx)
+    -> (sort : Universe)
+    -> (prf : IsRelevant sort)
+    -> (i : Elem Relevant ctx)
     -> Neutral ctx
-  App : (b : Bool) -> Neutral ctx -> NormalForm b ctx -> Neutral ctx
-  Fst : (b : Bool) -> Neutral ctx -> Neutral ctx
-  Snd : (b : Bool) -> Neutral ctx -> Neutral ctx
-  If : Neutral ctx -> (f, g : NormalForm True ctx) -> Neutral ctx
+  App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx
+  Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx
+  Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx
+  If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx
   Absurd : Neutral ctx
-  Equal : Neutral ctx -> NormalForm True ctx -> NormalForm True ctx -> Neutral ctx
-  EqualL : (a : Neutral ctx) -> (b : NormalForm True ctx) -> Neutral ctx
+  Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx
+  EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx
   EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
   EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
   CastL : (a : Neutral ctx) ->
-    (b : NormalForm True ctx) ->
-    NormalForm True ctx ->
+    (b : TypeNormalForm ctx) ->
+    NormalForm Relevant ctx ->
     Neutral ctx
-  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm True ctx -> Neutral ctx
-  CastStuck : (a, b : Constructor ctx) -> NormalForm True ctx -> Neutral ctx
+  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx
+  CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx
 
 public export
-data NormalForm : Sorted.Family Bool where
-  Ntrl : Neutral ~|> NormalForm True
-  Cnstr : Constructor ~|> NormalForm True
-  Irrel : NormalForm False ctx
+data NormalForm : Sorted.Family Relevance where
+  Ntrl : Neutral ~|> NormalForm Relevant
+  Cnstr : Constructor ~|> NormalForm Relevant
+  Irrel : NormalForm Irrelevant ctx
 
 %name Constructor t, u, v
 %name Neutral t, u, v
 %name NormalForm t, u, v
 
 public export
-record Definition (ctx : List Bool) where
+record Definition (ctx : List Relevance) where
   constructor MkDefinition
   name : WithBounds String
-  sort : Sort
-  ty   : NormalForm True ctx
-  tm   : NormalForm (isSet sort) ctx
+  sort : Universe
+  ty   : TypeNormalForm ctx
+  tm   : NormalForm (relevance sort) ctx
 
 public export
-data Context : List Bool -> Type where
+data Context : List Relevance -> Type where
   Nil  : Context []
-  (:<) : Context ctx -> (def : Definition ctx) -> Context (isSet def.sort :: ctx)
+  (:<) : Context ctx -> (def : Definition ctx) -> Context (relevance def.sort :: ctx)
 
 %name Context ctx, ctx', ctx''
 
 -- Convenience Casts -----------------------------------------------------------
 
 public export
-Cast Sort (Constructor ctx) where
-  cast s = Sort s
+Cast Universe (Constructor ctx) where
+  cast s = Universe s
 
 public export
-Cast Sort (NormalForm True ctx) where
+Cast Universe (NormalForm Relevant ctx) where
   cast s = Cnstr $ cast s
 
 -- Pretty Print ----------------------------------------------------------------
@@ -106,7 +109,7 @@ Cast Sort (NormalForm True ctx) where
 prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
 prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
-prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d (Universe s) = prettyPrec d s
 prettyPrecCnstr d (Pi s s' var a b) =
   let lhs = case var of
               "" => align (prettyPrec App a)
@@ -208,7 +211,7 @@ Pretty (NormalForm b ctx) where
 rename : NormalForm ~|> Hom Elem NormalForm
 
 renameCnstr : Constructor ~|> Hom Elem Constructor
-renameCnstr (Sort s) f = Sort s
+renameCnstr (Universe s) f = Universe s
 renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
 renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
 renameCnstr (Sigma s s' var a b) f =
@@ -240,18 +243,18 @@ rename (Cnstr t) f = Cnstr $ renameCnstr t f
 rename Irrel f = Irrel
 
 export
-Unsorted.Rename Bool Constructor where
+Unsorted.Rename Relevance Constructor where
   rename = renameCnstr
 
 export
-Unsorted.Rename Bool Neutral where
+Unsorted.Rename Relevance Neutral where
   rename = renameNtrl
   
 export
-Sorted.Rename Bool NormalForm where
+Sorted.Rename Relevance NormalForm where
   rename = NormalForm.rename
 
 export
-PointedRename Bool (\b => (String, (s : Sort ** isSet s = b))) NormalForm where
-  point {s = False} _ _ = Irrel
-  point {s = True} (var, (s ** prf)) i = Ntrl (Var var s (eqToSo prf) i)
+PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where
+  point {s = Irrelevant} _ _ = Irrel
+  point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i)
-- 
cgit v1.2.3