Add totality annotations.

The parser is unfortunately not classified as total.

9 files changed, 27 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 33c2460..bac6d04 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -9,6 +9,8 @@ import Obs.Term
 import System
 import Text.Bounded
 
+%default total
+
 public export
 Context : Nat -> Type
 Context n = List (String, Fin n)
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 2cf10e6..6142e77 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -12,11 +12,14 @@ import System
 import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
+%default total
+
 usage : IO ()
 usage = do
   () <- putStrLn "usage: obs <file>"
   exitFailure
 
+partial
 main : IO ()
 main = do
   [_, file] <- getArgs
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index c11c158..97a0d48 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -7,6 +7,8 @@ import Obs.Substitution
 
 import Text.PrettyPrint.Prettyprinter
 
+%default total
+
 -- Definition ------------------------------------------------------------------
 
 data Constructor : Nat -> Type
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
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index 281a053..d2c8c33 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -2,6 +2,8 @@ module Obs.Sort
 
 import Text.PrettyPrint.Prettyprinter
 
+%default total
+
 -- Definition ------------------------------------------------------------------
 
 public export
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 914e612..54df355 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -2,6 +2,8 @@ module Obs.Substitution
 
 import Data.Fin
 
+%default total
+
 public export
 interface Rename (x : Nat -> Type) where
   rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 9ec1d3d..71d070f 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -5,6 +5,8 @@ import Obs.Sort
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
+%default total
+
 -- Definition ------------------------------------------------------------------
 
 public export
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 3e2d4b7..d5213d2 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -6,6 +6,8 @@ import Obs.Sort
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
+%default total
+
 -- Definition ------------------------------------------------------------------
 
 public export
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 2a96a97..95ffc19 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -13,6 +13,8 @@ import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
+%default total
+
 -- Conversion ------------------------------------------------------------------
 
 -- invariant: all definitions fully expanded