27ed67d · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -256,6 +256,9 @@ Extra-source-files:

256 test/test030/run

257 test/test030/*.idr

258 test/test030/expected

259+ test/test031/run

260+ test/test031/*.idr

261+ test/test031/expected

259

262

260source-repository head

263source-repository head

261 type: git

264 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,

20

21 Providers,

22

23− Language.Reflection, Language.Reflection.Utils,

23+ Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

24

25 Data.Morphisms,

26 Data.Bits, Data.Mod2,

src/Idris/AbsSyntax.hs+8−1

@@ -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+7−2

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

2350 | 'logging' Natural

2351 | 'dynamic' StringList

2352 | 'language' 'TypeProviders'

2353+ | 'language' 'ErrorReflection'

2353 ;

2354 ;

2354-}

2355-}

2355directive :: SyntaxInfo -> IdrisParser [PDecl]

2356directive :: SyntaxInfo -> IdrisParser [PDecl]

@@ -2390,10 +2391,14 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

2390 Left lib -> addIBC (IBCDyLib (lib_name lib))

2391 Left lib -> addIBC (IBCDyLib (lib_name lib))

2391 Right msg ->

2392 Right msg ->

2392 fail $ msg)]

2393 fail $ msg)]

2393− <|> do try (lchar '%' *> reserved "language"); ext <- reserved "TypeProviders";

2394+ <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

2394− return [PDirective (addLangExt TypeProviders)]

2395+ return [PDirective (addLangExt ext)]

2395 <?> "directive"

2396 <?> "directive"

2396

2397

2398+pLangExt :: IdrisParser LanguageExt

2399+pLangExt = (reserved "TypeProviders" >> return TypeProviders)

2400+ <|> (reserved "ErrorReflection" >> return ErrorReflection)

2401+

2397{- | Parses a totality

2402{- | Parses a totality

2398Totality ::= 'partial' | 'total'

2403Totality ::= 'partial' | 'total'

2399-}

2404-}

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

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 ()