81030be · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3151 from ahmadsalim/colin-adams-covering

81030beAhmad Salim Al-Sibahi10 years ago

.gitignore+1

compare with master

unifiedsplit

@@ -32,6 +32,7 @@ test/output

32test/*[0-9][0-9][0-9]/output

33test/*[0-9][0-9][0-9]/*.exe

34test/runtest.exe

35+test/runtest

35tags

36tags

36TAGS

37TAGS

37src/Version_idris.hs

38src/Version_idris.hs

idris.cabal+3

@@ -409,6 +409,9 @@ Extra-source-files:

409 test/directives001/*.idr

410 test/directives001/run

411 test/directives001/expected

412+ test/directives002/*.idr

413+ test/directives002/run

414+ test/directives002/expected

412

415

413 test/delab001/*.idr

416 test/delab001/*.idr

414 test/delab001/run

417 test/delab001/run

libs/prelude/Prelude/File.idr+2−2

@@ -233,7 +233,7 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

233 return (p > 0)

234

235||| Read the contents of a file into a string

236−partial -- might be reading something infinitely long like /dev/null ...

236+-- might be reading something infinitely long like /dev/null ...

237covering export

238readFile : String -> IO (Either FileError String)

239readFile fn = do Right h <- openFile fn Read

@@ -242,7 +242,7 @@ readFile fn = do Right h <- openFile fn Read

242 closeFile h

243 return c

244 where

245− partial

245+ covering

246 readFile' : File -> String -> IO (Either FileError String)

247 readFile' h contents =

248 do x <- fEOF h

src/Idris/AbsSyntaxTree.hs+9−4

@@ -181,7 +181,12 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh

181 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

182 deriving (Show, Eq)

183

184−

184+-- | If a function has no totality annotation, what do we assume?

185+data DefaultTotality = DefaultCheckingTotal -- ^ Total

186+ | DefaultCheckingPartial -- ^ Partial

187+ | DefaultCheckingCovering -- ^Total coverage, but may diverge

188+ deriving (Show, Eq)

189+

185-- | The global state used in the Idris monad

190-- | The global state used in the Idris monad

186data IState = IState {

191data IState = IState {

187 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

192 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

@@ -245,7 +250,7 @@ data IState = IState {

245 idris_parsedSpan :: Maybe FC,

250 idris_parsedSpan :: Maybe FC,

246 hide_list :: Ctxt Accessibility,

251 hide_list :: Ctxt Accessibility,

247 default_access :: Accessibility,

252 default_access :: Accessibility,

248− default_total :: Bool,

253+ default_total :: DefaultTotality,

249 ibc_write :: [IBCWrite],

254 ibc_write :: [IBCWrite],

250 compiled_so :: Maybe String,

255 compiled_so :: Maybe String,

251 idris_dynamic_libs :: [DynamicLib],

256 idris_dynamic_libs :: [DynamicLib],

@@ -361,7 +366,7 @@ idrisInit = IState initContext S.empty []

361 emptyContext emptyContext emptyContext emptyContext

366 emptyContext emptyContext emptyContext emptyContext

362 emptyContext

367 emptyContext

363 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

368 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

364− [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []

369+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

365 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

370 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

366 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

371 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

367 emptyContext S.empty M.empty emptyContext

372 emptyContext S.empty M.empty emptyContext

@@ -771,7 +776,7 @@ data Directive = DLib Codegen String

771 | DHide Name

776 | DHide Name

772 | DFreeze Name

777 | DFreeze Name

773 | DAccess Accessibility

778 | DAccess Accessibility

774− | DDefault Bool

779+ | DDefault DefaultTotality

775 | DLogging Integer

780 | DLogging Integer

776 | DDynamicLibs [String]

781 | DDynamicLibs [String]

777 | DNameHint Name FC [(Name, FC)]

782 | DNameHint Name FC [(Name, FC)]

src/Idris/DeepSeq.hs+5−1

@@ -695,7 +695,11 @@ instance NFData OutputMode where

695 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

696 rnf (IdeMode x y) = rnf x `seq` ()

697

698−

698+instance NFData DefaultTotality where

699+ rnf DefaultCheckingTotal = ()

700+ rnf DefaultCheckingPartial = ()

701+ rnf DefaultCheckingCovering = ()

702+

699instance NFData IState where

703instance NFData IState where

700 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

704 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

701 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

705 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

src/Idris/Parser.hs+68−61

@@ -595,18 +595,12 @@ fnDecl' syn = checkFixity $

595 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

596 pushIndent

597 (doc, argDocs) <- docstring syn

598− ist <- get

599− let initOpts = if default_total ist

600− then [TotalFn]

601− else []

602− opts <- fnOpts initOpts

603− acc <- accessibility

604− opts' <- fnOpts opts

598+ (opts, acc) <- fnOpts

605 (n_in, nfc) <- fnName

599 (n_in, nfc) <- fnName

606 let n = expandNS syn n_in

600 let n = expandNS syn n_in

607 fc <- getFC

601 fc <- getFC

608 lchar ':'

602 lchar ':'

609− return (doc, argDocs, fc, opts', n, nfc, acc))

603+ return (doc, argDocs, fc, opts, n, nfc, acc))

610 ty <- typeExpr (allowImp syn)

604 ty <- typeExpr (allowImp syn)

611 terminator

605 terminator

612 -- If it's a top level function, note the accessibility

606 -- If it's a top level function, note the accessibility

@@ -634,10 +628,40 @@ fnDecl' syn = checkFixity $

634 | otherwise = return True

628 | otherwise = return True

635 fixityOK _ = return True

629 fixityOK _ = return True

636

630

637−{-| Parses function options given initial options

631+{-| Parses a series of function and accessbility options

638

632

639@

633@

634+FnOpts ::= FnOpt* Accessibility FnOpt*

635+@

636+ -}

637+fnOpts :: IdrisParser ([FnOpt], Accessibility)

638+fnOpts = do

639+ opts <- many fnOpt

640+ acc <- accessibility

641+ opts' <- many fnOpt

642+ let allOpts = opts ++ opts'

643+ let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]

644+ opts'' <- addDefaultTotality (nub existingTotality) allOpts

645+ return (opts'', acc)

646+ where prettyTot TotalFn = "total"

647+ prettyTot PartialFn = "partial"

648+ prettyTot CoveringFn = "covering"

649+ addDefaultTotality [] opts = do

650+ ist <- get

651+ case default_total ist of

652+ DefaultCheckingTotal -> return (TotalFn:opts)

653+ DefaultCheckingCovering -> return (CoveringFn:opts)

654+ DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary

655+ addDefaultTotality [tot] opts = return opts

656+ -- Should really be a semantics error instead of a parser error

657+ addDefaultTotality (tot1:tot2:tots) opts =

658+ fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)

659+

660+

661+{-| Parses a function option

662+

663+@

640−FnOpts ::= 'total'

664+FnOpt ::= 'total'

641 | 'partial'

665 | 'partial'

642 | 'covering'

666 | 'covering'

643 | 'implicit'

667 | 'implicit'

@@ -660,37 +684,31 @@ NameTimesList ::=

660 ;

684 ;

661@

685@

662-}

686-}

663−-- FIXME: Check compatability for function options (i.e. partal/total)

664−--

665−-- Issue #1574 on the issue tracker.

666−-- https://github.com/idris-lang/Idris-dev/issues/1574

667−fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

687+fnOpt :: IdrisParser FnOpt

668−fnOpts opts

669− = do reservedHL "total"; fnOpts (TotalFn : opts)

688+fnOpt = do reservedHL "total"; return TotalFn

670− <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

689+ <|> do reservedHL "partial"; return PartialFn

671− <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

690+ <|> do reservedHL "covering"; return CoveringFn

672− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

691+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

673− fnOpts (CExport c : opts)

692+ return $ CExport c

674− <|> do try (lchar '%' *> reserved "no_implicit");

693+ <|> do try (lchar '%' *> reserved "no_implicit");

675− fnOpts (NoImplicit : opts)

694+ return NoImplicit

676− <|> do try (lchar '%' *> reserved "inline");

695+ <|> do try (lchar '%' *> reserved "inline");

677− fnOpts (Inlinable : opts)

696+ return Inlinable

678− <|> do try (lchar '%' *> reserved "assert_total");

697+ <|> do try (lchar '%' *> reserved "assert_total");

679− fnOpts (AssertTotal : opts)

698+ return AssertTotal

680− <|> do try (lchar '%' *> reserved "error_handler");

699+ <|> do try (lchar '%' *> reserved "error_handler");

681− fnOpts (ErrorHandler : opts)

700+ return ErrorHandler

682− <|> do try (lchar '%' *> reserved "error_reverse");

701+ <|> do try (lchar '%' *> reserved "error_reverse");

683− fnOpts (ErrorReverse : opts)

702+ return ErrorReverse

684− <|> do try (lchar '%' *> reserved "reflection");

703+ <|> do try (lchar '%' *> reserved "reflection");

685− fnOpts (Reflection : opts)

704+ return Reflection

686− <|> do try (lchar '%' *> reserved "hint");

705+ <|> do try (lchar '%' *> reserved "hint");

687− fnOpts (AutoHint : opts)

706+ return AutoHint

688− <|> do lchar '%'; reserved "specialise";

707+ <|> do lchar '%'; reserved "specialise";

689− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

708+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

690− fnOpts (Specialise ns : opts)

709+ return $ Specialise ns

691− <|> do reservedHL "implicit"; fnOpts (Implicit : opts)

710+ <|> do reservedHL "implicit"; return Implicit

692− <|> return opts

693− <?> "function modifier"

711+ <?> "function modifier"

694 where nameTimes :: IdrisParser (Name, Maybe Int)

712 where nameTimes :: IdrisParser (Name, Maybe Int)

695 nameTimes = do n <- fst <$> fnName

713 nameTimes = do n <- fst <$> fnName

696 t <- option Nothing (do reds <- fmap fst natural

714 t <- option Nothing (do reds <- fmap fst natural

@@ -712,12 +730,7 @@ postulate syn = do (doc, ext)

712 ext <- ppostDecl

730 ext <- ppostDecl

713 return (doc, ext)

731 return (doc, ext)

714 ist <- get

732 ist <- get

715− let initOpts = if default_total ist

716− then [TotalFn]

717− else []

718− opts <- fnOpts initOpts

719− acc <- accessibility

720− opts' <- fnOpts opts

733+ (opts, acc) <- fnOpts

721 (n_in, nfc) <- fnName

734 (n_in, nfc) <- fnName

722 let n = expandNS syn n_in

735 let n = expandNS syn n_in

723 lchar ':'

736 lchar ':'

@@ -725,7 +738,7 @@ postulate syn = do (doc, ext)

725 fc <- getFC

738 fc <- getFC

726 terminator

739 terminator

727 addAcc n acc

740 addAcc n acc

728− return (PPostulate ext doc syn fc nfc opts' n ty)

741+ return (PPostulate ext doc syn fc nfc opts n ty)

729 <?> "postulate"

742 <?> "postulate"

730 where ppostDecl = do fc <- reservedHL "postulate"; return False

743 where ppostDecl = do fc <- reservedHL "postulate"; return False

731 <|> do lchar '%'; reserved "extern"; return True

744 <|> do lchar '%'; reserved "extern"; return True

@@ -940,15 +953,8 @@ InstanceName ::= '[' Name ']';

940instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

953instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

941instance_ kwopt syn

954instance_ kwopt syn

942 = do ist <- get

955 = do ist <- get

943− let initOpts = if default_total ist

944− then [TotalFn]

945− else []

946−

947 (doc, argDocs) <- docstring syn

956 (doc, argDocs) <- docstring syn

948− opts <- fnOpts initOpts

949− acc <- accessibility

950− opts' <- fnOpts opts

957+ (opts, acc) <- fnOpts

951−

952 if kwopt then optional instanceKeyword

958 if kwopt then optional instanceKeyword

953 else do instanceKeyword

959 else do instanceKeyword

954 return (Just ())

960 return (Just ())

@@ -963,7 +969,7 @@ instance_ kwopt syn

963 let t = bindList (PPi constraint) cs sc

969 let t = bindList (PPi constraint) cs sc

964 pnames <- instanceUsing

970 pnames <- instanceUsing

965 ds <- instanceBlock syn

971 ds <- instanceBlock syn

966− return [PInstance doc argDocs syn fc cs' pnames acc opts' cn cnfc args [] t en ds]

972+ return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

967 <?> "implementation declaration"

973 <?> "implementation declaration"

968 where instanceName :: IdrisParser Name

974 where instanceName :: IdrisParser Name

969 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

975 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

@@ -1424,14 +1430,15 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1424{- | Parses a totality

1430{- | Parses a totality

1425

1431

1426@

1432@

1427−Totality ::= 'partial' | 'total'

1433+Totality ::= 'partial' | 'total' | 'covering'

1428@

1434@

1429

1435

1430-}

1436-}

1431−totality :: IdrisParser Bool

1437+totality :: IdrisParser DefaultTotality

1432totality

1438totality

1433− = do reservedHL "total"; return True

1439+ = do reservedHL "total"; return DefaultCheckingTotal

1434− <|> do reservedHL "partial"; return False

1440+ <|> do reservedHL "partial"; return DefaultCheckingPartial

1441+ <|> do reservedHL "covering"; return DefaultCheckingCovering

1435

1442

1436{- | Parses a type provider

1443{- | Parses a type provider

1437

1444

src/Idris/REPL.hs+1−1

@@ -1703,7 +1703,7 @@ idrisMain opts =

1703 let port = getPort opts

1704

1705 when (DefaultTotal `elem` opts) $ do i <- getIState

1706− putIState (i { default_total = True })

1706+ putIState (i { default_total = DefaultCheckingTotal })

1707 tty <- runIO $ isATTY

1708 setColourise $ not quiet && last (tty : opt getColour opts)

1709

test/directives002/directives002.idrnew file+14

@@ -0,0 +1,14 @@

1+module directives002

3+%access export

4+%default covering

6+loop : ()

7+loop = loop

9+namespace Main

10+ total

11+ main : IO ()

12+ main = do

13+ pure loop

14+ putStrLn $ "Hello World"

test/directives002/expectednew file+2

@@ -0,0 +1,2 @@

1+directives002.idr:12:3:

2+directives002.Main.main is possibly not total due to: directives002.loop

test/directives002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ directives002.idr --check --nocolour

4+rm -f directives002 *.ibc