git.iko.soy/Idris-dev
on master help sign in
Added covering as a possible value for %default
41e3c52Colin Adams
src/Idris/AbsSyntaxTree.hs+9−4
compare with master
unifiedsplit
@@ -181,7 +181,12 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh
181 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
181 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
182 deriving (Show, Eq)
182 deriving (Show, Eq)
183
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
@@ -244,7 +249,7 @@ data IState = IState {
244 idris_parsedSpan :: Maybe FC,
249 idris_parsedSpan :: Maybe FC,
245 hide_list :: Ctxt Accessibility,
250 hide_list :: Ctxt Accessibility,
246 default_access :: Accessibility,
251 default_access :: Accessibility,
247− default_total :: Bool,
252+ default_total :: DefaultTotality,
248 ibc_write :: [IBCWrite],
253 ibc_write :: [IBCWrite],
249 compiled_so :: Maybe String,
254 compiled_so :: Maybe String,
250 idris_dynamic_libs :: [DynamicLib],
255 idris_dynamic_libs :: [DynamicLib],
@@ -360,7 +365,7 @@ idrisInit = IState initContext S.empty []
360 emptyContext emptyContext emptyContext emptyContext
365 emptyContext emptyContext emptyContext emptyContext
361 emptyContext
366 emptyContext
362 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
367 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
363− [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []
368+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
364 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
369 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
365 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
370 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
366 emptyContext S.empty M.empty emptyContext
371 emptyContext S.empty M.empty emptyContext
@@ -767,7 +772,7 @@ data Directive = DLib Codegen String
767 | DHide Name
772 | DHide Name
768 | DFreeze Name
773 | DFreeze Name
769 | DAccess Accessibility
774 | DAccess Accessibility
770− | DDefault Bool
775+ | DDefault DefaultTotality
771 | DLogging Integer
776 | DLogging Integer
772 | DDynamicLibs [String]
777 | DDynamicLibs [String]
773 | DNameHint Name FC [(Name, FC)]
778 | DNameHint Name FC [(Name, FC)]
src/Idris/DeepSeq.hs+5−1
@@ -694,7 +694,11 @@ instance NFData OutputMode where
694 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
694 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
695 rnf (IdeMode x y) = rnf x `seq` ()
695 rnf (IdeMode x y) = rnf x `seq` ()
696
696
697−
697+instance NFData DefaultTotality where
698+ rnf DefaultCheckingTotal = ()
699+ rnf DefaultCheckingPartial = ()
700+ rnf DefaultCheckingCovering = ()
701+
698instance NFData IState where
702instance NFData IState where
699 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
703 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
700 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
704 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 $
595 pushIndent
595 pushIndent
596 (doc, argDocs) <- docstring syn
596 (doc, argDocs) <- docstring syn
597 ist <- get
597 ist <- get
598− let initOpts = if default_total ist
598+ let initOpts = case default_total ist of
599− then [TotalFn]
599+ DefaultCheckingTotal -> [TotalFn]
600− else []
600+ DefaultCheckingCovering -> [CoveringFn]
601+ _ -> []
601 opts <- fnOpts initOpts
602 opts <- fnOpts initOpts
602 acc <- accessibility
603 acc <- accessibility
603 opts' <- fnOpts opts
604 opts' <- fnOpts opts
@@ -711,9 +712,10 @@ postulate syn = do (doc, ext)
711 ext <- ppostDecl
712 ext <- ppostDecl
712 return (doc, ext)
713 return (doc, ext)
713 ist <- get
714 ist <- get
714− let initOpts = if default_total ist
715+ let initOpts = case default_total ist of
715− then [TotalFn]
716+ DefaultCheckingTotal -> [TotalFn]
716− else []
717+ DefaultCheckingCovering -> [CoveringFn]
718+ _ -> []
717 opts <- fnOpts initOpts
719 opts <- fnOpts initOpts
718 acc <- accessibility
720 acc <- accessibility
719 opts' <- fnOpts opts
721 opts' <- fnOpts opts
@@ -919,9 +921,10 @@ InstanceName ::= '[' Name ']';
919instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
921instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
920instance_ kwopt syn
922instance_ kwopt syn
921 = do ist <- get
923 = do ist <- get
922− let initOpts = if default_total ist
924+ let initOpts = case default_total ist of
923− then [TotalFn]
925+ DefaultCheckingTotal -> [TotalFn]
924− else []
926+ DefaultCheckingCovering -> [CoveringFn]
927+ _ -> []
925
928
926 (doc, argDocs) <- docstring syn
929 (doc, argDocs) <- docstring syn
927 opts <- fnOpts initOpts
930 opts <- fnOpts initOpts
@@ -1396,14 +1399,15 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1396{- | Parses a totality
1399{- | Parses a totality
1397
1400
1398@
1401@
1399−Totality ::= 'partial' | 'total'
1402+Totality ::= 'partial' | 'total' | 'covering'
1400@
1403@
1401
1404
1402-}
1405-}
1403−totality :: IdrisParser Bool
1406+totality :: IdrisParser DefaultTotality
1404totality
1407totality
1405− = do reservedHL "total"; return True
1408+ = do reservedHL "total"; return DefaultCheckingTotal
1406− <|> do reservedHL "partial"; return False
1409+ <|> do reservedHL "partial"; return DefaultCheckingPartial
1410+ <|> do reservedHL "covering"; return DefaultCheckingCovering
1407
1411
1408{- | Parses a type provider
1412{- | Parses a type provider
1409
1413
src/Idris/REPL.hs+1−1
@@ -1703,7 +1703,7 @@ idrisMain opts =
1703 let port = getPort opts
1703 let port = getPort opts
1704
1704
1705 when (DefaultTotal `elem` opts) $ do i <- getIState
1705 when (DefaultTotal `elem` opts) $ do i <- getIState
1706− putIState (i { default_total = True })
1706+ putIState (i { default_total = DefaultCheckingTotal })
1707 tty <- runIO $ isATTY
1707 tty <- runIO $ isATTY
1708 setColourise $ not quiet && last (tty : opt getColour opts)
1708 setColourise $ not quiet && last (tty : opt getColour opts)
1709
1709