Merge pull request #195 from ohad/default-totality

Add support for `%default [total | covering | partial]` directive

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
@@ -1796,6 +1786,13 @@ setUnboundImplicits a
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
 
+export
+setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
+                TotalReq -> Core ()
+setDefaultTotalityOption tot
+    = do defs <- get Ctxt
+         put Ctxt (record { options->elabDirectives->totality = tot } defs)
+
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
                Core Bool
@@ -1810,6 +1807,13 @@ isUnboundImplicits
     = do defs <- get Ctxt
          pure (unboundImplicits (elabDirectives (options defs)))
 
+export
+getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
+                  Core TotalReq
+getDefaultTotalityOption
+    = do defs <- get Ctxt
+         pure (totality (elabDirectives (options defs)))
+
 export
 setPair : {auto c : Ref Ctxt Defs} ->
           FC -> (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->

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
@@ -84,6 +85,7 @@ record ElabDirectives where
   constructor MkElabDirectives
   lazyActive : Bool
   unboundImplicits : Bool
+  totality : TotalReq
 
 public export
 record Session where
@@ -142,7 +144,7 @@ defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez 0 False False
 
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True
+defaultElab = MkElabDirectives True True PartialOK
 
 export
 defaults : Options

src/Core/TT.idr

@@ -542,6 +542,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/Desugar.idr

@@ -566,7 +566,18 @@ mutual
                 List Name -> PDecl -> Core (List ImpDecl)
   desugarDecl ps (PClaim fc rig vis fnopts ty)
       = do opts <- traverse (desugarFnOpt ps) fnopts
+           opts <- if (isTotalityOption `any` opts)
+                   then pure opts
+                   else do PartialOK <- getDefaultTotalityOption
+                           | tot => pure (Totality tot :: opts)
+                           -- We assume PartialOK by default internally
+                           pure opts
            pure [IClaim fc rig vis opts !(desugarType ps ty)]
+        where
+          isTotalityOption : FnOpt -> Bool
+          isTotalityOption (Totality _) = True
+          isTotalityOption _            = False
+          
   desugarDecl ps (PDef fc clauses)
   -- The clauses won't necessarily all be from the same function, so split
   -- after desugaring, by function name, using collectDefs from RawImp
@@ -727,6 +738,8 @@ mutual
              StartExpr tm => pure [IPragma (\c, nest, env => throw (InternalError "%start not implemented"))] -- TODO!
              Overloadable n => pure [IPragma (\c, nest, env => setNameFlag fc n Overloadable)]
              Extension e => pure [IPragma (\c, nest, env => setExtension e)]
+             DefaultTotality tot => do setDefaultTotalityOption tot
+                                       pure []
 
   export
   desugar : {auto s : Ref Syn SyntaxInfo} ->

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"
@@ -983,6 +992,10 @@ directive fname indents
          e <- extension
          atEnd indents
          pure (Extension e)
+  <|> do exactIdent "default"
+         tot <- totalityOpt
+         atEnd indents
+         pure (DefaultTotality tot)
 
 fix : Rule Fixity
 fix
@@ -1048,16 +1061,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/Idris/Syntax.idr

@@ -161,6 +161,7 @@ mutual
        StartExpr : PTerm -> Directive
        Overloadable : Name -> Directive
        Extension : LangExt -> Directive
+       DefaultTotality : TotalReq -> Directive
 
   public export
   data PField : Type where

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,12 +46,8 @@ 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
-    = setFlag fc ndef (SetTotal Total)
-processFnOpt fc ndef Covering
-    = setFlag fc ndef (SetTotal CoveringOnly)
-processFnOpt fc ndef PartialOK
-    = setFlag fc ndef (SetTotal PartialOK)
+processFnOpt fc ndef (Totality tot)
+    = setFlag fc ndef (SetTotal tot)
 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"