82fe0c6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'origin/error-reflection' into error-reflection

82fe0c6David Christiansen13 years ago

src/Idris/AbsSyntaxTree.hs+6−2

compare with master

unifiedsplit

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

131 idris_outputmode :: OutputMode,

132 idris_colourRepl :: Bool,

133 idris_colourTheme :: ColourTheme,

134− idris_outh :: Handle

134+ idris_outh :: Handle,

135+ idris_errorhandlers :: [Name]

135 }

136 }

136

137

137data SizeChange = Smaller | Same | Bigger | Unknown

138data SizeChange = Smaller | Same | Bigger | Unknown

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

188 | IBCLineApp FilePath Int PTerm

189 | IBCLineApp FilePath Int PTerm

189 deriving Show

190 deriving Show

190

191

192+-- | The initial state for the compiler

193+idrisInit :: IState

191idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

194idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

192 emptyContext emptyContext emptyContext emptyContext

195 emptyContext emptyContext emptyContext emptyContext

193 emptyContext emptyContext emptyContext emptyContext

196 emptyContext emptyContext emptyContext emptyContext

194 emptyContext

197 emptyContext

195 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

198 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

196 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

199 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

197− True defaultTheme stdout

200+ True defaultTheme stdout []

198

201

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

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

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

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

@@ -379,6 +382,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

379 -- a function argument, and further evaluation resutls

382 -- a function argument, and further evaluation resutls

380 | Implicit -- implicit coercion

383 | Implicit -- implicit coercion

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

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

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

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

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

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

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

384 deriving (Show, Eq)

388 deriving (Show, Eq)

src/Idris/ElabDecls.hs+11

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

112 addIBC (IBCFlags n opts')

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

114 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+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

118+ when (ErrorHandler `elem` opts) $ do

119+ if errorReflection

120+ then do

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

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

123+ i <- getIState

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

125+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

115 when corec $ do setAccessibility n Frozen

126 when corec $ do setAccessibility n Frozen

116 addIBC (IBCAccess n Frozen)

127 addIBC (IBCAccess n Frozen)

117 return usety

128 return usety

src/Idris/IBC.hs+3−1

@@ -634,7 +634,7 @@ instance Binary NameType where

634 _ -> error "Corrupted binary data for NameType"

635

636

637−instance {-(Binary n) =>-} Binary (TT Name) where

637+instance {- (Binary n) => -} Binary (TT Name) where

638 put x

639 = {-# SCC "putTT" #-}

640 case x of

@@ -976,6 +976,7 @@ instance Binary FnOpt where

976 PartialFn -> putWord8 6

977 Implicit -> putWord8 7

978 Reflection -> putWord8 8

979+ ErrorHandler -> putWord8 9

979 get

980 get

980 = do i <- getWord8

981 = do i <- getWord8

981 case i of

982 case i of

@@ -989,6 +990,7 @@ instance Binary FnOpt where

989 6 -> return PartialFn

990 6 -> return PartialFn

990 7 -> return Implicit

991 7 -> return Implicit

991 8 -> return Reflection

992 8 -> return Reflection

993+ 9 -> return ErrorHandler

992 _ -> error "Corrupted binary data for FnOpt"

994 _ -> error "Corrupted binary data for FnOpt"

993

995

994instance Binary Fixity where

996instance Binary Fixity where

src/Idris/Parser.hs+3

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

309 | 'partial'

310 | 'implicit'

311 | '%' 'assert_total'

312+ | '%' 'error_handler'

312 | '%' 'reflection'

313 | '%' 'reflection'

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

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

314 ;

315 ;

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

330 fnOpts (CExport c : opts)

331 fnOpts (CExport c : opts)

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

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

332 fnOpts (AssertTotal : opts)

333 fnOpts (AssertTotal : opts)

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

335+ fnOpts (ErrorHandler : opts)

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

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

334 fnOpts (Reflection : opts)

337 fnOpts (Reflection : opts)

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

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