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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #794 from david-christiansen/error-reflection

60abf37Edwin Brady13 years ago

idris.cabal+3

compare with master

unifiedsplit

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

320 test/test037/run

321 test/test037/expected

322 test/test037/*.idr

323+ test/test038/run

324+ test/test038/expected

325+ test/test038/*.idr

323 test/test039/run

326 test/test039/run

324 test/test039/expected

327 test/test039/expected

325 test/test039/*.idr

328 test/test039/*.idr

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

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

23%name TTUExp uexp

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

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

29 | B8Type | B16Type | B32Type | B64Type

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

37instance ReflConst Int where

38 toConst x = I x

40−instance ReflConst Nat where

40+instance ReflConst Integer where

41 toConst = BI

43instance ReflConst Float where

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

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

3import Language.Reflection

5−record SourceLocation : Type where

5+data SourceLocation : Type where

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

8%name SourceLocation loc

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

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

232 show xs ++ " " ++ show y

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

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

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

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

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

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

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

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

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

src/IRTS/Compiler.hs+3−3

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

218 let collapse

219 = case lookupCtxtExact n

220 (idris_optimisation i) of

221− [oi] -> collapsible oi

221+ Just oi -> collapsible oi

222 _ -> False

223 let unused

224 = case lookupCtxtExact n

225 (idris_callgraph i) of

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

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

227− unusedpos

227+ unusedpos

228 _ -> []

229 if collapse

230 then return LNothing

src/IRTS/Defunctionalise.hs+8−8

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

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

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

83 case lookupCtxtExact n defs of

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

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

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

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

86− fixApply tc n args' arity

86+ fixApply tc n args' arity

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

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

88 aa env (LLazyApp n args)

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

90 case lookupCtxtExact n defs of

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

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

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

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

93− fixLazyApply n args' arity

93+ fixLazyApply n args' arity

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

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

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

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

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

48simplify tl (DV (Glob x))

49 = do ctxt <- ldefs

50 case lookupCtxtExact x ctxt of

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

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

52 _ -> return $ SV (Glob x)

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

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

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

90sVar (DV (Glob x))

91 = do ctxt <- ldefs

92 case lookupCtxtExact x ctxt of

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

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

94 _ -> return (Glob x, Nothing)

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

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

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

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

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

140 Nothing -> case lookupCtxtExact n ctxt of

141− [DConstructor _ i ar] ->

141+ Just (DConstructor _ i ar) ->

142 if True -- ar == 0

143 then return (SCon i n [])

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

145 " has arity " ++ show ar

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

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

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

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

148 sc env (SApp tc f args)

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

150 case lookupCtxtExact f ctxt of

151− [DConstructor n tag ar] ->

151+ Just (DConstructor n tag ar) ->

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

153 then return $ SCon tag n args'

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

155 " has arity " ++ show ar

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

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

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

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

158 sc env (SForeign l ty f args)

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

160 return (t, a')) args

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

162 sc env (SCon tag f args)

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

164 case lookupCtxtExact f ctxt of

165− [DConstructor n tag ar] ->

165+ Just (DConstructor n tag ar) ->

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

167 then return $ SCon tag n args'

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

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

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

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

201 Nothing -> case lookupCtxtExact n ctxt of

202− [DConstructor _ i ar] ->

202+ Just (DConstructor _ i ar) ->

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

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

204+ Just _ -> return (Glob n)

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

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

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

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

207 scVar _ x = return x

208

209 scalt env (SConCase _ i n args e)

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

211 tag <- case lookupCtxtExact n ctxt of

212− [DConstructor _ i ar] ->

212+ Just (DConstructor _ i ar) ->

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

214 then return i

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

src/Idris/AbsSyntax.hs+33−3

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

25import Data.Char

26import qualified Data.Text as T

27import Data.Either

28+import qualified Data.Map as M

28import Data.Maybe

29import Data.Maybe

30+import qualified Data.Set as S

29import Data.Word (Word)

31import Data.Word (Word)

31import Debug.Trace

33import Debug.Trace

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

152 = do i <- getIState

154 = do i <- getIState

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

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

154

156

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+

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

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

156getAllNames :: Name -> Idris [Name]

176getAllNames :: Name -> Idris [Name]

157getAllNames n = allNames [] n

177getAllNames n = allNames [] n

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

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

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

161allNames ns n = do i <- getIState

181allNames ns n = do i <- getIState

162 case lookupCtxtExact n (idris_callgraph i) of

182 case lookupCtxtExact n (idris_callgraph i) of

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

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

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

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

165 _ -> return [n]

185 _ -> return [n]

166

186

167addCoercion :: Name -> Idris ()

187addCoercion :: Name -> Idris ()

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

545 let opt' = opts { opt_repl = t }

565 let opt' = opts { opt_repl = t }

546 putIState $ i { idris_options = opt' }

566 putIState $ i { idris_options = opt' }

547

567

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+

548setNoBanner :: Bool -> Idris ()

578setNoBanner :: Bool -> Idris ()

549setNoBanner n = do i <- getIState

579setNoBanner n = do i <- getIState

550 let opts = idris_options i

580 let opts = idris_options i

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

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

552 putIState $ i { idris_options = opt' }

582 putIState $ i { idris_options = opt' }

553

583

554getNoBanner :: Idris Bool

584getNoBanner :: Idris Bool

src/Idris/AbsSyntaxTree.hs+12−3

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

25import Data.List

26import Data.Char

27+import qualified Data.Map as M

27import qualified Data.Text as T

28import qualified Data.Text as T

28import qualified Data.Map as M

29import qualified Data.Map as M

29import Data.Either

30import Data.Either

31+import qualified Data.Set as S

30import Data.Word (Word)

32import Data.Word (Word)

32import Debug.Trace

34import Debug.Trace

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

50 opt_triple :: String,

52 opt_triple :: String,

51 opt_cpu :: String,

53 opt_cpu :: String,

52 opt_optLevel :: Word,

54 opt_optLevel :: Word,

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

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

56+ opt_origerr :: Bool

54 }

57 }

55 deriving (Show, Eq)

58 deriving (Show, Eq)

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

72 , opt_cpu = ""

75 , opt_cpu = ""

73 , opt_optLevel = 2

76 , opt_optLevel = 2

74 , opt_cmdline = []

77 , opt_cmdline = []

78+ , opt_origerr = False

75 }

79 }

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

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

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

137 idris_colourRepl :: Bool,

141 idris_colourRepl :: Bool,

138 idris_colourTheme :: ColourTheme,

142 idris_colourTheme :: ColourTheme,

139 idris_outh :: Handle,

143 idris_outh :: Handle,

140− idris_errorhandlers :: [Name],

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

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

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

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

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

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

148+

143 }

149 }

144

150

145data SizeChange = Smaller | Same | Bigger | Unknown

151data SizeChange = Smaller | Same | Bigger | Unknown

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

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

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

197 | IBCNameHint (Name, Name)

203 | IBCNameHint (Name, Name)

198 | IBCLineApp FilePath Int PTerm

204 | IBCLineApp FilePath Int PTerm

205+ | IBCErrorHandler Name

206+ | IBCFunctionErrorHandler Name Name Name

199 deriving Show

207 deriving Show

200

208

201-- | The initial state for the compiler

209-- | The initial state for the compiler

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

206 emptyContext

214 emptyContext

207 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

215 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

208 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

216 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

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

210

218

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

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

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

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

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

315 | TargetCPU String

323 | TargetCPU String

316 | OptLevel Word

324 | OptLevel Word

317 | Client String

325 | Client String

326+ | ShowOrigErr

318 deriving (Show, Eq)

327 deriving (Show, Eq)

319

328

320-- Parsed declarations

329-- Parsed declarations

src/Idris/Completion.hs+1−1

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

104

105completeOption :: CompletionFunc Idris

106completeOption = completeWord Nothing " \t" completeOpt

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

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

108

109isWhitespace :: Char -> Bool

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

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

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

401undo :: Elab' aux ()

402undo = processTactic' Undo

403

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

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

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

405−prepare_apply fn imps =

408+prepare_apply fn imps =

406 do ty <- get_type fn

409 do ty <- get_type fn

407 ctxt <- get_context

410 ctxt <- get_context

408 env <- get_env

411 env <- get_env

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

414 let n = length (filter not imps)

417 let n = length (filter not imps)

415 let (h : hs) = holes p

418 let (h : hs) = holes p

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

419 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

420 return $! claims

421 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.

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

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

423 do let t = rebind hs t_in

428 do let t = rebind hs t_in

424 n <- getNameFrom (mkMN n')

429 n <- getNameFrom (mkMN n')

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

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

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

428 claim n (forget t)

433 claim n (forget t)

429 when i (movelast n)

434 when i (movelast n)

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

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

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

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

432 mkClaims _ _ _ _

437 mkClaims _ _ _ _

433 | Var n <- fn

438 | Var n <- fn

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

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

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

453 rebind hs t = t

458 rebind hs t = t

454

459

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

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

456apply = apply' fill

461apply = apply' fill

457match_apply = apply' match_fill

462match_apply = apply' match_fill

458

463

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

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

460apply' fillt fn imps =

465apply' fillt fn imps =

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

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

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

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

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

468 let dont = head hs : dontunify p ++

473 let dont = head hs : dontunify p ++

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

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

470 else

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

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

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

473 unified p

478 unified p

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

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

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

477 keepGiven dont hunis hs

482 keepGiven dont hunis hs

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

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

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

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

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

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

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

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

482 end_unify

487 end_unify

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

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

484 where updateUnify us n = case lookup n us of

489 where updateUnify us n = case lookup n us of

485 Just (P _ t _) -> t

490 Just (P _ t _) -> t

486 _ -> n

491 _ -> n

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

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

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

489apply2 fn elabs =

494apply2 fn elabs =

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

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

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

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

492− elabArgs args elabs

497+ elabArgs (map snd args) elabs

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

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

494 let (n, hs) = unified p

499 let (n, hs) = unified p

495 end_unify

500 end_unify

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

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

29import Data.Char

30import qualified Data.Text as T

31import Data.List

32+import Data.Maybe (listToMaybe)

32import Data.Vector.Unboxed (Vector)

33import Data.Vector.Unboxed (Vector)

33import qualified Data.Vector.Unboxed as V

34import qualified Data.Vector.Unboxed as V

34import qualified Data.Binary as B

35import qualified Data.Binary as B

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

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

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

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

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

414

415

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

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

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

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

417

418

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

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

419updateDef n f ctxt

420updateDef n f ctxt

src/Idris/Delaborate.hs+4−2

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

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

207pprintErr' i (ReflectionError parts orig) =

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

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

209+ vsep parts' <>

210+ if (opt_origerr (idris_options i))

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

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

212+ else empty

211 where showPart :: ErrorReportPart -> Doc OutputAnnotation

213 where showPart :: ErrorReportPart -> Doc OutputAnnotation

212 showPart (TextPart str) = text str

214 showPart (TextPart str) = text str

213 showPart (NamePart n) = annName n

215 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

126 if tyIsHandler nty'

127 then do i <- getIState

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

129+ addIBC (IBCErrorHandler n)

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

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

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

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

131 when corec $ do setAccessibility n Frozen

132 when corec $ do setAccessibility n Frozen

src/Idris/ElabTerm.hs+112−54

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

13import Idris.Core.Evaluate

14import Idris.Core.Typecheck (check)

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

16import Control.Monad

17import Control.Monad

17import Control.Monad.State.Strict

18import Control.Monad.State.Strict

18import Data.List

19import Data.List

20+import qualified Data.Map as M

19import Data.Maybe (mapMaybe)

21import Data.Maybe (mapMaybe)

22+import qualified Data.Set as S

23+import qualified Data.Text as T

21import Debug.Trace

25import Debug.Trace

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

153

157

154 local f = do e <- get_env

158 local f = do e <- get_env

155 return (f `elem` map fst e)

159 return (f `elem` map fst e)

156−

160+

161+ -- | Is a constant a type?

162+ constType :: Const -> Bool

157 constType (AType _) = True

163 constType (AType _) = True

158 constType StrType = True

164 constType StrType = True

159 constType PtrType = True

165 constType PtrType = True

160 constType VoidType = True

166 constType VoidType = True

161 constType _ = False

167 constType _ = False

162

168

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

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

171+ -> ElabD ()

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

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

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

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

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

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

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

387 solve

396 solve

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

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

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

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

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

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

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

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

393 = do env <- get_env

402 = do env <- get_env

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

410 _ -> mapM_ setInjective (map getTm args)

419 _ -> mapM_ setInjective (map getTm args)

411 ctxt <- get_context

420 ctxt <- get_context

412 let guarded = isConName f ctxt

421 let guarded = isConName f ctxt

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

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

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

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

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

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

415 let (ns', eargs) = unzip $

426 let (ns', eargs) = unzip $

416 sortBy cmpArg (zip ns args)

427 sortBy cmpArg (zip ns args)

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

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

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

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

419 solve

430 solve

420 ivs' <- get_instances

431 ivs' <- get_instances

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

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

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

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

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

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

424 mapM_ (\n -> do focus n

435 mapM_ (\n -> do focus n

425 g <- goal

436 g <- goal

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

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

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

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

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

605

616

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

606− elabArgs ina failed fc retry [] _

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

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

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

608-- elabArgs ina [] False ns ts

629-- elabArgs ina [] False ns ts

609 | otherwise = return ()

630 | otherwise = return ()

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

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

611− = elabArgs ina failed fc r ns args

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

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

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

613 | lazy && not pattern

634 | lazy && not pattern

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

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

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

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

616− pexp t]);

637+ pexp t])

617− | otherwise = elabArg n t

638+ | otherwise = elabArg argName holeName t

618− where elabArg n t

639+ where elabArg argName holeName t =

640+ reflectFunctionErrors ist f argName $

619− = do hs <- get_holes

641+ do hs <- get_holes

620− tm <- get_term

642+ tm <- get_term

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

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

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

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

623− case n `elem` hs of

645+ case holeName `elem` hs of

624− True ->

625−-- if r

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

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

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

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

629− False -> return failed

647+ False -> return failed

630− elabArgs ina failed fc r ns args

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

631

685

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

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

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

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

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

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

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

765 ps <- get_probs

819 ps <- get_probs

766 tm <- get_term

820 tm <- get_term

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

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

768− (match_apply (Var n) imps) True

822+ (match_apply (Var n) imps) True

769 ps' <- get_probs

823 ps' <- get_probs

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

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

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

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

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

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

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

779 hs <- get_holes

833 hs <- get_holes

780 ulog <- getUnifyLog

834 ulog <- getUnifyLog

781− solve

835+ solve

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

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

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

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

784 isImp arg = (False, priority arg)

838 isImp arg = (False, priority arg)

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

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

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

1135

1189

1136reifyTTName :: Term -> ElabD Name

1190reifyTTName :: Term -> ElabD Name

1137−reifyTTName t@(App _ _)

1191+reifyTTName t

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

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

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

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

1140

1194

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

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

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

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

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

1472

1526

1527+

1473withErrorReflection :: Idris a -> Idris a

1528withErrorReflection :: Idris a -> Idris a

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

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

1475 where handle :: Err -> Idris Err

1530 where handle :: Err -> Idris Err

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

1495

1550

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

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

1497 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1552 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1498− errorparts <- mapM (mapM reifyReportPart) errorpartsTT

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

1499−

1554+ Left err -> ierror err

1555+ Right ok -> return ok

1500 return $ case errorparts of

1556 return $ case errorparts of

1501 [] -> e

1557 [] -> e

1502 parts -> ReflectionError errorparts e

1558 parts -> ReflectionError errorparts e

1503

1559

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

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

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

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

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

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

1507− fromTTMaybe x = Nothing

1563+fromTTMaybe x = Nothing

1508

1564

1509reflErrName :: String -> Name

1565reflErrName :: String -> Name

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

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

1511

1567

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.

1512−reifyReportPart :: Term -> Idris ErrorReportPart

1571+reifyReportPart :: Term -> Either Err ErrorReportPart

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

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

1514− return (TextPart msg)

1573+ Right (TextPart msg)

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

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

1516 | n == reflErrName "NamePart" =

1575 | n == reflErrName "NamePart" =

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

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

1518− Error e -> ierror . InternalMsg $

1577+ Error e -> Left . InternalMsg $

1519 "could not reify name term " ++

1578 "could not reify name term " ++

1520 show ttn ++

1579 show ttn ++

1521− " when reflecting an error"

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

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

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

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

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

1524 | n == reflErrName "TermPart" =

1583 | n == reflErrName "TermPart" =

1525− do ist <- getIState

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

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

1527− Error e -> ierror . InternalMsg $

1585+ Error e -> Left . InternalMsg $

1528− "could not reify reflected term " ++

1586+ "could not reify reflected term " ++

1529− show tm ++

1587+ show tm ++

1530− " when reflecting an error"

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

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

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

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

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

1533 | n == reflErrName "SubReport" =

1591 | n == reflErrName "SubReport" =

1534− case unList tm of

1592+ case unList tm of

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

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

1536− return (SubReport subParts)

1594+ Right (SubReport subParts)

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

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

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

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

1539

1597

1540envTupleType :: Raw

1598envTupleType :: Raw

1541envTupleType

1599envTupleType

src/Idris/IBC.hs+26−4

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

28ibcVersion :: Word8

29ibcVersion = 56

31+

31data IBCFile = IBCFile { ver :: Word8,

32data IBCFile = IBCFile { ver :: Word8,

32 sourcefile :: FilePath,

33 sourcefile :: FilePath,

33 symbols :: [Name],

34 symbols :: [Name],

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

58 ibc_coercions :: [Name],

59 ibc_coercions :: [Name],

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

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

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

61 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

62 }

65 }

63 deriving Show

66 deriving Show

64{-!

67{-!

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

66!-}

69!-}

68initIBC :: IBCFile

71initIBC :: IBCFile

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

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

73+

71loadIBC :: FilePath -> Idris ()

75loadIBC :: FilePath -> Idris ()

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

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

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

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

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

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

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

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

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

218

225

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

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

220process i fn

227process i fn

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

253 pLineApps (ibc_lineapps i)

260 pLineApps (ibc_lineapps i)

254 pNameHints (ibc_namehints i)

261 pNameHints (ibc_namehints i)

255 pMetaInformation (ibc_metainformation i)

262 pMetaInformation (ibc_metainformation i)

263+ pErrorHandlers (ibc_errorhandlers i)

264+ pFunctionErrorHandlers (ibc_function_errorhandlers i)

256

265

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

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

258timestampOlder src ibc = do srct <- getModificationTime src

267timestampOlder src ibc = do srct <- getModificationTime src

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

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

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

435 ds

444 ds

436

445

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

437----- Generated by 'derive'

454----- Generated by 'derive'

438

455

439instance Binary SizeChange where

456instance Binary SizeChange where

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

1018 return (DataMI x1)

1035 return (DataMI x1)

1019

1036

1020instance Binary IBCFile where

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

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

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

1023 do put x1

1040 do put x1

1024 put x2

1041 put x2

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

1051 put x29

1068 put x29

1052 put x30

1069 put x30

1053 put x31

1070 put x31

1071+ put x32

1072+ put x33

1073+

1054 get

1074 get

1055 = do x1 <- get

1075 = do x1 <- get

1056 if x1 == ibcVersion then

1076 if x1 == ibcVersion then

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

1084 x29 <- get

1104 x29 <- get

1085 x30 <- get

1105 x30 <- get

1086 x31 <- get

1106 x31 <- get

1107+ x32 <- get

1108+ x33 <- 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)

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)

1088 else return (initIBC { ver = x1 })

1110 else return (initIBC { ver = x1 })

1089

1111

1090instance Binary DataOpt where

1112instance Binary DataOpt where

src/Idris/ParseExpr.hs+1

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

1035@

1036VerbatimString_t ::=

1037 '\"\"\"' ~'\"\"\"' '\"\"\"'

1038+;

1038@

1039@

1039 -}

1040 -}

1040verbatimStringLiteral :: MonadicParsing m => m String

1041verbatimStringLiteral :: MonadicParsing m => m String

src/Idris/Parser.hs+32−21

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

58import qualified Data.HashSet as HS

59import qualified Data.Text as T

60import qualified Data.ByteString.UTF8 as UTF8

61+import qualified Data.Set as S

62import Debug.Trace

63import Debug.Trace

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

937@

938@

938

939

939@

940@

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

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

941− | 'link' CodeGen String_t

942+ | 'link' CodeGen String_t

942− | 'flag' CodeGen String_t

943+ | 'flag' CodeGen String_t

943− | 'include' CodeGen String_t

944+ | 'include' CodeGen String_t

944− | 'hide' Name

945+ | 'hide' Name

945− | 'freeze' Name

946+ | 'freeze' Name

946− | 'access' Accessibility

947+ | 'access' Accessibility

947− | 'default' Totality

948+ | 'default' Totality

948− | 'logging' Natural

949+ | 'logging' Natural

949− | 'dynamic' StringList

950+ | 'dynamic' StringList

950− | 'name' Name NameList

951+ | 'name' Name NameList

952+ | 'error_handlers' Name NameList

951− | 'language' 'TypeProviders'

953+ | 'language' 'TypeProviders'

952− | 'language' 'ErrorReflection'

954+ | 'language' 'ErrorReflection'

953 ;

955 ;

954@

956@

955-}

957-}

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

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

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

995 ty <- iName []

997 ty <- iName []

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

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

997− return [PDirective

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

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

1000+ mapM_ (addNameHint ty') ns

1004− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) 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')]

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

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

1006 return [PDirective (addLangExt ext)]

1011 return [PDirective (addLangExt ext)]

1007 <?> "directive"

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

1008

1019

1009pLangExt :: IdrisParser LanguageExt

1020pLangExt :: IdrisParser LanguageExt

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

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

src/Idris/ProofSearch.hs+2−1

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

10import Idris.Delaborate

11import Idris.Error

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

13import Control.Monad

14import Control.Monad

14import Debug.Trace

15import Debug.Trace

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

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

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

87 _ -> fail "Ambiguous name"

88 _ -> fail "Ambiguous name"

88 ps <- get_probs

89 ps <- get_probs

89− args <- apply (Var n) imps

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

90 ps' <- get_probs

91 ps' <- get_probs

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

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

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

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

312 iPrintResult ""

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

314 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 ""

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

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

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

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

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

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

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

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

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

906process h fn NOP = return ()

910process h fn NOP = return ()

907

911

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

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

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

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

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

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

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

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

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

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

912

918

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

105pOption :: P.IdrisParser Opt

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

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

108−

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

109

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

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

test/test037/expected−14

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

1In file ErrorReflection.idr line 78 column 5

2 When elaborating right hand side of Main.bad :

3 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

3+import Language.Reflection

4+import Language.Reflection.Errors

5+import Language.Reflection.Utils

7+%language ErrorReflection

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

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

3./test038

4rm -f test038 *.ibc