de6bb41 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'total' keyword and positivity check

commitde6bb4109928896c8671d51f5be437b67ac8012a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 25 Jan 2012, 10:47 (15 years ago) parent8baaa42

10 files changed+134−35

compare with master

unifiedsplit

src/Core/CoreParser.hs+1−1 src/Core/Evaluate.hs+8−1 src/Idris/AbsSyntax.hs+17−9 src/Idris/Coverage.hs+17−1 src/Idris/ElabDecls.hs+42−17 src/Idris/IBC.hs+25−5 src/Idris/Parser.hs+7−1 test/test010/expected+1 test/test010/run+2 test/test010/test010.idr+14

src/Core/CoreParser.hs+1−1

@@ -21,7 +21,7 @@ idrisDef = haskellDef {

2121 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

2222 reservedNames = ["let", "in", "data", "record", "Set",

2323 "do", "dsl", "import", "impossible",

24− "case", "of",

24+ "case", "of", "total",

2525 "infix", "infixl", "infixr", "prefix",

2626 "where", "with", "forall", "syntax", "proof",

2727 "using", "params", "namespace", "class", "instance",

src/Core/Evaluate.hs+8−1

@@ -473,11 +473,18 @@ data Accessibility = Public | Frozen | Hidden

473473 deriving (Show, Eq)

474474

475475data Totality = Total | Partial PReason

476− deriving (Show, Eq)

476+ deriving Eq

477477

478478data PReason = Other [Name] | Itself | NotCovering | NotPositive

479479 deriving (Show, Eq)

480480

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+

481488{-!

482489deriving instance Binary Accessibility

483490!-}

src/Idris/AbsSyntax.hs+17−9

@@ -44,6 +44,7 @@ data IState = IState { tt_ctxt :: Context,

4444 idris_optimisation :: Ctxt OptInfo,

4545 idris_datatypes :: Ctxt TypeInfo,

4646 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

47+ idris_flags :: Ctxt [FnOpt],

4748 idris_log :: String,

4849 idris_options :: IOption,

4950 idris_name :: Int,

@@ -82,11 +83,12 @@ data IBCWrite = IBCFix FixDecl

8283 | IBCHeader String

8384 | IBCAccess Name Accessibility

8485 | IBCTotal Name Totality

86+ | IBCFlags Name [FnOpt]

8587 | IBCDef Name -- i.e. main context

8688 deriving Show

8789

8890idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

89− emptyContext emptyContext emptyContext emptyContext

91+ emptyContext emptyContext emptyContext emptyContext emptyContext

9092 "" defaultOpts 6 [] [] [] [] [] [] [] []

9193 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

9294

@@ -112,6 +114,9 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

112114addHdr :: String -> Idris ()

113115addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

114116

117+setFlags :: Name -> [FnOpt] -> Idris ()

118+setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })

119+

115120setAccessibility :: Name -> Accessibility -> Idris ()

116121setAccessibility n a

117122 = do i <- get

@@ -356,8 +361,11 @@ impl = Imp False Dynamic

356361expl = Exp False Dynamic

357362constraint = Constraint False Static

358363

359−data FnOpt = Inlinable | Abstract | Private | TCGen

364+data FnOpt = Inlinable | TotalFn | TCGen

360365 deriving (Show, Eq)

366+{-!

367+deriving instance Binary FnOpt

368+!-}

361369

362370type FnOpts = [FnOpt]

363371

@@ -365,7 +373,7 @@ inlinable :: FnOpts -> Bool

365373inlinable = elem Inlinable

366374

367375data 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

369377 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

370378 | PData SyntaxInfo FC (PData' t) -- data declaration

371379 | PParams FC [(Name, t)] [PDecl' t] -- params block

@@ -408,7 +416,7 @@ type PClause = PClause' PTerm

408416

409417declared :: PDecl -> [Name]

410418declared (PFix _ _ _) = []

411−declared (PTy _ _ n t) = [n]

419+declared (PTy _ _ _ n t) = [n]

412420declared (PClauses _ _ n _) = [] -- not a declaration

413421declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

414422 where fstt (a, _, _) = a

@@ -635,7 +643,7 @@ instance Show PTerm where

635643

636644instance Show PDecl where

637645 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

639647 show (PClauses _ _ n c) = showSep "\n" (map show c)

640648 show (PData _ _ d) = show d

641649

@@ -926,10 +934,10 @@ expandParams dec ps ns tm = en tm

926934

927935expandParamsD :: IState ->

928936 (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)

930938 = if n `elem` ns

931− then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

932− else PTy syn fc n (expandParams dec ps ns ty)

939+ then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

940+ else PTy syn fc o n (expandParams dec ps ns ty)

933941expandParamsD ist dec ps ns (PClauses fc opts n cs)

934942 = let n' = if n `elem` ns then dec n else n in

935943 PClauses fc opts n' (map expandParamsC cs)

@@ -1208,7 +1216,7 @@ dumpDecls [] = ""

12081216dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

12091217

12101218dumpDecl (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

12121220dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

12131221dumpDecl (PData _ _ d) = showDImp True d

12141222dumpDecl (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

116116 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]

117117 wff ns (Case n as) = do is <- mapM (wffC ns) as

118118 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

120121 wffC ns (ConstCase _ sc) = wff ns sc

121122 wffC ns (DefaultCase sc) = wff ns sc

122123 wff ns (STerm t) = argPos ns t

@@ -148,4 +149,19 @@ wellFounded i n sc = case wff [] sc of

148149 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs

149150 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs

150151

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

151167

src/Idris/ElabDecls.hs+42−17

@@ -35,8 +35,8 @@ checkDef fc ns = do ctxt <- getContext

3535 mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t

3636 return (n, t')) ns

3737

38−elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()

39−elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

38+elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()

39+elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

4040 n = liftname info n_in in -}

4141 do checkUndefined fc n

4242 ctxt <- getContext

@@ -52,6 +52,8 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

5252 ds <- checkDef fc ((n, nty):defer)

5353 addIBC (IBCDef n)

5454 addDeferred ds

55+ setFlags n opts

56+ addIBC (IBCFlags n opts)

5557 mapM_ (elabCaseBlock info) is

5658

5759elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

@@ -79,6 +81,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

7981 addIBC (IBCData n)

8082 collapseCons n cons

8183 updateContext (addDatatype (Data n ttag cty cons))

84+ mapM_ (checkPositive n) cons

8285

8386elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

8487 PTerm -> Name -> PTerm -> Idris ()

@@ -142,6 +145,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

142145 return Total

143146 else do logLvl 2 $ show n ++ " does not cover all cases"

144147 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 ()

145155 case tree of

146156 CaseDef _ _ [] -> return ()

147157 CaseDef _ _ xs -> mapM_ (\x ->

@@ -199,8 +209,12 @@ elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

199209 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

200210 OK ((lhs', _, _), _) ->

201211 do let lhs_tm = orderPats (getInferTerm lhs')

202− checkInferred fc (delab' i lhs_tm True) lhs

203− fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case"

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 ()

216+ else fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++

217+ " is a possible case"

204218 ++ "\n" ++ showImp True lhs

205219 Error _ -> return ()

206220 return Nothing

@@ -419,10 +433,10 @@ elabClass info syn fc constraints tn ps ds

419433 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

420434 conbind [] x = x

421435

422− tdecl (PTy syn _ n t) = do t' <- implicit syn n t

423− return ( (n, (toExp (map fst ps) Exp t')),

424− (n, (toExp (map fst ps) Imp t')),

425− (n, (syn, t) ) )

436+ tdecl (PTy syn _ _ n t) = do t' <- implicit syn n t

437+ return ( (n, (toExp (map fst ps) Exp t')),

438+ (n, (toExp (map fst ps) Imp t')),

439+ (n, (syn, t) ) )

426440 tdecl _ = fail "Not allowed in a class declaration"

427441

428442 -- Create default definitions

@@ -430,7 +444,7 @@ elabClass info syn fc constraints tn ps ds

430444 case lookup n mtys of

431445 Just (syn, ty) -> do let ty' = insertConstraint c ty

432446 let ds = map (decorateid defaultdec)

433− [PTy syn fc n ty',

447+ [PTy syn fc [] n ty',

434448 PClauses fc (TCGen:opts) n cs]

435449 iLOG (show ds)

436450 return (n, (defaultdec n, ds))

@@ -440,7 +454,7 @@ elabClass info syn fc constraints tn ps ds

440454 defaultdec (UN n) = UN ("default#" ++ n)

441455 defaultdec (NS n ns) = NS (defaultdec n) ns

442456

443− tydecl (PTy _ _ _ _) = True

457+ tydecl (PTy _ _ _ _ _) = True

444458 tydecl _ = False

445459 clause (PClauses _ _ _ _) = True

446460 clause _ = False

@@ -454,7 +468,7 @@ elabClass info syn fc constraints tn ps ds

454468 let ty = PPi constraint (MN 0 "pc") c con

455469 iLOG (showImp True ty)

456470 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

457− return [PTy syn fc cfn ty,

471+ return [PTy syn fc [] cfn ty,

458472 PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]

459473

460474 tfun cn c syn all (m, ty)

@@ -468,7 +482,7 @@ elabClass info syn fc constraints tn ps ds

468482 iLOG (showImp True ty)

469483 iLOG (show (m, ty', capp, margs))

470484 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

471− return [PTy syn fc m ty',

485+ return [PTy syn fc [] m ty',

472486 PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]

473487

474488 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

@@ -509,7 +523,7 @@ elabInstance info syn fc cs n ps t ds

509523 [c] -> return c

510524 _ -> fail $ show n ++ " is not a type class"

511525 let iname = UN ('@':show n ++ "$" ++ show ps)

512− elabType info syn fc iname t

526+ elabType info syn fc [] iname t

513527 let ips = zip (class_params ci) ps

514528 let ns = case n of

515529 NS n ns' -> ns'

@@ -549,7 +563,7 @@ elabInstance info syn fc cs n ps t ds

549563 decorate ns (UN n) = NS (UN ('!':n)) ns

550564 decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns

551565

552− mkTyDecl (n, t, _) = PTy syn fc n t

566+ mkTyDecl (n, t, _) = PTy syn fc [] n t

553567

554568 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

555569 conbind [] x = x

@@ -577,7 +591,7 @@ elabInstance info syn fc cs n ps t ds

577591 clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'

578592 clauseFor m ns _ = False

579593

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

581595decorateid decorate (PClauses f o n cs)

582596 = PClauses f o (decorate n) (map dc cs)

583597 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)

612626

613627elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

614628elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

615−elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n

616− elabType info s f n ty

629+elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n

630+ elabType info s f o n ty

617631elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

618632 elabData info s f d

619633elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

@@ -667,3 +681,14 @@ checkInferred fc inf user =

667681 ++ show x ++ " and " ++ show y)

668682-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

669683

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

1313import Data.Binary

1414import Data.List

1515import Data.ByteString.Lazy as B hiding (length, elem)

16−-- import Data.DeriveTH

1716import Control.Monad

1817import Control.Monad.State hiding (get, put)

1918import System.FilePath

@@ -22,7 +21,7 @@ import System.Directory

2221import Paths_idris

2322

2423ibcVersion :: Word8

25−ibcVersion = 14

24+ibcVersion = 15

2625

2726data IBCFile = IBCFile { ver :: Word8,

2827 sourcefile :: FilePath,

@@ -41,13 +40,14 @@ data IBCFile = IBCFile { ver :: Word8,

4140 ibc_hdrs :: [String],

4241 ibc_access :: [(Name, Accessibility)],

4342 ibc_total :: [(Name, Totality)],

43+ ibc_flags :: [(Name, [FnOpt])],

4444 ibc_defs :: [(Name, Def)] }

4545{-!

4646deriving instance Binary IBCFile

4747!-}

4848

4949initIBC :: IBCFile

50−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

50+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

5151

5252loadIBC :: FilePath -> Idris ()

5353loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -107,6 +107,7 @@ ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

107107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

108108 _ -> fail "IBC write failed"

109109ibc 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 }

110111ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

111112

112113process :: IBCFile -> FilePath -> Idris ()

@@ -234,6 +235,9 @@ pAccess ds = mapM_ (\ (n, a) ->

234235 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

235236 ds

236237

238+pFlags :: [(Name, [FnOpt])] -> Idris ()

239+pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

240+

237241pTotal :: [(Name, Totality)] -> Idris ()

238242pTotal ds = mapM_ (\ (n, a) ->

239243 do i <- getIState

@@ -622,7 +626,7 @@ instance Binary Totality where

622626 _ -> error "Corrupted binary data for Totality"

623627

624628instance 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)

626630 = do put x1

627631 put x2

628632 put x3

@@ -641,6 +645,7 @@ instance Binary IBCFile where

641645 put x16

642646 put x17

643647 put x18

648+ put x19

644649 get

645650 = do x1 <- get

646651 if x1 == ibcVersion then

@@ -661,9 +666,24 @@ instance Binary IBCFile where

661666 x16 <- get

662667 x17 <- get

663668 x18 <- get

664− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)

669+ x19 <- get

670+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19)

665671 else return (initIBC { ver = x1 })

666672

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+

667687instance Binary Fixity where

668688 put x

669689 = case x of

src/Idris/Parser.hs+7−1

@@ -397,7 +397,9 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

397397

398398pFunDecl' :: SyntaxInfo -> IParser PDecl

399399pFunDecl' syn = try (do push_indent

400+ opts <- pFnOpts

400401 acc <- pAccessibility

402+ opts' <- pFnOpts

401403 n_in <- pfName

402404 let n = expandNS syn n_in

403405 ty <- pTSig syn

@@ -405,7 +407,7 @@ pFunDecl' syn = try (do push_indent

405407 pTerminator

406408-- ty' <- implicit syn n ty

407409 addAcc n acc

408− return (PTy syn fc n ty))

410+ return (PTy syn fc (opts ++ opts') n ty))

409411 <|> try (pPattern syn)

410412

411413pUsing :: SyntaxInfo -> IParser [PDecl]

@@ -611,6 +613,10 @@ pAccessibility

611613 = do acc <- pAccessibility'; return (Just acc)

612614 <|> return Nothing

613615

616+pFnOpts :: IParser [FnOpt]

617+pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)

618+ <|> return []

619+

614620addAcc :: Name -> Maybe Accessibility -> IParser ()

615621addAcc n a = do i <- getState

616622 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

3+data Bad = MkBad (Bad -> Int) Int

4+ | MkBad' Int

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