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

git.iko.soy/Idris-dev

Document --warnpartial

Behaviour fixed so that it doesn't report declared partial functions

commit7438e0f638ddc2cf89dfb996188215fe1bfd058b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 29 Oct 2012, 10:35 (14 years ago) parent2541a16

5 files changed+9−4

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Coverage.hs+2−1 src/Idris/Parser.hs+1−1 tutorial/theorems.tex+2−1

CHANGELOG+2

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

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

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

1414 line options.

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

16+ partial functions, without error.

1517* New termination checker supporting mutually recursive definitions.

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

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

src/Idris/AbsSyntaxTree.hs+2−1

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

260260constraint = Constraint False Dynamic

261261tacimpl = TacImp False Dynamic

262262

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

263+data FnOpt = Inlinable | TotalFn | PartialFn

264+ | Coinductive | AssertTotal | TCGen

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

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

266267 deriving (Show, Eq)

src/Idris/Coverage.hs+2−1

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

363363 e -> do w <- cmdOptSet WarnPartial

364364 if TotalFn `elem` opts

365365 then totalityError t'

366− else do when w $ warnPartial n t'

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

367+ warnPartial n t'

367368 return t'

368369 where

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

src/Idris/Parser.hs+1−1

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

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

648648pFnOpts opts

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

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

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

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

652652 pFnOpts (CExport c : opts))

653653 <|> 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

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

438438the requirement is relaxed.

439439

440−

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

441+a warning for any undeclared partial function.