Decouple totality annotations from IFnOpt using the existing TotalReq value

This requires moving `TotalReq` into `src/Core/TT.idr`.

src/Core/Context.idr

@@ -122,9 +122,6 @@ data Clause : Type where
      MkClause : (env : Env Term vars) ->
                 (lhs : Term vars) -> (rhs : Term vars) -> Clause
 
-public export
-data TotalReq = Total | CoveringOnly | PartialOK
-
 public export
 data DefFlag
     = Inline
@@ -142,13 +139,6 @@ data DefFlag
     | BlockedHint -- a hint, but blocked for the moment (so don't use)
     | Macro
 
-export
-Eq TotalReq where
-    (==) Total Total = True
-    (==) CoveringOnly CoveringOnly = True
-    (==) PartialOK PartialOK = True
-    (==) _ _ = False
-
 export
 Eq DefFlag where
     (==) Inline Inline = True

src/Core/Options.idr

@@ -2,6 +2,7 @@ module Core.Options
 
 import Core.Core
 import Core.Name
+import Core.TT
 import Utils.Binary
 
 import System.Info

src/Core/TT.idr

@@ -508,6 +508,16 @@ Ord Visibility where
   compare Public Private = GT
   compare Public Export = GT
 
+public export
+data TotalReq = Total | CoveringOnly | PartialOK
+
+export
+Eq TotalReq where
+    (==) Total Total = True
+    (==) CoveringOnly CoveringOnly = True
+    (==) PartialOK PartialOK = True
+    (==) _ _ = False
+
 public export
 data PartialReason
        = NotStrictlyPositive

src/Idris/Parser.idr

@@ -921,6 +921,15 @@ extension
     = do exactIdent "Borrowing"
          pure Borrowing
 
+totalityOpt : Rule TotalReq
+totalityOpt
+    = do keyword "partial"
+         pure PartialOK
+  <|> do keyword "total"
+         pure Total
+  <|> do keyword "covering"
+         pure CoveringOnly
+
 directive : FileName -> IndentInfo -> Rule Directive
 directive fname indents
     = do exactIdent "hide"
@@ -1048,16 +1057,11 @@ usingDecls fname indents
          ds <- assert_total (nonEmptyBlock (topDecl fname))
          end <- location
          pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
-
+         
 fnOpt : Rule PFnOpt
-fnOpt
-    = do keyword "partial"
-         pure $ IFnOpt PartialOK
-  <|> do keyword "total"
-         pure $ IFnOpt Total
-  <|> do keyword "covering"
-         pure $ IFnOpt Covering
-
+fnOpt = do x <- totalityOpt          
+           pure $ IFnOpt (Totality x)
+           
 fnDirectOpt : FileName -> Rule PFnOpt
 fnDirectOpt fname
     = do exactIdent "hint"

src/TTImp/Parser.idr

@@ -65,14 +65,18 @@ visibility
     = visOption
   <|> pure Private
 
-fnOpt : Rule FnOpt
-fnOpt
+totalityOpt : Rule TotalReq
+totalityOpt
     = do keyword "partial"
          pure PartialOK
   <|> do keyword "total"
          pure Total
   <|> do keyword "covering"
-         pure Covering
+         pure CoveringOnly
+
+fnOpt : Rule FnOpt
+fnOpt = do x <- totalityOpt          
+           pure $ Totality x
 
 fnDirectOpt : Rule FnOpt
 fnDirectOpt

src/TTImp/ProcessType.idr

@@ -46,11 +46,11 @@ processFnOpt fc ndef (ForeignFn _)
     = setFlag fc ndef Inline -- if externally defined, inline when compiling
 processFnOpt fc ndef Invertible
     = setFlag fc ndef Invertible
-processFnOpt fc ndef Total
+processFnOpt fc ndef (Totality Total)
     = setFlag fc ndef (SetTotal Total)
-processFnOpt fc ndef Covering
+processFnOpt fc ndef (Totality Covering)
     = setFlag fc ndef (SetTotal CoveringOnly)
-processFnOpt fc ndef PartialOK
+processFnOpt fc ndef (Totality PartialOK)
     = setFlag fc ndef (SetTotal PartialOK)
 processFnOpt fc ndef Macro
     = setFlag fc ndef Macro

src/TTImp/TTImp.idr

@@ -187,9 +187,7 @@ mutual
        ForeignFn : List RawImp -> FnOpt
        -- assume safe to cancel arguments in unification
        Invertible : FnOpt
-       Total : FnOpt
-       Covering : FnOpt
-       PartialOK : FnOpt
+       Totality : TotalReq -> FnOpt
        Macro : FnOpt
 
   export
@@ -200,9 +198,9 @@ mutual
     show ExternFn = "%extern"
     show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs)
     show Invertible = "%invertible"
-    show Total = "total"
-    show Covering = "covering"
-    show PartialOK = "partial"
+    show (Totality Total) = "total"
+    show (Totality CoveringOnly) = "covering"
+    show (Totality PartialOK) = "partial"
     show Macro = "%macro"
 
   export
@@ -213,9 +211,7 @@ mutual
     ExternFn == ExternFn = True
     (ForeignFn xs) == (ForeignFn ys) = True -- xs == ys
     Invertible == Invertible = True
-    Total == Total = True
-    Covering == Covering = True
-    PartialOK == PartialOK = True
+    (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs
     Macro == Macro = True
     _ == _ = False
 
@@ -858,9 +854,9 @@ mutual
     toBuf b ExternFn = tag 3
     toBuf b (ForeignFn cs) = do tag 4; toBuf b cs
     toBuf b Invertible = tag 5
-    toBuf b Total = tag 6
-    toBuf b Covering = tag 7
-    toBuf b PartialOK = tag 8
+    toBuf b (Totality Total) = tag 6
+    toBuf b (Totality CoveringOnly) = tag 7
+    toBuf b (Totality PartialOK) = tag 8
     toBuf b Macro = tag 9
 
     fromBuf b
@@ -871,9 +867,9 @@ mutual
                3 => pure ExternFn
                4 => do cs <- fromBuf b; pure (ForeignFn cs)
                5 => pure Invertible
-               6 => pure Total
-               7 => pure Covering
-               8 => pure PartialOK
+               6 => pure (Totality Total)
+               7 => pure (Totality CoveringOnly)
+               8 => pure (Totality PartialOK)
                9 => pure Macro
                _ => corrupt "FnOpt"