Added simple productivity checker for coinductive definitions

Recursive calls must be an argument to a coinductive constructor

src/Core/Evaluate.hs

@@ -607,7 +607,7 @@ data Totality = Total [Int] -- well-founded arguments
     deriving Eq
 
 data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
-             | Mutual [Name]
+             | Mutual [Name] | NotProductive
     deriving (Show, Eq)
 
 instance Show Totality where
@@ -616,6 +616,7 @@ instance Show Totality where
     show (Partial Itself) = "possibly not total as it is not well founded"
     show (Partial NotCovering) = "not total as there are missing cases"
     show (Partial NotPositive) = "not strictly positive"
+    show (Partial NotProductive) = "not productive"
     show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
     show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++ 
                                  showSep " --> " (map show ns)

src/Idris/AbsSyntaxTree.hs

@@ -248,7 +248,7 @@ expl = Exp False Dynamic
 constraint = Constraint False Dynamic
 tacimpl = TacImp False Dynamic
 
-data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
+data FnOpt = Inlinable | TotalFn | Coinductive | AssertTotal | TCGen
            | CExport String    -- export, with a C name
            | Specialise [Name] -- specialise it, freeze these names
     deriving (Show, Eq)

src/Idris/Coverage.hs

@@ -262,17 +262,50 @@ checkPositive n (cn, ty)
 data LexOrder = LexXX | LexEQ | LexLT
     deriving (Show, Eq, Ord)
 
+calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
+calcProd i fc n pats 
+    | and (map prodRec pats) = return (Total [])
+    | otherwise = return (Partial NotProductive)
+   where
+     -- every application of n must be in an argument of a coinductive constructor
+
+     prodRec :: ([Name], Term, Term) -> Bool
+     prodRec (_, _, tm) = prod False tm 
+
+     prod ok ap@(App _ _)
+        | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
+        | (P _ f ty, args) <- unApply ap
+            = let co = cotype ty in
+                  if f == n then and (ok : map (prod co) args)
+                     else and (map (prod co) args)
+     prod ok (App f a) = prod False f && prod False a
+     prod ok (Bind _ (Let t v) sc) = prod False v && prod False v
+     prod ok (Bind _ b sc) = prod False sc
+     prod ok t = True 
+    
+     cotype ty 
+        | (P _ t _, _) <- unApply (getRetTy ty)
+            = case lookupCtxt Nothing t (idris_datatypes i) of
+                   [TI _ True] -> True
+                   _ -> False
+        | otherwise = False
+
 calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
 calcTotality path fc n pats 
-    = do orders <- mapM ctot pats 
-         let order = sortBy cmpOrd $ concat orders
-         let (errs, valid) = partitionEithers order
-         let lex = stripNoLT (stripXX valid)
-         case errs of
-            [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex) 
-                     logLvl 10 $ show pats
-                     checkDecreasing lex
-            (e : _) -> return e -- FIXME: should probably combine them
+    = do i <- get
+         let opts = case lookupCtxt Nothing n (idris_flags i) of
+                            [fs] -> fs
+                            _ -> []
+         if (Coinductive `elem` opts) then calcProd i fc n pats
+           else do orders <- mapM ctot pats 
+                   let order = sortBy cmpOrd $ concat orders
+                   let (errs, valid) = partitionEithers order
+                   let lex = stripNoLT (stripXX valid)
+                   case errs of
+                      [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex) 
+                               logLvl 10 $ show pats
+                               checkDecreasing lex
+                      (e : _) -> return e -- FIXME: should probably combine them
   where
     cmpOrd (Left _) (Left _) = EQ
     cmpOrd (Left _) (Right _) = LT

src/Idris/ElabDecls.hs

@@ -60,19 +60,20 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
          let nty = cty -- normalise ctxt [] cty
          -- if the return type is something coinductive, freeze the definition
          let nty' = normalise ctxt [] nty
+         let (t, _) = unApply (getRetTy nty')
+         let corec = case t of
+                        P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of
+                                        [TI _ True] -> True
+                                        _ -> False
+                        _ -> False
+         let opts' = if corec then (Coinductive : opts) else opts
          ds <- checkDef fc [(n, nty)]
          addIBC (IBCDef n)
          addDeferred ds
-         setFlags n opts
-         addIBC (IBCFlags n opts)
-         let (t, _) = unApply (getRetTy nty')
-         case t of
-            P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of
-                               [TI _ True] -> do setAccessibility n Frozen
-                                                 addIBC (IBCAccess n Frozen)
-                                                 iputStrLn $ "Co " ++ show n
-                               _ -> return ()
-            _ -> return ()
+         setFlags n opts'
+         addIBC (IBCFlags n opts')
+         when corec $ do setAccessibility n Frozen
+                         addIBC (IBCAccess n Frozen)
 
 elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()
 elabData info syn fc codata (PDatadecl n t_in dcons)

src/Idris/IBC.hs

@@ -649,6 +649,7 @@ instance Binary PReason where
                 NotPositive -> putWord8 3
                 Mutual x1 -> do putWord8 4
                                 put x1
+                NotProductive -> putWord8 5
         get
           = do i <- getWord8
                case i of
@@ -659,6 +660,7 @@ instance Binary PReason where
                    3 -> return NotPositive
                    4 -> do x1 <- get
                            return (Mutual x1)
+                   5 -> return NotProductive
                    _ -> error "Corrupted binary data for PReason"
 
 instance Binary Totality where
@@ -737,6 +739,7 @@ instance Binary FnOpt where
                 AssertTotal -> putWord8 3
                 Specialise x -> do putWord8 4
                                    put x
+                Coinductive -> putWord8 5
         get
           = do i <- getWord8
                case i of
@@ -746,6 +749,7 @@ instance Binary FnOpt where
                    3 -> return AssertTotal
                    4 -> do x <- get
                            return (Specialise x)
+                   5 -> return Coinductive
                    _ -> error "Corrupted binary data for FnOpt"
 
 instance Binary Fixity where

test/README

@@ -15,5 +15,6 @@ Tests:
 013: binding syntax
 014: resource DSL
 015: verified binary adder
+016: codata
 
 regxxx: various regression tests

test/test016/expected

@@ -0,0 +1 @@
+[10, 11, 12, 13, 14, 15, 16, 17, 18, 19]

test/test016/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test016.idr -o test016
+./test016
+rm -f test016 *.ibc

test/test016/test016.idr

@@ -0,0 +1,20 @@
+module main
+
+%default total
+
+codata Stream a = Nil | (::) a (Stream a)
+
+countFrom : Int -> Stream Int
+countFrom x = x :: countFrom (x + 1)
+
+take : Int -> Stream a -> List a
+take 0 _ = []
+take n (x :: xs) = x :: take (n - 1) xs
+take n [] = []
+
+-- foo : main.countFrom 4 = 4 :: main.countFrom 5
+-- foo = refl
+
+main : IO ()
+main = do print (take 10 (main.countFrom 10))
+