7438e0f · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -12,6 +12,8 @@ User visible changes:

12 for functions, and a corresponding "partial" reserved words to mark functions

13 as allowed to be partial. Also "--total" and "--partial" added as command

14 line options.

15+* Command line option "--warnpartial" for flagging all undeclared

16+ partial functions, without error.

15* New termination checker supporting mutually recursive definitions.

17* New termination checker supporting mutually recursive definitions.

16* Added ':load' command to REPL, for loading a new file

18* Added ':load' command to REPL, for loading a new file

17* Added ':module' command to REPL, for adding modules

19* Added ':module' command to REPL, for adding modules

src/Idris/AbsSyntaxTree.hs+2−1

@@ -260,7 +260,8 @@ expl = Exp False Dynamic

260constraint = Constraint False Dynamic

261tacimpl = TacImp False Dynamic

262

263+data FnOpt = Inlinable | TotalFn | PartialFn

263−data FnOpt = Inlinable | TotalFn | Coinductive | AssertTotal | TCGen

264+ | Coinductive | AssertTotal | TCGen

264 | CExport String -- export, with a C name

265 | CExport String -- export, with a C name

265 | Specialise [Name] -- specialise it, freeze these names

266 | Specialise [Name] -- specialise it, freeze these names

266 deriving (Show, Eq)

267 deriving (Show, Eq)

src/Idris/Coverage.hs+2−1

@@ -363,7 +363,8 @@ checkTotality path fc n

363 e -> do w <- cmdOptSet WarnPartial

364 if TotalFn `elem` opts

365 then totalityError t'

366+ else do when (w && not (PartialFn `elem` opts)) $

366− else do when w $ warnPartial n t'

367+ warnPartial n t'

367 return t'

368 return t'

368 where

369 where

369 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

370 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

src/Idris/Parser.hs+1−1

@@ -647,7 +647,7 @@ pAccessibility

647pFnOpts :: [FnOpt] -> IParser [FnOpt]

648pFnOpts opts

649 = do reserved "total"; pFnOpts (TotalFn : opts)

650− <|> do reserved "partial"; pFnOpts (opts \\ [TotalFn])

650+ <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))

651 <|> try (do lchar '%'; reserved "export"; c <- strlit;

652 pFnOpts (CExport c : opts))

653 <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)

tutorial/theorems.tex+2−1

@@ -437,4 +437,5 @@ All functions \remph{after} a \texttt{\%default total} declaration are required

437to be total. Correspondingly, after a \texttt{\%default partial} declaration,

438the requirement is relaxed.

439

440−

440+Finally, the compiler flag \texttt{--warnpartial} causes \Idris{} to print

441+a warning for any undeclared partial function.