git.iko.soy/Idris-dev
on master help sign in
Check the type of elaborated error handlers
acf4b24David Christiansen
libs/base/Language/Reflection/Errors.idr+3−3
compare with master
unifiedsplit
@@ -34,9 +34,9 @@ data Err = Msg String
34 | ProviderError String
34 | ProviderError String
35
35
36-- | Error reports are a list of report parts
36-- | Error reports are a list of report parts
37−data ErrorReport = Message String
37+data ErrorReportPart = Message String
38− | Name TTName
38+ | Name TTName
39− | Term TT
39+ | Term TT
40
40
41
41
42-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
42-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
src/Idris/ElabDecls.hs+16−4
@@ -117,11 +117,13 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
117 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
117 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
118 when (ErrorHandler `elem` opts) $ do
118 when (ErrorHandler `elem` opts) $ do
119 if errorReflection
119 if errorReflection
120− then do
120+ then
121 -- TODO: Check that the declared type is the correct type for an error handler:
121 -- TODO: Check that the declared type is the correct type for an error handler:
122− -- handler : List (TTName, TT) -> Err -> ErrorReport
122+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
123+ if tyIsHandler nty'
123− i <- getIState
124+ then do i <- getIState
124− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
125+ putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
126+ else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
125 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
127 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
126 when corec $ do setAccessibility n Frozen
128 when corec $ do setAccessibility n Frozen
127 addIBC (IBCAccess n Frozen)
129 addIBC (IBCAccess n Frozen)
@@ -135,6 +137,16 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
135 | otherwise = mergeTy sc sc'
137 | otherwise = mergeTy sc sc'
136 mergeTy _ sc = sc
138 mergeTy _ sc = sc
137
139
140+ tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))
141+ (App (P _ (NS (UN "Maybe") ns2) _)
142+ (App (P _ (NS (UN "List") ns3) _)
143+ (P _ (NS (UN "ErrorReportPart") ns4) _))))
144+ | ns1 == ["Errors","Reflection","Language"]
145+ , ns2 == ["Maybe", "Prelude"]
146+ , ns3 == ["List", "Prelude"]
147+ , ns4 == ["Errors","Reflection","Language"] = True
148+ tyIsHandler _ = False
149+
138
150
139elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
151elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
140 FC -> FnOpts -> Name -> PTerm -> Idris ()
152 FC -> FnOpts -> Name -> PTerm -> Idris ()