8f95300 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow functions to be declared as error handlers

commit8f95300abeafc108c66c4632aaf692ccaaa9886a authorDavid Christiansen <david@davidchristiansen.dk> dateSat 28 Sep 2013, 21:01 (13 years ago) parent6808ce5

3 files changed+15−2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+6−2 src/Idris/ElabDecls.hs+6 src/Idris/Parser.hs+3

src/Idris/AbsSyntaxTree.hs+6−2

@@ -131,7 +131,8 @@ data IState = IState {

131131 idris_outputmode :: OutputMode,

132132 idris_colourRepl :: Bool,

133133 idris_colourTheme :: ColourTheme,

134− idris_outh :: Handle

134+ idris_outh :: Handle,

135+ idris_errorhandlers :: [Name]

135136 }

136137

137138data SizeChange = Smaller | Same | Bigger | Unknown

@@ -189,13 +190,15 @@ data IBCWrite = IBCFix FixDecl

189190 | IBCLineApp FilePath Int PTerm

190191 deriving Show

191192

193+-- | The initial state for the compiler

194+idrisInit :: IState

192195idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

193196 emptyContext emptyContext emptyContext emptyContext

194197 emptyContext emptyContext emptyContext emptyContext

195198 emptyContext

196199 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

197200 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

198− True defaultTheme stdout

201+ True defaultTheme stdout []

199202

200203-- | The monad for the main REPL - reading and processing files and updating

201204-- global state (hence the IO inner monad).

@@ -380,6 +383,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

380383 -- a function argument, and further evaluation resutls

381384 | Implicit -- implicit coercion

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

386+ | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

383387 | Reflection -- a reflecting function, compile-time only

384388 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

385389 deriving (Show, Eq)

src/Idris/ElabDecls.hs+6

@@ -112,6 +112,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

112112 addIBC (IBCFlags n opts')

113113 when (Implicit `elem` opts) $ do addCoercion n

114114 addIBC (IBCCoercion n)

115+ -- If the function is declared as an error handler and the language

116+ -- extension is enabled, then add it to the list of error handlers.

117+ when (ErrorReflection `elem` idris_language_extensions i && ErrorHandler `elem` opts) $

118+ -- TODO: Check that the declared type is the correct type for an error handler:

119+ -- handler : List (TTName, TT) -> Err -> ErrorReport

120+ putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }

115121 when corec $ do setAccessibility n Frozen

116122 addIBC (IBCAccess n Frozen)

117123 return usety

src/Idris/Parser.hs+3

@@ -309,6 +309,7 @@ FnOpts ::= 'total'

309309 | 'partial'

310310 | 'implicit'

311311 | '%' 'assert_total'

312+ | '%' 'error_handler'

312313 | '%' 'reflection'

313314 | '%' 'specialise' '[' NameTimesList? ']'

314315 ;

@@ -330,6 +331,8 @@ fnOpts opts

330331 fnOpts (CExport c : opts)

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

332333 fnOpts (AssertTotal : opts)

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

335+ fnOpts (ErrorHandler : opts)

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

334337 fnOpts (Reflection : opts)

335338 <|> do lchar '%'; reserved "specialise";