1f67398 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Specific-function error reflection: basic infrastructure

1f67398David Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+10

compare with master

unifiedsplit

@@ -26,6 +26,7 @@ import Data.Char

26import qualified Data.Text as T

27import Data.Either

28import Data.Maybe

29+import qualified Data.Set as S

29import Data.Word (Word)

30import Data.Word (Word)

31import Debug.Trace

32import Debug.Trace

@@ -148,6 +149,15 @@ addToCG n cg

148 = do i <- getIState

149 = do i <- getIState

149 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

150 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

150

151

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+

151-- Trace all the names in a call graph starting at the given name

161-- Trace all the names in a call graph starting at the given name

152getAllNames :: Name -> Idris [Name]

162getAllNames :: Name -> Idris [Name]

153getAllNames n = allNames [] n

163getAllNames n = allNames [] n

src/Idris/AbsSyntaxTree.hs+5−3

@@ -26,6 +26,7 @@ import Data.List

26import Data.Char

27import qualified Data.Text as T

28import Data.Either

29+import qualified Data.Set as S

29import Data.Word (Word)

30import Data.Word (Word)

31import Debug.Trace

32import Debug.Trace

@@ -133,8 +134,9 @@ data IState = IState {

133 idris_colourRepl :: Bool,

134 idris_colourRepl :: Bool,

134 idris_colourTheme :: ColourTheme,

135 idris_colourTheme :: ColourTheme,

135 idris_outh :: Handle,

136 idris_outh :: Handle,

136− idris_errorhandlers :: [Name],

137+ idris_errorhandlers :: [Name], -- ^ Global error handlers

137− idris_nameIdx :: (Int, Ctxt (Int, Name))

138+ idris_nameIdx :: (Int, Ctxt (Int, Name)),

139+ idris_function_errorhandlers :: Ctxt (S.Set Name) -- ^ Specific error handlers

138 }

140 }

139

141

140data SizeChange = Smaller | Same | Bigger | Unknown

142data SizeChange = Smaller | Same | Bigger | Unknown

@@ -200,7 +202,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

200 emptyContext

202 emptyContext

201 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

203 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

202 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

204 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

203− True defaultTheme stdout [] (0, emptyContext)

205+ True defaultTheme stdout [] (0, emptyContext) emptyContext

204

206

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

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

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

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

src/Idris/ElabTerm.hs+14−7

@@ -427,8 +427,8 @@ elab ist info pattern opts fn tm

427 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

428 solve

429 ivs' <- get_instances

430− -- Attempt to resolve any type classes which have 'complete' types,

430+ -- Attempt to resolve any type classes which have 'complete' types,

431− -- i.e. no holes in them

431+ -- i.e. no holes in them

432 when (not pattern || (ina && not tcgen && not guarded)) $

433 mapM_ (\n -> do focus n

434 g <- goal

@@ -638,14 +638,21 @@ elab ist info pattern opts fn tm

638 failed' <- -- trace (show (n, t, hs, tm)) $

639 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

640 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

646 False -> return failed

642 False -> return failed

647 elabArgs ina failed fc r ns args

643 elabArgs ina failed fc r ns args

648

644

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+

649-- For every alternative, look at the function at the head. Automatically resolve

656-- For every alternative, look at the function at the head. Automatically resolve

650-- any nested alternatives where that function is also at the head

657-- any nested alternatives where that function is also at the head

651

658

src/Idris/Parser.hs+27−19

@@ -813,19 +813,20 @@ StringList ::=

813

814Directive ::= '%' Directive';

815

816−Directive' ::= 'lib' CodeGen String_t

816+Directive' ::= 'lib' CodeGen String_t

817− | 'link' CodeGen String_t

817+ | 'link' CodeGen String_t

818− | 'flag' CodeGen String_t

818+ | 'flag' CodeGen String_t

819− | 'include' CodeGen String_t

819+ | 'include' CodeGen String_t

820− | 'hide' Name

820+ | 'hide' Name

821− | 'freeze' Name

821+ | 'freeze' Name

822− | 'access' Accessibility

822+ | 'access' Accessibility

823− | 'default' Totality

823+ | 'default' Totality

824− | 'logging' Natural

824+ | 'logging' Natural

825− | 'dynamic' StringList

825+ | 'dynamic' StringList

826− | 'name' Name NameList

826+ | 'name' Name NameList

827+ | 'error_handlers' Name NameList

827− | 'language' 'TypeProviders'

828+ | 'language' 'TypeProviders'

828− | 'language' 'ErrorReflection'

829+ | 'language' 'ErrorReflection'

829 ;

830 ;

830-}

831-}

831directive :: SyntaxInfo -> IdrisParser [PDecl]

832directive :: SyntaxInfo -> IdrisParser [PDecl]

@@ -870,16 +871,23 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

870 ty <- iName []

871 ty <- iName []

871 ns <- sepBy1 name (lchar ',')

872 ns <- sepBy1 name (lchar ',')

872 return [PDirective

873 return [PDirective

873− (do i <- getIState

874+ (do ty' <- disambiguate ty

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)))

878 mapM_ (addNameHint ty') ns

875 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]

880 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

882 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

881 return [PDirective (addLangExt ext)]

883 return [PDirective (addLangExt ext)]

882 <?> "directive"

884 <?> "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))

883

891

884pLangExt :: IdrisParser LanguageExt

892pLangExt :: IdrisParser LanguageExt

885pLangExt = (reserved "TypeProviders" >> return TypeProviders)

893pLangExt = (reserved "TypeProviders" >> return TypeProviders)