fe3f03f · Idris-dev · git.iko.soy

CHANGELOG+4

@@ -7,12 +7,16 @@ New in 0.9.11:

77 This is intended for field/effect disambiguation. "name" can be any

88 valid identifier. Two labels are definitionally equal if they have the

99 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

1013

1114Internal changes

1215

1316* Faster elaboration

1417* Smaller .ibc files

1518

19+

1620New in 0.9.10:

1721--------------

1822

idris.cabal+1

@@ -377,6 +377,7 @@ Library

377377 , Idris.ElabDecls

378378 , Idris.ElabTerm

379379 , Idris.Error

380+ , Idris.ErrReverse

380381 , Idris.Help

381382 , Idris.IBC

382383 , Idris.IdeSlave

libs/effects/Effects.idr+1

@@ -10,6 +10,7 @@ import Control.Catchable

1010Effect : Type

1111Effect = Type -> Type -> Type -> Type

1212

13+%error_reverse

1314data EFFECT : Type where

1415 MkEff : Type -> Effect -> EFFECT

1516

libs/neweffects/Effects.idr+1

@@ -11,6 +11,7 @@ import Effect.Default

1111Effect : Type

1212Effect = (x : Type) -> Type -> (x -> Type) -> Type

1313

14+%error_reverse

1415data EFFECT : Type where

1516 MkEff : Type -> Effect -> EFFECT

1617

src/Idris/AbsSyntax.hs+4

@@ -95,6 +95,10 @@ addTrans :: (Term, Term) -> Idris ()

9595addTrans t = do i <- getIState

9696 putIState $ i { idris_transforms = t : idris_transforms i }

9797

98+addErrRev :: (Term, Term) -> Idris ()

99+addErrRev t = do i <- getIState

100+ putIState $ i { idris_errRev = t : idris_errRev i }

101+

98102totcheck :: (FC, Name) -> Idris ()

99103totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

100104

src/Idris/AbsSyntaxTree.hs+9−1

@@ -109,6 +109,7 @@ data IState = IState {

109109 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

110110 idris_coercions :: [Name],

111111 idris_transforms :: [(Term, Term)],

112+ idris_errRev :: [(Term, Term)],

112113 syntax_rules :: [Syntax],

113114 syntax_keywords :: [String],

114115 imported :: [FilePath], -- ^ The imported modules

@@ -184,6 +185,7 @@ data IBCWrite = IBCFix FixDecl

184185 | IBCTotal Name Totality

185186 | IBCFlags Name [FnOpt]

186187 | IBCTrans (Term, Term)

188+ | IBCErrRev (Term, Term)

187189 | IBCCG Name

188190 | IBCDoc Name

189191 | IBCCoercion Name

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

198200 emptyContext emptyContext emptyContext emptyContext

199201 emptyContext emptyContext emptyContext emptyContext

200202 emptyContext

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

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

202204 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

203205 True defaultTheme stdout [] (0, emptyContext)

204206

@@ -391,6 +393,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

391393 | Implicit -- implicit coercion

392394 | CExport String -- export, with a C name

393395 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

396+ | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

394397 | Reflection -- a reflecting function, compile-time only

395398 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

396399 deriving (Show, Eq)

@@ -411,6 +414,7 @@ dictionary = elem Dictionary

411414-- | Data declaration options

412415data DataOpt = Codata -- Set if the the data-type is coinductive

413416 | DefaultEliminator -- Set if an eliminator should be generated for data type

417+ | DataErrRev

414418 deriving (Show, Eq)

415419

416420type DataOpts = [DataOpt]

@@ -809,6 +813,7 @@ deriving instance NFData OptInfo

809813

810814data TypeInfo = TI { con_names :: [Name],

811815 codata :: Bool,

816+ data_opts :: DataOpts,

812817 param_pos :: [Int] }

813818 deriving Show

814819{-!

@@ -1255,6 +1260,9 @@ showImp ist impl colour tm = se 10 [] tm where

12551260 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

12561261 se 10 ((n, False):bnd) sc

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

12581266 se p bnd (PApp _ hd@(PRef _ f) [])

12591267 | not impl = se p bnd hd

12601268 se p bnd (PAppBind _ hd@(PRef _ f) [])

src/Idris/Core/TT.hs+24−20

@@ -90,41 +90,45 @@ data ErrorReportPart = TextPart String

9090

9191-- | Idris errors. Used as exceptions in the compiler, but reported to users

9292-- if they reach the top level.

93−data Err = Msg String

93+data Err' t

94+ = Msg String

9495 | InternalMsg String

95− | CantUnify Bool Term Term Err [(Name, Type)] Int

96+ | CantUnify Bool t t (Err' t) [(Name, t)] Int

9697 -- Int is 'score' - how much we did unify

9798 -- Bool indicates recoverability, True indicates more info may make

9899 -- unification succeed

99− | InfiniteUnify Name Term [(Name, Type)]

100− | CantConvert Term Term [(Name, Type)]

101− | CantSolveGoal Term [(Name, Type)]

102− | UnifyScope Name Name Term [(Name, Type)]

100+ | InfiniteUnify Name t [(Name, t)]

101+ | CantConvert t t [(Name, t)]

102+ | CantSolveGoal t [(Name, t)]

103+ | UnifyScope Name Name t [(Name, t)]

103104 | CantInferType String

104− | NonFunctionType Term Term

105− | NotEquality Term Term

105+ | NonFunctionType t t

106+ | NotEquality t t

106107 | TooManyArguments Name

107− | CantIntroduce Term

108+ | CantIntroduce t

108109 | NoSuchVariable Name

109110 | NoTypeDecl Name

110− | NotInjective Term Term Term

111− | CantResolve Term

111+ | NotInjective t t t

112+ | CantResolve t

112113 | CantResolveAlts [String]

113− | IncompleteTerm Term

114+ | IncompleteTerm t

114115 | UniverseError

115116 | ProgramLineComment

116117 | Inaccessible Name

117118 | NonCollapsiblePostulate Name

118119 | AlreadyDefined Name

119− | ProofSearchFail Err

120− | NoRewriting Term

121− | At FC Err

122− | Elaborating String Name Err

120+ | ProofSearchFail (Err' t)

121+ | NoRewriting t

122+ | At FC (Err' t)

123+ | Elaborating String Name (Err' t)

123124 | ProviderError String

124− | LoadingFailed String Err

125− | ReflectionError [[ErrorReportPart]] Err

126− | ReflectionFailed String Err

127− deriving Eq

125+ | LoadingFailed String (Err' t)

126+ | ReflectionError [[ErrorReportPart]] (Err' t)

127+ | ReflectionFailed String (Err' t)

128+ deriving (Eq, Functor)

129+

130+type Err = Err' Term

131+

128132{-!

129133deriving instance NFData Err

130134!-}

src/Idris/Coverage.hs+4−4

@@ -183,7 +183,7 @@ genAll i args

183183 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

184184 let tyn = getTy n (tt_ctxt i)

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

187187 _ -> [p]

188188 ops fc n arg o = return Placeholder

189189

@@ -289,7 +289,7 @@ calcProd i fc topn pats

289289 cotype (DCon _ _) n ty

290290 | (P _ t _, _) <- unApply (getRetTy ty)

291291 = case lookupCtxt t (idris_datatypes i) of

292− [TI _ True _] -> True

292+ [TI _ True _ _] -> True

293293 _ -> False

294294 cotype nt n ty = False

295295

@@ -466,7 +466,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

466466

467467 isInductive (P _ nty _) (P _ nty' _) =

468468 let co = case lookupCtxt nty (idris_datatypes ist) of

469− [TI _ x _] -> x

469+ [TI _ x _ _] -> x

470470 _ -> False in

471471 nty == nty' && not co

472472 isInductive _ _ = False

@@ -507,7 +507,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

507507 [ty] = lookupTy n ctxt -- must exist!

508508 P _ nty _ = fst (unApply (getRetTy ty))

509509 co = case lookupCtxt nty (idris_datatypes ist) of

510− [TI _ x _] -> x

510+ [TI _ x _ _] -> x

511511 _ -> False

512512 args = map snd (getArgTys ty) in

513513 map (getRel co nty) (map (fst . unApply . getRetTy) args)

src/Idris/DeepSeq.hs+1−1

@@ -243,7 +243,7 @@ instance NFData OptInfo where

243243 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

244244

245245instance 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` ()

247247

248248instance (NFData t) => NFData (DSL' t) where

249249 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

88import Idris.AbsSyntax

99import Idris.Core.TT

1010import Idris.Core.Evaluate

11+import Idris.ErrReverse

1112

1213import Data.List (intersperse)

1314

@@ -121,11 +122,13 @@ indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where

121122 else [c]

122123

123124pshow :: IState -> Err -> String

124−pshow i (Msg s) = s

125−pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

125+pshow i err = pshow' i (fmap (errReverse i) err)

126+

127+pshow' i (Msg s) = s

128+pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

126129 "\nThis is probably a bug, or a missing error message.\n" ++

127130 "Please consider reporting at " ++ bugaddr

128−pshow i (CantUnify _ x y e sc s)

131+pshow' i (CantUnify _ x y e sc s)

129132 = let imps = opt_showimp (idris_options i) in

130133 let colour = idris_colourRepl i in

131134 "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))

@@ -134,72 +137,72 @@ pshow i (CantUnify _ x y e sc s)

134137 case e of

135138 Msg "" -> ""

136139 _ -> "\nSpecifically:" ++

137− indented (pshow i e) ++

140+ indented (pshow' i e) ++

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

140143 = let imps = opt_showimp (idris_options i) in

141144 let colour = idris_colourRepl i in

142145 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

143146 ++ indented (showImp (Just i) imps colour (delab i y)) ++

144147 if (opt_errContext (idris_options i)) then showSc i env else ""

145−pshow i (CantSolveGoal x env)

148+pshow' i (CantSolveGoal x env)

146149 = let imps = opt_showimp (idris_options i) in

147150 let colour = idris_colourRepl i in

148151 "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

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

151154 = let imps = opt_showimp (idris_options i) in

152155 let colour = idris_colourRepl i in

153156 "Can't unify" ++ indented (show n) ++ "with"

154157 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

155158 indented (show out) ++ "is not in scope" ++

156159 if (opt_errContext (idris_options i)) then showSc i env else ""

157−pshow i (CantInferType t)

160+pshow' i (CantInferType t)

158161 = "Can't infer type for " ++ t

159−pshow i (NonFunctionType f ty)

162+pshow' i (NonFunctionType f ty)

160163 = let imps = opt_showimp (idris_options i) in

161164 let colour = idris_colourRepl i in

162165 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

163166 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

164−pshow i (NotEquality tm ty)

167+pshow' i (NotEquality tm ty)

165168 = let imps = opt_showimp (idris_options i) in

166169 let colour = idris_colourRepl i in

167170 showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

168171 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

169−pshow i (TooManyArguments f)

172+pshow' i (TooManyArguments f)

170173 = "Too many arguments for " ++ show f

171−pshow i (CantIntroduce ty)

174+pshow' i (CantIntroduce ty)

172175 = let imps = opt_showimp (idris_options i) in

173176 let colour = idris_colourRepl i in

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

176179 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

177180 " would lead to infinite value" ++

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

180− " when unifying " ++ show (delab i x) ++ " and " ++

181− show (delab i y)

182−pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

183−pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

184−pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

185−pshow i (NoSuchVariable n) = "No such variable " ++ show n

186−pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

187−pshow i UniverseError = "Universe inconsistency"

188−pshow i ProgramLineComment = "Program line next to comment"

189−pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

190−pshow i (NonCollapsiblePostulate n)

182+pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

183+ " when unifying " ++ show (delab i x) ++ " and " ++

184+ show (delab i y)

185+pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

186+pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

187+pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n

188+pshow' i (NoSuchVariable n) = "No such variable " ++ show n

189+pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

190+pshow' i UniverseError = "Universe inconsistency"

191+pshow' i ProgramLineComment = "Program line next to comment"

192+pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

193+pshow' i (NonCollapsiblePostulate n)

191194 = "The return type of postulate " ++ show n ++ " is not collapsible"

192−pshow i (AlreadyDefined n) = show n ++ " is already defined"

193−pshow i (ProofSearchFail e) = pshow i e

194−pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

195−pshow i (At f e) = show f ++ ":" ++ pshow i e

196−pshow i (Elaborating s n e) = "When elaborating " ++ s ++

197− showqual i n ++ ":\n" ++ pshow i e

198−pshow i (ProviderError msg) = "Type provider error: " ++ msg

199−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

195+pshow' i (AlreadyDefined n) = show n ++ " is already defined"

196+pshow' i (ProofSearchFail e) = pshow' i e

197+pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

198+pshow' i (At f e) = show f ++ ":" ++ pshow' i e

199+pshow' i (Elaborating s n e) = "When elaborating " ++ s ++

200+ showqual i n ++ ":\n" ++ pshow' i e

201+pshow' i (ProviderError msg) = "Type provider error: " ++ msg

202+pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e

203+pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

201204 concat (intersperse "\n" parts') ++

202− "\nOriginal error:\n" ++ indented (pshow i orig)

205+ "\nOriginal error:\n" ++ indented (pshow' i orig)

203206 where showPart :: ErrorReportPart -> String

204207 showPart (TextPart str) = str

205208 showPart (NamePart n) = let colour = idris_colourRepl i in

@@ -207,8 +210,8 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "

207210 showPart (TermPart tm) = let colour = idris_colourRepl i

208211 in showImp (Just i) False colour (delab i tm)

209212 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" ++

211− indented (pshow i err) ++

213+pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

214+ indented (pshow' i err) ++

212215 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

213216

214217

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

100100 let (t, _) = unApply (getRetTy nty')

101101 let corec = case t of

102102 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

103− [TI _ True _] -> True

103+ [TI _ True _ _] -> True

104104 _ -> False

105105 _ -> False

106106 let opts' = if corec then (Coinductive : opts) else opts

@@ -228,7 +228,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

228228 let as = map (const Nothing) (getArgTys cty)

229229 let params = findParams (map snd cons)

230230 logLvl 2 $ "Parameters : " ++ show params

231− putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

231+ putIState (i { idris_datatypes =

232+ addDef n (TI (map fst cons) codata opts params)

232233 (idris_datatypes i) })

233234 addIBC (IBCDef n)

234235 addIBC (IBCData n)

@@ -1357,6 +1358,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13571358 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

13581359 i <- getIState

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

13601375 return $ Right (clhs, crhs)

13611376 where

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

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 54

29+ibcVersion = 56

3030

3131data IBCFile = IBCFile { ver :: Word8,

3232 sourcefile :: FilePath,

@@ -54,6 +54,7 @@ data IBCFile = IBCFile { ver :: Word8,

5454 ibc_defs :: [(Name, Def)],

5555 ibc_docstrings :: [(Name, String)],

5656 ibc_transforms :: [(Term, Term)],

57+ ibc_errRev :: [(Term, Term)],

5758 ibc_coercions :: [Name],

5859 ibc_lineapps :: [(FilePath, Int, PTerm)],

5960 ibc_namehints :: [(Name, Name)],

@@ -65,7 +66,7 @@ deriving instance Binary IBCFile

6566!-}

6667

6768initIBC :: IBCFile

68−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

69+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

6970

7071loadIBC :: FilePath -> Idris ()

7172loadIBC 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 }

208209ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

209210ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

210211ibc 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 }

211213ibc i (IBCLineApp fp l t) f

212214 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

213215ibc i (IBCNameHint (n, ty)) f

@@ -247,6 +249,7 @@ process i fn

247249 pDocs (ibc_docstrings i)

248250 pCoercions (ibc_coercions i)

249251 pTrans (ibc_transforms i)

252+ pErrRev (ibc_errRev i)

250253 pLineApps (ibc_lineapps i)

251254 pNameHints (ibc_namehints i)

252255 pMetaInformation (ibc_metainformation i)

@@ -416,6 +419,9 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns

416419pTrans :: [(Term, Term)] -> Idris ()

417420pTrans ts = mapM_ addTrans ts

418421

422+pErrRev :: [(Term, Term)] -> Idris ()

423+pErrRev ts = mapM_ addErrRev ts

424+

419425pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

420426pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

421427

@@ -1012,7 +1018,7 @@ instance Binary MetaInformation where

10121018 return (DataMI x1)

10131019

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

10161022 = {-# SCC "putIBCFile" #-}

10171023 do put x1

10181024 put x2

@@ -1044,6 +1050,7 @@ instance Binary IBCFile where

10441050 put x28

10451051 put x29

10461052 put x30

1053+ put x31

10471054 get

10481055 = do x1 <- get

10491056 if x1 == ibcVersion then

@@ -1076,17 +1083,20 @@ instance Binary IBCFile where

10761083 x28 <- get

10771084 x29 <- get

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

1086+ x31 <- get

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)

10801088 else return (initIBC { ver = x1 })

10811089

10821090instance Binary DataOpt where

10831091 put x = case x of

10841092 Codata -> putWord8 0

10851093 DefaultEliminator -> putWord8 1

1094+ DataErrRev -> putWord8 2

10861095 get = do i <- getWord8

10871096 case i of

10881097 0 -> return Codata

10891098 1 -> return DefaultEliminator

1099+ 2 -> return DataErrRev

10901100

10911101instance Binary FnOpt where

10921102 put x

@@ -1102,6 +1112,7 @@ instance Binary FnOpt where

11021112 Implicit -> putWord8 7

11031113 Reflection -> putWord8 8

11041114 ErrorHandler -> putWord8 9

1115+ ErrorReverse -> putWord8 10

11051116 get

11061117 = do i <- getWord8

11071118 case i of

@@ -1116,6 +1127,7 @@ instance Binary FnOpt where

11161127 7 -> return Implicit

11171128 8 -> return Reflection

11181129 9 -> return ErrorHandler

1130+ 10 -> return ErrorReverse

11191131 _ -> error "Corrupted binary data for FnOpt"

11201132

11211133instance Binary Fixity where

@@ -1932,13 +1944,15 @@ instance Binary OptInfo where

19321944 return (Optimise x1 x2 x3 x4)

19331945

19341946instance Binary TypeInfo where

1935− put (TI x1 x2 x3) = do put x1

1936− put x2

1937− put x3

1947+ put (TI x1 x2 x3 x4) = do put x1

1948+ put x2

1949+ put x3

1950+ put x4

19381951 get = do x1 <- get

19391952 x2 <- get

19401953 x3 <- get

1941− return (TI x1 x2 x3)

1954+ x4 <- get

1955+ return (TI x1 x2 x3 x4)

19421956

19431957instance Binary SynContext where

19441958 put x

src/Idris/ParseData.hs+10−4

@@ -77,8 +77,12 @@ dataI = do reserved "data"; return []

7777{- | Parses if a data should not have a default eliminator

7878DefaultEliminator ::= 'noelim'?

7979 -}

80−defaultEliminator :: IdrisParser DataOpts

81−defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])

80+dataOpts :: DataOpts -> IdrisParser DataOpts

81+dataOpts opts

82+ = do reserved "%elim"; dataOpts (DefaultEliminator : opts)

83+ <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

84+ <|> return opts

85+ <?> "data options"

8286

8387{- | Parses a data type declaration

8488Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

@@ -100,7 +104,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

100104 doc <- option "" (docComment '|')

101105 pushIndent

102106 acc <- optional accessibility

103− elim <- defaultEliminator

107+ elim <- dataOpts []

104108 co <- dataI

105109 let dataOpts = combineDataOpts(elim ++ co)

106110 return (doc, acc, dataOpts))

@@ -146,7 +150,9 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

146150 bindArgs :: [PTerm] -> PTerm -> PTerm

147151 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

148152 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

150156

151157

152158{- | Parses a type constructor declaration

src/Idris/Parser.hs+2

@@ -337,6 +337,8 @@ fnOpts opts

337337 fnOpts (AssertTotal : opts)

338338 <|> do try (lchar '%' *> reserved "error_handler");

339339 fnOpts (ErrorHandler : opts)

340+ <|> do try (lchar '%' *> reserved "error_reverse");

341+ fnOpts (ErrorReverse : opts)

340342 <|> do try (lchar '%' *> reserved "reflection");

341343 fnOpts (Reflection : opts)

342344 <|> do lchar '%'; reserved "specialise";