bc553c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

%error_reduce for more control over errors

bc553c7Edwin Brady10 years ago

src/Idris/AbsSyntax.hs+8

compare with master

unifiedsplit

@@ -153,10 +153,18 @@ addTrans basefn t

153 putIState $ i { idris_transforms = addDef basefn t'

154 (idris_transforms i) }

155

156+-- | Add transformation rules from a definition, which will reverse the

157+-- definition for an error to make it more readable

156addErrRev :: (Term, Term) -> Idris ()

158addErrRev :: (Term, Term) -> Idris ()

157addErrRev t = do i <- getIState

159addErrRev t = do i <- getIState

158 putIState $ i { idris_errRev = t : idris_errRev i }

160 putIState $ i { idris_errRev = t : idris_errRev i }

159

161

162+-- | Say that the name should always be reduced in error messages, to

163+-- help readability/error reflection

164+addErrReduce :: Name -> Idris ()

165+addErrReduce t = do i <- getIState

166+ putIState $ i { idris_errReduce = t : idris_errReduce i }

167+

160addErasureUsage :: Name -> Int -> Idris ()

168addErasureUsage :: Name -> Int -> Idris ()

161addErasureUsage n i = do ist <- getIState

169addErasureUsage n i = do ist <- getIState

162 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

170 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

src/Idris/AbsSyntaxTree.hs+4−1

@@ -257,6 +257,7 @@ data IState = IState {

257 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]

258 , idris_coercions :: [Name]

259 , idris_errRev :: [(Term, Term)]

260+ , idris_errReduce :: [Name]

260 , syntax_rules :: SyntaxRules

261 , syntax_rules :: SyntaxRules

261 , syntax_keywords :: [String]

262 , syntax_keywords :: [String]

262 , imported :: [FilePath] -- ^ The imported modules

263 , imported :: [FilePath] -- ^ The imported modules

@@ -373,6 +374,7 @@ data IBCWrite = IBCFix FixDecl

373 | IBCFnInfo Name FnInfo

374 | IBCFnInfo Name FnInfo

374 | IBCTrans Name (Term, Term)

375 | IBCTrans Name (Term, Term)

375 | IBCErrRev (Term, Term)

376 | IBCErrRev (Term, Term)

377+ | IBCErrReduce Name

376 | IBCCG Name

378 | IBCCG Name

377 | IBCDoc Name

379 | IBCDoc Name

378 | IBCCoercion Name

380 | IBCCoercion Name

@@ -408,7 +410,7 @@ idrisInit = IState initContext S.empty []

408 emptyContext emptyContext emptyContext emptyContext

410 emptyContext emptyContext emptyContext emptyContext

409 emptyContext emptyContext emptyContext emptyContext

411 emptyContext emptyContext emptyContext emptyContext

410 emptyContext

412 emptyContext

411− [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

413+ [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

412 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

413 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

415 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

414 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

416 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

@@ -676,6 +678,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

676 | CExport String -- ^ export, with a C name

678 | CExport String -- ^ export, with a C name

677 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension

679 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension

678 | ErrorReverse -- ^ attempt to reverse normalise before showing in error

680 | ErrorReverse -- ^ attempt to reverse normalise before showing in error

681+ | ErrorReduce -- ^ unfold definition before showing an error

679 | Reflection -- ^ a reflecting function, compile-time only

682 | Reflection -- ^ a reflecting function, compile-time only

680 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names

683 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names

681 | UnfoldIface Name [Name]

684 | UnfoldIface Name [Name]

src/Idris/Elab/Clause.hs+3

@@ -942,6 +942,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

942 when (rev || ErrorReverse `elem` opts) $ do

943 addIBC (IBCErrRev (crhs, clhs))

944 addErrRev (crhs, clhs)

945+ when (rev || ErrorReduce `elem` opts) $ do

946+ addIBC (IBCErrReduce fname)

947+ addErrReduce fname

945 pop_estack

948 pop_estack

946 return (Right (clhs, crhs), lhs)

949 return (Right (clhs, crhs), lhs)

947 where

950 where

src/Idris/ErrReverse.hs+10−2

@@ -11,16 +11,24 @@ module Idris.ErrReverse(errReverse) where

12import Idris.AbsSyntax

13import Idris.Core.TT

14+import Idris.Core.Evaluate(unfold)

14import Util.Pretty

15import Util.Pretty

16import Data.List

17import Data.List

17import Debug.Trace

18import Debug.Trace

19-- | For display purposes, apply any 'error reversal' transformations

20-- | For display purposes, apply any 'error reversal' transformations

20−-- so that errors will be more readable

21+-- so that errors will be more readable,

22+-- and any 'error reduce' transformations

21errReverse :: IState -> Term -> Term

23errReverse :: IState -> Term -> Term

22−errReverse ist t = rewrite 5 t -- (elideLambdas t)

24+errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)

23 where

25 where

26+ do_unfold :: Term -> Term

27+ do_unfold t = let ns = idris_errReduce ist in

28+ if null ns then t

29+ else unfold (tt_ctxt ist) []

30+ (map (\x -> (x, 1000)) (idris_errReduce ist))

31+ t

25 rewrite 0 t = t

33 rewrite 0 t = t

26 rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in

34 rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in

src/Idris/IBC.hs+12−1

@@ -86,6 +86,7 @@ data IBCFile = IBCFile {

86 , ibc_moduledocs :: ![(Name, Docstring D.DocTerm)]

87 , ibc_transforms :: ![(Name, (Term, Term))]

88 , ibc_errRev :: ![(Term, Term)]

89+ , ibc_errReduce :: ![Name]

89 , ibc_coercions :: ![Name]

90 , ibc_coercions :: ![Name]

90 , ibc_lineapps :: ![(FilePath, Int, PTerm)]

91 , ibc_lineapps :: ![(FilePath, Int, PTerm)]

91 , ibc_namehints :: ![(Name, Name)]

92 , ibc_namehints :: ![(Name, Name)]

@@ -114,7 +115,7 @@ deriving instance Binary IBCFile

114!-}

115!-}

