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/Parser.idr | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

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

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 758b019..f92a0e2 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -4,7 +4,7 @@ import Data.String
 import Data.Vect
 
 import Obs.Logging
-import Obs.Sort
+import Obs.Universe
 import Obs.Syntax
 
 import System
@@ -299,13 +299,13 @@ parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* m
 var : Grammar state ObsToken True (WithBounds Syntax)
 var = map (map Var) ident
 
-noArgSort : Grammar state ObsToken True (WithBounds Sort)
-noArgSort = bounds $
+noArgUniverse : Grammar state ObsToken True (WithBounds Universe)
+noArgUniverse = bounds $
   map (const Prop) (match OTProp <* commit) <|>
   map (const (Set 0)) (match OTSet <* commit)
 
-sort : Grammar state ObsToken True (WithBounds Sort)
-sort = bounds $
+universe : Grammar state ObsToken True (WithBounds Universe)
+universe = bounds $
   map (const Prop) (match OTProp <* commit) <|>
   map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
 
@@ -326,7 +326,7 @@ lambda p =
   [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
 
 partial
-noSortsTerm : Grammar state ObsToken True (WithBounds Syntax)
+noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax)
 partial
 term : Grammar state ObsToken True (WithBounds Syntax)
 partial
@@ -340,17 +340,17 @@ equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
 exp : Grammar state ObsToken True (WithBounds Syntax)
 
-noSortsTerm =
+noUniversesTerm =
   parens exp <|>
   var <|>
   bounds (map (uncurry Pair) (pair exp)) <|>
   bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
 
-term = noSortsTerm <|> map (map Sort) noArgSort
+term = noUniversesTerm <|> map (map Universe) noArgUniverse
 
 head =
-  noSortsTerm <|>
-  map (map Sort) sort <|>
+  noUniversesTerm <|>
+  map (map Universe) universe <|>
   bounds
     (choiceMap
       (\(hd, (n ** f)) => match hd *> commit *>
-- 
cgit v1.2.3