3db1e91 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added flag for error reflection extension

commit3db1e910050c03caaca254f704e10318a802b749 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 26 Sep 2013, 21:11 (13 years ago) parent9bdde71

5 files changed+17−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+8−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabTerm.hs+6 src/Idris/Parser.hs+1 src/Idris/REPL.hs+1

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+1

@@ -2359,6 +2359,7 @@ Directive' ::= 'lib' CodeGen String_t

23592359 | 'logging' Natural

23602360 | 'dynamic' StringList

23612361 | 'language' 'TypeProviders'

2362+ | 'language' 'ErrorReflection'

23622363 ;

23632364-}

23642365directive :: SyntaxInfo -> IdrisParser [PDecl]

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