Merge pull request #144 from idris-lang/coverage

%default covering

CHANGELOG.md

@@ -8,6 +8,9 @@ or build from the generated Scheme, using `make bootstrap`.
 Language changes:
 
 * `total`, `covering` and `partial` flags on functions now have an effect.
+* `%default <totality status>` has been implemented. By default, functions must
+  be at least `covering`
+  + That is, `%default covering` is the default status.
 * Fields of records can be accessed (and updated) using the dot syntax,
   such as `r.field1.field2` or `record { field1.field2 = 42 }`.
   For details, see https://idris2.readthedocs.io/en/latest/reference/records.html

docs/source/typedd/typedd.rst

@@ -77,6 +77,9 @@ confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
 In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
 ``stringToNatOrZ``
 
+In ``ReadNum.idr``, since functions must now be ``covering`` by default, add
+a ``partial`` annotation to ``readNumber_v2``.
+
 Chapter 6
 ---------
 
@@ -137,6 +140,9 @@ longer part of the prelude, so add ``import Decidable.Equality``.
 
 In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
 
+In ``Void.idr``, since functions must now be ``covering`` by default, add
+a ``partial`` annotation to ``nohead`` and its helper function ``getHead``.
+
 Chapter 9
 ---------
 
@@ -306,6 +312,8 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also
 since export rules are per-namespace now, rather than per-file, you need to
 export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
 
+In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
+
 Chapter 12
 ----------
 

docs/source/updates/updates.rst

@@ -428,8 +428,11 @@ used with care. Too many hints can lead to a large search space!
 Totality and Coverage
 ---------------------
 
-``%default covering`` is now the default status [Actually still TODO, but
-planned soon!]
+``%default covering`` is now the default status, so all functions must cover
+all their inputs unless stated otherwise with a ``partial`` annotation, or
+switching to ``%default partial`` (which is not recommended - use a ``partial``
+annotation instead to have the smallest possible place where functions are
+partial).
 
 Build artefacts
 ---------------

libs/base/Data/List.idr

@@ -159,7 +159,7 @@ split : (a -> Bool) -> List a -> List (List a)
 split p xs =
   case break p xs of
     (chunk, [])          => [chunk]
