Add totality annotations.

The parser is unfortunately not classified as total.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 2802690..278ff0f 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -11,6 +11,8 @@ import System.File
 import Text.Lexer
 import Text.Parser
 
+%default total
+
 Error : Type -> Type -> Type
 Error tok = Either (List1 (ParsingError tok))
 
@@ -120,18 +122,23 @@ sort = do
   sort <- prop <|> set
   pure (Sort sort.bounds sort.val)
 
+partial
 exp  : Grammar state ObsToken True Syntax
+partial
 term : Grammar state ObsToken True Syntax
 
 exp = term
 term = var <|> sort <|> parens exp
 
+partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
 decl = [| MkPair ident (match OTColon *> exp) |]
 
+partial
 def : Grammar state ObsToken True (WithBounds String, Syntax)
 def = [| MkPair ident (match OTEqual *> exp) |]
 
+partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
@@ -141,9 +148,11 @@ fullDef =
         then pure (MkDefinition {bounds = name.bounds, name = name.val, ty, tm})
         else fatalLoc name.bounds "name mismatch for declaration and definition")
 
+partial
 file : Grammar state ObsToken False (List Definition)
 file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef
 
+partial
 export
 parse : String -> Error ObsToken (List Definition)
 parse str = do
@@ -164,6 +173,7 @@ reportErrs (e :: errs) = do
   () <- printErr e
   reportErrs errs
 
+partial
 export
 parseFile : (fname : String) -> IO (List Definition)
 parseFile fname = do