git.iko.soy/Idris-dev
on master help sign in
Merge pull request #775 from david-christiansen/error-reflection
ebc5318Edwin Brady
idris.cabal+6
compare with master
unifiedsplit
@@ -303,6 +303,12 @@ Extra-source-files:
303 test/test035/run
303 test/test035/run
304 test/test035/expected
304 test/test035/expected
305 test/test035/*.idr
305 test/test035/*.idr
306+ test/test036/run
307+ test/test036/expected
308+ test/test036/*.idr
309+ test/test037/run
310+ test/test037/expected
311+ test/test037/*.idr
306
312
307source-repository head
313source-repository head
308 type: git
314 type: git
libs/base/Language/Reflection.idr+11−2
@@ -10,6 +10,7 @@ data TTName = UN String
10 -- ^ Machine chosen names
10 -- ^ Machine chosen names
11 | NErased
11 | NErased
12 -- ^ Name of somethng which is never used in scope
12 -- ^ Name of somethng which is never used in scope
13+%name TTName n, n'
13
14
14implicit
15implicit
15userSuppliedName : String -> TTName
16userSuppliedName : String -> TTName
@@ -19,6 +20,7 @@ data TTUExp = UVar Int
19 -- ^ universe variable
20 -- ^ universe variable
20 | UVal Int
21 | UVal Int
21 -- ^ explicit universe variable
22 -- ^ explicit universe variable
23+%name TTUExp uexp
22
24
23-- | Primitive constants
25-- | Primitive constants
24data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
26data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
@@ -27,6 +29,8 @@ data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
27 | B8Type | B16Type | B32Type | B64Type
29 | B8Type | B16Type | B32Type | B64Type
28 | PtrType | VoidType | Forgot
30 | PtrType | VoidType | Forgot
29
31
32+%name Const c, c'
33+
30abstract class ReflConst (a : Type) where
34abstract class ReflConst (a : Type) where
31 toConst : a -> Const
35 toConst : a -> Const
32
36
@@ -71,6 +75,7 @@ data NameType = Bound
71 -- ^ constructor with tag and number
75 -- ^ constructor with tag and number
72 | TCon Int Int
76 | TCon Int Int
73 -- ^ type constructor with tag and number
77 -- ^ type constructor with tag and number
78+%name NameType nt, nt'
74
79
75-- | Types annotations for bound variables in different
80-- | Types annotations for bound variables in different
76-- binding contexts
81-- binding contexts
@@ -83,7 +88,7 @@ data Binder a = Lam a
83 | Guess a a
88 | Guess a a
84 | PVar a
89 | PVar a
85 | PVTy a
90 | PVTy a
86−
91+%name Binder b, b'
87
92
88instance Functor Binder where
93instance Functor Binder where
89 map f (Lam x) = Lam (f x)
94 map f (Lam x) = Lam (f x)
@@ -139,6 +144,8 @@ data TT = P NameType TTName TT
139 | TType TTUExp
144 | TType TTUExp
140 -- ^ types
145 -- ^ types
141
146
147+%name TT tm, tm'
148+
142-- | Raw terms without types
149-- | Raw terms without types
143data Raw = Var TTName
150data Raw = Var TTName
144 | RBind TTName (Binder Raw) Raw
151 | RBind TTName (Binder Raw) Raw
@@ -147,6 +154,8 @@ data Raw = Var TTName
147 | RForce Raw
154 | RForce Raw
148 | RConstant Const
155 | RConstant Const
149
156
157+%name Raw tm, tm'
158+
150data Tactic = Try Tactic Tactic
159data Tactic = Try Tactic Tactic
151 -- ^ try the first tactic and resort to the second one on failure
160 -- ^ try the first tactic and resort to the second one on failure
152 | GoalType String Tactic
161 | GoalType String Tactic
@@ -185,4 +194,4 @@ data Tactic = Try Tactic Tactic
185 -- ^ name a reflected term and type it
194 -- ^ name a reflected term and type it
186 | Compute
195 | Compute
187 -- ^ normalise the context
196 -- ^ normalise the context
188−
197+%name Tactic tac, tac'
libs/base/Language/Reflection/Errors.idr+17−6
@@ -2,7 +2,10 @@ module Language.Reflection.Errors
2
2
3import Language.Reflection
3import Language.Reflection
4
4
5−data SourceLocation = FileLoc String Int
5+record SourceLocation : Type where
6+ FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation
7+
8+%name SourceLocation loc
6
9
7data Err = Msg String
10data Err = Msg String
8 | InternalMsg String
11 | InternalMsg String
@@ -15,13 +18,15 @@ data Err = Msg String
15 | UnifyScope TTName TTName TT (List (TTName, TT))
18 | UnifyScope TTName TTName TT (List (TTName, TT))
16 | CantInferType String
19 | CantInferType String
17 | NonFunctionType TT TT
20 | NonFunctionType TT TT
21+ | NotEquality TT TT
22+ | TooManyArguments TTName
18 | CantIntroduce TT
23 | CantIntroduce TT
19 | NoSuchVariable TTName
24 | NoSuchVariable TTName
20 | NoTypeDecl TTName
25 | NoTypeDecl TTName
21 | NotInjective TT TT TT
26 | NotInjective TT TT TT
22 | CantResolve TT
27 | CantResolve TT
23 | CantResolveAlts (List String)
28 | CantResolveAlts (List String)
24− | IncompleteTT TT
29+ | IncompleteTerm TT
25 | UniverseError
30 | UniverseError
26 | ProgramLineComment
31 | ProgramLineComment
27 | Inaccessible TTName
32 | Inaccessible TTName
@@ -32,11 +37,17 @@ data Err = Msg String
32 | At SourceLocation Err
37 | At SourceLocation Err
33 | Elaborating String TTName Err
38 | Elaborating String TTName Err
34 | ProviderError String
39 | ProviderError String
40+ | LoadingFailed String Err
35
41
36−-- | Error reports are a list of report parts
42+%name Err err, e
37−data ErrorReport = Message String
38− | Name TTName
39− | Term TT
40
43
44+-- | Error reports are a list of report parts
45+data ErrorReportPart = TextPart String
46+ | NamePart TTName
47+ | TermPart TT
48+ | SubReport (List ErrorReportPart)
49+%name ErrorReportPart part, p
41
50
42-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
51-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
52+ErrorHandler : Type
53+ErrorHandler = Err -> Maybe (List ErrorReportPart)
libs/base/Language/Reflection/Utils.idr+71
@@ -1,6 +1,7 @@
1module Language.Reflection.Utils
1module Language.Reflection.Utils
2
2
3import Language.Reflection
3import Language.Reflection
4+import Language.Reflection.Errors
4
5
5--------------------------------------------------------
6--------------------------------------------------------
6-- Tactic construction conveniences
7-- Tactic construction conveniences
@@ -185,3 +186,73 @@ instance Eq TT where
185 equalp Impossible Impossible = True
186 equalp Impossible Impossible = True
186 equalp (TType u) (TType u') = u == u'
187 equalp (TType u) (TType u') = u == u'
187 equalp x y = False
188 equalp x y = False
189+
190+total
191+forget : TT -> Maybe Raw
192+forget tm = fe [] tm
193+ where
194+ atIndex : List a -> Int -> Maybe a
195+ atIndex [] _ = Nothing
196+ atIndex (x::xs) n =
197+ case compare n 0 of
198+ EQ => Just x
199+ LT => Nothing
200+ GT => atIndex xs (n-1)
201+
202+ %assert_total
203+ fe : List TTName -> TT -> Maybe Raw
204+ fe env (P _ n _) = Just $ Var n
205+ fe env (V i) = map Var (atIndex env i)
206+ fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
207+ fe env (App f a) = [| RApp (fe env f) (fe env a) |]
208+ fe env (TConst c) = Just $ RConstant c
209+ fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
210+ fe env (TType i) = Just RType
211+ fe env Erased = Just $ RConstant Forgot
212+ fe env Impossible = Nothing
213+
214+instance Show Raw where
215+ show r = my_show r
216+ where %assert_total my_show : Raw -> String
217+ my_show (Var n) = "Var " ++ show n
218+ my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
219+ my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
220+ my_show RType = "RType"
221+ my_show (RForce tm) = "RForce " ++ my_show tm
222+ my_show (RConstant c) = "RConstant " ++ show c
223+
224+instance Show SourceLocation where
225+ show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
226+
227+instance Show Err where
228+ show (Msg x) = "Msg \"" ++ x ++ "\""
229+ show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
230+ show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
231+ " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
232+ show xs ++ " " ++ show y
233+ show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
234+ show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
235+ show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
236+ show (CantInferType x) = "CantInferType " ++ show x
237+ show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
238+ show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
239+ show (TooManyArguments n) = "TooManyArguments " ++ show n
240+ show (CantIntroduce tm) = "CantIntroduce " ++ show tm
241+ show (NoSuchVariable n) = "NoSuchVariable " ++ show n
242+ show (NoTypeDecl n) = "NoTypeDecl " ++ show n
243+ show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
244+ show (CantResolve tm) = "CantResolve " ++ show tm
245+ show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
246+ show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
247+ show UniverseError = "UniverseError"
248+ show ProgramLineComment = "ProgramLineComment"
249+ show (Inaccessible n) = "Inaccessible " ++ show n
250+ show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
251+ show (AlreadyDefined n) = "AlreadyDefined " ++ show n
252+ show (ProofSearchFail err) = "ProofSearchFail " ++ show err
253+ show (NoRewriting tm) = "NoRewriting " ++ show tm
254+ show (At loc err) = "At " ++ show loc ++ " " ++ show err
255+ show (Elaborating x n err) = "Elaborating " ++ show x ++ " " ++ show x ++ " " ++ show n ++ " (" ++ show err ++ ")"
256+ show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
257+ show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
258+
src/Idris/AbsSyntaxTree.hs+7−2
@@ -131,7 +131,8 @@ data IState = IState {
131 idris_outputmode :: OutputMode,
131 idris_outputmode :: OutputMode,
132 idris_colourRepl :: Bool,
132 idris_colourRepl :: Bool,
133 idris_colourTheme :: ColourTheme,
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
@@ -189,13 +190,15 @@ data IBCWrite = IBCFix FixDecl
189 | IBCLineApp FilePath Int PTerm
190 | IBCLineApp FilePath Int PTerm
190 deriving Show
191 deriving Show
191
192
193+-- | The initial state for the compiler
194+idrisInit :: IState
192idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
195idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
193 emptyContext emptyContext emptyContext emptyContext
196 emptyContext emptyContext emptyContext emptyContext
194 emptyContext emptyContext emptyContext emptyContext
197 emptyContext emptyContext emptyContext emptyContext
195 emptyContext
198 emptyContext
196 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
199 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
197 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
200 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
198− True defaultTheme stdout
201+ True defaultTheme stdout []
199
202
200-- | The monad for the main REPL - reading and processing files and updating
203-- | The monad for the main REPL - reading and processing files and updating
201-- global state (hence the IO inner monad).
204-- global state (hence the IO inner monad).
@@ -258,6 +261,7 @@ data Command = Quit
258 | SetColour ColourType IdrisColour
261 | SetColour ColourType IdrisColour
259 | ColourOn
262 | ColourOn
260 | ColourOff
263 | ColourOff
264+ | ListErrorHandlers
261
265
262data Opt = Filename String
266data Opt = Filename String
263 | Ver
267 | Ver
@@ -380,6 +384,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
380 -- a function argument, and further evaluation resutls
384 -- a function argument, and further evaluation resutls
381 | Implicit -- implicit coercion
385 | Implicit -- implicit coercion
382 | CExport String -- export, with a C name
386 | CExport String -- export, with a C name
387+ | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
383 | Reflection -- a reflecting function, compile-time only
388 | Reflection -- a reflecting function, compile-time only
384 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
389 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
385 deriving (Show, Eq)
390 deriving (Show, Eq)
src/Idris/Core/Execute.hs−8
@@ -499,14 +499,6 @@ getFTy (EP _ (UN t) _) =
499 _ -> Nothing
499 _ -> Nothing
500getFTy _ = Nothing
500getFTy _ = Nothing
501
501
502−unList :: Term -> Maybe [Term]
503−unList tm = case unApply tm of
504− (nil, [_]) -> Just []
505− (cons, ([_, x, xs])) ->
506− do rest <- unList xs
507− return $ x:rest
508− (f, args) -> Nothing
509−
510unEList :: ExecVal -> Maybe [ExecVal]
502unEList :: ExecVal -> Maybe [ExecVal]
511unEList tm = case unApplyV tm of
503unEList tm = case unApplyV tm of
512 (nil, [_]) -> Just []
504 (nil, [_]) -> Just []
src/Idris/Core/TT.hs+53−30
@@ -74,37 +74,52 @@ instance Sized FC where
74instance Show FC where
74instance Show FC where
75 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
75 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
76
76
77+-- | Used for error reflection
78+data ErrorReportPart = TextPart String
79+ | NamePart Name
80+ | TermPart Term
81+ | SubReport [ErrorReportPart]
82+ deriving (Show, Eq)
83+
84+
85+-- Please remember to keep Err synchronised with
86+-- Language.Reflection.Errors.Err in the stdlib!
87+
88+-- | Idris errors. Used as exceptions in the compiler, but reported to users
89+-- if they reach the top level.
77data Err = Msg String
90data Err = Msg String
78− | InternalMsg String
91+ | InternalMsg String
79− | CantUnify Bool Term Term Err [(Name, Type)] Int
92+ | CantUnify Bool Term Term Err [(Name, Type)] Int
80− -- Int is 'score' - how much we did unify
93+ -- Int is 'score' - how much we did unify
81− -- Bool indicates recoverability, True indicates more info may make
94+ -- Bool indicates recoverability, True indicates more info may make
82− -- unification succeed
95+ -- unification succeed
83− | InfiniteUnify Name Term [(Name, Type)]
96+ | InfiniteUnify Name Term [(Name, Type)]
84− | CantConvert Term Term [(Name, Type)]
97+ | CantConvert Term Term [(Name, Type)]
85− | UnifyScope Name Name Term [(Name, Type)]
98+ | UnifyScope Name Name Term [(Name, Type)]
86− | CantInferType String
99+ | CantInferType String
87− | NonFunctionType Term Term
100+ | NonFunctionType Term Term
88− | NotEquality Term Term
101+ | NotEquality Term Term
89− | TooManyArguments Name
102+ | TooManyArguments Name
90− | CantIntroduce Term
103+ | CantIntroduce Term
91− | NoSuchVariable Name
104+ | NoSuchVariable Name
92− | NoTypeDecl Name
105+ | NoTypeDecl Name
93− | NotInjective Term Term Term
106+ | NotInjective Term Term Term
94− | CantResolve Term
107+ | CantResolve Term
95− | CantResolveAlts [String]
108+ | CantResolveAlts [String]
96− | IncompleteTerm Term
109+ | IncompleteTerm Term
97− | UniverseError
110+ | UniverseError
98− | ProgramLineComment
111+ | ProgramLineComment
99− | Inaccessible Name
112+ | Inaccessible Name
100− | NonCollapsiblePostulate Name
113+ | NonCollapsiblePostulate Name
101− | AlreadyDefined Name
114+ | AlreadyDefined Name
102− | ProofSearchFail Err
115+ | ProofSearchFail Err
103− | NoRewriting Term
116+ | NoRewriting Term
104− | At FC Err
117+ | At FC Err
105− | Elaborating String Name Err
118+ | Elaborating String Name Err
106− | ProviderError String
119+ | ProviderError String
107− | LoadingFailed String Err
120+ | LoadingFailed String Err
121+ | ReflectionError [[ErrorReportPart]] Err
122+ | ReflectionFailed String Err
108 deriving Eq
123 deriving Eq
109{-!
124{-!
110deriving instance NFData Err
125deriving instance NFData Err
@@ -793,6 +808,14 @@ mkApp :: TT n -> [TT n] -> TT n
793mkApp f [] = f
808mkApp f [] = f
794mkApp f (a:as) = mkApp (App f a) as
809mkApp f (a:as) = mkApp (App f a) as
795
810
811+unList :: Term -> Maybe [Term]
812+unList tm = case unApply tm of
813+ (nil, [_]) -> Just []
814+ (cons, ([_, x, xs])) ->
815+ do rest <- unList xs
816+ return $ x:rest
817+ (f, args) -> Nothing
818+
796forget :: TT Name -> Raw
819forget :: TT Name -> Raw
797forget tm = fe [] tm
820forget tm = fe [] tm
798 where
821 where
src/Idris/Delaborate.hs+16
@@ -9,6 +9,8 @@ import Idris.AbsSyntax
9import Idris.Core.TT
9import Idris.Core.TT
10import Idris.Core.Evaluate
10import Idris.Core.Evaluate
11
11
12+import Data.List (intersperse)
13+
12import Debug.Trace
14import Debug.Trace
13
15
14bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
16bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
@@ -190,6 +192,20 @@ pshow i (Elaborating s n e) = "When elaborating " ++ s ++
190 showqual i n ++ ":\n" ++ pshow i e
192 showqual i n ++ ":\n" ++ pshow i e
191pshow i (ProviderError msg) = "Type provider error: " ++ msg
193pshow i (ProviderError msg) = "Type provider error: " ++ msg
192pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e
194pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e
195+pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
196+ concat (intersperse "\n" parts') ++
197+ "\nOriginal error:\n" ++ indented (pshow i orig)
198+ where showPart :: ErrorReportPart -> String
199+ showPart (TextPart str) = str
200+ showPart (NamePart n) = let colour = idris_colourRepl i in
201+ showName (Just i) [] False colour n
202+ showPart (TermPart tm) = let colour = idris_colourRepl i
203+ in showImp (Just i) False colour (delab i tm)
204+ showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
205+pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
206+ indented (pshow i err) ++
207+ "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
208+
193
209
194showSc i [] = ""
210showSc i [] = ""
195showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
211showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
src/Idris/ElabDecls.hs+24−1
@@ -112,6 +112,19 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
112 addIBC (IBCFlags n opts')
112 addIBC (IBCFlags n opts')
113 when (Implicit `elem` opts) $ do addCoercion n
113 when (Implicit `elem` opts) $ do addCoercion n
114 addIBC (IBCCoercion 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
121+ -- TODO: Check that the declared type is the correct type for an error handler:
122+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
123+ if tyIsHandler nty'
124+ then do i <- getIState
125+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
126+ else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
127+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
115 when corec $ do setAccessibility n Frozen
128 when corec $ do setAccessibility n Frozen
116 addIBC (IBCAccess n Frozen)
129 addIBC (IBCAccess n Frozen)
117 return usety
130 return usety
@@ -124,6 +137,16 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
124 | otherwise = mergeTy sc sc'
137 | otherwise = mergeTy sc sc'
125 mergeTy _ sc = sc
138 mergeTy _ sc = sc
126
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+
127
150
128elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
151elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
129 FC -> FnOpts -> Name -> PTerm -> Idris ()
152 FC -> FnOpts -> Name -> PTerm -> Idris ()
@@ -1980,7 +2003,7 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds
1980
2003
1981elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
2004elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
1982elabDecl what info d
2005elabDecl what info d
1983− = idrisCatch (elabDecl' what info d) (setAndReport)
2006+ = idrisCatch (withErrorReflection $ elabDecl' what info d) (setAndReport)
1984
2007
1985elabDecl' _ info (PFix _ _ _)
2008elabDecl' _ info (PFix _ _ _)
1986 = return () -- nothing to elaborate
2009 = return () -- nothing to elaborate
src/Idris/ElabTerm.hs+169−4
@@ -5,15 +5,18 @@ module Idris.ElabTerm where
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.DSL
6import Idris.DSL
7import Idris.Delaborate
7import Idris.Delaborate
8+import Idris.Error
8import Idris.ProofSearch
9import Idris.ProofSearch
9
10
10import Idris.Core.Elaborate hiding (Tactic(..))
11import Idris.Core.Elaborate hiding (Tactic(..))
11import Idris.Core.TT
12import Idris.Core.TT
12import Idris.Core.Evaluate
13import Idris.Core.Evaluate
14+import Idris.Core.Typecheck (check)
13
15
14import Control.Monad
16import Control.Monad
15import Control.Monad.State
17import Control.Monad.State
16import Data.List
18import Data.List
19+import Data.Maybe (mapMaybe)
17
20
18import Debug.Trace
21import Debug.Trace
19
22
@@ -1031,7 +1034,7 @@ runTac autoSolve ist tac
1031 runReflected t = do t' <- reify ist t
1034 runReflected t = do t' <- reify ist t
1032 runTac autoSolve ist t'
1035 runTac autoSolve ist t'
1033
1036
1034−-- | Prefix a name with the "Reflection.Language" namespace
1037+-- | Prefix a name with the "Language.Reflection" namespace
1035reflm :: String -> Name
1038reflm :: String -> Name
1036reflm n = NS (UN n) ["Reflection", "Language"]
1039reflm n = NS (UN n) ["Reflection", "Language"]
1037
1040
@@ -1370,10 +1373,172 @@ reflectEnv = foldr consToEnvList emptyEnvList
1370 [envTupleType]
1373 [envTupleType]
1371
1374
1372-- | Reflect an error into the internal datatype of Idris -- TODO
1375-- | Reflect an error into the internal datatype of Idris -- TODO
1376+rawBool :: Bool -> Raw
1377+rawBool True = Var (NS (UN "True") ["Bool", "Prelude"])
1378+rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])
1379+
1380+rawNil :: Raw -> Raw
1381+rawNil ty = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"])) [ty]
1382+
1383+rawCons :: Raw -> Raw -> Raw -> Raw
1384+rawCons ty hd tl = raw_apply (Var (NS (UN "::") ["List", "Prelude"])) [ty, hd, tl]
1385+
1386+rawList :: Raw -> [Raw] -> Raw
1387+rawList ty = foldr (rawCons ty) (rawNil ty)
1388+
1389+rawPairTy :: Raw -> Raw -> Raw
1390+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
1391+
1392+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
1393+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
1394+
1395+reflectCtxt :: [(Name, Type)] -> Raw
1396+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
1397+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
1398+ (reflectName n, reflect t)))
1399+ ctxt)
1400+
1373reflectErr :: Err -> Raw
1401reflectErr :: Err -> Raw
1374−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1402+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
1375−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1403+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
1376−reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]
1404+reflectErr (CantUnify b t1 t2 e ctxt i) =
1405+ raw_apply (Var $ reflErrName "CantUnify")
1406+ [ rawBool b
1407+ , reflect t1
1408+ , reflect t2
1409+ , reflectErr e
1410+ , reflectCtxt ctxt
1411+ , RConstant (I i)]
1412+reflectErr (InfiniteUnify n tm ctxt) =
1413+ raw_apply (Var $ reflErrName "InfiniteUnify")
1414+ [ reflectName n
1415+ , reflect tm
1416+ , reflectCtxt ctxt
1417+ ]
1418+reflectErr (CantConvert t t' ctxt) =
1419+ raw_apply (Var $ reflErrName "CantConvert")
1420+ [ reflect t
1421+ , reflect t'
1422+ , reflectCtxt ctxt
1423+ ]
1424+reflectErr (UnifyScope n n' t ctxt) =
1425+ raw_apply (Var $ reflErrName "UnifyScope")
1426+ [ reflectName n
1427+ , reflectName n'
1428+ , reflect t
1429+ , reflectCtxt ctxt
1430+ ]
1431+reflectErr (CantInferType str) =
1432+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
1433+reflectErr (NonFunctionType t t') =
1434+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
1435+reflectErr (NotEquality t t') =
1436+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
1437+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
1438+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
1439+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
1440+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
1441+reflectErr (NotInjective t1 t2 t3) =
1442+ raw_apply (Var $ reflErrName "NotInjective")
1443+ [ reflect t1
1444+ , reflect t2
1445+ , reflect t3
1446+ ]
1447+reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
1448+reflectErr (CantResolveAlts ss) =
1449+ raw_apply (Var $ reflErrName "CantResolve")
1450+ [rawList (Var $ (UN "String")) (map (RConstant . Str) ss)]
1451+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
1452+reflectErr UniverseError = Var $ reflErrName "UniverseError"
1453+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
1454+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
1455+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
1456+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
1457+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
1458+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
1459+reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]
1460+ where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")
1461+ [ RConstant (Str source)
1462+ , RConstant (I line)
1463+ , RConstant (I col)
1464+ ]
1465+reflectErr (Elaborating str n e) =
1466+ raw_apply (Var $ reflErrName "Elaborating")
1467+ [ RConstant (Str str)
1468+ , reflectName n
1469+ , reflectErr e
1470+ ]
1471+reflectErr (ProviderError str) =
1472+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
1473+reflectErr (LoadingFailed str err) =
1474+ raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
1475+reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
1476+
1477+withErrorReflection :: Idris a -> Idris a
1478+withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1479+ where handle :: Err -> Idris Err
1480+ handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
1481+ return e -- Don't do meta-reflection of errors
1482+ handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
1483+ return e
1484+ handle e = do ist <- getIState
1485+ logLvl 2 "Starting error reflection"
1486+ let handlers = idris_errorhandlers ist
1487+ logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1488+ let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
1489+
1490+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1491+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1492+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1493+ OK hs -> return hs
1494+
1495+ -- Normalize error handler terms to produce the new messages
1496+ ctxt <- getContext
1497+ let results = map (normalise ctxt []) (map fst handlers)
1498+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1499+
1500+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1501+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1502+ errorparts <- mapM (mapM reifyReportPart) errorpartsTT
1503+
1504+ return $ case errorparts of
1505+ [] -> e
1506+ parts -> ReflectionError errorparts e
1507+
1508+ fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1509+ fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm
1510+ fromTTMaybe x = Nothing
1511+
1512+reflErrName :: String -> Name
1513+reflErrName n = NS (UN n) ["Errors", "Reflection", "Language"]
1514+
1515+reifyReportPart :: Term -> Idris ErrorReportPart
1516+reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
1517+ return (TextPart msg)
1518+reifyReportPart (App (P (DCon _ _) n _) ttn)
1519+ | n == reflErrName "NamePart" =
1520+ case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
1521+ Error e -> ierror . InternalMsg $
1522+ "could not reify name term " ++
1523+ show ttn ++
1524+ " when reflecting an error"
1525+ OK (n', _)-> return $ NamePart n'
1526+reifyReportPart (App (P (DCon _ _) n _) tm)
1527+ | n == reflErrName "TermPart" =
1528+ do ist <- getIState
1529+ case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
1530+ Error e -> ierror . InternalMsg $
1531+ "could not reify reflected term " ++
1532+ show tm ++
1533+ " when reflecting an error"
1534+ OK (tm', _) -> return $ TermPart tm'
1535+reifyReportPart (App (P (DCon _ _) n _) tm)
1536+ | n == reflErrName "SubReport" =
1537+ case unList tm of
1538+ Just xs -> do subParts <- mapM reifyReportPart xs
1539+ return (SubReport subParts)
1540+ Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm
1541+reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x
1377
1542
1378envTupleType :: Raw
1543envTupleType :: Raw
1379envTupleType
1544envTupleType
src/Idris/Error.hs+2
@@ -38,6 +38,7 @@ report e
38idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
38idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
39idrisCatch = catchError
39idrisCatch = catchError
40
40
41+
41setAndReport :: Err -> Idris ()
42setAndReport :: Err -> Idris ()
42setAndReport e = do ist <- getIState
43setAndReport e = do ist <- getIState
43 let h = idris_outh ist
44 let h = idris_outh ist
@@ -71,3 +72,4 @@ getErrLine _ = 0
71getErrColumn :: Err -> Int
72getErrColumn :: Err -> Int
72getErrColumn (At (FC _ _ c) _) = c
73getErrColumn (At (FC _ _ c) _) = c
73getErrColumn _ = 0
74getErrColumn _ = 0
75+
src/Idris/IBC.hs+3−1
@@ -643,7 +643,7 @@ instance Binary NameType where
643 _ -> error "Corrupted binary data for NameType"
643 _ -> error "Corrupted binary data for NameType"
644
644
645
645
646−instance {-(Binary n) =>-} Binary (TT Name) where
646+instance {- (Binary n) => -} Binary (TT Name) where
647 put x
647 put x
648 = {-# SCC "putTT" #-}
648 = {-# SCC "putTT" #-}
649 case x of
649 case x of
@@ -1001,6 +1001,7 @@ instance Binary FnOpt where
1001 PartialFn -> putWord8 6
1001 PartialFn -> putWord8 6
1002 Implicit -> putWord8 7
1002 Implicit -> putWord8 7
1003 Reflection -> putWord8 8
1003 Reflection -> putWord8 8
1004+ ErrorHandler -> putWord8 9
1004 get
1005 get
1005 = do i <- getWord8
1006 = do i <- getWord8
1006 case i of
1007 case i of
@@ -1014,6 +1015,7 @@ instance Binary FnOpt where
1014 6 -> return PartialFn
1015 6 -> return PartialFn
1015 7 -> return Implicit
1016 7 -> return Implicit
1016 8 -> return Reflection
1017 8 -> return Reflection
1018+ 9 -> return ErrorHandler
1017 _ -> error "Corrupted binary data for FnOpt"
1019 _ -> error "Corrupted binary data for FnOpt"
1018
1020
1019instance Binary Fixity where
1021instance Binary Fixity where
src/Idris/Parser.hs+3
@@ -309,6 +309,7 @@ FnOpts ::= 'total'
309 | 'partial'
309 | 'partial'
310 | 'implicit'
310 | 'implicit'
311 | '%' 'assert_total'
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";
src/Idris/REPL.hs+19−13
@@ -436,19 +436,19 @@ process h fn (ChangeDirectory f)
436 = do runIO $ setCurrentDirectory f
436 = do runIO $ setCurrentDirectory f
437 return ()
437 return ()
438process h fn (Eval t)
438process h fn (Eval t)
439− = do (tm, ty) <- elabVal toplevel False t
439+ = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
440− ctxt <- getContext
440+ ctxt <- getContext
441− let tm' = force (normaliseAll ctxt [] tm)
441+ let tm' = force (normaliseAll ctxt [] tm)
442− let ty' = force (normaliseAll ctxt [] ty)
442+ let ty' = force (normaliseAll ctxt [] ty)
443− -- Add value to context, call it "it"
443+ -- Add value to context, call it "it"
444− updateContext (addCtxtDef (UN "it") (Function ty' tm'))
444+ updateContext (addCtxtDef (UN "it") (Function ty' tm'))
445− ist <- getIState
445+ ist <- getIState
446− logLvl 3 $ "Raw: " ++ show (tm', ty')
446+ logLvl 3 $ "Raw: " ++ show (tm', ty')
447− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
447+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
448− imp <- impShow
448+ imp <- impShow
449− c <- colourise
449+ c <- colourise
450− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
450+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
451− showImp (Just ist) imp c (delab ist ty'))
451+ showImp (Just ist) imp c (delab ist ty'))
452process h fn (ExecVal t)
452process h fn (ExecVal t)
453 = do ctxt <- getContext
453 = do ctxt <- getContext
454 ist <- getIState
454 ist <- getIState
@@ -919,6 +919,12 @@ process h fn ColourOn
919process h fn ColourOff
919process h fn ColourOff
920 = do ist <- getIState
920 = do ist <- getIState
921 putIState $ ist { idris_colourRepl = False }
921 putIState $ ist { idris_colourRepl = False }
922+process h fn ListErrorHandlers =
923+ do ist <- getIState
924+ case idris_errorhandlers ist of
925+ [] -> iPrintResult "No registered error handlers"
926+ handlers ->
927+ iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
922
928
923classInfo :: ClassInfo -> Idris ()
929classInfo :: ClassInfo -> Idris ()
924classInfo ci = do iputStrLn "Methods:\n"
930classInfo ci = do iputStrLn "Methods:\n"
src/Idris/REPLParser.hs+1
@@ -96,6 +96,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)
96 eof; return (AddProof n))
96 eof; return (AddProof n))
97 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))
97 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))
98 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))
98 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))
99+ <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)
99 <|> do P.whiteSpace; do eof; return NOP
100 <|> do P.whiteSpace; do eof; return NOP
100 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
101 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
101
102
test/test037/ErrorReflection.idrnew file+79
@@ -0,0 +1,79 @@
1+module Main
2+
3+import Language.Reflection
4+import Language.Reflection.Errors
5+import Language.Reflection.Utils
6+
7+%language ErrorReflection
8+
9+-- Well-typed terms
10+
11+data Ty = TUnit | TFun Ty Ty
12+
13+instance Show Ty where
14+ show TUnit = "()"
15+ show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"
16+
17+using (n : Nat, G : Vect n Ty)
18+ data HasType : Vect n Ty -> Ty -> Type where
19+ Here : HasType (t::G) t
20+ There : HasType G t -> HasType (t' :: G) t
21+
22+ data Tm : Vect n Ty -> Ty -> Type where
23+ U : Tm G TUnit
24+ Var : HasType G t -> Tm G t
25+ Lam : Tm (t :: G) t' -> Tm G (TFun t t')
26+ App : Tm G (TFun t t') -> Tm G t -> Tm G t'
27+
28+-- Extract the type from a reflected term type
29+
30+namespace ErrorReports
31+ data Ty' = TUnit
32+ | TFun Ty' Ty'
33+ | TVar Int String -- To show in unification failures
34+
35+ instance Show Ty' where
36+ show TUnit = "()"
37+ show (TFun x y) = "(" ++ show x ++ " => " ++ show y ++ ")"
38+ show (TVar i n) = n ++ "(" ++ cast i ++ ")"
39+
40+getTmTy : TT -> Maybe TT
41+getTmTy (App (App (App (P (TCon _ _) (NS (UN "Tm") _) _) _) _) ty) = Just ty
42+getTmTy _ = Nothing
43+
44+
45+reifyTy : TT -> Maybe Ty'
46+reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit
47+reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1
48+ ty2 <- reifyTy t2
49+ return $ TFun ty1 ty2
50+reifyTy (P _ (MN i n) _) = Just (TVar i n)
51+reifyTy _ = Nothing
52+
53+-- Friendly error reporting
54+
55+total %error_handler
56+dslerr : Err -> Maybe (List ErrorReportPart)
57+dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1
58+ tm2' <- getTmTy tm2
59+ ty1 <- reifyTy tm1'
60+ ty2 <- reifyTy tm2'
61+ return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]
62+dslerr (At (FileLoc f l c) err) = do err' <- dslerr err
63+ return [ TextPart "In file"
64+ , TextPart f
65+ , TextPart "line", TextPart (cast l)
66+ , TextPart "column", TextPart (cast c)
67+ , SubReport err']
68+dslerr (Elaborating s n err) = do err' <- dslerr err
69+ return ([ TextPart $ "When elaborating " ++ s
70+ , NamePart n
71+ , TextPart ":"
72+ , SubReport err'])
73+dslerr _ = Nothing
74+
75+
76+-- Report the error
77+bad : Tm [] TUnit
78+bad = Lam (Var Here)
79+
test/test037/expectednew file+18
@@ -0,0 +1,18 @@
1+In file ErrorReflection.idr line 78 column 5
2+ When elaborating right hand side of Main.bad :
3+ DSL type error: (t'(1000) => t'(1000)) doesn't match ()
4+
5+Original error:
6+
7+ ErrorReflection.idr:78:5:When elaborating right hand side of bad:
8+ Can't unify
9+ Tm [] (Main.TFun t' t')
10+ with
11+ Tm [] Main.TUnit
12+
13+ Specifically:
14+ Can't unify
15+ Main.TFun t' t'
16+ with
17+ Main.TUnit
18+
test/test037/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ ErrorReflection.idr --nocolour --check
3+rm -f *.ibc