git.iko.soy/Idris-dev
on master help sign in
Added 'total' keyword and positivity check
de6bb41Edwin Brady
src/Core/CoreParser.hs+1−1
compare with master
unifiedsplit
@@ -21,7 +21,7 @@ idrisDef = haskellDef {
21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
22 reservedNames = ["let", "in", "data", "record", "Set",
22 reservedNames = ["let", "in", "data", "record", "Set",
23 "do", "dsl", "import", "impossible",
23 "do", "dsl", "import", "impossible",
24− "case", "of",
24+ "case", "of", "total",
25 "infix", "infixl", "infixr", "prefix",
25 "infix", "infixl", "infixr", "prefix",
26 "where", "with", "forall", "syntax", "proof",
26 "where", "with", "forall", "syntax", "proof",
27 "using", "params", "namespace", "class", "instance",
27 "using", "params", "namespace", "class", "instance",
src/Core/Evaluate.hs+8−1
@@ -473,11 +473,18 @@ data Accessibility = Public | Frozen | Hidden
473 deriving (Show, Eq)
473 deriving (Show, Eq)
474
474
475data Totality = Total | Partial PReason
475data Totality = Total | Partial PReason
476− deriving (Show, Eq)
476+ deriving Eq
477
477
478data PReason = Other [Name] | Itself | NotCovering | NotPositive
478data PReason = Other [Name] | Itself | NotCovering | NotPositive
479 deriving (Show, Eq)
479 deriving (Show, Eq)
480
480
481+instance Show Totality where
482+ show Total = "Total"
483+ show (Partial Itself) = "not total as it is not well founded"
484+ show (Partial NotCovering) = "not total as there are missing cases"
485+ show (Partial NotPositive) = "not strictly positive"
486+ show (Partial (Other ns)) = "not total due to: " ++ showSep ", " (map show ns)
487+
481{-!
488{-!
482deriving instance Binary Accessibility
489deriving instance Binary Accessibility
483!-}
490!-}
src/Idris/AbsSyntax.hs+17−9
@@ -44,6 +44,7 @@ data IState = IState { tt_ctxt :: Context,
44 idris_optimisation :: Ctxt OptInfo,
44 idris_optimisation :: Ctxt OptInfo,
45 idris_datatypes :: Ctxt TypeInfo,
45 idris_datatypes :: Ctxt TypeInfo,
46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported
46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported
47+ idris_flags :: Ctxt [FnOpt],
47 idris_log :: String,
48 idris_log :: String,
48 idris_options :: IOption,
49 idris_options :: IOption,
49 idris_name :: Int,
50 idris_name :: Int,
@@ -82,11 +83,12 @@ data IBCWrite = IBCFix FixDecl
82 | IBCHeader String
83 | IBCHeader String
83 | IBCAccess Name Accessibility
84 | IBCAccess Name Accessibility
84 | IBCTotal Name Totality
85 | IBCTotal Name Totality
86+ | IBCFlags Name [FnOpt]
85 | IBCDef Name -- i.e. main context
87 | IBCDef Name -- i.e. main context
86 deriving Show
88 deriving Show
87
89
88idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
90idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
89− emptyContext emptyContext emptyContext emptyContext
91+ emptyContext emptyContext emptyContext emptyContext emptyContext
90 "" defaultOpts 6 [] [] [] [] [] [] [] []
92 "" defaultOpts 6 [] [] [] [] [] [] [] []
91 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
93 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
92
94
@@ -112,6 +114,9 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
112addHdr :: String -> Idris ()
114addHdr :: String -> Idris ()
113addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
115addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
114
116
117+setFlags :: Name -> [FnOpt] -> Idris ()
118+setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
119+
115setAccessibility :: Name -> Accessibility -> Idris ()
120setAccessibility :: Name -> Accessibility -> Idris ()
116setAccessibility n a
121setAccessibility n a
117 = do i <- get
122 = do i <- get
@@ -356,8 +361,11 @@ impl = Imp False Dynamic
356expl = Exp False Dynamic
361expl = Exp False Dynamic
357constraint = Constraint False Static
362constraint = Constraint False Static
358
363
359−data FnOpt = Inlinable | Abstract | Private | TCGen
364+data FnOpt = Inlinable | TotalFn | TCGen
360 deriving (Show, Eq)
365 deriving (Show, Eq)
366+{-!
367+deriving instance Binary FnOpt
368+!-}
361
369
362type FnOpts = [FnOpt]
370type FnOpts = [FnOpt]
363
371
@@ -365,7 +373,7 @@ inlinable :: FnOpts -> Bool
365inlinable = elem Inlinable
373inlinable = elem Inlinable
366
374
367data PDecl' t = PFix FC Fixity [String] -- fixity declaration
375data PDecl' t = PFix FC Fixity [String] -- fixity declaration
368− | PTy SyntaxInfo FC Name t -- type declaration
376+ | PTy SyntaxInfo FC FnOpts Name t -- type declaration
369 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
377 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
370 | PData SyntaxInfo FC (PData' t) -- data declaration
378 | PData SyntaxInfo FC (PData' t) -- data declaration
371 | PParams FC [(Name, t)] [PDecl' t] -- params block
379 | PParams FC [(Name, t)] [PDecl' t] -- params block
@@ -408,7 +416,7 @@ type PClause = PClause' PTerm
408
416
409declared :: PDecl -> [Name]
417declared :: PDecl -> [Name]
410declared (PFix _ _ _) = []
418declared (PFix _ _ _) = []
411−declared (PTy _ _ n t) = [n]
419+declared (PTy _ _ _ n t) = [n]
412declared (PClauses _ _ n _) = [] -- not a declaration
420declared (PClauses _ _ n _) = [] -- not a declaration
413declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
421declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
414 where fstt (a, _, _) = a
422 where fstt (a, _, _) = a
@@ -635,7 +643,7 @@ instance Show PTerm where
635
643
636instance Show PDecl where
644instance Show PDecl where
637 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
645 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
638− show (PTy _ _ n ty) = show n ++ " : " ++ show ty
646+ show (PTy _ _ _ n ty) = show n ++ " : " ++ show ty
639 show (PClauses _ _ n c) = showSep "\n" (map show c)
647 show (PClauses _ _ n c) = showSep "\n" (map show c)
640 show (PData _ _ d) = show d
648 show (PData _ _ d) = show d
641
649
@@ -926,10 +934,10 @@ expandParams dec ps ns tm = en tm
926
934
927expandParamsD :: IState ->
935expandParamsD :: IState ->
928 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
936 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
929−expandParamsD ist dec ps ns (PTy syn fc n ty)
937+expandParamsD ist dec ps ns (PTy syn fc o n ty)
930 = if n `elem` ns
938 = if n `elem` ns
931− then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
939+ then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
932− else PTy syn fc n (expandParams dec ps ns ty)
940+ else PTy syn fc o n (expandParams dec ps ns ty)
933expandParamsD ist dec ps ns (PClauses fc opts n cs)
941expandParamsD ist dec ps ns (PClauses fc opts n cs)
934 = let n' = if n `elem` ns then dec n else n in
942 = let n' = if n `elem` ns then dec n else n in
935 PClauses fc opts n' (map expandParamsC cs)
943 PClauses fc opts n' (map expandParamsC cs)
@@ -1208,7 +1216,7 @@ dumpDecls [] = ""
1208dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1216dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1209
1217
1210dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1218dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1211−dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1219+dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1212dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1220dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1213dumpDecl (PData _ _ d) = showDImp True d
1221dumpDecl (PData _ _ d) = showDImp True d
1214dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1222dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
src/Idris/Coverage.hs+17−1
@@ -116,7 +116,8 @@ wellFounded i n sc = case wff [] sc of
116 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]
116 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]
117 wff ns (Case n as) = do is <- mapM (wffC ns) as
117 wff ns (Case n as) = do is <- mapM (wffC ns) as
118 return $ concat is
118 return $ concat is
119− where wffC ns (ConCase _ i ns' sc) = wff (ns ++ ns') sc
119+ where wffC ns (ConCase n i ns' sc) = do checkOK n
120+ wff (ns ++ ns') sc
120 wffC ns (ConstCase _ sc) = wff ns sc
121 wffC ns (ConstCase _ sc) = wff ns sc
121 wffC ns (DefaultCase sc) = wff ns sc
122 wffC ns (DefaultCase sc) = wff ns sc
122 wff ns (STerm t) = argPos ns t
123 wff ns (STerm t) = argPos ns t
@@ -148,4 +149,19 @@ wellFounded i n sc = case wff [] sc of
148 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs
149 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs
149 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs
150 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs
150
151
152+checkPositive :: Name -> (Name, Type) -> Idris ()
153+checkPositive n (cn, ty)
154+ = do let p = cp ty
155+ i <- getIState
156+ let ctxt' = setTotal cn (if p then Total else Partial NotPositive)
157+ (tt_ctxt i)
158+ putIState (i { tt_ctxt = ctxt' })
159+ where
160+ cp (Bind n (Pi aty) sc) = posArg aty && cp sc
161+ cp t = True
162+
163+ posArg (Bind _ (Pi nty) sc)
164+ | (P _ n' _, args) <- unApply nty
165+ = n /= n' && posArg sc
166+ posArg t = True
151
167
src/Idris/ElabDecls.hs+42−17
@@ -35,8 +35,8 @@ checkDef fc ns = do ctxt <- getContext
35 mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t
35 mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t
36 return (n, t')) ns
36 return (n, t')) ns
37
37
38−elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()
38+elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()
39−elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in
39+elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
40 n = liftname info n_in in -}
40 n = liftname info n_in in -}
41 do checkUndefined fc n
41 do checkUndefined fc n
42 ctxt <- getContext
42 ctxt <- getContext
@@ -52,6 +52,8 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in
52 ds <- checkDef fc ((n, nty):defer)
52 ds <- checkDef fc ((n, nty):defer)
53 addIBC (IBCDef n)
53 addIBC (IBCDef n)
54 addDeferred ds
54 addDeferred ds
55+ setFlags n opts
56+ addIBC (IBCFlags n opts)
55 mapM_ (elabCaseBlock info) is
57 mapM_ (elabCaseBlock info) is
56
58
57elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
59elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
@@ -79,6 +81,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
79 addIBC (IBCData n)
81 addIBC (IBCData n)
80 collapseCons n cons
82 collapseCons n cons
81 updateContext (addDatatype (Data n ttag cty cons))
83 updateContext (addDatatype (Data n ttag cty cons))
84+ mapM_ (checkPositive n) cons
82
85
83elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
86elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
84 PTerm -> Name -> PTerm -> Idris ()
87 PTerm -> Name -> PTerm -> Idris ()
@@ -142,6 +145,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
142 return Total
145 return Total
143 else do logLvl 2 $ show n ++ " does not cover all cases"
146 else do logLvl 2 $ show n ++ " does not cover all cases"
144 return $ Partial NotCovering
147 return $ Partial NotCovering
148+ case lookupCtxt (namespace info) n (idris_flags ist) of
149+ [fs] -> if TotalFn `elem` fs
150+ then case tot of
151+ Total -> return ()
152+ t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
153+ else return ()
154+ _ -> return ()
145 case tree of
155 case tree of
146 CaseDef _ _ [] -> return ()
156 CaseDef _ _ [] -> return ()
147 CaseDef _ _ xs -> mapM_ (\x ->
157 CaseDef _ _ xs -> mapM_ (\x ->
@@ -199,8 +209,12 @@ elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])
199 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of
209 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of
200 OK ((lhs', _, _), _) ->
210 OK ((lhs', _, _), _) ->
201 do let lhs_tm = orderPats (getInferTerm lhs')
211 do let lhs_tm = orderPats (getInferTerm lhs')
202− checkInferred fc (delab' i lhs_tm True) lhs
212+-- checkInferred fc (delab' i lhs_tm True) lhs
213+ b <- inferredDiff fc (delab' i lhs_tm True) lhs
214+ if b
215+ then return ()
203− fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case"
216+ else fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++
217+ " is a possible case"
204 ++ "\n" ++ showImp True lhs
218 ++ "\n" ++ showImp True lhs
205 Error _ -> return ()
219 Error _ -> return ()
206 return Nothing
220 return Nothing
@@ -419,10 +433,10 @@ elabClass info syn fc constraints tn ps ds
419 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
433 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
420 conbind [] x = x
434 conbind [] x = x
421
435
422− tdecl (PTy syn _ n t) = do t' <- implicit syn n t
436+ tdecl (PTy syn _ _ n t) = do t' <- implicit syn n t
423− return ( (n, (toExp (map fst ps) Exp t')),
437+ return ( (n, (toExp (map fst ps) Exp t')),
424− (n, (toExp (map fst ps) Imp t')),
438+ (n, (toExp (map fst ps) Imp t')),
425− (n, (syn, t) ) )
439+ (n, (syn, t) ) )
426 tdecl _ = fail "Not allowed in a class declaration"
440 tdecl _ = fail "Not allowed in a class declaration"
427
441
428 -- Create default definitions
442 -- Create default definitions
@@ -430,7 +444,7 @@ elabClass info syn fc constraints tn ps ds
430 case lookup n mtys of
444 case lookup n mtys of
431 Just (syn, ty) -> do let ty' = insertConstraint c ty
445 Just (syn, ty) -> do let ty' = insertConstraint c ty
432 let ds = map (decorateid defaultdec)
446 let ds = map (decorateid defaultdec)
433− [PTy syn fc n ty',
447+ [PTy syn fc [] n ty',
434 PClauses fc (TCGen:opts) n cs]
448 PClauses fc (TCGen:opts) n cs]
435 iLOG (show ds)
449 iLOG (show ds)
436 return (n, (defaultdec n, ds))
450 return (n, (defaultdec n, ds))
@@ -440,7 +454,7 @@ elabClass info syn fc constraints tn ps ds
440 defaultdec (UN n) = UN ("default#" ++ n)
454 defaultdec (UN n) = UN ("default#" ++ n)
441 defaultdec (NS n ns) = NS (defaultdec n) ns
455 defaultdec (NS n ns) = NS (defaultdec n) ns
442
456
443− tydecl (PTy _ _ _ _) = True
457+ tydecl (PTy _ _ _ _ _) = True
444 tydecl _ = False
458 tydecl _ = False
445 clause (PClauses _ _ _ _) = True
459 clause (PClauses _ _ _ _) = True
446 clause _ = False
460 clause _ = False
@@ -454,7 +468,7 @@ elabClass info syn fc constraints tn ps ds
454 let ty = PPi constraint (MN 0 "pc") c con
468 let ty = PPi constraint (MN 0 "pc") c con
455 iLOG (showImp True ty)
469 iLOG (showImp True ty)
456 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
470 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
457− return [PTy syn fc cfn ty,
471+ return [PTy syn fc [] cfn ty,
458 PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]
472 PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]
459
473
460 tfun cn c syn all (m, ty)
474 tfun cn c syn all (m, ty)
@@ -468,7 +482,7 @@ elabClass info syn fc constraints tn ps ds
468 iLOG (showImp True ty)
482 iLOG (showImp True ty)
469 iLOG (show (m, ty', capp, margs))
483 iLOG (show (m, ty', capp, margs))
470 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
484 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
471− return [PTy syn fc m ty',
485+ return [PTy syn fc [] m ty',
472 PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]
486 PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]
473
487
474 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc
488 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc
@@ -509,7 +523,7 @@ elabInstance info syn fc cs n ps t ds
509 [c] -> return c
523 [c] -> return c
510 _ -> fail $ show n ++ " is not a type class"
524 _ -> fail $ show n ++ " is not a type class"
511 let iname = UN ('@':show n ++ "$" ++ show ps)
525 let iname = UN ('@':show n ++ "$" ++ show ps)
512− elabType info syn fc iname t
526+ elabType info syn fc [] iname t
513 let ips = zip (class_params ci) ps
527 let ips = zip (class_params ci) ps
514 let ns = case n of
528 let ns = case n of
515 NS n ns' -> ns'
529 NS n ns' -> ns'
@@ -549,7 +563,7 @@ elabInstance info syn fc cs n ps t ds
549 decorate ns (UN n) = NS (UN ('!':n)) ns
563 decorate ns (UN n) = NS (UN ('!':n)) ns
550 decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns
564 decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns
551
565
552− mkTyDecl (n, t, _) = PTy syn fc n t
566+ mkTyDecl (n, t, _) = PTy syn fc [] n t
553
567
554 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
568 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
555 conbind [] x = x
569 conbind [] x = x
@@ -577,7 +591,7 @@ elabInstance info syn fc cs n ps t ds
577 clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'
591 clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'
578 clauseFor m ns _ = False
592 clauseFor m ns _ = False
579
593
580−decorateid decorate (PTy s f n t) = PTy s f (decorate n) t
594+decorateid decorate (PTy s f o n t) = PTy s f o (decorate n) t
581decorateid decorate (PClauses f o n cs)
595decorateid decorate (PClauses f o n cs)
582 = PClauses f o (decorate n) (map dc cs)
596 = PClauses f o (decorate n) (map dc cs)
583 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds
597 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds
@@ -612,8 +626,8 @@ elabDecl info d = idrisCatch (elabDecl' info d)
612
626
613elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate
627elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate
614elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate
628elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate
615−elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n
629+elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n
616− elabType info s f n ty
630+ elabType info s f o n ty
617elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)
631elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)
618 elabData info s f d
632 elabData info s f d
619elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n
633elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n
@@ -667,3 +681,14 @@ checkInferred fc inf user =
667 ++ show x ++ " and " ++ show y)
681 ++ show x ++ " and " ++ show y)
668-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)
682-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)
669
683
684+-- Return whether inferred term is different from given term
685+-- (as above, but return a Bool)
686+
687+inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
688+inferredDiff fc inf user =
689+ do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++
690+ showImp True user
691+ tclift $ case matchClause' True user inf of
692+ Right vs -> return False
693+ Left (x, y) -> return True
694+
src/Idris/IBC.hs+25−5
@@ -13,7 +13,6 @@ import Idris.Error
13import Data.Binary
13import Data.Binary
14import Data.List
14import Data.List
15import Data.ByteString.Lazy as B hiding (length, elem)
15import Data.ByteString.Lazy as B hiding (length, elem)
16−-- import Data.DeriveTH
17import Control.Monad
16import Control.Monad
18import Control.Monad.State hiding (get, put)
17import Control.Monad.State hiding (get, put)
19import System.FilePath
18import System.FilePath
@@ -22,7 +21,7 @@ import System.Directory
22import Paths_idris
21import Paths_idris
23
22
24ibcVersion :: Word8
23ibcVersion :: Word8
25−ibcVersion = 14
24+ibcVersion = 15
26
25
27data IBCFile = IBCFile { ver :: Word8,
26data IBCFile = IBCFile { ver :: Word8,
28 sourcefile :: FilePath,
27 sourcefile :: FilePath,
@@ -41,13 +40,14 @@ data IBCFile = IBCFile { ver :: Word8,
41 ibc_hdrs :: [String],
40 ibc_hdrs :: [String],
42 ibc_access :: [(Name, Accessibility)],
41 ibc_access :: [(Name, Accessibility)],
43 ibc_total :: [(Name, Totality)],
42 ibc_total :: [(Name, Totality)],
43+ ibc_flags :: [(Name, [FnOpt])],
44 ibc_defs :: [(Name, Def)] }
44 ibc_defs :: [(Name, Def)] }
45{-!
45{-!
46deriving instance Binary IBCFile
46deriving instance Binary IBCFile
47!-}
47!-}
48
48
49initIBC :: IBCFile
49initIBC :: IBCFile
50−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
50+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
51
51
52loadIBC :: FilePath -> Idris ()
52loadIBC :: FilePath -> Idris ()
53loadIBC fp = do iLOG $ "Loading ibc " ++ fp
53loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -107,6 +107,7 @@ ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of
107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }
107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }
108 _ -> fail "IBC write failed"
108 _ -> fail "IBC write failed"
109ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
109ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
110+ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
110ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
111ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
111
112
112process :: IBCFile -> FilePath -> Idris ()
113process :: IBCFile -> FilePath -> Idris ()
@@ -234,6 +235,9 @@ pAccess ds = mapM_ (\ (n, a) ->
234 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))
235 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))
235 ds
236 ds
236
237
238+pFlags :: [(Name, [FnOpt])] -> Idris ()
239+pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds
240+
237pTotal :: [(Name, Totality)] -> Idris ()
241pTotal :: [(Name, Totality)] -> Idris ()
238pTotal ds = mapM_ (\ (n, a) ->
242pTotal ds = mapM_ (\ (n, a) ->
239 do i <- getIState
243 do i <- getIState
@@ -622,7 +626,7 @@ instance Binary Totality where
622 _ -> error "Corrupted binary data for Totality"
626 _ -> error "Corrupted binary data for Totality"
623
627
624instance Binary IBCFile where
628instance Binary IBCFile where
625− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)
629+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19)
626 = do put x1
630 = do put x1
627 put x2
631 put x2
628 put x3
632 put x3
@@ -641,6 +645,7 @@ instance Binary IBCFile where
641 put x16
645 put x16
642 put x17
646 put x17
643 put x18
647 put x18
648+ put x19
644 get
649 get
645 = do x1 <- get
650 = do x1 <- get
646 if x1 == ibcVersion then
651 if x1 == ibcVersion then
@@ -661,9 +666,24 @@ instance Binary IBCFile where
661 x16 <- get
666 x16 <- get
662 x17 <- get
667 x17 <- get
663 x18 <- get
668 x18 <- get
669+ x19 <- get
664− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)
670+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19)
665 else return (initIBC { ver = x1 })
671 else return (initIBC { ver = x1 })
666
672
673+instance Binary FnOpt where
674+ put x
675+ = case x of
676+ Inlinable -> putWord8 0
677+ TotalFn -> putWord8 1
678+ TCGen -> putWord8 2
679+ get
680+ = do i <- getWord8
681+ case i of
682+ 0 -> return Inlinable
683+ 1 -> return TotalFn
684+ 2 -> return TCGen
685+ _ -> error "Corrupted binary data for FnOpt"
686+
667instance Binary Fixity where
687instance Binary Fixity where
668 put x
688 put x
669 = case x of
689 = case x of
src/Idris/Parser.hs+7−1
@@ -397,7 +397,9 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
397
397
398pFunDecl' :: SyntaxInfo -> IParser PDecl
398pFunDecl' :: SyntaxInfo -> IParser PDecl
399pFunDecl' syn = try (do push_indent
399pFunDecl' syn = try (do push_indent
400+ opts <- pFnOpts
400 acc <- pAccessibility
401 acc <- pAccessibility
402+ opts' <- pFnOpts
401 n_in <- pfName
403 n_in <- pfName
402 let n = expandNS syn n_in
404 let n = expandNS syn n_in
403 ty <- pTSig syn
405 ty <- pTSig syn
@@ -405,7 +407,7 @@ pFunDecl' syn = try (do push_indent
405 pTerminator
407 pTerminator
406-- ty' <- implicit syn n ty
408-- ty' <- implicit syn n ty
407 addAcc n acc
409 addAcc n acc
408− return (PTy syn fc n ty))
410+ return (PTy syn fc (opts ++ opts') n ty))
409 <|> try (pPattern syn)
411 <|> try (pPattern syn)
410
412
411pUsing :: SyntaxInfo -> IParser [PDecl]
413pUsing :: SyntaxInfo -> IParser [PDecl]
@@ -611,6 +613,10 @@ pAccessibility
611 = do acc <- pAccessibility'; return (Just acc)
613 = do acc <- pAccessibility'; return (Just acc)
612 <|> return Nothing
614 <|> return Nothing
613
615
616+pFnOpts :: IParser [FnOpt]
617+pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)
618+ <|> return []
619+
614addAcc :: Name -> Maybe Accessibility -> IParser ()
620addAcc :: Name -> Maybe Accessibility -> IParser ()
615addAcc n a = do i <- getState
621addAcc n a = do i <- getState
616 setState (i { hide_list = (n, a) : hide_list i })
622 setState (i { hide_list = (n, a) : hide_list i })
test/test010/expectednew file+1
@@ -0,0 +1 @@
1+test010.idr:14:foo is not total due to: MkBad
test/test010/runnew file+2
@@ -0,0 +1,2 @@
1+#!/bin/bash
2+idris test010.idr -o test010
test/test010/test010.idrnew file+14
@@ -0,0 +1,14 @@
1+data MyNat = MyO | MyS MyNat
2+
3+data Bad = MkBad (Bad -> Int) Int
4+ | MkBad' Int
5+
6+total
7+vapp : Vect a n -> Vect a m -> Vect a (n + m)
8+vapp [] ys = ys
9+vapp (x :: xs) ys = x :: vapp xs ys
10+
11+total
12+foo : Bad -> Int
13+foo (MkBad f i) = f (MkBad' i)
14+foo (MkBad' x) = x