115

116

116initIBC :: IBCFile

117initIBC :: IBCFile

117−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

118+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

118

119

119hasValidIBCVersion :: FilePath -> Idris Bool

120hasValidIBCVersion :: FilePath -> Idris Bool

120hasValidIBCVersion fp = do

121hasValidIBCVersion fp = do

@@ -191,6 +192,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

191 makeEntry "ibc_moduledocs" (ibc_moduledocs i),

192 makeEntry "ibc_moduledocs" (ibc_moduledocs i),

192 makeEntry "ibc_transforms" (ibc_transforms i),

193 makeEntry "ibc_transforms" (ibc_transforms i),

193 makeEntry "ibc_errRev" (ibc_errRev i),

194 makeEntry "ibc_errRev" (ibc_errRev i),

195+ makeEntry "ibc_errReduce" (ibc_errReduce i),

194 makeEntry "ibc_coercions" (ibc_coercions i),

196 makeEntry "ibc_coercions" (ibc_coercions i),

195 makeEntry "ibc_lineapps" (ibc_lineapps i),

197 makeEntry "ibc_lineapps" (ibc_lineapps i),

196 makeEntry "ibc_namehints" (ibc_namehints i),

198 makeEntry "ibc_namehints" (ibc_namehints i),

@@ -324,6 +326,7 @@ ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

324ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }

326ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }

325ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

327ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

326ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

328ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

329+ibc i (IBCErrReduce t) f = return f { ibc_errReduce = t : ibc_errReduce f }

327ibc i (IBCLineApp fp l t) f

330ibc i (IBCLineApp fp l t) f

328 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

331 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

329ibc i (IBCNameHint (n, ty)) f

332ibc i (IBCNameHint (n, ty)) f

@@ -416,6 +419,7 @@ process reexp phase archive fn = do

416 processCoercions archive

419 processCoercions archive

417 processTransforms archive

420 processTransforms archive

418 processErrRev archive

421 processErrRev archive

422+ processErrReduce archive

419 processLineApps archive

423 processLineApps archive

420 processNameHints archive

424 processNameHints archive

421 processMetaInformation archive

425 processMetaInformation archive

@@ -797,6 +801,11 @@ processErrRev ar = do

797 ts <- getEntry [] "ibc_errRev" ar

801 ts <- getEntry [] "ibc_errRev" ar

798 mapM_ addErrRev ts

802 mapM_ addErrRev ts

799

803

804+processErrReduce :: Archive -> Idris ()

805+processErrReduce ar = do

806+ ts <- getEntry [] "ibc_errReduce" ar

807+ mapM_ addErrReduce ts

808+

800processLineApps :: Archive -> Idris ()

809processLineApps :: Archive -> Idris ()

801processLineApps ar = do

810processLineApps ar = do

802 ls <- getEntry [] "ibc_lineapps" ar

811 ls <- getEntry [] "ibc_lineapps" ar

@@ -1232,6 +1241,7 @@ instance Binary FnOpt where

1232 UnfoldIface x ns -> do putWord8 19

1241 UnfoldIface x ns -> do putWord8 19

1233 put x

1242 put x

1234 put ns

1243 put ns

1244+ ErrorReduce -> putWord8 20

1235 get

1245 get

1236 = do i <- getWord8

1246 = do i <- getWord8

1237 case i of

1247 case i of

@@ -1259,6 +1269,7 @@ instance Binary FnOpt where

1259 19 -> do x <- get

1269 19 -> do x <- get

1260 ns <- get

1270 ns <- get

1261 return (UnfoldIface x ns)

1271 return (UnfoldIface x ns)

1272+ 20 -> return ErrorReduce

1262 _ -> error "Corrupted binary data for FnOpt"

1273 _ -> error "Corrupted binary data for FnOpt"

1263

1274

1264instance Binary Fixity where

1275instance Binary Fixity where

src/Idris/Parser.hs+2

@@ -688,6 +688,8 @@ fnOpt = do reservedHL "total"; return TotalFn

688 return ErrorHandler

689 <|> do try (lchar '%' *> reserved "error_reverse");

690 return ErrorReverse

691+ <|> do try (lchar '%' *> reserved "error_reduce");

692+ return ErrorReduce

691 <|> do try (lchar '%' *> reserved "reflection");

693 <|> do try (lchar '%' *> reserved "reflection");

692 return Reflection

694 return Reflection

693 <|> do try (lchar '%' *> reserved "hint");

695 <|> do try (lchar '%' *> reserved "hint");