52d8165 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow functions to be declared as error handlers

52d8165David Christiansen13 years ago

src/Idris/AbsSyntaxTree.hs+6−2

compare with master

unifiedsplit

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

128 idris_outputmode :: OutputMode,

129 idris_colourRepl :: Bool,

130 idris_colourTheme :: ColourTheme,

131− idris_outh :: Handle

131+ idris_outh :: Handle,

132+ idris_errorhandlers :: [Name]

132 }

133 }

133

134

134data SizeChange = Smaller | Same | Bigger | Unknown

135data SizeChange = Smaller | Same | Bigger | Unknown

@@ -182,12 +183,14 @@ data IBCWrite = IBCFix FixDecl

182 | IBCLineApp FilePath Int PTerm

183 | IBCLineApp FilePath Int PTerm

183 deriving Show

184 deriving Show

184

185

186+-- | The initial state for the compiler

187+idrisInit :: IState

185idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

188idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

186 emptyContext emptyContext emptyContext emptyContext

189 emptyContext emptyContext emptyContext emptyContext

187 emptyContext emptyContext emptyContext emptyContext

190 emptyContext emptyContext emptyContext emptyContext

188 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

191 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

189 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

192 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

190− True defaultTheme stdout

193+ True defaultTheme stdout []

191

194

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

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

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

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

@@ -368,6 +371,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

368 -- a function argument, and further evaluation resutls

371 -- a function argument, and further evaluation resutls

369 | Implicit -- implicit coercion

372 | Implicit -- implicit coercion

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

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

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

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

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

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

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

373 deriving (Show, Eq)

377 deriving (Show, Eq)

src/Idris/ElabDecls.hs+6

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

96 addIBC (IBCFlags n opts')

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

98 addIBC (IBCCoercion n)

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

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

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

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

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

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

99 when corec $ do setAccessibility n Frozen

105 when corec $ do setAccessibility n Frozen

100 addIBC (IBCAccess n Frozen)

106 addIBC (IBCAccess n Frozen)

101 where

107 where

src/Idris/Parser.hs+3

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

292 | 'partial'

293 | 'implicit'

294 | '%' 'assert_total'

295+ | '%' 'error_handler'

295 | '%' 'reflection'

296 | '%' 'reflection'

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

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

297 ;

298 ;

@@ -313,6 +314,8 @@ fnOpts opts

313 fnOpts (CExport c : opts)

314 fnOpts (CExport c : opts)

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

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

315 fnOpts (AssertTotal : opts)

316 fnOpts (AssertTotal : opts)

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

318+ fnOpts (ErrorHandler : opts)

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

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

317 fnOpts (Reflection : opts)

320 fnOpts (Reflection : opts)

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

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