git.iko.soy/Idris-dev
on master help sign in
Specific-function error reflection: basic infrastructure
commit1f67398800c496bfbba9905107b2362bf2926a88 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 22 Jan 2014, 17:40 (13 years ago) parent6b811a4
4 files changed+56−29
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+10 src/Idris/AbsSyntaxTree.hs+5−3 src/Idris/ElabTerm.hs+14−7 src/Idris/Parser.hs+27−19
src/Idris/AbsSyntax.hs+10
@@ -26,6 +26,7 @@ import Data.Char
2626import qualified Data.Text as T
2727import Data.Either
2828import Data.Maybe
29+import qualified Data.Set as S
2930import Data.Word (Word)
3031
3132import Debug.Trace
@@ -148,6 +149,15 @@ addToCG n cg
148149 = do i <- getIState
149150 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
150151
152+-- | Adds hs as error handlers for n. If n is ambiguous, all matching ns are updated.
153+addFunctionErrorHandlers :: Name -> [Name] -> Idris ()
154+addFunctionErrorHandlers n hs = do i <- getIState
155+ let currentHandlers = idris_function_errorhandlers i
156+ let newHandlers = updateDef n
157+ (\handlers -> handlers `S.union` S.fromList hs)
158+ currentHandlers
159+ putIState $ i { idris_function_errorhandlers = newHandlers }
160+
151161-- Trace all the names in a call graph starting at the given name
152162getAllNames :: Name -> Idris [Name]
153163getAllNames n = allNames [] n
src/Idris/AbsSyntaxTree.hs+5−3
@@ -26,6 +26,7 @@ import Data.List
2626import Data.Char
2727import qualified Data.Text as T
2828import Data.Either
29+import qualified Data.Set as S
2930import Data.Word (Word)
3031
3132import Debug.Trace
@@ -133,8 +134,9 @@ data IState = IState {
133134 idris_colourRepl :: Bool,
134135 idris_colourTheme :: ColourTheme,
135136 idris_outh :: Handle,
136− idris_errorhandlers :: [Name],
137− idris_nameIdx :: (Int, Ctxt (Int, Name))
137+ idris_errorhandlers :: [Name], -- ^ Global error handlers
138+ idris_nameIdx :: (Int, Ctxt (Int, Name)),
139+ idris_function_errorhandlers :: Ctxt (S.Set Name) -- ^ Specific error handlers
138140 }
139141
140142data SizeChange = Smaller | Same | Bigger | Unknown
@@ -200,7 +202,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
200202 emptyContext
201203 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
202204 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
203− True defaultTheme stdout [] (0, emptyContext)
205+ True defaultTheme stdout [] (0, emptyContext) emptyContext
204206
205207-- | The monad for the main REPL - reading and processing files and updating
206208-- global state (hence the IO inner monad).
src/Idris/ElabTerm.hs+14−7
@@ -427,8 +427,8 @@ elab ist info pattern opts fn tm
427427 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
428428 solve
429429 ivs' <- get_instances
430− -- Attempt to resolve any type classes which have 'complete' types,
431− -- i.e. no holes in them
430+ -- Attempt to resolve any type classes which have 'complete' types,
431+ -- i.e. no holes in them
432432 when (not pattern || (ina && not tcgen && not guarded)) $
433433 mapM_ (\n -> do focus n
434434 g <- goal
@@ -638,14 +638,21 @@ elab ist info pattern opts fn tm
638638 failed' <- -- trace (show (n, t, hs, tm)) $
639639 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
640640 case n `elem` hs of
641− True ->
642−-- if r
643−-- then try (do focus n; elabE ina t; return failed)
644−-- (return ((n,(lazy, t)):failed))
645− do focus n; elabE ina t; return failed
641+ True -> do focus n; elabE ina t; return failed
646642 False -> return failed
647643 elabArgs ina failed fc r ns args
648644
645+-- | Perform error reflection for functions with specific error handlers
646+reflectFunctionErrors :: IState -> Name -> ElabD a -> ElabD a
647+reflectFunctionErrors ist f action =
648+ do elabState <- get
649+ (result, newState) <- case runStateT action elabState of
650+ OK (res, newState) -> return (res, newState)
651+ Error e -> lift (tfail e) -- TODO: actual error reflection!
652+ put newState
653+ return result
654+
655+
649656-- For every alternative, look at the function at the head. Automatically resolve
650657-- any nested alternatives where that function is also at the head
651658
src/Idris/Parser.hs+27−19
@@ -813,19 +813,20 @@ StringList ::=
813813
814814Directive ::= '%' Directive';
815815
816−Directive' ::= 'lib' CodeGen String_t
817− | 'link' CodeGen String_t
818− | 'flag' CodeGen String_t
819− | 'include' CodeGen String_t
820− | 'hide' Name
821− | 'freeze' Name
822− | 'access' Accessibility
823− | 'default' Totality
824− | 'logging' Natural
825− | 'dynamic' StringList
826− | 'name' Name NameList
827− | 'language' 'TypeProviders'
828− | 'language' 'ErrorReflection'
816+Directive' ::= 'lib' CodeGen String_t
817+ | 'link' CodeGen String_t
818+ | 'flag' CodeGen String_t
819+ | 'include' CodeGen String_t
820+ | 'hide' Name
821+ | 'freeze' Name
822+ | 'access' Accessibility
823+ | 'default' Totality
824+ | 'logging' Natural
825+ | 'dynamic' StringList
826+ | 'name' Name NameList
827+ | 'error_handlers' Name NameList
828+ | 'language' 'TypeProviders'
829+ | 'language' 'ErrorReflection'
829830 ;
830831-}
831832directive :: SyntaxInfo -> IdrisParser [PDecl]
@@ -870,16 +871,23 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
870871 ty <- iName []
871872 ns <- sepBy1 name (lchar ',')
872873 return [PDirective
873− (do i <- getIState
874− ty' <- case lookupCtxtName ty (idris_implicits i) of
875− [(tyn, _)] -> return tyn
876− [] -> throwError (NoSuchVariable ty)
877− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
874+ (do ty' <- disambiguate ty
878875 mapM_ (addNameHint ty') ns
879− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
876+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
877+ <|> do try (lchar '%' *> reserved "error_handlers")
878+ fn <- iName []
879+ ns <- sepBy1 name (lchar ',')
880+ return [PDirective $ do n' <- disambiguate fn
881+ addFunctionErrorHandlers fn ns]
880882 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
881883 return [PDirective (addLangExt ext)]
882884 <?> "directive"
885+ where disambiguate :: Name -> Idris Name
886+ disambiguate n = do i <- getIState
887+ case lookupCtxtName n (idris_implicits i) of
888+ [(n', _)] -> return n'
889+ [] -> throwError (NoSuchVariable n)
890+ more -> throwError (CantResolveAlts (map (show . fst) more))
883891
884892pLangExt :: IdrisParser LanguageExt
885893pLangExt = (reserved "TypeProviders" >> return TypeProviders)