git.iko.soy/Idris-dev
on master help sign in
Added %error_reverse annotation
fe3f03fEdwin Brady
CHANGELOG+4
compare with master
unifiedsplit
@@ -7,12 +7,16 @@ New in 0.9.11:
7 This is intended for field/effect disambiguation. "name" can be any
7 This is intended for field/effect disambiguation. "name" can be any
8 valid identifier. Two labels are definitionally equal if they have the
8 valid identifier. Two labels are definitionally equal if they have the
9 same name.
9 same name.
10+* General improvements in error messages, especially %error_reverse
11+ annotation, which allows a hint as to how to display a term in error
12+ messages
10
13
11Internal changes
14Internal changes
12
15
13* Faster elaboration
16* Faster elaboration
14* Smaller .ibc files
17* Smaller .ibc files
15
18
19+
16New in 0.9.10:
20New in 0.9.10:
17--------------
21--------------
18
22
idris.cabal+1
@@ -377,6 +377,7 @@ Library
377 , Idris.ElabDecls
377 , Idris.ElabDecls
378 , Idris.ElabTerm
378 , Idris.ElabTerm
379 , Idris.Error
379 , Idris.Error
380+ , Idris.ErrReverse
380 , Idris.Help
381 , Idris.Help
381 , Idris.IBC
382 , Idris.IBC
382 , Idris.IdeSlave
383 , Idris.IdeSlave
libs/effects/Effects.idr+1
@@ -10,6 +10,7 @@ import Control.Catchable
10Effect : Type
10Effect : Type
11Effect = Type -> Type -> Type -> Type
11Effect = Type -> Type -> Type -> Type
12
12
13+%error_reverse
13data EFFECT : Type where
14data EFFECT : Type where
14 MkEff : Type -> Effect -> EFFECT
15 MkEff : Type -> Effect -> EFFECT
15
16
libs/neweffects/Effects.idr+1
@@ -11,6 +11,7 @@ import Effect.Default
11Effect : Type
11Effect : Type
12Effect = (x : Type) -> Type -> (x -> Type) -> Type
12Effect = (x : Type) -> Type -> (x -> Type) -> Type
13
13
14+%error_reverse
14data EFFECT : Type where
15data EFFECT : Type where
15 MkEff : Type -> Effect -> EFFECT
16 MkEff : Type -> Effect -> EFFECT
16
17
src/Idris/AbsSyntax.hs+4
@@ -95,6 +95,10 @@ addTrans :: (Term, Term) -> Idris ()
95addTrans t = do i <- getIState
95addTrans t = do i <- getIState
96 putIState $ i { idris_transforms = t : idris_transforms i }
96 putIState $ i { idris_transforms = t : idris_transforms i }
97
97
98+addErrRev :: (Term, Term) -> Idris ()
99+addErrRev t = do i <- getIState
100+ putIState $ i { idris_errRev = t : idris_errRev i }
101+
98totcheck :: (FC, Name) -> Idris ()
102totcheck :: (FC, Name) -> Idris ()
99totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
103totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
100
104
src/Idris/AbsSyntaxTree.hs+9−1
@@ -109,6 +109,7 @@ data IState = IState {
109 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
109 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
110 idris_coercions :: [Name],
110 idris_coercions :: [Name],
111 idris_transforms :: [(Term, Term)],
111 idris_transforms :: [(Term, Term)],
112+ idris_errRev :: [(Term, Term)],
112 syntax_rules :: [Syntax],
113 syntax_rules :: [Syntax],
113 syntax_keywords :: [String],
114 syntax_keywords :: [String],
114 imported :: [FilePath], -- ^ The imported modules
115 imported :: [FilePath], -- ^ The imported modules
@@ -184,6 +185,7 @@ data IBCWrite = IBCFix FixDecl
184 | IBCTotal Name Totality
185 | IBCTotal Name Totality
185 | IBCFlags Name [FnOpt]
186 | IBCFlags Name [FnOpt]
186 | IBCTrans (Term, Term)
187 | IBCTrans (Term, Term)
188+ | IBCErrRev (Term, Term)
187 | IBCCG Name
189 | IBCCG Name
188 | IBCDoc Name
190 | IBCDoc Name
189 | IBCCoercion Name
191 | IBCCoercion Name
@@ -198,7 +200,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
198 emptyContext emptyContext emptyContext emptyContext
200 emptyContext emptyContext emptyContext emptyContext
199 emptyContext emptyContext emptyContext emptyContext
201 emptyContext 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)
204
206
@@ -391,6 +393,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
391 | Implicit -- implicit coercion
393 | Implicit -- implicit coercion
392 | CExport String -- export, with a C name
394 | CExport String -- export, with a C name
393 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
395 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
396+ | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
394 | Reflection -- a reflecting function, compile-time only
397 | Reflection -- a reflecting function, compile-time only
395 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
398 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
396 deriving (Show, Eq)
399 deriving (Show, Eq)
@@ -411,6 +414,7 @@ dictionary = elem Dictionary
411-- | Data declaration options
414-- | Data declaration options
412data DataOpt = Codata -- Set if the the data-type is coinductive
415data DataOpt = Codata -- Set if the the data-type is coinductive
413 | DefaultEliminator -- Set if an eliminator should be generated for data type
416 | DefaultEliminator -- Set if an eliminator should be generated for data type
417+ | DataErrRev
414 deriving (Show, Eq)
418 deriving (Show, Eq)
415
419
416type DataOpts = [DataOpt]
420type DataOpts = [DataOpt]
@@ -809,6 +813,7 @@ deriving instance NFData OptInfo
809
813
810data TypeInfo = TI { con_names :: [Name],
814data TypeInfo = TI { con_names :: [Name],
811 codata :: Bool,
815 codata :: Bool,
816+ data_opts :: DataOpts,
812 param_pos :: [Int] }
817 param_pos :: [Int] }
813 deriving Show
818 deriving Show
814{-!
819{-!
@@ -1255,6 +1260,9 @@ showImp ist impl colour tm = se 10 [] tm where
1255 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1260 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1256 se 10 ((n, False):bnd) sc
1261 se 10 ((n, False):bnd) sc
1257 se p bnd (PMatchApp _ f) = "match " ++ show f
1262 se p bnd (PMatchApp _ f) = "match " ++ show f
1263+ se p bnd (PApp _ hd@(PRef fc f) [tm])
1264+ | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1265+ f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))
1258 se p bnd (PApp _ hd@(PRef _ f) [])
1266 se p bnd (PApp _ hd@(PRef _ f) [])
1259 | not impl = se p bnd hd
1267 | not impl = se p bnd hd
1260 se p bnd (PAppBind _ hd@(PRef _ f) [])
1268 se p bnd (PAppBind _ hd@(PRef _ f) [])
src/Idris/Core/TT.hs+24−20
@@ -90,41 +90,45 @@ data ErrorReportPart = TextPart String
90
90
91-- | Idris errors. Used as exceptions in the compiler, but reported to users
91-- | Idris errors. Used as exceptions in the compiler, but reported to users
92-- if they reach the top level.
92-- if they reach the top level.
93+data Err' t
93−data Err = Msg String
94+ = Msg String
94 | InternalMsg String
95 | InternalMsg String
95− | CantUnify Bool Term Term Err [(Name, Type)] Int
96+ | CantUnify Bool t t (Err' t) [(Name, t)] Int
96 -- Int is 'score' - how much we did unify
97 -- Int is 'score' - how much we did unify
97 -- Bool indicates recoverability, True indicates more info may make
98 -- Bool indicates recoverability, True indicates more info may make
98 -- unification succeed
99 -- unification succeed
99− | InfiniteUnify Name Term [(Name, Type)]
100+ | InfiniteUnify Name t [(Name, t)]
100− | CantConvert Term Term [(Name, Type)]
101+ | CantConvert t t [(Name, t)]
101− | CantSolveGoal Term [(Name, Type)]
102+ | CantSolveGoal t [(Name, t)]
102− | UnifyScope Name Name Term [(Name, Type)]
103+ | UnifyScope Name Name t [(Name, t)]
103 | CantInferType String
104 | CantInferType String
104− | NonFunctionType Term Term
105+ | NonFunctionType t t
105− | NotEquality Term Term
106+ | NotEquality t t
106 | TooManyArguments Name
107 | TooManyArguments Name
107− | CantIntroduce Term
108+ | CantIntroduce t
108 | NoSuchVariable Name
109 | NoSuchVariable Name
109 | NoTypeDecl Name
110 | NoTypeDecl Name
110− | NotInjective Term Term Term
111+ | NotInjective t t t
111− | CantResolve Term
112+ | CantResolve t
112 | CantResolveAlts [String]
113 | CantResolveAlts [String]
113− | IncompleteTerm Term
114+ | IncompleteTerm t
114 | UniverseError
115 | UniverseError
115 | ProgramLineComment
116 | ProgramLineComment
116 | Inaccessible Name
117 | Inaccessible Name
117 | NonCollapsiblePostulate Name
118 | NonCollapsiblePostulate Name
118 | AlreadyDefined Name
119 | AlreadyDefined Name
119− | ProofSearchFail Err
120+ | ProofSearchFail (Err' t)
120− | NoRewriting Term
121+ | NoRewriting t
121− | At FC Err
122+ | At FC (Err' t)
122− | Elaborating String Name Err
123+ | Elaborating String Name (Err' t)
123 | ProviderError String
124 | ProviderError String
124− | LoadingFailed String Err
125+ | LoadingFailed String (Err' t)
125− | ReflectionError [[ErrorReportPart]] Err
126+ | ReflectionError [[ErrorReportPart]] (Err' t)
126− | ReflectionFailed String Err
127+ | ReflectionFailed String (Err' t)
127− deriving Eq
128+ deriving (Eq, Functor)
129+
130+type Err = Err' Term
131+
128{-!
132{-!
129deriving instance NFData Err
133deriving instance NFData Err
130!-}
134!-}
src/Idris/Coverage.hs+4−4
@@ -183,7 +183,7 @@ genAll i args
183 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
183 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
184 let tyn = getTy n (tt_ctxt i)
184 let tyn = getTy n (tt_ctxt i)
185 case lookupCtxt tyn (idris_datatypes i) of
185 case lookupCtxt tyn (idris_datatypes i) of
186− (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
186+ (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
187 _ -> [p]
187 _ -> [p]
188 ops fc n arg o = return Placeholder
188 ops fc n arg o = return Placeholder
189
189
@@ -289,7 +289,7 @@ calcProd i fc topn pats
289 cotype (DCon _ _) n ty
289 cotype (DCon _ _) n ty
290 | (P _ t _, _) <- unApply (getRetTy ty)
290 | (P _ t _, _) <- unApply (getRetTy ty)
291 = case lookupCtxt t (idris_datatypes i) of
291 = case lookupCtxt t (idris_datatypes i) of
292− [TI _ True _] -> True
292+ [TI _ True _ _] -> True
293 _ -> False
293 _ -> False
294 cotype nt n ty = False
294 cotype nt n ty = False
295
295
@@ -466,7 +466,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
466
466
467 isInductive (P _ nty _) (P _ nty' _) =
467 isInductive (P _ nty _) (P _ nty' _) =
468 let co = case lookupCtxt nty (idris_datatypes ist) of
468 let co = case lookupCtxt nty (idris_datatypes ist) of
469− [TI _ x _] -> x
469+ [TI _ x _ _] -> x
470 _ -> False in
470 _ -> False in
471 nty == nty' && not co
471 nty == nty' && not co
472 isInductive _ _ = False
472 isInductive _ _ = False
@@ -507,7 +507,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
507 [ty] = lookupTy n ctxt -- must exist!
507 [ty] = lookupTy n ctxt -- must exist!
508 P _ nty _ = fst (unApply (getRetTy ty))
508 P _ nty _ = fst (unApply (getRetTy ty))
509 co = case lookupCtxt nty (idris_datatypes ist) of
509 co = case lookupCtxt nty (idris_datatypes ist) of
510− [TI _ x _] -> x
510+ [TI _ x _ _] -> x
511 _ -> False
511 _ -> False
512 args = map snd (getArgTys ty) in
512 args = map snd (getArgTys ty) in
513 map (getRel co nty) (map (fst . unApply . getRetTy) args)
513 map (getRel co nty) (map (fst . unApply . getRetTy) args)
src/Idris/DeepSeq.hs+1−1
@@ -243,7 +243,7 @@ instance NFData OptInfo where
243 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
243 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
244
244
245instance NFData TypeInfo where
245instance NFData TypeInfo where
246− rnf (TI x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
246+ rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
247
247
248instance (NFData t) => NFData (DSL' t) where
248instance (NFData t) => NFData (DSL' t) where
249 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
249 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
src/Idris/Delaborate.hs+40−37
@@ -8,6 +8,7 @@ module Idris.Delaborate where
8import Idris.AbsSyntax
8import Idris.AbsSyntax
9import Idris.Core.TT
9import Idris.Core.TT
10import Idris.Core.Evaluate
10import Idris.Core.Evaluate
11+import Idris.ErrReverse
11
12
12import Data.List (intersperse)
13import Data.List (intersperse)
13
14
@@ -121,11 +122,13 @@ indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
121 else [c]
122 else [c]
122
123
123pshow :: IState -> Err -> String
124pshow :: IState -> Err -> String
125+pshow i err = pshow' i (fmap (errReverse i) err)
126+
124−pshow i (Msg s) = s
127+pshow' i (Msg s) = s
125−pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
128+pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
126 "\nThis is probably a bug, or a missing error message.\n" ++
129 "\nThis is probably a bug, or a missing error message.\n" ++
127 "Please consider reporting at " ++ bugaddr
130 "Please consider reporting at " ++ bugaddr
128−pshow i (CantUnify _ x y e sc s)
131+pshow' i (CantUnify _ x y e sc s)
129 = let imps = opt_showimp (idris_options i) in
132 = let imps = opt_showimp (idris_options i) in
130 let colour = idris_colourRepl i in
133 let colour = idris_colourRepl i in
131 "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
134 "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
@@ -134,72 +137,72 @@ pshow i (CantUnify _ x y e sc s)
134 case e of
137 case e of
135 Msg "" -> ""
138 Msg "" -> ""
136 _ -> "\nSpecifically:" ++
139 _ -> "\nSpecifically:" ++
137− indented (pshow i e) ++
140+ indented (pshow' i e) ++
138 if (opt_errContext (idris_options i)) then showSc i sc else ""
141 if (opt_errContext (idris_options i)) then showSc i sc else ""
139−pshow i (CantConvert x y env)
142+pshow' i (CantConvert x y env)
140 = let imps = opt_showimp (idris_options i) in
143 = let imps = opt_showimp (idris_options i) in
141 let colour = idris_colourRepl i in
144 let colour = idris_colourRepl i in
142 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
145 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
143 ++ indented (showImp (Just i) imps colour (delab i y)) ++
146 ++ indented (showImp (Just i) imps colour (delab i y)) ++
144 if (opt_errContext (idris_options i)) then showSc i env else ""
147 if (opt_errContext (idris_options i)) then showSc i env else ""
145−pshow i (CantSolveGoal x env)
148+pshow' i (CantSolveGoal x env)
146 = let imps = opt_showimp (idris_options i) in
149 = let imps = opt_showimp (idris_options i) in
147 let colour = idris_colourRepl i in
150 let colour = idris_colourRepl i in
148 "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++
151 "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++
149 if (opt_errContext (idris_options i)) then showSc i env else ""
152 if (opt_errContext (idris_options i)) then showSc i env else ""
150−pshow i (UnifyScope n out tm env)
153+pshow' i (UnifyScope n out tm env)
151 = let imps = opt_showimp (idris_options i) in
154 = let imps = opt_showimp (idris_options i) in
152 let colour = idris_colourRepl i in
155 let colour = idris_colourRepl i in
153 "Can't unify" ++ indented (show n) ++ "with"
156 "Can't unify" ++ indented (show n) ++ "with"
154 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
157 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
155 indented (show out) ++ "is not in scope" ++
158 indented (show out) ++ "is not in scope" ++
156 if (opt_errContext (idris_options i)) then showSc i env else ""
159 if (opt_errContext (idris_options i)) then showSc i env else ""
157−pshow i (CantInferType t)
160+pshow' i (CantInferType t)
158 = "Can't infer type for " ++ t
161 = "Can't infer type for " ++ t
159−pshow i (NonFunctionType f ty)
162+pshow' i (NonFunctionType f ty)
160 = let imps = opt_showimp (idris_options i) in
163 = let imps = opt_showimp (idris_options i) in
161 let colour = idris_colourRepl i in
164 let colour = idris_colourRepl i in
162 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
165 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
163 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
166 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
164−pshow i (NotEquality tm ty)
167+pshow' i (NotEquality tm ty)
165 = let imps = opt_showimp (idris_options i) in
168 = let imps = opt_showimp (idris_options i) in
166 let colour = idris_colourRepl i in
169 let colour = idris_colourRepl i in
167 showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
170 showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
168 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
171 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
169−pshow i (TooManyArguments f)
172+pshow' i (TooManyArguments f)
170 = "Too many arguments for " ++ show f
173 = "Too many arguments for " ++ show f
171−pshow i (CantIntroduce ty)
174+pshow' i (CantIntroduce ty)
172 = let imps = opt_showimp (idris_options i) in
175 = let imps = opt_showimp (idris_options i) in
173 let colour = idris_colourRepl i in
176 let colour = idris_colourRepl i in
174 "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
177 "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
175−pshow i (InfiniteUnify x tm env)
178+pshow' i (InfiniteUnify x tm env)
176 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
179 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
177 " would lead to infinite value" ++
180 " would lead to infinite value" ++
178 if (opt_errContext (idris_options i)) then showSc i env else ""
181 if (opt_errContext (idris_options i)) then showSc i env else ""
179−pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
182+pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
180− " when unifying " ++ show (delab i x) ++ " and " ++
183+ " when unifying " ++ show (delab i x) ++ " and " ++
181− show (delab i y)
184+ show (delab i y)
182−pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
185+pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
183−pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
186+pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
184−pshow i (NoTypeDecl n) = "No type declaration for " ++ show n
187+pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n
185−pshow i (NoSuchVariable n) = "No such variable " ++ show n
188+pshow' i (NoSuchVariable n) = "No such variable " ++ show n
186−pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
189+pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
187−pshow i UniverseError = "Universe inconsistency"
190+pshow' i UniverseError = "Universe inconsistency"
188−pshow i ProgramLineComment = "Program line next to comment"
191+pshow' i ProgramLineComment = "Program line next to comment"
189−pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
192+pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
190−pshow i (NonCollapsiblePostulate n)
193+pshow' i (NonCollapsiblePostulate n)
191 = "The return type of postulate " ++ show n ++ " is not collapsible"
194 = "The return type of postulate " ++ show n ++ " is not collapsible"
192−pshow i (AlreadyDefined n) = show n ++ " is already defined"
195+pshow' i (AlreadyDefined n) = show n ++ " is already defined"
193−pshow i (ProofSearchFail e) = pshow i e
196+pshow' i (ProofSearchFail e) = pshow' i e
194−pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
197+pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
195−pshow i (At f e) = show f ++ ":" ++ pshow i e
198+pshow' i (At f e) = show f ++ ":" ++ pshow' i e
196−pshow i (Elaborating s n e) = "When elaborating " ++ s ++
199+pshow' i (Elaborating s n e) = "When elaborating " ++ s ++
197− showqual i n ++ ":\n" ++ pshow i e
200+ showqual i n ++ ":\n" ++ pshow' i e
198−pshow i (ProviderError msg) = "Type provider error: " ++ msg
201+pshow' i (ProviderError msg) = "Type provider error: " ++ msg
199−pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e
202+pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e
200−pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
203+pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
201 concat (intersperse "\n" parts') ++
204 concat (intersperse "\n" parts') ++
202− "\nOriginal error:\n" ++ indented (pshow i orig)
205+ "\nOriginal error:\n" ++ indented (pshow' i orig)
203 where showPart :: ErrorReportPart -> String
206 where showPart :: ErrorReportPart -> String
204 showPart (TextPart str) = str
207 showPart (TextPart str) = str
205 showPart (NamePart n) = let colour = idris_colourRepl i in
208 showPart (NamePart n) = let colour = idris_colourRepl i in
@@ -207,8 +210,8 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "
207 showPart (TermPart tm) = let colour = idris_colourRepl i
210 showPart (TermPart tm) = let colour = idris_colourRepl i
208 in showImp (Just i) False colour (delab i tm)
211 in showImp (Just i) False colour (delab i tm)
209 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
212 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
210−pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
213+pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
211− indented (pshow i err) ++
214+ indented (pshow' i err) ++
212 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
215 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
213
216
214
217
src/Idris/ElabDecls.hs+17−2
@@ -100,7 +100,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
100 let (t, _) = unApply (getRetTy nty')
100 let (t, _) = unApply (getRetTy nty')
101 let corec = case t of
101 let corec = case t of
102 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
102 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
103− [TI _ True _] -> True
103+ [TI _ True _ _] -> True
104 _ -> False
104 _ -> False
105 _ -> False
105 _ -> False
106 let opts' = if corec then (Coinductive : opts) else opts
106 let opts' = if corec then (Coinductive : opts) else opts
@@ -228,7 +228,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
228 let as = map (const Nothing) (getArgTys cty)
228 let as = map (const Nothing) (getArgTys cty)
229 let params = findParams (map snd cons)
229 let params = findParams (map snd cons)
230 logLvl 2 $ "Parameters : " ++ show params
230 logLvl 2 $ "Parameters : " ++ show params
231+ putIState (i { idris_datatypes =
231− putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
232+ addDef n (TI (map fst cons) codata opts params)
232 (idris_datatypes i) })
233 (idris_datatypes i) })
233 addIBC (IBCDef n)
234 addIBC (IBCDef n)
234 addIBC (IBCData n)
235 addIBC (IBCData n)
@@ -1357,6 +1358,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1357 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
1358 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
1358 i <- getIState
1359 i <- getIState
1359 checkInferred fc (delab' i crhs True True) rhs
1360 checkInferred fc (delab' i crhs True True) rhs
1361+ -- if the function is declared '%error_reverse', or its type,
1362+ -- then we'll try running it in reverse to improve error messages
1363+ let (ret_fam, _) = unApply (getRetTy crhsty)
1364+ rev <- case ret_fam of
1365+ P _ rfamn _ ->
1366+ case lookupCtxt rfamn (idris_datatypes i) of
1367+ [TI _ _ dopts _] ->
1368+ return (DataErrRev `elem` dopts)
1369+ _ -> return False
1370+ _ -> return False
1371+
1372+ when (rev || ErrorReverse `elem` opts) $ do
1373+ addIBC (IBCErrRev (crhs, clhs))
1374+ addErrRev (crhs, clhs)
1360 return $ Right (clhs, crhs)
1375 return $ Right (clhs, crhs)
1361 where
1376 where
1362 decorate (NS x ns)
1377 decorate (NS x ns)
src/Idris/ErrReverse.hsnew file+72
@@ -0,0 +1,72 @@
1+{-# LANGUAGE PatternGuards #-}
2+
3+module Idris.ErrReverse where
4+
5+import Idris.AbsSyntax
6+import Idris.Core.TT
7+import Util.Pretty
8+
9+import Data.List
10+import Debug.Trace
11+
12+-- For display purposes, apply any 'error reversal' transformations so that
13+-- errors will be more readable
14+
15+errReverse :: IState -> Term -> Term
16+errReverse ist t = rewrite 5 (elideLambdas t)
17+ where
18+
19+ rewrite 0 t = t
20+ rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in
21+ if t == t' then t
22+ else rewrite (n - 1) t'
23+
24+ applyRule :: Term -> (Term, Term) -> Term
25+ applyRule t (l, r) = applyNames [] t l r
26+
27+ -- Assume pattern bindings match in l and r (if they don't just treat
28+ -- the rule as invalid and return t)
29+
30+ applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)
31+ | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)
32+ (instantiate (P Ref n' ty') scr)
33+ | otherwise = t
34+ applyNames ns t l r = matchTerm ns l r t
35+
36+ matchTerm ns l r t
37+ | Just nmap <- match ns l t = substNames nmap r
38+ matchTerm ns l r (App f a) = let f' = matchTerm ns l r f
39+ a' = matchTerm ns l r a in
40+ App f' a'
41+ matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b
42+ sc' = matchTerm ns l r sc in
43+ Bind n b' sc'
44+ matchTerm ns l r t = t
45+
46+ match ns l t = do ms <- match' ns l t
47+ combine (nub ms)
48+
49+ -- If any duplicate mappings, it's a failure
50+ combine [] = Just []
51+ combine ((x, t) : xs)
52+ | Just _ <- lookup x xs = Nothing
53+ | otherwise = do xs' <- combine xs
54+ Just ((x, t) : xs')
55+
56+ match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]
57+ match' ns (App f a) (App f' a') = do fs <- match' ns f f'
58+ as <- match' ns a a'
59+ Just (fs ++ as)
60+ -- no matching Binds, for now...
61+ match' ns x y = if x == y then Just [] else Nothing
62+
63+ -- if the term under a lambda is huge, there's no much point in showing
64+ -- it as it won't be very enlightening.
65+
66+ elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)
67+ elideLambdas (Bind n (Lam t) sc)
68+ | size sc > 100 = P Ref (sUN "...") Erased
69+ elideLambdas (Bind n b sc)
70+ = Bind n (fmap elideLambdas b) (elideLambdas sc)
71+ elideLambdas t = t
72+
src/Idris/IBC.hs+22−8
@@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)
26
26
27
27
28ibcVersion :: Word8
28ibcVersion :: Word8
29−ibcVersion = 54
29+ibcVersion = 56
30
30
31data IBCFile = IBCFile { ver :: Word8,
31data IBCFile = IBCFile { ver :: Word8,
32 sourcefile :: FilePath,
32 sourcefile :: FilePath,
@@ -54,6 +54,7 @@ data IBCFile = IBCFile { ver :: Word8,
54 ibc_defs :: [(Name, Def)],
54 ibc_defs :: [(Name, Def)],
55 ibc_docstrings :: [(Name, String)],
55 ibc_docstrings :: [(Name, String)],
56 ibc_transforms :: [(Term, Term)],
56 ibc_transforms :: [(Term, Term)],
57+ ibc_errRev :: [(Term, Term)],
57 ibc_coercions :: [Name],
58 ibc_coercions :: [Name],
58 ibc_lineapps :: [(FilePath, Int, PTerm)],
59 ibc_lineapps :: [(FilePath, Int, PTerm)],
59 ibc_namehints :: [(Name, Name)],
60 ibc_namehints :: [(Name, Name)],
@@ -65,7 +66,7 @@ deriving instance Binary IBCFile
65!-}
66!-}
66
67
67initIBC :: IBCFile
68initIBC :: IBCFile
68−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
69+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
69
70
70loadIBC :: FilePath -> Idris ()
71loadIBC :: FilePath -> Idris ()
71loadIBC fp = do iLOG $ "Loading ibc " ++ fp
72loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -208,6 +209,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
208ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
209ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
209ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
210ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
210ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }
211ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }
212+ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }
211ibc i (IBCLineApp fp l t) f
213ibc i (IBCLineApp fp l t) f
212 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
214 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
213ibc i (IBCNameHint (n, ty)) f
215ibc i (IBCNameHint (n, ty)) f
@@ -247,6 +249,7 @@ process i fn
247 pDocs (ibc_docstrings i)
249 pDocs (ibc_docstrings i)
248 pCoercions (ibc_coercions i)
250 pCoercions (ibc_coercions i)
249 pTrans (ibc_transforms i)
251 pTrans (ibc_transforms i)
252+ pErrRev (ibc_errRev i)
250 pLineApps (ibc_lineapps i)
253 pLineApps (ibc_lineapps i)
251 pNameHints (ibc_namehints i)
254 pNameHints (ibc_namehints i)
252 pMetaInformation (ibc_metainformation i)
255 pMetaInformation (ibc_metainformation i)
@@ -416,6 +419,9 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns
416pTrans :: [(Term, Term)] -> Idris ()
419pTrans :: [(Term, Term)] -> Idris ()
417pTrans ts = mapM_ addTrans ts
420pTrans ts = mapM_ addTrans ts
418
421
422+pErrRev :: [(Term, Term)] -> Idris ()
423+pErrRev ts = mapM_ addErrRev ts
424+
419pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
425pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
420pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
426pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
421
427
@@ -1012,7 +1018,7 @@ instance Binary MetaInformation where
1012 return (DataMI x1)
1018 return (DataMI x1)
1013
1019
1014instance Binary IBCFile where
1020instance Binary IBCFile where
1015− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)
1021+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31)
1016 = {-# SCC "putIBCFile" #-}
1022 = {-# SCC "putIBCFile" #-}
1017 do put x1
1023 do put x1
1018 put x2
1024 put x2
@@ -1044,6 +1050,7 @@ instance Binary IBCFile where
1044 put x28
1050 put x28
1045 put x29
1051 put x29
1046 put x30
1052 put x30
1053+ put x31
1047 get
1054 get
1048 = do x1 <- get
1055 = do x1 <- get
1049 if x1 == ibcVersion then
1056 if x1 == ibcVersion then
@@ -1076,17 +1083,20 @@ instance Binary IBCFile where
1076 x28 <- get
1083 x28 <- get
1077 x29 <- get
1084 x29 <- get
1078 x30 <- get
1085 x30 <- get
1086+ x31 <- get
1079− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)
1087+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31)
1080 else return (initIBC { ver = x1 })
1088 else return (initIBC { ver = x1 })
1081
1089
1082instance Binary DataOpt where
1090instance Binary DataOpt where
1083 put x = case x of
1091 put x = case x of
1084 Codata -> putWord8 0
1092 Codata -> putWord8 0
1085 DefaultEliminator -> putWord8 1
1093 DefaultEliminator -> putWord8 1
1094+ DataErrRev -> putWord8 2
1086 get = do i <- getWord8
1095 get = do i <- getWord8
1087 case i of
1096 case i of
1088 0 -> return Codata
1097 0 -> return Codata
1089 1 -> return DefaultEliminator
1098 1 -> return DefaultEliminator
1099+ 2 -> return DataErrRev
1090
1100
1091instance Binary FnOpt where
1101instance Binary FnOpt where
1092 put x
1102 put x
@@ -1102,6 +1112,7 @@ instance Binary FnOpt where
1102 Implicit -> putWord8 7
1112 Implicit -> putWord8 7
1103 Reflection -> putWord8 8
1113 Reflection -> putWord8 8
1104 ErrorHandler -> putWord8 9
1114 ErrorHandler -> putWord8 9
1115+ ErrorReverse -> putWord8 10
1105 get
1116 get
1106 = do i <- getWord8
1117 = do i <- getWord8
1107 case i of
1118 case i of
@@ -1116,6 +1127,7 @@ instance Binary FnOpt where
1116 7 -> return Implicit
1127 7 -> return Implicit
1117 8 -> return Reflection
1128 8 -> return Reflection
1118 9 -> return ErrorHandler
1129 9 -> return ErrorHandler
1130+ 10 -> return ErrorReverse
1119 _ -> error "Corrupted binary data for FnOpt"
1131 _ -> error "Corrupted binary data for FnOpt"
1120
1132
1121instance Binary Fixity where
1133instance Binary Fixity where
@@ -1932,13 +1944,15 @@ instance Binary OptInfo where
1932 return (Optimise x1 x2 x3 x4)
1944 return (Optimise x1 x2 x3 x4)
1933
1945
1934instance Binary TypeInfo where
1946instance Binary TypeInfo where
1935− put (TI x1 x2 x3) = do put x1
1947+ put (TI x1 x2 x3 x4) = do put x1
1936− put x2
1948+ put x2
1937− put x3
1949+ put x3
1950+ put x4
1938 get = do x1 <- get
1951 get = do x1 <- get
1939 x2 <- get
1952 x2 <- get
1940 x3 <- get
1953 x3 <- get
1954+ x4 <- get
1941− return (TI x1 x2 x3)
1955+ return (TI x1 x2 x3 x4)
1942
1956
1943instance Binary SynContext where
1957instance Binary SynContext where
1944 put x
1958 put x
src/Idris/ParseData.hs+10−4
@@ -77,8 +77,12 @@ dataI = do reserved "data"; return []
77{- | Parses if a data should not have a default eliminator
77{- | Parses if a data should not have a default eliminator
78DefaultEliminator ::= 'noelim'?
78DefaultEliminator ::= 'noelim'?
79 -}
79 -}
80−defaultEliminator :: IdrisParser DataOpts
80+dataOpts :: DataOpts -> IdrisParser DataOpts
81−defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])
81+dataOpts opts
82+ = do reserved "%elim"; dataOpts (DefaultEliminator : opts)
83+ <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
84+ <|> return opts
85+ <?> "data options"
82
86
83{- | Parses a data type declaration
87{- | Parses a data type declaration
84Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
88Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
@@ -100,7 +104,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do
100 doc <- option "" (docComment '|')
104 doc <- option "" (docComment '|')
101 pushIndent
105 pushIndent
102 acc <- optional accessibility
106 acc <- optional accessibility
103− elim <- defaultEliminator
107+ elim <- dataOpts []
104 co <- dataI
108 co <- dataI
105 let dataOpts = combineDataOpts(elim ++ co)
109 let dataOpts = combineDataOpts(elim ++ co)
106 return (doc, acc, dataOpts))
110 return (doc, acc, dataOpts))
@@ -146,7 +150,9 @@ data_ syn = do (doc, acc, dataOpts) <- try (do
146 bindArgs :: [PTerm] -> PTerm -> PTerm
150 bindArgs :: [PTerm] -> PTerm -> PTerm
147 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs
151 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs
148 combineDataOpts :: DataOpts -> DataOpts
152 combineDataOpts :: DataOpts -> DataOpts
149− combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts
153+ combineDataOpts opts = if Codata `elem` opts
154+ then delete DefaultEliminator opts
155+ else opts
150
156
151
157
152{- | Parses a type constructor declaration
158{- | Parses a type constructor declaration
src/Idris/Parser.hs+2
@@ -337,6 +337,8 @@ fnOpts opts
337 fnOpts (AssertTotal : opts)
337 fnOpts (AssertTotal : opts)
338 <|> do try (lchar '%' *> reserved "error_handler");
338 <|> do try (lchar '%' *> reserved "error_handler");
339 fnOpts (ErrorHandler : opts)
339 fnOpts (ErrorHandler : opts)
340+ <|> do try (lchar '%' *> reserved "error_reverse");
341+ fnOpts (ErrorReverse : opts)
340 <|> do try (lchar '%' *> reserved "reflection");
342 <|> do try (lchar '%' *> reserved "reflection");
341 fnOpts (Reflection : opts)
343 fnOpts (Reflection : opts)
342 <|> do lchar '%'; reserved "specialise";
344 <|> do lchar '%'; reserved "specialise";