2b25114 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'covering' of https://github.com/colin-adams/Idris-dev into colin-adams-covering

commit2b2511443d0fc09bb3a565a640b64f6ce55f8490 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSat 7 May 2016, 18:05 (10 years ago) parent57136cc 6074f1c

9 files changed+56−19

compare with master

unifiedsplit

.gitignore+1 idris.cabal+3 src/Idris/AbsSyntaxTree.hs+9−4 src/Idris/DeepSeq.hs+5−1 src/Idris/Parser.hs+17−13 src/Idris/REPL.hs+1−1 test/directives002/directives002.idr+14 test/directives002/expected+2 test/directives002/run+4

.gitignore+1

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

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

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

3434test/runtest.exe

35+test/runtest

3536tags

3637TAGS

3738src/Version_idris.hs

idris.cabal+3

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

409409 test/directives001/*.idr

410410 test/directives001/run

411411 test/directives001/expected

412+ test/directives002/*.idr

413+ test/directives002/run

414+ test/directives002/expected

412415

413416 test/delab001/*.idr

414417 test/delab001/run

src/Idris/AbsSyntaxTree.hs+9−4

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

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

182182 deriving (Show, Eq)

183183

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+

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

186191data IState = IState {

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

@@ -244,7 +249,7 @@ data IState = IState {

244249 idris_parsedSpan :: Maybe FC,

245250 hide_list :: Ctxt Accessibility,

246251 default_access :: Accessibility,

247− default_total :: Bool,

252+ default_total :: DefaultTotality,

248253 ibc_write :: [IBCWrite],

249254 compiled_so :: Maybe String,

250255 idris_dynamic_libs :: [DynamicLib],

@@ -360,7 +365,7 @@ idrisInit = IState initContext S.empty []

360365 emptyContext emptyContext emptyContext emptyContext

361366 emptyContext

362367 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

363− [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []

368+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

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

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

366371 emptyContext S.empty M.empty emptyContext

@@ -767,7 +772,7 @@ data Directive = DLib Codegen String

767772 | DHide Name

768773 | DFreeze Name

769774 | DAccess Accessibility

770− | DDefault Bool

775+ | DDefault DefaultTotality

771776 | DLogging Integer

772777 | DDynamicLibs [String]

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

src/Idris/DeepSeq.hs+5−1

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

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

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

696696

697−

697+instance NFData DefaultTotality where

698+ rnf DefaultCheckingTotal = ()

699+ rnf DefaultCheckingPartial = ()

700+ rnf DefaultCheckingCovering = ()

701+

698702instance NFData IState where

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

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

src/Idris/Parser.hs+17−13

@@ -595,9 +595,10 @@ fnDecl' syn = checkFixity $

595595 pushIndent

596596 (doc, argDocs) <- docstring syn

597597 ist <- get

598− let initOpts = if default_total ist

599− then [TotalFn]

600− else []

598+ let initOpts = case default_total ist of

599+ DefaultCheckingTotal -> [TotalFn]

600+ DefaultCheckingCovering -> [CoveringFn]

601+ _ -> []

601602 opts <- fnOpts initOpts

602603 acc <- accessibility

603604 opts' <- fnOpts opts

@@ -711,9 +712,10 @@ postulate syn = do (doc, ext)

711712 ext <- ppostDecl

712713 return (doc, ext)

713714 ist <- get

714− let initOpts = if default_total ist

715− then [TotalFn]

716− else []

715+ let initOpts = case default_total ist of

716+ DefaultCheckingTotal -> [TotalFn]

717+ DefaultCheckingCovering -> [CoveringFn]

718+ _ -> []

717719 opts <- fnOpts initOpts

718720 acc <- accessibility

719721 opts' <- fnOpts opts

@@ -919,9 +921,10 @@ InstanceName ::= '[' Name ']';

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

920922instance_ kwopt syn

921923 = do ist <- get

922− let initOpts = if default_total ist

923− then [TotalFn]

924− else []

924+ let initOpts = case default_total ist of

925+ DefaultCheckingTotal -> [TotalFn]

926+ DefaultCheckingCovering -> [CoveringFn]

927+ _ -> []

925928

926929 (doc, argDocs) <- docstring syn

927930 opts <- fnOpts initOpts

@@ -1396,14 +1399,15 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)

13961399{- | Parses a totality

13971400

13981401@

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

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

14001403@

14011404

14021405-}

1403−totality :: IdrisParser Bool

1406+totality :: IdrisParser DefaultTotality

14041407totality

1405− = do reservedHL "total"; return True

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

1408+ = do reservedHL "total"; return DefaultCheckingTotal

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

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

14071411

14081412{- | Parses a type provider

14091413

src/Idris/REPL.hs+1−1

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

17031703 let port = getPort opts

17041704

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

1706− putIState (i { default_total = True })

1706+ putIState (i { default_total = DefaultCheckingTotal })

17071707 tty <- runIO $ isATTY

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

17091709

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