-    (chunk, (c :: rest)) => chunk :: split p rest
+    (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
 
 public export
 splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

libs/base/Data/Nat.idr

@@ -170,7 +170,7 @@ export
 SIsNotZ : (S x = Z) -> Void
 SIsNotZ Refl impossible
 
-export
+export partial
 modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
 modNatNZ left Z         p = void (p Refl)
 modNatNZ left (S right) _ = mod' left left right
@@ -183,11 +183,11 @@ modNatNZ left (S right) _ = mod' left left right
       else
         mod' left (minus centre (S right)) right
 
-export
+export partial
 modNat : Nat -> Nat -> Nat
 modNat left (S right) = modNatNZ left (S right) SIsNotZ
 
-export
+export partial
 divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
 divNatNZ left Z         p = void (p Refl)
 divNatNZ left (S right) _ = div' left left right
@@ -200,17 +200,17 @@ divNatNZ left (S right) _ = div' left left right
       else
         S (div' left (minus centre (S right)) right)
 
-export
+export partial
 divNat : Nat -> Nat -> Nat
 divNat left (S right) = divNatNZ left (S right) SIsNotZ
 
-export
+export partial
 divCeilNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
 divCeilNZ x y p = case (modNatNZ x y p) of
   Z   => divNatNZ x y p
   S _ => S (divNatNZ x y p)
 
-export
+export partial
 divCeil : Nat -> Nat -> Nat
 divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
 
@@ -225,7 +225,7 @@ gcd a Z     = a
 gcd Z b     = b
 gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNotZ)
 
-export
+export partial
 lcm : Nat -> Nat -> Nat
 lcm _ Z     = Z
 lcm Z _     = Z

libs/base/Data/Strings.idr

@@ -167,11 +167,11 @@ export
 toLower : String -> String
 toLower str = pack (map toLower (unpack str))
 
-export
+export partial
 strIndex : String -> Int -> Char
 strIndex = prim__strIndex
 
-export
+export partial
 strTail : String -> String
 strTail = prim__strTail
 

libs/contrib/Language/JSON/Data.idr

@@ -38,7 +38,8 @@ intToHexString n =
     13 => "D"
     14 => "E"
     15 => "F"
-    other => intToHexString (shiftR n 4) ++ intToHexString (mod n 16)
+    other => assert_total $
+               intToHexString (shiftR n 4) ++ intToHexString (mod n 16)
 
 private
 showChar : Char -> String

libs/prelude/Builtin.idr

@@ -6,6 +6,9 @@ module Builtin
 
 ||| Assert to the totality checker that the given expression will always
 ||| terminate.
+||| Note: assert_total can reduce at compile time, if required for unification,
+||| which might mean that it's no longer guarded a subexpression. Therefore,
+||| it is best to use it around the smallest possible subexpression.
 %inline
 public export
 assert_total : {0 a : _} -> a -> a

libs/prelude/Prelude.idr

@@ -353,14 +353,18 @@ interface Num ty => Abs ty where
 
 public export
 interface Num ty => Fractional ty where
+  partial
   (/) : ty -> ty -> ty
+  partial
   recip : ty -> ty
 
   recip x = 1 / x
 
 public export
 interface Num ty => Integral ty where
+  partial
   div : ty -> ty -> ty
+  partial
   mod : ty -> ty -> ty
 
 ----- Instances for primitives
@@ -1117,13 +1121,13 @@ fastPack xs
 ||| ```
 public export
 unpack : String -> List Char
-unpack str = assert_total $ unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
+unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
   where
     unpack' : Int -> Int -> String -> List Char
     unpack' pos len str
         = if pos >= len
              then []
-             else (prim__strIndex str pos) :: unpack' (pos + 1) len str
+             else assert_total (prim__strIndex str pos) :: assert_total (unpack' (pos + 1) len str)
 
 public export
 Semigroup String where

src/Core/Directory.idr

@@ -13,7 +13,7 @@ import System.Directory
 import System.File
 import System.Info
 
-%default total
+%default covering
 
 fullPath : String -> List String
 fullPath fp = filter (/="") $ split (==sep) fp

src/Core/GetType.idr

@@ -59,6 +59,7 @@ mutual
                 NDelayed fc _ fty =>
                     do defs <- get Ctxt
                        pure $ glueBack defs env fty
+                _ => throw (GenericMsg fc "Not a delayed type")
   chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)
   chk env (TType fc) = pure (gType fc)
   chk env (Erased fc _) = pure (gErased fc)

src/Core/Options.idr

@@ -159,7 +159,7 @@ defaultSession = MkSessionOpts False False False Chez 0 False False
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True PartialOK 3 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 True
 
 export
 defaults : Options

src/Core/Termination.idr

@@ -110,6 +110,31 @@ Show Guardedness where
   show Guarded = "Guarded"
   show InDelay = "InDelay"
 
+-- Remove all force and delay annotations which are nothing to do with
+-- coinduction meaning that all Delays left guard coinductive calls.
+delazy : Defs -> Term vars -> Term vars
+delazy defs (TDelayed fc r tm)
+    = let tm' = delazy defs tm in
+          case r of
+               LInf => TDelayed fc r tm'
+               _ => tm'
+delazy defs (TDelay fc r ty tm)
+    = let ty' = delazy defs ty
+          tm' = delazy defs tm in
+          case r of
+               LInf => TDelay fc r ty' tm'
+               _ => tm'
+delazy defs (TForce fc r t)
+    = case r of
+           LInf => TForce fc r (delazy defs t)
+           _ => delazy defs t
+delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
+delazy defs (Bind fc x b sc)
+    = Bind fc x (map (delazy defs) b) (delazy defs sc)
+delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a)
+delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p)
+delazy defs tm = tm
+
 mutual
   findSC : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
@@ -346,32 +371,7 @@ mutual
                       pure ("Looking in case args " ++ show ps))
           logTermNF 10 "        =" env tm
           rhs <- normaliseOpts tcOnly defs env tm
-          findSC defs env g pats rhs
-
--- Remove all force and delay annotations which are nothing to do with
--- coinduction meaning that all Delays left guard coinductive calls.
-delazy : Defs -> Term vars -> Term vars
-delazy defs (TDelayed fc r tm)
-    = let tm' = delazy defs tm in
-          case r of
-               LInf => TDelayed fc r tm'
-               _ => tm'
-delazy defs (TDelay fc r ty tm)
-    = let ty' = delazy defs ty
-          tm' = delazy defs tm in
-          case r of
-               LInf => TDelay fc r ty' tm'
-               _ => tm'
-delazy defs (TForce fc r t)
-    = case r of
-           LInf => TForce fc r (delazy defs t)
-           _ => delazy defs t
-delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
-delazy defs (Bind fc x b sc)
-    = Bind fc x (map (delazy defs) b) (delazy defs sc)
-delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a)
-delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p)
-delazy defs tm = tm
+          findSC defs env g pats (delazy defs rhs)
 
 findCalls : {auto c : Ref Ctxt Defs} ->
             Defs -> (vars ** (Env Term vars, Term vars, Term vars)) ->

src/Idris/Elab/Interface.idr

@@ -245,9 +245,7 @@ updateIfaceSyn iname cn ps cs ms ds
     totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
               Core (Name, RigCount, TotalReq, (Bool, RawImp))
     totMeth (n, c, opts, t)
-        = do let treq = fromMaybe PartialOK (findSetTotal opts)
---         = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
--- TODO: Put the above back when totality checker is properly working
+        = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
              pure (n, c, treq, t)
 
 export
@@ -395,6 +393,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
         changeName : Name -> ImpClause -> ImpClause
         changeName dn (PatClause fc lhs rhs)
             = PatClause fc (changeNameTerm dn lhs) rhs
+        changeName dn (WithClause fc lhs wval cs)
+            = WithClause fc (changeNameTerm dn lhs) wval
+                         (map (changeName dn) cs)
         changeName dn (ImpossibleClause fc lhs)
             = ImpossibleClause fc (changeNameTerm dn lhs)
 

src/Parser/Source.idr

@@ -26,7 +26,7 @@ runParser : {e : _} ->
             Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
 runParser lit = runParserTo lit (const False)
 
-export
+export covering -- readFile might not terminate
 parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty)
 parseFile fn p
     = do Right str <- readFile fn

src/TTImp/Elab/Case.idr

@@ -203,6 +203,9 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
          cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top)
                                       [] casefnty Private None)
+         -- don't worry about totality of the case block; it'll be handled
+         -- by the totality of the parent function
+         setFlag fc (Resolved cidx) (SetTotal PartialOK)
          let caseRef : Term vars = Ref fc Func (Resolved cidx)
 
          -- If there's no duplication of the scrutinee in the block,

src/TTImp/Elab/Term.idr

@@ -117,6 +117,7 @@ checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
                    Explicit => genVarName "arg"
                    Implicit => genVarName "impArg"
                    AutoImplicit => genVarName "conArg"
+                   (DefImplicit _) => genVarName "defArg"
          checkPi rig elabinfo nest env fc r p n argTy retTy exp
 checkTerm rig elabinfo nest env (ILam fc r p (Just n) argTy scope) exp
     = checkLambda rig elabinfo nest env fc r p n argTy scope exp

src/TTImp/ProcessDecls.idr

@@ -65,9 +65,7 @@ checkTotalityOK n
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
               | Nothing => pure Nothing
---          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
--- TODO: Put the above back when totality checker is properly working
-         let treq = fromMaybe PartialOK (findSetTotal (flags gdef))
+         let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
          let tot = totality gdef
          let fc = location gdef
          log 3 $ show n ++ " must be: " ++ show treq