diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-02 15:43:24 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-02 15:43:24 +0000 |
| commit | 74f0dc953839179aae071dda1ddb924295bc6061 (patch) | |
| tree | 6a4b29383502ec1ebbe12d5e46f5658d382859d2 /src/Obs/Parser.idr | |
| parent | 7e184c20d545afb55f6e962b8bfea882b23699fa (diff) | |
Add more program structure to type universes.
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 20 |
1 files changed, 10 insertions, 10 deletions
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 *> |