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

src/Idris/AbsSyntax.hs+8−1

compare with master

unifiedsplit

@@ -76,7 +76,14 @@ addHdr :: Codegen -> String -> Idris ()

76addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

77

78addLangExt :: 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+ }

80

87

81addTrans :: (Term, Term) -> Idris ()

88addTrans :: (Term, Term) -> Idris ()

82addTrans t = do i <- getIState

89addTrans t = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1−1

@@ -67,7 +67,7 @@ defaultOpts = IOption { opt_logLevel = 0

67 , opt_cmdline = []

68 }

69

70−data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)

70+data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

71

72-- | The output mode in use

73data OutputMode = RawOutput | IdeSlave Integer deriving Show

src/Idris/ElabTerm.hs+6

@@ -1282,6 +1282,12 @@ reflectEnv = foldr consToEnvList emptyEnvList

1282 emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))

1283 [envTupleType]

1284

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+

1285envTupleType :: Raw

1291envTupleType :: Raw

1286envTupleType

1292envTupleType

1287 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

1293 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/Parser.hs+1

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

2359 | 'logging' Natural

2360 | 'dynamic' StringList

2361 | 'language' 'TypeProviders'

2362+ | 'language' 'ErrorReflection'

2362 ;

2363 ;

2363-}

2364-}

2364directive :: SyntaxInfo -> IdrisParser [PDecl]

2365directive :: SyntaxInfo -> IdrisParser [PDecl]

src/Idris/REPL.hs+1

@@ -648,6 +648,7 @@ parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

648parseArgs ["--exec"] = InterpretScript "Main.main" : []

649parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

650parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

651+parseArgs ("-XErrorReflection":ns) = Extension ErrorReflection : (parseArgs ns)

651parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

652parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

652parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

653parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

653parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns

654parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns