git.iko.soy/Idris-dev
on master help sign in
Add datatype for reflected errors
e472447David Christiansen
lib/Language/Reflection/Errors.idrnew file+41
compare with master
unifiedsplit
@@ -0,0 +1,41 @@
1+module Language.Reflection.Errors
2+
3+import Language.Reflection
4+
5+data SourceLocation = FileLoc String Int
6+
7+data 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
35+
36+data ErrorReport = Message String
37+ | Name TTName
38+ | Term TT
39+
40+
41+-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
lib/base.ipkg+1−1
@@ -20,7 +20,7 @@ modules = Builtins, Prelude, IO, System,
20
20
21 Providers,
21 Providers,
22
22
23− Language.Reflection, Language.Reflection.Utils,
23+ Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
24
24
25 Data.Morphisms,
25 Data.Morphisms,
26 Data.Bits, Data.Mod2,
26 Data.Bits, Data.Mod2,