ebc5318 · Idris-dev · git.iko.soy

idris.cabal+6

@@ -303,6 +303,12 @@ Extra-source-files:

303303 test/test035/run

304304 test/test035/expected

305305 test/test035/*.idr

306+ test/test036/run

307+ test/test036/expected

308+ test/test036/*.idr

309+ test/test037/run

310+ test/test037/expected

311+ test/test037/*.idr

306312

307313source-repository head

308314 type: git

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

@@ -10,6 +10,7 @@ data TTName = UN String

1010 -- ^ Machine chosen names

1111 | NErased

1212 -- ^ Name of somethng which is never used in scope

13+%name TTName n, n'

1314

1415implicit

1516userSuppliedName : String -> TTName

@@ -19,6 +20,7 @@ data TTUExp = UVar Int

1920 -- ^ universe variable

2021 | UVal Int

2122 -- ^ explicit universe variable

23+%name TTUExp uexp

2224

2325-- | Primitive constants

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

@@ -27,6 +29,8 @@ data Const = I Int | BI Nat | Fl Float | Ch Char | Str String

2729 | B8Type | B16Type | B32Type | B64Type

2830 | PtrType | VoidType | Forgot

2931

32+%name Const c, c'

33+

3034abstract class ReflConst (a : Type) where

3135 toConst : a -> Const

3236

@@ -71,6 +75,7 @@ data NameType = Bound

7175 -- ^ constructor with tag and number

7276 | TCon Int Int

7377 -- ^ type constructor with tag and number

78+%name NameType nt, nt'

7479

7580-- | Types annotations for bound variables in different

7681-- binding contexts

@@ -83,7 +88,7 @@ data Binder a = Lam a

8388 | Guess a a

8489 | PVar a

8590 | PVTy a

86−

91+%name Binder b, b'

8792

8893instance Functor Binder where

8994 map f (Lam x) = Lam (f x)

@@ -139,6 +144,8 @@ data TT = P NameType TTName TT

139144 | TType TTUExp

140145 -- ^ types

141146

147+%name TT tm, tm'

148+

142149-- | Raw terms without types

143150data Raw = Var TTName

144151 | RBind TTName (Binder Raw) Raw

@@ -147,6 +154,8 @@ data Raw = Var TTName

147154 | RForce Raw

148155 | RConstant Const

149156

157+%name Raw tm, tm'

158+

150159data Tactic = Try Tactic Tactic

151160 -- ^ try the first tactic and resort to the second one on failure

152161 | GoalType String Tactic

@@ -185,4 +194,4 @@ data Tactic = Try Tactic Tactic

185194 -- ^ name a reflected term and type it

186195 | Compute

187196 -- ^ normalise the context

188−

197+%name Tactic tac, tac'

libs/base/Language/Reflection/Errors.idr+17−6

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

22

33import Language.Reflection

44

5−data SourceLocation = FileLoc String Int

5+record SourceLocation : Type where

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

7+

8+%name SourceLocation loc

69

710data Err = Msg String

811 | InternalMsg String

@@ -15,13 +18,15 @@ data Err = Msg String

1518 | UnifyScope TTName TTName TT (List (TTName, TT))

1619 | CantInferType String

1720 | NonFunctionType TT TT

21+ | NotEquality TT TT

22+ | TooManyArguments TTName

1823 | CantIntroduce TT

1924 | NoSuchVariable TTName

2025 | NoTypeDecl TTName

2126 | NotInjective TT TT TT

2227 | CantResolve TT

2328 | CantResolveAlts (List String)

24− | IncompleteTT TT

29+ | IncompleteTerm TT

2530 | UniverseError

2631 | ProgramLineComment

2732 | Inaccessible TTName

@@ -32,11 +37,17 @@ data Err = Msg String

3237 | At SourceLocation Err

3338 | Elaborating String TTName Err

3439 | ProviderError String

40+ | LoadingFailed String Err

3541

36−-- | Error reports are a list of report parts

37−data ErrorReport = Message String

38− | Name TTName

39− | Term TT

42+%name Err err, e

4043

44+-- | Error reports are a list of report parts

45+data ErrorReportPart = TextPart String

46+ | NamePart TTName

47+ | TermPart TT

48+ | SubReport (List ErrorReportPart)

49+%name ErrorReportPart part, p

4150

4251-- Error reports become functions in List (String, TT) -> Err -> ErrorReport

52+ErrorHandler : Type

53+ErrorHandler = Err -> Maybe (List ErrorReportPart)

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

@@ -1,6 +1,7 @@

11module Language.Reflection.Utils

22

33import Language.Reflection

4+import Language.Reflection.Errors

45

56--------------------------------------------------------

67-- Tactic construction conveniences

@@ -185,3 +186,73 @@ instance Eq TT where

185186 equalp Impossible Impossible = True

186187 equalp (TType u) (TType u') = u == u'

187188 equalp x y = False

189+

190+total

191+forget : TT -> Maybe Raw

192+forget tm = fe [] tm

193+ where

194+ atIndex : List a -> Int -> Maybe a

195+ atIndex [] _ = Nothing

196+ atIndex (x::xs) n =

197+ case compare n 0 of

198+ EQ => Just x

199+ LT => Nothing

200+ GT => atIndex xs (n-1)

201+

202+ %assert_total

203+ fe : List TTName -> TT -> Maybe Raw

204+ fe env (P _ n _) = Just $ Var n

205+ fe env (V i) = map Var (atIndex env i)

206+ fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]

207+ fe env (App f a) = [| RApp (fe env f) (fe env a) |]

208+ fe env (TConst c) = Just $ RConstant c

209+ fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming

210+ fe env (TType i) = Just RType

211+ fe env Erased = Just $ RConstant Forgot

212+ fe env Impossible = Nothing

213+

214+instance Show Raw where

215+ show r = my_show r

216+ where %assert_total my_show : Raw -> String

217+ my_show (Var n) = "Var " ++ show n

218+ my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"

219+ my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'

220+ my_show RType = "RType"

221+ my_show (RForce tm) = "RForce " ++ my_show tm

222+ my_show (RConstant c) = "RConstant " ++ show c

223+

224+instance Show SourceLocation where

225+ show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col

226+

227+instance Show Err where

228+ show (Msg x) = "Msg \"" ++ x ++ "\""

229+ show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""

230+ show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++

231+ " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++

232+ show xs ++ " " ++ show y

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

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

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

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

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

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

239+ show (TooManyArguments n) = "TooManyArguments " ++ show n

240+ show (CantIntroduce tm) = "CantIntroduce " ++ show tm

241+ show (NoSuchVariable n) = "NoSuchVariable " ++ show n

242+ show (NoTypeDecl n) = "NoTypeDecl " ++ show n

243+ show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

244+ show (CantResolve tm) = "CantResolve " ++ show tm

245+ show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

246+ show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

247+ show UniverseError = "UniverseError"

248+ show ProgramLineComment = "ProgramLineComment"

249+ show (Inaccessible n) = "Inaccessible " ++ show n

250+ show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n

251+ show (AlreadyDefined n) = "AlreadyDefined " ++ show n

252+ show (ProofSearchFail err) = "ProofSearchFail " ++ show err

253+ show (NoRewriting tm) = "NoRewriting " ++ show tm

254+ show (At loc err) = "At " ++ show loc ++ " " ++ show err

255+ show (Elaborating x n err) = "Elaborating " ++ show x ++ " " ++ show x ++ " " ++ show n ++ " (" ++ show err ++ ")"

256+ show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""

257+ show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"

258+

src/Idris/AbsSyntaxTree.hs+7−2

@@ -131,7 +131,8 @@ data IState = IState {

131131 idris_outputmode :: OutputMode,

132132 idris_colourRepl :: Bool,

133133 idris_colourTheme :: ColourTheme,

134− idris_outh :: Handle

134+ idris_outh :: Handle,

135+ idris_errorhandlers :: [Name]

135136 }

136137

137138data SizeChange = Smaller | Same | Bigger | Unknown

@@ -189,13 +190,15 @@ data IBCWrite = IBCFix FixDecl

189190 | IBCLineApp FilePath Int PTerm

190191 deriving Show

191192

193+-- | The initial state for the compiler

194+idrisInit :: IState

192195idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

193196 emptyContext emptyContext emptyContext emptyContext

194197 emptyContext emptyContext emptyContext emptyContext

195198 emptyContext

196199 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

197200 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

198− True defaultTheme stdout

201+ True defaultTheme stdout []

199202

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

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

@@ -258,6 +261,7 @@ data Command = Quit

258261 | SetColour ColourType IdrisColour

259262 | ColourOn

260263 | ColourOff

264+ | ListErrorHandlers

261265

262266data Opt = Filename String

263267 | Ver

@@ -380,6 +384,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

380384 -- a function argument, and further evaluation resutls

381385 | Implicit -- implicit coercion

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

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

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

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

385390 deriving (Show, Eq)

src/Idris/Core/Execute.hs−8

@@ -499,14 +499,6 @@ getFTy (EP _ (UN t) _) =

499499 _ -> Nothing

500500getFTy _ = Nothing

501501

502−unList :: Term -> Maybe [Term]

503−unList tm = case unApply tm of

504− (nil, [_]) -> Just []

505− (cons, ([_, x, xs])) ->

506− do rest <- unList xs

507− return $ x:rest

508− (f, args) -> Nothing

509−

510502unEList :: ExecVal -> Maybe [ExecVal]

511503unEList tm = case unApplyV tm of

512504 (nil, [_]) -> Just []

src/Idris/Core/TT.hs+53−30

@@ -74,37 +74,52 @@ instance Sized FC where

7474instance Show FC where

7575 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

7676

77+-- | Used for error reflection

78+data ErrorReportPart = TextPart String

79+ | NamePart Name

80+ | TermPart Term

81+ | SubReport [ErrorReportPart]

82+ deriving (Show, Eq)

83+

84+

85+-- Please remember to keep Err synchronised with

86+-- Language.Reflection.Errors.Err in the stdlib!

87+

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

89+-- if they reach the top level.

7790data Err = Msg String

78− | InternalMsg String

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

80− -- Int is 'score' - how much we did unify

81− -- Bool indicates recoverability, True indicates more info may make

82− -- unification succeed

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

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

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

86− | CantInferType String

87− | NonFunctionType Term Term

88− | NotEquality Term Term

89− | TooManyArguments Name

90− | CantIntroduce Term

91− | NoSuchVariable Name

92− | NoTypeDecl Name

93− | NotInjective Term Term Term

94− | CantResolve Term

95− | CantResolveAlts [String]

96− | IncompleteTerm Term

97− | UniverseError

98− | ProgramLineComment

99− | Inaccessible Name

100− | NonCollapsiblePostulate Name

101− | AlreadyDefined Name

102− | ProofSearchFail Err

103− | NoRewriting Term

104− | At FC Err

105− | Elaborating String Name Err

106− | ProviderError String

107− | LoadingFailed String Err

91+ | InternalMsg String

92+ | CantUnify Bool Term Term Err [(Name, Type)] Int

93+ -- Int is 'score' - how much we did unify

94+ -- Bool indicates recoverability, True indicates more info may make

95+ -- unification succeed

96+ | InfiniteUnify Name Term [(Name, Type)]

97+ | CantConvert Term Term [(Name, Type)]

98+ | UnifyScope Name Name Term [(Name, Type)]

99+ | CantInferType String

100+ | NonFunctionType Term Term

101+ | NotEquality Term Term

102+ | TooManyArguments Name

103+ | CantIntroduce Term

104+ | NoSuchVariable Name

105+ | NoTypeDecl Name

106+ | NotInjective Term Term Term

107+ | CantResolve Term

108+ | CantResolveAlts [String]

109+ | IncompleteTerm Term

110+ | UniverseError

111+ | ProgramLineComment

112+ | Inaccessible Name

113+ | NonCollapsiblePostulate Name

114+ | AlreadyDefined Name

115+ | ProofSearchFail Err

116+ | NoRewriting Term

117+ | At FC Err

118+ | Elaborating String Name Err

119+ | ProviderError String

120+ | LoadingFailed String Err

121+ | ReflectionError [[ErrorReportPart]] Err

122+ | ReflectionFailed String Err

108123 deriving Eq

109124{-!

110125deriving instance NFData Err

@@ -793,6 +808,14 @@ mkApp :: TT n -> [TT n] -> TT n

793808mkApp f [] = f

794809mkApp f (a:as) = mkApp (App f a) as

795810

811+unList :: Term -> Maybe [Term]

812+unList tm = case unApply tm of

813+ (nil, [_]) -> Just []

814+ (cons, ([_, x, xs])) ->

815+ do rest <- unList xs

816+ return $ x:rest

817+ (f, args) -> Nothing

818+

796819forget :: TT Name -> Raw

797820forget tm = fe [] tm

798821 where

src/Idris/Delaborate.hs+16

@@ -9,6 +9,8 @@ import Idris.AbsSyntax

99import Idris.Core.TT

1010import Idris.Core.Evaluate

1111

12+import Data.List (intersperse)

13+

1214import Debug.Trace

1315

1416bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

@@ -190,6 +192,20 @@ pshow i (Elaborating s n e) = "When elaborating " ++ s ++

190192 showqual i n ++ ":\n" ++ pshow i e

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

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

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

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

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

198+ where showPart :: ErrorReportPart -> String

199+ showPart (TextPart str) = str

200+ showPart (NamePart n) = let colour = idris_colourRepl i in

201+ showName (Just i) [] False colour n

202+ showPart (TermPart tm) = let colour = idris_colourRepl i

203+ in showImp (Just i) False colour (delab i tm)

204+ showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

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

206+ indented (pshow i err) ++

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

208+

193209

194210showSc i [] = ""

195211showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/ElabDecls.hs+24−1

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

112112 addIBC (IBCFlags n opts')

113113 when (Implicit `elem` opts) $ do addCoercion n

114114 addIBC (IBCCoercion n)

115+ -- If the function is declared as an error handler and the language

116+ -- extension is enabled, then add it to the list of error handlers.

117+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

118+ when (ErrorHandler `elem` opts) $ do

119+ if errorReflection

120+ then

121+ -- TODO: Check that the declared type is the correct type for an error handler:

122+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt

123+ if tyIsHandler nty'

124+ then do i <- getIState

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

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

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

115128 when corec $ do setAccessibility n Frozen

116129 addIBC (IBCAccess n Frozen)

117130 return usety

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

124137 | otherwise = mergeTy sc sc'

125138 mergeTy _ sc = sc

126139

140+ tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))

141+ (App (P _ (NS (UN "Maybe") ns2) _)

142+ (App (P _ (NS (UN "List") ns3) _)

143+ (P _ (NS (UN "ErrorReportPart") ns4) _))))

144+ | ns1 == ["Errors","Reflection","Language"]

145+ , ns2 == ["Maybe", "Prelude"]

146+ , ns3 == ["List", "Prelude"]

147+ , ns4 == ["Errors","Reflection","Language"] = True

148+ tyIsHandler _ = False

149+

127150

128151elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

129152 FC -> FnOpts -> Name -> PTerm -> Idris ()

@@ -1980,7 +2003,7 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds

19802003

19812004elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

19822005elabDecl what info d

1983− = idrisCatch (elabDecl' what info d) (setAndReport)

2006+ = idrisCatch (withErrorReflection $ elabDecl' what info d) (setAndReport)

19842007

19852008elabDecl' _ info (PFix _ _ _)

19862009 = return () -- nothing to elaborate

src/Idris/ElabTerm.hs+169−4

@@ -5,15 +5,18 @@ module Idris.ElabTerm where

55import Idris.AbsSyntax

66import Idris.DSL

77import Idris.Delaborate

8+import Idris.Error

89import Idris.ProofSearch

910

1011import Idris.Core.Elaborate hiding (Tactic(..))

1112import Idris.Core.TT

1213import Idris.Core.Evaluate

14+import Idris.Core.Typecheck (check)

1315

1416import Control.Monad

1517import Control.Monad.State

1618import Data.List

19+import Data.Maybe (mapMaybe)

1720

1821import Debug.Trace

1922

@@ -1031,7 +1034,7 @@ runTac autoSolve ist tac

10311034 runReflected t = do t' <- reify ist t

10321035 runTac autoSolve ist t'

10331036

1034−-- | Prefix a name with the "Reflection.Language" namespace

1037+-- | Prefix a name with the "Language.Reflection" namespace

10351038reflm :: String -> Name

10361039reflm n = NS (UN n) ["Reflection", "Language"]

10371040

@@ -1370,10 +1373,172 @@ reflectEnv = foldr consToEnvList emptyEnvList

13701373 [envTupleType]

13711374

13721375-- | Reflect an error into the internal datatype of Idris -- TODO

1376+rawBool :: Bool -> Raw

1377+rawBool True = Var (NS (UN "True") ["Bool", "Prelude"])

1378+rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])

1379+

1380+rawNil :: Raw -> Raw

1381+rawNil ty = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"])) [ty]

1382+

1383+rawCons :: Raw -> Raw -> Raw -> Raw

1384+rawCons ty hd tl = raw_apply (Var (NS (UN "::") ["List", "Prelude"])) [ty, hd, tl]

1385+

1386+rawList :: Raw -> [Raw] -> Raw

1387+rawList ty = foldr (rawCons ty) (rawNil ty)

1388+

1389+rawPairTy :: Raw -> Raw -> Raw

1390+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

1391+

1392+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

1393+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

1394+

1395+reflectCtxt :: [(Name, Type)] -> Raw

1396+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

1397+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

1398+ (reflectName n, reflect t)))

1399+ ctxt)

1400+

13731401reflectErr :: Err -> Raw

1374−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]

1375−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]

1376−reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]

1402+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

1403+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

1404+reflectErr (CantUnify b t1 t2 e ctxt i) =

1405+ raw_apply (Var $ reflErrName "CantUnify")

1406+ [ rawBool b

1407+ , reflect t1

1408+ , reflect t2

1409+ , reflectErr e

1410+ , reflectCtxt ctxt

1411+ , RConstant (I i)]

1412+reflectErr (InfiniteUnify n tm ctxt) =

1413+ raw_apply (Var $ reflErrName "InfiniteUnify")

1414+ [ reflectName n

1415+ , reflect tm

1416+ , reflectCtxt ctxt

1417+ ]

1418+reflectErr (CantConvert t t' ctxt) =

1419+ raw_apply (Var $ reflErrName "CantConvert")

1420+ [ reflect t

1421+ , reflect t'

1422+ , reflectCtxt ctxt

1423+ ]

1424+reflectErr (UnifyScope n n' t ctxt) =

1425+ raw_apply (Var $ reflErrName "UnifyScope")

1426+ [ reflectName n

1427+ , reflectName n'

1428+ , reflect t

1429+ , reflectCtxt ctxt

1430+ ]

1431+reflectErr (CantInferType str) =

1432+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]

1433+reflectErr (NonFunctionType t t') =

1434+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']

1435+reflectErr (NotEquality t t') =

1436+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']

1437+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

1438+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

1439+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

1440+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

1441+reflectErr (NotInjective t1 t2 t3) =

1442+ raw_apply (Var $ reflErrName "NotInjective")

1443+ [ reflect t1

1444+ , reflect t2

1445+ , reflect t3

1446+ ]

1447+reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

1448+reflectErr (CantResolveAlts ss) =

1449+ raw_apply (Var $ reflErrName "CantResolve")

1450+ [rawList (Var $ (UN "String")) (map (RConstant . Str) ss)]

1451+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1452+reflectErr UniverseError = Var $ reflErrName "UniverseError"

1453+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

1454+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

1455+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

1456+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

1457+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

1458+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

1459+reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]

1460+ where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")

1461+ [ RConstant (Str source)

1462+ , RConstant (I line)

1463+ , RConstant (I col)

1464+ ]

1465+reflectErr (Elaborating str n e) =

1466+ raw_apply (Var $ reflErrName "Elaborating")

1467+ [ RConstant (Str str)

1468+ , reflectName n

1469+ , reflectErr e

1470+ ]

1471+reflectErr (ProviderError str) =

1472+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

1473+reflectErr (LoadingFailed str err) =

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

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

1476+

1477+withErrorReflection :: Idris a -> Idris a

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

1479+ where handle :: Err -> Idris Err

1480+ handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"

1481+ return e -- Don't do meta-reflection of errors

1482+ handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

1483+ return e

1484+ handle e = do ist <- getIState

1485+ logLvl 2 "Starting error reflection"

1486+ let handlers = idris_errorhandlers ist

1487+ logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))

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

1489+

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

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

1492+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e

1493+ OK hs -> return hs

1494+

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

1496+ ctxt <- getContext

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

1498+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

1499+

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

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

1502+ errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1503+

1504+ return $ case errorparts of

1505+ [] -> e

1506+ parts -> ReflectionError errorparts e

1507+

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

1509+ fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm

1510+ fromTTMaybe x = Nothing

1511+

1512+reflErrName :: String -> Name

1513+reflErrName n = NS (UN n) ["Errors", "Reflection", "Language"]

1514+

1515+reifyReportPart :: Term -> Idris ErrorReportPart

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

1517+ return (TextPart msg)

1518+reifyReportPart (App (P (DCon _ _) n _) ttn)

1519+ | n == reflErrName "NamePart" =

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

1521+ Error e -> ierror . InternalMsg $

1522+ "could not reify name term " ++

1523+ show ttn ++

1524+ " when reflecting an error"

1525+ OK (n', _)-> return $ NamePart n'

1526+reifyReportPart (App (P (DCon _ _) n _) tm)

1527+ | n == reflErrName "TermPart" =

1528+ do ist <- getIState

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

1530+ Error e -> ierror . InternalMsg $

1531+ "could not reify reflected term " ++

1532+ show tm ++

1533+ " when reflecting an error"

1534+ OK (tm', _) -> return $ TermPart tm'

1535+reifyReportPart (App (P (DCon _ _) n _) tm)

1536+ | n == reflErrName "SubReport" =

1537+ case unList tm of

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

1539+ return (SubReport subParts)

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

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

13771542

13781543envTupleType :: Raw

13791544envTupleType

src/Idris/Error.hs+2

@@ -38,6 +38,7 @@ report e

3838idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

3939idrisCatch = catchError

4040

41+

4142setAndReport :: Err -> Idris ()

4243setAndReport e = do ist <- getIState

4344 let h = idris_outh ist

@@ -71,3 +72,4 @@ getErrLine _ = 0

7172getErrColumn :: Err -> Int

7273getErrColumn (At (FC _ _ c) _) = c

7374getErrColumn _ = 0

75+

src/Idris/IBC.hs+3−1

@@ -643,7 +643,7 @@ instance Binary NameType where

643643 _ -> error "Corrupted binary data for NameType"

644644

645645

646−instance {-(Binary n) =>-} Binary (TT Name) where

646+instance {- (Binary n) => -} Binary (TT Name) where

647647 put x

648648 = {-# SCC "putTT" #-}

649649 case x of

@@ -1001,6 +1001,7 @@ instance Binary FnOpt where

10011001 PartialFn -> putWord8 6

10021002 Implicit -> putWord8 7

10031003 Reflection -> putWord8 8

1004+ ErrorHandler -> putWord8 9

10041005 get

10051006 = do i <- getWord8

10061007 case i of

@@ -1014,6 +1015,7 @@ instance Binary FnOpt where

10141015 6 -> return PartialFn

10151016 7 -> return Implicit

10161017 8 -> return Reflection

1018+ 9 -> return ErrorHandler

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

10181020

10191021instance Binary Fixity where

src/Idris/Parser.hs+3

@@ -309,6 +309,7 @@ FnOpts ::= 'total'

309309 | 'partial'

310310 | 'implicit'

311311 | '%' 'assert_total'

312+ | '%' 'error_handler'

312313 | '%' 'reflection'

313314 | '%' 'specialise' '[' NameTimesList? ']'

314315 ;

@@ -330,6 +331,8 @@ fnOpts opts

330331 fnOpts (CExport c : opts)

331332 <|> do try (lchar '%' *> reserved "assert_total");

332333 fnOpts (AssertTotal : opts)

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

335+ fnOpts (ErrorHandler : opts)

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

334337 fnOpts (Reflection : opts)

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

src/Idris/REPL.hs+19−13

@@ -436,19 +436,19 @@ process h fn (ChangeDirectory f)

436436 = do runIO $ setCurrentDirectory f

437437 return ()

438438process h fn (Eval t)

439− = do (tm, ty) <- elabVal toplevel False t

440− ctxt <- getContext

441− let tm' = force (normaliseAll ctxt [] tm)

442− let ty' = force (normaliseAll ctxt [] ty)

443− -- Add value to context, call it "it"

444− updateContext (addCtxtDef (UN "it") (Function ty' tm'))

445− ist <- getIState

446− logLvl 3 $ "Raw: " ++ show (tm', ty')

447− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

448− imp <- impShow

449− c <- colourise

450− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

451− showImp (Just ist) imp c (delab ist ty'))

439+ = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t

440+ ctxt <- getContext

441+ let tm' = force (normaliseAll ctxt [] tm)

442+ let ty' = force (normaliseAll ctxt [] ty)

443+ -- Add value to context, call it "it"

444+ updateContext (addCtxtDef (UN "it") (Function ty' tm'))

445+ ist <- getIState

446+ logLvl 3 $ "Raw: " ++ show (tm', ty')

447+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

448+ imp <- impShow

449+ c <- colourise

450+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

451+ showImp (Just ist) imp c (delab ist ty'))

452452process h fn (ExecVal t)

453453 = do ctxt <- getContext

454454 ist <- getIState

@@ -919,6 +919,12 @@ process h fn ColourOn

919919process h fn ColourOff

920920 = do ist <- getIState

921921 putIState $ ist { idris_colourRepl = False }

922+process h fn ListErrorHandlers =

923+ do ist <- getIState

924+ case idris_errorhandlers ist of

925+ [] -> iPrintResult "No registered error handlers"

926+ handlers ->

927+ iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

922928

923929classInfo :: ClassInfo -> Idris ()

924930classInfo ci = do iputStrLn "Methods:\n"

src/Idris/REPLParser.hs+1

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

9696 eof; return (AddProof n))

9797 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

9898 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

99+ <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

99100 <|> do P.whiteSpace; do eof; return NOP

100101 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

101102

test/test037/ErrorReflection.idrnew file+79

@@ -0,0 +1,79 @@

1+module Main

2+

3+import Language.Reflection

4+import Language.Reflection.Errors

5+import Language.Reflection.Utils

6+

7+%language ErrorReflection

8+

9+-- Well-typed terms

10+

11+data Ty = TUnit | TFun Ty Ty

12+

13+instance Show Ty where

14+ show TUnit = "()"

15+ show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"

16+

17+using (n : Nat, G : Vect n Ty)

18+ data HasType : Vect n Ty -> Ty -> Type where

19+ Here : HasType (t::G) t

20+ There : HasType G t -> HasType (t' :: G) t

21+

22+ data Tm : Vect n Ty -> Ty -> Type where

23+ U : Tm G TUnit

24+ Var : HasType G t -> Tm G t

25+ Lam : Tm (t :: G) t' -> Tm G (TFun t t')

26+ App : Tm G (TFun t t') -> Tm G t -> Tm G t'

27+

28+-- Extract the type from a reflected term type

29+

30+namespace ErrorReports

31+ data Ty' = TUnit

32+ | TFun Ty' Ty'

33+ | TVar Int String -- To show in unification failures

34+

35+ instance Show Ty' where

36+ show TUnit = "()"

37+ show (TFun x y) = "(" ++ show x ++ " => " ++ show y ++ ")"

38+ show (TVar i n) = n ++ "(" ++ cast i ++ ")"

39+

40+getTmTy : TT -> Maybe TT

41+getTmTy (App (App (App (P (TCon _ _) (NS (UN "Tm") _) _) _) _) ty) = Just ty

42+getTmTy _ = Nothing

43+

44+

45+reifyTy : TT -> Maybe Ty'

46+reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit

47+reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1

48+ ty2 <- reifyTy t2

49+ return $ TFun ty1 ty2

50+reifyTy (P _ (MN i n) _) = Just (TVar i n)

51+reifyTy _ = Nothing

52+

53+-- Friendly error reporting

54+

55+total %error_handler

56+dslerr : Err -> Maybe (List ErrorReportPart)

57+dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1

58+ tm2' <- getTmTy tm2

59+ ty1 <- reifyTy tm1'

60+ ty2 <- reifyTy tm2'

61+ return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

62+dslerr (At (FileLoc f l c) err) = do err' <- dslerr err

63+ return [ TextPart "In file"

64+ , TextPart f

65+ , TextPart "line", TextPart (cast l)

66+ , TextPart "column", TextPart (cast c)

67+ , SubReport err']

68+dslerr (Elaborating s n err) = do err' <- dslerr err

69+ return ([ TextPart $ "When elaborating " ++ s

70+ , NamePart n

71+ , TextPart ":"

72+ , SubReport err'])

73+dslerr _ = Nothing

74+

75+

76+-- Report the error

77+bad : Tm [] TUnit

78+bad = Lam (Var Here)

79+

test/test037/expectednew file+18

@@ -0,0 +1,18 @@

1+In file ErrorReflection.idr line 78 column 5

2+ When elaborating right hand side of Main.bad :

3+ DSL type error: (t'(1000) => t'(1000)) doesn't match ()

4+

5+Original error:

6+

7+ ErrorReflection.idr:78:5:When elaborating right hand side of bad:

8+ Can't unify

9+ Tm [] (Main.TFun t' t')

10+ with

11+ Tm [] Main.TUnit

12+

13+ Specifically:

14+ Can't unify

15+ Main.TFun t' t'

16+ with

17+ Main.TUnit

18+

test/test037/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc