git.iko.soy/Idris-dev
on de0bcbd help sign in
Idris-dev/lib/Language/Reflection/Errors.idr
42 lines 1.4 kB history raw
1module Language.Reflection.Errors
3import Language.Reflection
5data SourceLocation = FileLoc String Int
7data Err = Msg String
8 | InternalMsg String
9 | CantUnify Bool TT TT Err (List (TTName, TT)) Int
10 -- Int is 'score' - how much we did unify
11 -- Bool indicates recoverability, True indicates more info may make
12 -- unification succeed
13 | InfiniteUnify TTName TT (List (TTName, TT))
14 | CantConvert TT TT (List (TTName, TT))
15 | UnifyScope TTName TTName TT (List (TTName, TT))
16 | CantInferType String
17 | NonFunctionType TT TT
18 | CantIntroduce TT
19 | NoSuchVariable TTName
20 | NoTypeDecl TTName
21 | NotInjective TT TT TT
22 | CantResolve TT
23 | CantResolveAlts (List String)
24 | IncompleteTT TT
25 | UniverseError
26 | ProgramLineComment
27 | Inaccessible TTName
28 | NonCollapsiblePostulate TTName
29 | AlreadyDefined TTName
30 | ProofSearchFail Err
31 | NoRewriting TT
32 | At SourceLocation Err
33 | Elaborating String TTName Err
34 | ProviderError String
36-- | Error reports are a list of report parts
37data ErrorReport = Message String
38 | Name TTName
39 | Term TT
42-- Error reports become functions in List (String, TT) -> Err -> ErrorReport