60abf37 · Idris-dev · git.iko.soy

idris.cabal+3

@@ -320,6 +320,9 @@ Extra-source-files:

320320 test/test037/run

321321 test/test037/expected

322322 test/test037/*.idr

323+ test/test038/run

324+ test/test038/expected

325+ test/test038/*.idr

323326 test/test039/run

324327 test/test039/expected

325328 test/test039/*.idr

libs/base/Language/Reflection.idr+2−2

@@ -23,7 +23,7 @@ data TTUExp = UVar Int

2323%name TTUExp uexp

2424

2525-- | Primitive constants

26−data Const = I Int | BI Nat | Fl Float | Ch Char | Str String

26+data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

2828 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

2929 | B8Type | B16Type | B32Type | B64Type

@@ -37,7 +37,7 @@ abstract class ReflConst (a : Type) where

3737instance ReflConst Int where

3838 toConst x = I x

3939

40−instance ReflConst Nat where

40+instance ReflConst Integer where

4141 toConst = BI

4242

4343instance ReflConst Float where

libs/base/Language/Reflection/Errors.idr+1−1

@@ -2,7 +2,7 @@ module Language.Reflection.Errors

22

33import Language.Reflection

44

5−record SourceLocation : Type where

5+data SourceLocation : Type where

66 FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation

77

88%name SourceLocation loc

libs/base/Language/Reflection/Utils.idr+1

@@ -232,6 +232,7 @@ instance Show Err where

232232 show xs ++ " " ++ show y

233233 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs

234234 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs

235+ show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt

235236 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs

236237 show (CantInferType x) = "CantInferType " ++ show x

237238 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'

src/IRTS/Compiler.hs+3−3

@@ -218,13 +218,13 @@ instance ToIR (TT Name) where

218218 let collapse

219219 = case lookupCtxtExact n

220220 (idris_optimisation i) of

221− [oi] -> collapsible oi

221+ Just oi -> collapsible oi

222222 _ -> False

223223 let unused

224224 = case lookupCtxtExact n

225225 (idris_callgraph i) of

226− [CGInfo _ _ _ _ unusedpos] ->

227− unusedpos

226+ Just (CGInfo _ _ _ _ unusedpos) ->

227+ unusedpos

228228 _ -> []

229229 if collapse

230230 then return LNothing

src/IRTS/Defunctionalise.hs+8−8

@@ -81,17 +81,17 @@ addApps defs (n, LFun _ _ args e)

8181 aa env (LApp tc (LV (Glob n)) args)

8282 = do args' <- mapM (aa env) args

8383 case lookupCtxtExact n defs of

84− [LConstructor _ i ar] -> return $ DApp tc n args'

85− [LFun _ _ as _] -> let arity = length as in

86− fixApply tc n args' arity

87− [] -> return $ chainAPPLY (DV (Glob n)) args'

84+ Just (LConstructor _ i ar) -> return $ DApp tc n args'

85+ Just (LFun _ _ as _) -> let arity = length as in

86+ fixApply tc n args' arity

87+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'

8888 aa env (LLazyApp n args)

8989 = do args' <- mapM (aa env) args

9090 case lookupCtxtExact n defs of

91− [LConstructor _ i ar] -> return $ DApp False n args'

92− [LFun _ _ as _] -> let arity = length as in

93− fixLazyApply n args' arity

94− [] -> return $ chainAPPLY (DV (Glob n)) args'

91+ Just (LConstructor _ i ar) -> return $ DApp False n args'

92+ Just (LFun _ _ as _) -> let arity = length as in

93+ fixLazyApply n args' arity

94+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'

9595 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)

9696 aa env (LForce e) = liftM eEVAL (aa env e)

9797 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)

src/IRTS/Simplified.hs+14−14

@@ -48,7 +48,7 @@ simplify tl (DV (Loc i)) = return (SV (Loc i))

4848simplify tl (DV (Glob x))

4949 = do ctxt <- ldefs

5050 case lookupCtxtExact x ctxt of

51− [DConstructor _ t 0] -> return $ SCon t x []

51+ Just (DConstructor _ t 0) -> return $ SCon t x []

5252 _ -> return $ SV (Glob x)

5353simplify tl (DApp tc n args) = do args' <- mapM sVar args

5454 mkapp (SApp (tl || tc) n) args'

@@ -90,7 +90,7 @@ simplify tl (DError str) = return $ SError str

9090sVar (DV (Glob x))

9191 = do ctxt <- ldefs

9292 case lookupCtxtExact x ctxt of

93− [DConstructor _ t 0] -> sVar (DC t x [])

93+ Just (DConstructor _ t 0) -> sVar (DC t x [])

9494 _ -> return (Glob x, Nothing)

9595sVar (DV x) = return (x, Nothing)

9696sVar e = do e' <- simplify False e

@@ -138,23 +138,23 @@ scopecheck ctxt envTop tm = sc envTop tm where

138138 case lookup n (reverse env) of -- most recent first

139139 Just i -> do lvar i; return (SV (Loc i))

140140 Nothing -> case lookupCtxtExact n ctxt of

141− [DConstructor _ i ar] ->

141+ Just (DConstructor _ i ar) ->

142142 if True -- ar == 0

143143 then return (SCon i n [])

144144 else fail $ "Codegen error: Constructor " ++ show n ++

145145 " has arity " ++ show ar

146− [_] -> return (SV (Glob n))

147− [] -> fail $ "Codegen error: No such variable " ++ show n

146+ Just _ -> return (SV (Glob n))

147+ Nothing -> fail $ "Codegen error: No such variable " ++ show n

148148 sc env (SApp tc f args)

149149 = do args' <- mapM (scVar env) args

150150 case lookupCtxtExact f ctxt of

151− [DConstructor n tag ar] ->

151+ Just (DConstructor n tag ar) ->

152152 if True -- (ar == length args)

153153 then return $ SCon tag n args'

154154 else fail $ "Codegen error: Constructor " ++ show f ++

155155 " has arity " ++ show ar

156− [_] -> return $ SApp tc f args'

157− [] -> fail $ "Codegen error: No such variable " ++ show f

156+ Just _ -> return $ SApp tc f args'

157+ Nothing -> fail $ "Codegen error: No such variable " ++ show f

158158 sc env (SForeign l ty f args)

159159 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

160160 return (t, a')) args

@@ -162,7 +162,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

162162 sc env (SCon tag f args)

163163 = do args' <- mapM (scVar env) args

164164 case lookupCtxtExact f ctxt of

165− [DConstructor n tag ar] ->

165+ Just (DConstructor n tag ar) ->

166166 if True -- (ar == length args)

167167 then return $ SCon tag n args'

168168 else fail $ "Codegen error: Constructor " ++ show f ++

@@ -199,17 +199,17 @@ scopecheck ctxt envTop tm = sc envTop tm where

199199 case lookup n (reverse env) of -- most recent first

200200 Just i -> do lvar i; return (Loc i)

201201 Nothing -> case lookupCtxtExact n ctxt of

202− [DConstructor _ i ar] ->

202+ Just (DConstructor _ i ar) ->

203203 fail $ "Codegen error : can't pass constructor here"

204− [_] -> return (Glob n)

205− [] -> fail $ "Codegen error: No such variable " ++ show n ++

206− " in " ++ show tm ++ " " ++ show envTop

204+ Just _ -> return (Glob n)

205+ Nothing -> fail $ "Codegen error: No such variable " ++ show n ++

206+ " in " ++ show tm ++ " " ++ show envTop

207207 scVar _ x = return x

208208

209209 scalt env (SConCase _ i n args e)

210210 = do let env' = env ++ zip args [length env..]

211211 tag <- case lookupCtxtExact n ctxt of

212− [DConstructor _ i ar] ->

212+ Just (DConstructor _ i ar) ->

213213 if True -- (length args == ar)

214214 then return i

215215 else fail $ "Codegen error: Constructor " ++ show n ++

src/Idris/AbsSyntax.hs+33−3

@@ -25,7 +25,9 @@ import Data.List

2525import Data.Char

2626import qualified Data.Text as T

2727import Data.Either

28+import qualified Data.Map as M

2829import Data.Maybe

30+import qualified Data.Set as S

2931import Data.Word (Word)

3032

3133import Debug.Trace

@@ -152,6 +154,24 @@ addToCG n cg

152154 = do i <- getIState

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

154156

157+-- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.

158+addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

159+addFunctionErrorHandlers f arg hs =

160+ do i <- getIState

161+ let oldHandlers = idris_function_errorhandlers i

162+ let newHandlers = flip (addDef f) oldHandlers $

163+ case lookupCtxtExact f oldHandlers of

164+ Nothing -> M.singleton arg (S.fromList hs)

165+ Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers

166+ -- will always be one of those two, thus no extra case

167+ putIState $ i { idris_function_errorhandlers = newHandlers }

168+

169+getFunctionErrorHandlers :: Name -> Name -> Idris [Name]

170+getFunctionErrorHandlers f arg = do i <- getIState

171+ return . maybe [] S.toList $

172+ undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)

173+

174+

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

156176getAllNames :: Name -> Idris [Name]

157177getAllNames n = allNames [] n

@@ -160,8 +180,8 @@ allNames :: [Name] -> Name -> Idris [Name]

160180allNames ns n | n `elem` ns = return []

161181allNames ns n = do i <- getIState

162182 case lookupCtxtExact n (idris_callgraph i) of

163− [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

164− return (nub (n : concat more))

183+ Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

184+ return (nub (n : concat more))

165185 _ -> return [n]

166186

167187addCoercion :: Name -> Idris ()

@@ -545,10 +565,20 @@ setREPL t = do i <- getIState

545565 let opt' = opts { opt_repl = t }

546566 putIState $ i { idris_options = opt' }

547567

568+showOrigErr :: Idris Bool

569+showOrigErr = do i <- getIState

570+ return (opt_origerr (idris_options i))

571+

572+setShowOrigErr :: Bool -> Idris ()

573+setShowOrigErr b = do i <- getIState

574+ let opts = idris_options i

575+ let opt' = opts { opt_origerr = b }

576+ putIState $ i { idris_options = opt' }

577+

548578setNoBanner :: Bool -> Idris ()

549579setNoBanner n = do i <- getIState

550580 let opts = idris_options i

551− let opt' = opts {opt_nobanner = n}

581+ let opt' = opts { opt_nobanner = n }

552582 putIState $ i { idris_options = opt' }

553583

554584getNoBanner :: Idris Bool

src/Idris/AbsSyntaxTree.hs+12−3

@@ -24,9 +24,11 @@ import Control.Monad.Trans.Error

2424

2525import Data.List

2626import Data.Char

27+import qualified Data.Map as M

2728import qualified Data.Text as T

2829import qualified Data.Map as M

2930import Data.Either

31+import qualified Data.Set as S

3032import Data.Word (Word)

3133

3234import Debug.Trace

@@ -50,7 +52,8 @@ data IOption = IOption { opt_logLevel :: Int,

5052 opt_triple :: String,

5153 opt_cpu :: String,

5254 opt_optLevel :: Word,

53− opt_cmdline :: [Opt] -- remember whole command line

55+ opt_cmdline :: [Opt], -- remember whole command line

56+ opt_origerr :: Bool

5457 }

5558 deriving (Show, Eq)

5659

@@ -72,6 +75,7 @@ defaultOpts = IOption { opt_logLevel = 0

7275 , opt_cpu = ""

7376 , opt_optLevel = 2

7477 , opt_cmdline = []

78+ , opt_origerr = False

7579 }

7680

7781data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

@@ -137,9 +141,11 @@ data IState = IState {

137141 idris_colourRepl :: Bool,

138142 idris_colourTheme :: ColourTheme,

139143 idris_outh :: Handle,

140− idris_errorhandlers :: [Name],

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

141145 idris_nameIdx :: (Int, Ctxt (Int, Name)),

146+ idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

142147 module_aliases :: M.Map [T.Text] [T.Text]

148+

143149 }

144150

145151data SizeChange = Smaller | Same | Bigger | Unknown

@@ -196,6 +202,8 @@ data IBCWrite = IBCFix FixDecl

196202 | IBCDef Name -- i.e. main context

197203 | IBCNameHint (Name, Name)

198204 | IBCLineApp FilePath Int PTerm

205+ | IBCErrorHandler Name

206+ | IBCFunctionErrorHandler Name Name Name

199207 deriving Show

200208

201209-- | The initial state for the compiler

@@ -206,7 +214,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

206214 emptyContext

207215 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

208216 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

209− True defaultTheme stdout [] (0, emptyContext) M.empty

217+ True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

210218

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

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

@@ -315,6 +323,7 @@ data Opt = Filename String

315323 | TargetCPU String

316324 | OptLevel Word

317325 | Client String

326+ | ShowOrigErr

318327 deriving (Show, Eq)

319328

320329-- Parsed declarations

src/Idris/Completion.hs+1−1

@@ -104,7 +104,7 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

104104

105105completeOption :: CompletionFunc Idris

106106completeOption = completeWord Nothing " \t" completeOpt

107− where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])

107+ where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]

108108

109109isWhitespace :: Char -> Bool

110110isWhitespace = (flip elem) " \t\n"

src/Idris/Core/Elaborate.hs+18−13

@@ -401,8 +401,11 @@ qed = do processTactic' QED

401401undo :: Elab' aux ()

402402undo = processTactic' Undo

403403

404−prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]

405−prepare_apply fn imps =

404+-- | Prepare to apply a function by creating holes to be filled by the arguments

405+prepare_apply :: Raw -- ^ The operation being applied

406+ -> [Bool] -- ^ Whether arguments are implicit

407+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes to be filled with elaborated argument values

408+prepare_apply fn imps =

406409 do ty <- get_type fn

407410 ctxt <- get_context

408411 env <- get_env

@@ -414,11 +417,13 @@ prepare_apply fn imps =

414417 let n = length (filter not imps)

415418 let (h : hs) = holes p

416419 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

417−-- case claims of

418−-- [] -> return ()

419−-- (h : _) -> reorder_claims h

420420 return $! claims

421421 where

422+ mkClaims :: Type -- ^ The type of the operation being applied

423+ -> [Bool] -- ^ Whether the arguments are implicit

424+ -> [(Name, Name)] -- ^ Accumulator for produced claims

425+ -> [Name] -- ^ Hypotheses

426+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

422427 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

423428 do let t = rebind hs t_in

424429 n <- getNameFrom (mkMN n')

@@ -427,7 +432,7 @@ prepare_apply fn imps =

427432-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

428433 claim n (forget t)

429434 when i (movelast n)

430− mkClaims sc' is (n : claims) hs

435+ mkClaims sc' is ((n', n) : claims) hs

431436 mkClaims t [] claims _ = return $! (reverse claims)

432437 mkClaims _ _ _ _

433438 | Var n <- fn

@@ -452,11 +457,11 @@ prepare_apply fn imps =

452457 rebind hs (App f a) = App (rebind hs f) (rebind hs a)

453458 rebind hs t = t

454459

455−apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

460+apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

456461apply = apply' fill

457462match_apply = apply' match_fill

458463

459−apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

464+apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

460465apply' fillt fn imps =

461466 do args <- prepare_apply fn (map fst imps)

462467 -- _Don't_ solve the arguments we're specifying by hand.

@@ -468,7 +473,7 @@ apply' fillt fn imps =

468473 let dont = head hs : dontunify p ++

469474 if null imps then [] -- do all we can

470475 else

471− map fst (filter (not.snd) (zip args (map fst imps)))

476+ map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

472477 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

473478 unified p

474479 let unify = -- trace ("Not done " ++ show hs) $

@@ -477,10 +482,10 @@ apply' fillt fn imps =

477482 keepGiven dont hunis hs

478483 put (ES (p { dontunify = dont, unified = (n, unify),

479484 notunified = notunify ++ notunified p }, a) s prev)

480− fillt (raw_apply fn (map Var args))

485+ fillt (raw_apply fn (map (Var . snd) args))

481486-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

482487 end_unify

483− return $! (map (updateUnify unify) args)

488+ return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

484489 where updateUnify us n = case lookup n us of

485490 Just (P _ t _) -> t

486491 _ -> n

@@ -488,8 +493,8 @@ apply' fillt fn imps =

488493apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

489494apply2 fn elabs =

490495 do args <- prepare_apply fn (map isJust elabs)

491− fill (raw_apply fn (map Var args))

492− elabArgs args elabs

496+ fill (raw_apply fn (map (Var . snd) args))

497+ elabArgs (map snd args) elabs

493498 ES (p, a) s prev <- get

494499 let (n, hs) = unified p

495500 end_unify

src/Idris/Core/TT.hs+3−2

@@ -29,6 +29,7 @@ import qualified Data.Map.Strict as Map

2929import Data.Char

3030import qualified Data.Text as T

3131import Data.List

32+import Data.Maybe (listToMaybe)

3233import Data.Vector.Unboxed (Vector)

3334import qualified Data.Vector.Unboxed as V

3435import qualified Data.Binary as B

@@ -412,8 +413,8 @@ lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of

412413lookupCtxt :: Name -> Ctxt a -> [a]

413414lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

414415

415−lookupCtxtExact :: Name -> Ctxt a -> [a]

416−lookupCtxtExact n ctxt = [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

416+lookupCtxtExact :: Name -> Ctxt a -> Maybe a

417+lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

417418

418419updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

419420updateDef n f ctxt

src/Idris/Delaborate.hs+4−2

@@ -206,8 +206,10 @@ pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

206206pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

207207pprintErr' i (ReflectionError parts orig) =

208208 let parts' = map (hsep . map showPart) parts in

209− vsep parts' <> line <> line <>

210− text "Original error:" <$> indented (pprintErr' i orig)

209+ vsep parts' <>

210+ if (opt_origerr (idris_options i))

211+ then line <> line <> text "Original error:" <$> indented (pprintErr' i orig)

212+ else empty

211213 where showPart :: ErrorReportPart -> Doc OutputAnnotation

212214 showPart (TextPart str) = text str

213215 showPart (NamePart n) = annName n

src/Idris/ElabDecls.hs+1

@@ -126,6 +126,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

126126 if tyIsHandler nty'

127127 then do i <- getIState

128128 putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }

129+ addIBC (IBCErrorHandler n)

129130 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

130131 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

131132 when corec $ do setAccessibility n Frozen

src/Idris/ElabTerm.hs+112−54

@@ -13,10 +13,14 @@ import Idris.Core.TT

1313import Idris.Core.Evaluate

1414import Idris.Core.Typecheck (check)

1515

16+import Control.Applicative ((<$>))

1617import Control.Monad

1718import Control.Monad.State.Strict

1819import Data.List

20+import qualified Data.Map as M

1921import Data.Maybe (mapMaybe)

22+import qualified Data.Set as S

23+import qualified Data.Text as T

2024

2125import Debug.Trace

2226

@@ -153,13 +157,18 @@ elab ist info pattern opts fn tm

153157

154158 local f = do e <- get_env

155159 return (f `elem` map fst e)

156−

160+

161+ -- | Is a constant a type?

162+ constType :: Const -> Bool

157163 constType (AType _) = True

158164 constType StrType = True

159165 constType PtrType = True

160166 constType VoidType = True

161167 constType _ = False

162168

169+ elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

170+ -> PTerm -- ^ The term to elaborate

171+ -> ElabD ()

163172 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

164173 elab' ina PType = do apply RType []; solve

165174 elab' (_,_,inty) (PConstant c)

@@ -387,7 +396,7 @@ elab ist info pattern opts fn tm

387396 solve

388397 elab' (_, _, inty) (PApp fc (PRef _ f) args')

389398 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

390− = lift $ tfail (Msg "Typecase is not allowed")

399+ = lift $ tfail (Msg "Typecase is not allowed")

391400 -- if f is local, just do a simple_app

392401 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

393402 = do env <- get_env

@@ -410,16 +419,18 @@ elab ist info pattern opts fn tm

410419 _ -> mapM_ setInjective (map getTm args)

411420 ctxt <- get_context

412421 let guarded = isConName f ctxt

422+-- trace ("args is " ++ show args) $ return ()

413423 ns <- apply (Var f) (map isph args)

424+-- trace ("ns is " ++ show ns) $ return ()

414425 -- Sort so that the implicit tactics and alternatives go last

415426 let (ns', eargs) = unzip $

416427 sortBy cmpArg (zip ns args)

417− elabArgs (ina || not isinf, guarded, inty)

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

428+ elabArgs ist (ina || not isinf, guarded, inty)

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

419430 solve

420431 ivs' <- get_instances

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

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

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

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

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

424435 mapM_ (\n -> do focus n

425436 g <- goal

@@ -603,31 +614,74 @@ elab ist info pattern opts fn tm

603614 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

604615 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

605616

606− elabArgs ina failed fc retry [] _

617+ -- | Elaborate the arguments to a function

618+ elabArgs :: IState -- ^ The current Idris state

619+ -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

620+ -> [Bool]

621+ -> FC -- ^ Source location

622+ -> Bool

623+ -> Name -- ^ Name of the function being applied

624+ -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

625+ -> [(Bool, PTerm)] -- ^ (Laziness, argument)

626+ -> ElabD ()

627+ elabArgs ist ina failed fc retry f [] _

607628-- | retry = let (ns, ts) = unzip (reverse failed) in

608629-- elabArgs ina [] False ns ts

609630 | otherwise = return ()

610− elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args)

611− = elabArgs ina failed fc r ns args

612− elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

631+ elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args)

632+ = elabArgs ist ina failed fc r f ns args

633+ elabArgs ist ina failed fc r f ((argName, holeName):ns) ((lazy, t) : args)

613634 | lazy && not pattern

614− = do elabArg n (PApp bi (PRef bi (sUN "lazy"))

615− [pimp (sUN "a") Placeholder True,

616− pexp t]);

617− | otherwise = elabArg n t

618− where elabArg n t

619− = do hs <- get_holes

620− tm <- get_term

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

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

623− case n `elem` hs of

624− True ->

625−-- if r

626−-- then try (do focus n; elabE ina t; return failed)

627−-- (return ((n,(lazy, t)):failed))

628− do focus n; elabE ina t; return failed

629− False -> return failed

630− elabArgs ina failed fc r ns args

635+ = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

636+ [pimp (sUN "a") Placeholder True,

637+ pexp t])

638+ | otherwise = elabArg argName holeName t

639+ where elabArg argName holeName t =

640+ reflectFunctionErrors ist f argName $

641+ do hs <- get_holes

642+ tm <- get_term

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

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

645+ case holeName `elem` hs of

646+ True -> do focus holeName; elabE ina t; return failed

647+ False -> return failed

648+ elabArgs ist ina failed fc r f ns args

649+

650+-- | Perform error reflection for function applicaitons with specific error handlers

651+reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a

652+reflectFunctionErrors ist f arg action =

653+ do elabState <- get

654+ (result, newState) <- case runStateT action elabState of

655+ OK (res, newState) -> return (res, newState)

656+ Error e@(ReflectionError _ _) -> (lift . tfail) e

657+ Error e@(ReflectionFailed _ _) -> (lift . tfail) e

658+ Error e -> handle e >>= lift . tfail

659+ put newState

660+ return result

661+ where handle :: Err -> ElabD Err

662+ handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist

663+ handlers = (maybe [] S.toList . M.lookup arg) funhandlers

664+ reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

665+

666+

667+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!

668+ handlers <- case mapM (check (tt_ctxt ist) []) reports of

669+ Error e -> lift . tfail $

670+ ReflectionFailed "Type error while constructing reflected error" e

671+ OK hs -> return hs

672+

673+ -- Normalize error handler terms to produce the new messages

674+ let ctxt = tt_ctxt ist

675+ results = map (normalise ctxt []) (map fst handlers)

676+

677+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

678+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

679+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

680+ Left err -> lift (tfail err)

681+ Right ok -> return ok

682+ return $ case errorparts of

683+ [] -> e

684+ parts -> ReflectionError errorparts e

631685

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

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

@@ -764,8 +818,8 @@ resolveTC depth topg fn ist

764818 [args] -> map isImp (snd args) -- won't be overloaded!

765819 ps <- get_probs

766820 tm <- get_term

767− args <- try' (apply (Var n) imps)

768− (match_apply (Var n) imps) True

821+ args <- map snd <$> try' (apply (Var n) imps)

822+ (match_apply (Var n) imps) True

769823 ps' <- get_probs

770824 when (length ps < length ps') $ fail "Can't apply type class"

771825-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

@@ -778,7 +832,7 @@ resolveTC depth topg fn ist

778832 -- if there's any arguments left, we've failed to resolve

779833 hs <- get_holes

780834 ulog <- getUnifyLog

781− solve

835+ solve

782836 traceWhen ulog ("Got " ++ show n) $ return ()

783837 where isImp (PImp p _ _ _ _ _) = (True, p)

784838 isImp arg = (False, priority arg)

@@ -1134,7 +1188,7 @@ reifyRawApp t [c]

11341188reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

11351189

11361190reifyTTName :: Term -> ElabD Name

1137−reifyTTName t@(App _ _)

1191+reifyTTName t

11381192 | (P _ f _, args) <- unApply t = reifyTTNameApp f args

11391193reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

11401194

@@ -1470,6 +1524,7 @@ reflectErr (LoadingFailed str err) =

14701524 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

14711525reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

14721526

1527+

14731528withErrorReflection :: Idris a -> Idris a

14741529withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

14751530 where handle :: Err -> Idris Err

@@ -1495,47 +1550,50 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

14951550

14961551 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

14971552 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1498− errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1499−

1553+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

1554+ Left err -> ierror err

1555+ Right ok -> return ok

15001556 return $ case errorparts of

15011557 [] -> e

15021558 parts -> ReflectionError errorparts e

15031559

1504− fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1505− fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1506− | just == txt "Just" = Just tm

1507− fromTTMaybe x = Nothing

1560+fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1561+fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1562+ | just == txt "Just" = Just tm

1563+fromTTMaybe x = Nothing

15081564

15091565reflErrName :: String -> Name

15101566reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

15111567

1512−reifyReportPart :: Term -> Idris ErrorReportPart

1568+-- | Attempt to reify a report part from TT to the internal

1569+-- representation. Not in Idris or ElabD monads because it should be usable

1570+-- from either.

1571+reifyReportPart :: Term -> Either Err ErrorReportPart

15131572reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

1514− return (TextPart msg)

1573+ Right (TextPart msg)

15151574reifyReportPart (App (P (DCon _ _) n _) ttn)

15161575 | n == reflErrName "NamePart" =

15171576 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

1518− Error e -> ierror . InternalMsg $

1577+ Error e -> Left . InternalMsg $

15191578 "could not reify name term " ++

15201579 show ttn ++

1521− " when reflecting an error"

1522− OK (n', _)-> return $ NamePart n'

1580+ " when reflecting an error:" ++ show e

1581+ OK (n', _)-> Right $ NamePart n'

15231582reifyReportPart (App (P (DCon _ _) n _) tm)

15241583 | n == reflErrName "TermPart" =

1525− do ist <- getIState

1526− case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1527− Error e -> ierror . InternalMsg $

1528− "could not reify reflected term " ++

1529− show tm ++

1530− " when reflecting an error"

1531− OK (tm', _) -> return $ TermPart tm'

1584+ case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1585+ Error e -> Left . InternalMsg $

1586+ "could not reify reflected term " ++

1587+ show tm ++

1588+ " when reflecting an error:" ++ show e

1589+ OK (tm', _) -> Right $ TermPart tm'

15321590reifyReportPart (App (P (DCon _ _) n _) tm)

15331591 | n == reflErrName "SubReport" =

1534− case unList tm of

1535− Just xs -> do subParts <- mapM reifyReportPart xs

1536− return (SubReport subParts)

1537− Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm

1538−reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x

1592+ case unList tm of

1593+ Just xs -> do subParts <- mapM reifyReportPart xs

1594+ Right (SubReport subParts)

1595+ Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

1596+reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

15391597

15401598envTupleType :: Raw

15411599envTupleType

src/Idris/IBC.hs+26−4

@@ -28,6 +28,7 @@ import Util.Zlib (decompressEither)

2828ibcVersion :: Word8

2929ibcVersion = 56

3030

31+

3132data IBCFile = IBCFile { ver :: Word8,

3233 sourcefile :: FilePath,

3334 symbols :: [Name],

@@ -58,7 +59,9 @@ data IBCFile = IBCFile { ver :: Word8,

5859 ibc_coercions :: [Name],

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

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

61− ibc_metainformation :: [(Name, MetaInformation)]

62+ ibc_metainformation :: [(Name, MetaInformation)],

63+ ibc_errorhandlers :: [Name],

64+ ibc_function_errorhandlers :: [(Name, Name, Name)] -- fn, arg, handler

6265 }

6366 deriving Show

6467{-!

@@ -66,7 +69,8 @@ deriving instance Binary IBCFile

6669!-}

6770

6871initIBC :: IBCFile

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

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

73+

7074

7175loadIBC :: FilePath -> Idris ()

7276loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -215,6 +219,9 @@ ibc i (IBCLineApp fp l t) f

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

216220 = return f { ibc_namehints = (n, ty) : ibc_namehints f }

217221ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_metainformation f }

222+ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

223+ibc i (IBCFunctionErrorHandler fn a n) f =

224+ return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

218225

219226process :: IBCFile -> FilePath -> Idris ()

220227process i fn

@@ -253,6 +260,8 @@ process i fn

253260 pLineApps (ibc_lineapps i)

254261 pNameHints (ibc_namehints i)

255262 pMetaInformation (ibc_metainformation i)

263+ pErrorHandlers (ibc_errorhandlers i)

264+ pFunctionErrorHandlers (ibc_function_errorhandlers i)

256265

257266timestampOlder :: FilePath -> FilePath -> IO ()

258267timestampOlder src ibc = do srct <- getModificationTime src

@@ -434,6 +443,14 @@ pMetaInformation ds = mapM_ (\ (n, m) ->

434443 putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))

435444 ds

436445

446+pErrorHandlers :: [Name] -> Idris ()

447+pErrorHandlers ns = do i <- getIState

448+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ ns }

449+

450+pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

451+pFunctionErrorHandlers [] = return ()

452+pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

453+ pFunctionErrorHandlers ns

437454----- Generated by 'derive'

438455

439456instance Binary SizeChange where

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

10181035 return (DataMI x1)

10191036

10201037instance Binary IBCFile where

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)

1038+ 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 x32 x33)

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

10231040 do put x1

10241041 put x2

@@ -1051,6 +1068,9 @@ instance Binary IBCFile where

10511068 put x29

10521069 put x30

10531070 put x31

1071+ put x32

1072+ put x33

1073+

10541074 get

10551075 = do x1 <- get

10561076 if x1 == ibcVersion then

@@ -1084,7 +1104,9 @@ instance Binary IBCFile where

10841104 x29 <- get

10851105 x30 <- get

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

1107+ x32 <- get

1108+ x33 <- get

1109+ 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 x32 x33)

10881110 else return (initIBC { ver = x1 })

10891111

10901112instance Binary DataOpt where

src/Idris/ParseExpr.hs+1

@@ -1035,6 +1035,7 @@ constant = do reserved "Integer";return (AType (ATInt ITBig))

10351035@

10361036VerbatimString_t ::=

10371037 '\"\"\"' ~'\"\"\"' '\"\"\"'

1038+;

10381039@

10391040 -}

10401041verbatimStringLiteral :: MonadicParsing m => m String

src/Idris/Parser.hs+32−21

@@ -58,6 +58,7 @@ import qualified Data.Map as M

5858import qualified Data.HashSet as HS

5959import qualified Data.Text as T

6060import qualified Data.ByteString.UTF8 as UTF8

61+import qualified Data.Set as S

6162

6263import Debug.Trace

6364

@@ -937,19 +938,20 @@ Directive ::= '%' Directive';

937938@

938939

939940@

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

941− | 'link' CodeGen String_t

942− | 'flag' CodeGen String_t

943− | 'include' CodeGen String_t

944− | 'hide' Name

945− | 'freeze' Name

946− | 'access' Accessibility

947− | 'default' Totality

948− | 'logging' Natural

949− | 'dynamic' StringList

950− | 'name' Name NameList

951− | 'language' 'TypeProviders'

952− | 'language' 'ErrorReflection'

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

942+ | 'link' CodeGen String_t

943+ | 'flag' CodeGen String_t

944+ | 'include' CodeGen String_t

945+ | 'hide' Name

946+ | 'freeze' Name

947+ | 'access' Accessibility

948+ | 'default' Totality

949+ | 'logging' Natural

950+ | 'dynamic' StringList

951+ | 'name' Name NameList

952+ | 'error_handlers' Name NameList

953+ | 'language' 'TypeProviders'

954+ | 'language' 'ErrorReflection'

953955 ;

954956@

955957-}

@@ -994,17 +996,26 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

994996 <|> do try (lchar '%' *> reserved "name")

995997 ty <- iName []

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

997− return [PDirective

998− (do i <- getIState

999− ty' <- case lookupCtxtName ty (idris_implicits i) of

1000− [(tyn, _)] -> return tyn

1001− [] -> throwError (NoSuchVariable ty)

1002− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

1003− mapM_ (addNameHint ty') ns

1004− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

999+ return [PDirective (do ty' <- disambiguate ty

1000+ mapM_ (addNameHint ty') ns

1001+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1002+ <|> do try (lchar '%' *> reserved "error_handlers")

1003+ fn <- iName []

1004+ arg <- iName []

1005+ ns <- sepBy1 name (lchar ',')

1006+ return [PDirective (do fn' <- disambiguate fn

1007+ ns' <- mapM disambiguate ns

1008+ addFunctionErrorHandlers fn' arg ns'

1009+ mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]

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

10061011 return [PDirective (addLangExt ext)]

10071012 <?> "directive"

1013+ where disambiguate :: Name -> Idris Name

1014+ disambiguate n = do i <- getIState

1015+ case lookupCtxtName n (idris_implicits i) of

1016+ [(n', _)] -> return n'

1017+ [] -> throwError (NoSuchVariable n)

1018+ more -> throwError (CantResolveAlts (map (show . fst) more))

10081019

10091020pLangExt :: IdrisParser LanguageExt

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

src/Idris/ProofSearch.hs+2−1

@@ -10,6 +10,7 @@ import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

1212

13+import Control.Applicative ((<$>))

1314import Control.Monad

1415import Debug.Trace

1516

@@ -86,7 +87,7 @@ proofSearch elab fn nroot hints ist = psRec maxDepth

8687 [args] -> map isImp (snd args)

8788 _ -> fail "Ambiguous name"

8889 ps <- get_probs

89− args <- apply (Var n) imps

90+ args <- map snd <$> apply (Var n) imps

9091 ps' <- get_probs

9192 when (length ps < length ps') $ fail "Can't apply constructor"

9293 mapM_ (\ (_, h) -> do focus h

src/Idris/REPL.hs+10−4

@@ -312,6 +312,10 @@ ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)

312312 iPrintResult ""

313313ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)

314314 iPrintResult ""

315+ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)

316+ iPrintResult ""

317+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)

318+ iPrintResult ""

315319ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

316320ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

317321ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

@@ -905,10 +909,12 @@ process h fn Metavars

905909 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

906910process h fn NOP = return ()

907911

908−process h fn (SetOpt ErrContext) = setErrContext True

909−process h fn (UnsetOpt ErrContext) = setErrContext False

910−process h fn (SetOpt ShowImpl) = setImpShow True

911−process h fn (UnsetOpt ShowImpl) = setImpShow False

912+process h fn (SetOpt ErrContext) = setErrContext True

913+process h fn (UnsetOpt ErrContext) = setErrContext False

914+process h fn (SetOpt ShowImpl) = setImpShow True

915+process h fn (UnsetOpt ShowImpl) = setImpShow False

916+process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

917+process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

912918

913919process h fn (SetOpt _) = iPrintError "Not a valid option"

914920process h fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs+3−3

@@ -61,8 +61,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

6161 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

6262 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

6363 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

64− <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

65− <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

64+ <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

65+ <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

6666 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

6767 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

6868 upd <- option False (do P.lchar '!'; return True)

@@ -105,7 +105,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

105105pOption :: P.IdrisParser Opt

106106pOption = do discard (P.symbol "errorcontext"); return ErrContext

107107 <|> do discard (P.symbol "showimplicits"); return ShowImpl

108−

108+ <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

109109

110110colours :: [(String, Maybe Color)]

111111colours = [ ("black", Just Black)

test/test037/expected−14

@@ -1,17 +1,3 @@

11In file ErrorReflection.idr line 78 column 5

22 When elaborating right hand side of Main.bad :

33 DSL type error: (t'(504) => t'(504)) 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 [] (TFun t' t')

10− with

11− Tm [] TUnit

12−

13− Specifically:

14− Can't unify

15− TFun t' t'

16− with

17− TUnit

test/test038/FunErrTest.idrnew file+41

@@ -0,0 +1,41 @@

1+module FunErrTest

2+

3+import Language.Reflection

4+import Language.Reflection.Errors

5+import Language.Reflection.Utils

6+

7+%language ErrorReflection

8+

9+total

10+cadr : (xs : List a)

11+ -> {auto cons1 : isCons xs = True}

12+ -> {auto cons2 : isCons (tail xs cons1) = True}

13+ -> a

14+cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

15+cadr (x :: []) {cons1=refl} {cons2=refl} impossible

16+

17+extractList : TT -> Maybe TT

18+extractList (App (App reflCon (App isCons lst)) _) = Just lst

19+extractList _ = Nothing

20+

21+

22+total

23+has2elts : Err -> Maybe (List ErrorReportPart)

24+has2elts (CantSolveGoal tm _) = do lst <- extractList tm

25+ return [ TextPart "Could not prove that"

26+ , TermPart lst

27+ , TextPart "has at least two elements."

28+ ]

29+has2elts e = Just [TextPart (show e)]

30+

31+%error_handlers cadr cons1 has2elts

32+%error_handlers cadr cons2 has2elts

33+

34+badCadr1 : Int

35+badCadr1 = cadr []

36+

37+badCadr2 : Int

38+badCadr2 = cadr [1]

39+

40+goodCadr : Int

41+goodCadr = cadr [1, 2]

test/test038/expectednew file+4

@@ -0,0 +1,4 @@

1+FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

2+Could not prove that [] has at least two elements.

3+FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

4+Could not prove that tail [(fromInteger 1)] refl has at least two elements.

test/test038/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ FunErrTest.idr --nocolour --check

3+rm -f *.ibc

test/test039/run+1

@@ -2,3 +2,4 @@

22idris $@ -o test038 test038.idr --nocolour

33./test038

44rm -f test038 *.ibc

5+