git.iko.soy/Idris-dev
on master help sign in
Merge pull request #501 from david-christiansen/error-reflection

Basic infrastructure for error reflection in compiler

commit27ed67d57fb2c2b4568117654ca617fd68d5698d authorEdwin Brady <edwin.brady@gmail.com> dateTue 1 Oct 2013, 07:46 (13 years ago) parent70a041f7ae55f9
11 files changed+81−5
compare with master
unifiedsplit
idris.cabal+3 lib/Language/Reflection/Errors.idr+42 lib/base.ipkg+1−1 src/Idris/AbsSyntax.hs+8−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabTerm.hs+6 src/Idris/Parser.hs+7−2 src/Idris/REPL.hs+1 test/test031/expected test/test031/run+4 test/test031/test031.idr+8
idris.cabal+3
@@ -256,6 +256,9 @@ Extra-source-files:
256256 test/test030/run
257257 test/test030/*.idr
258258 test/test030/expected
259+ test/test031/run
260+ test/test031/*.idr
261+ test/test031/expected
259262
260263source-repository head
261264 type: git
lib/Language/Reflection/Errors.idrnew file+42
@@ -0,0 +1,42 @@
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+-- | Error reports are a list of report parts
37+data ErrorReport = Message String
38+ | Name TTName
39+ | Term TT
40+
41+
42+-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
lib/base.ipkg+1−1
@@ -20,7 +20,7 @@ modules = Builtins, Prelude, IO, System,
2020
2121 Providers,
2222
23− Language.Reflection, Language.Reflection.Utils,
23+ Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
2424
2525 Data.Morphisms,
2626 Data.Bits, Data.Mod2,
src/Idris/AbsSyntax.hs+8−1
@@ -76,7 +76,14 @@ addHdr :: Codegen -> String -> Idris ()
7676addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
7777
7878addLangExt :: LanguageExt -> Idris ()
79−addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }
79+addLangExt TypeProviders = do i <- getIState
80+ putIState $ i {
81+ idris_language_extensions = TypeProviders : idris_language_extensions i
82+ }
83+addLangExt ErrorReflection = do i <- getIState
84+ putIState $ i {
85+ idris_language_extensions = ErrorReflection : idris_language_extensions i
86+ }
8087
8188addTrans :: (Term, Term) -> Idris ()
8289addTrans t = do i <- getIState
src/Idris/AbsSyntaxTree.hs+1−1
@@ -67,7 +67,7 @@ defaultOpts = IOption { opt_logLevel = 0
6767 , opt_cmdline = []
6868 }
6969
70−data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)
70+data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
7171
7272-- | The output mode in use
7373data OutputMode = RawOutput | IdeSlave Integer deriving Show
src/Idris/ElabTerm.hs+6
@@ -1282,6 +1282,12 @@ reflectEnv = foldr consToEnvList emptyEnvList
12821282 emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))
12831283 [envTupleType]
12841284
1285+-- | Reflect an error into the internal datatype of Idris -- TODO
1286+reflectErr :: Err -> Raw
1287+reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1288+reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1289+reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]
1290+
12851291envTupleType :: Raw
12861292envTupleType
12871293 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
src/Idris/Parser.hs+7−2
@@ -2350,6 +2350,7 @@ Directive' ::= 'lib' CodeGen String_t
23502350 | 'logging' Natural
23512351 | 'dynamic' StringList
23522352 | 'language' 'TypeProviders'
2353+ | 'language' 'ErrorReflection'
23532354 ;
23542355-}
23552356directive :: SyntaxInfo -> IdrisParser [PDecl]
@@ -2390,10 +2391,14 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
23902391 Left lib -> addIBC (IBCDyLib (lib_name lib))
23912392 Right msg ->
23922393 fail $ msg)]
2393− <|> do try (lchar '%' *> reserved "language"); ext <- reserved "TypeProviders";
2394− return [PDirective (addLangExt TypeProviders)]
2394+ <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
2395+ return [PDirective (addLangExt ext)]
23952396 <?> "directive"
23962397
2398+pLangExt :: IdrisParser LanguageExt
2399+pLangExt = (reserved "TypeProviders" >> return TypeProviders)
2400+ <|> (reserved "ErrorReflection" >> return ErrorReflection)
2401+
23972402{- | Parses a totality
23982403Totality ::= 'partial' | 'total'
23992404-}
src/Idris/REPL.hs+1
@@ -648,6 +648,7 @@ parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
648648parseArgs ["--exec"] = InterpretScript "Main.main" : []
649649parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
650650parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)
651+parseArgs ("-XErrorReflection":ns) = Extension ErrorReflection : (parseArgs ns)
651652parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns
652653parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns
653654parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns
test/test031/expectednew file

No changes to the content.

test/test031/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris $@ test031.idr -o test031
3+./test031
4+rm -f test031 *.ibc
test/test031/test031.idrnew file+8
@@ -0,0 +1,8 @@
1+module Main
2+
3+-- Test enabling the ErrorReflection extension
4+
5+%language ErrorReflection
6+
7+main : IO ()
8+main = return ()