git.iko.soy/Idris-dev
on master help sign in
%error_reduce for more control over errors

A function marked %error_reduce will always be unfolded as far as possible before displaying an error message. This can help with error reflection, in particular.

commitbc553c70eb8357359a07d3954e07de2baf368483 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 10 Feb 2017, 10:57 (10 years ago) parent823d5d7
6 files changed+39−4
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+8 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Elab/Clause.hs+3 src/Idris/ErrReverse.hs+10−2 src/Idris/IBC.hs+12−1 src/Idris/Parser.hs+2
src/Idris/AbsSyntax.hs+8
@@ -153,10 +153,18 @@ addTrans basefn t
153153 putIState $ i { idris_transforms = addDef basefn t'
154154 (idris_transforms i) }
155155
156+-- | Add transformation rules from a definition, which will reverse the
157+-- definition for an error to make it more readable
156158addErrRev :: (Term, Term) -> Idris ()
157159addErrRev t = do i <- getIState
158160 putIState $ i { idris_errRev = t : idris_errRev i }
159161
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+
160168addErasureUsage :: Name -> Int -> Idris ()
161169addErasureUsage n i = do ist <- getIState
162170 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
src/Idris/AbsSyntaxTree.hs+4−1
@@ -257,6 +257,7 @@ data IState = IState {
257257 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
258258 , idris_coercions :: [Name]
259259 , idris_errRev :: [(Term, Term)]
260+ , idris_errReduce :: [Name]
260261 , syntax_rules :: SyntaxRules
261262 , syntax_keywords :: [String]
262263 , imported :: [FilePath] -- ^ The imported modules
@@ -373,6 +374,7 @@ data IBCWrite = IBCFix FixDecl
373374 | IBCFnInfo Name FnInfo
374375 | IBCTrans Name (Term, Term)
375376 | IBCErrRev (Term, Term)
377+ | IBCErrReduce Name
376378 | IBCCG Name
377379 | IBCDoc Name
378380 | IBCCoercion Name
@@ -408,7 +410,7 @@ idrisInit = IState initContext S.empty []
408410 emptyContext emptyContext emptyContext emptyContext
409411 emptyContext emptyContext emptyContext emptyContext
410412 emptyContext
411− [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
413+ [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
412414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
413415 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
414416 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
@@ -676,6 +678,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying
676678 | CExport String -- ^ export, with a C name
677679 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
678680 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
681+ | ErrorReduce -- ^ unfold definition before showing an error
679682 | Reflection -- ^ a reflecting function, compile-time only
680683 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
681684 | 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
942942 when (rev || ErrorReverse `elem` opts) $ do
943943 addIBC (IBCErrRev (crhs, clhs))
944944 addErrRev (crhs, clhs)
945+ when (rev || ErrorReduce `elem` opts) $ do
946+ addIBC (IBCErrReduce fname)
947+ addErrReduce fname
945948 pop_estack
946949 return (Right (clhs, crhs), lhs)
947950 where
src/Idris/ErrReverse.hs+10−2
@@ -11,16 +11,24 @@ module Idris.ErrReverse(errReverse) where
1111
1212import Idris.AbsSyntax
1313import Idris.Core.TT
14+import Idris.Core.Evaluate(unfold)
1415import Util.Pretty
1516
1617import Data.List
1718import Debug.Trace
1819
1920-- | 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
2123errReverse :: IState -> Term -> Term
22−errReverse ist t = rewrite 5 t -- (elideLambdas t)
24+errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)
2325 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
2432
2533 rewrite 0 t = t
2634 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 {
8686 , ibc_moduledocs :: ![(Name, Docstring D.DocTerm)]
8787 , ibc_transforms :: ![(Name, (Term, Term))]
8888 , ibc_errRev :: ![(Term, Term)]
89+ , ibc_errReduce :: ![Name]
8990 , ibc_coercions :: ![Name]
9091 , ibc_lineapps :: ![(FilePath, Int, PTerm)]
9192 , ibc_namehints :: ![(Name, Name)]
@@ -114,7 +115,7 @@ deriving instance Binary IBCFile
114115!-}
115116
116117initIBC :: IBCFile
117−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
118+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
118119
119120hasValidIBCVersion :: FilePath -> Idris Bool
120121hasValidIBCVersion fp = do
@@ -191,6 +192,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
191192 makeEntry "ibc_moduledocs" (ibc_moduledocs i),
192193 makeEntry "ibc_transforms" (ibc_transforms i),
193194 makeEntry "ibc_errRev" (ibc_errRev i),
195+ makeEntry "ibc_errReduce" (ibc_errReduce i),
194196 makeEntry "ibc_coercions" (ibc_coercions i),
195197 makeEntry "ibc_lineapps" (ibc_lineapps i),
196198 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 }
324326ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }
325327ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }
326328ibc 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 }
327330ibc i (IBCLineApp fp l t) f
328331 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
329332ibc i (IBCNameHint (n, ty)) f
@@ -416,6 +419,7 @@ process reexp phase archive fn = do
416419 processCoercions archive
417420 processTransforms archive
418421 processErrRev archive
422+ processErrReduce archive
419423 processLineApps archive
420424 processNameHints archive
421425 processMetaInformation archive
@@ -797,6 +801,11 @@ processErrRev ar = do
797801 ts <- getEntry [] "ibc_errRev" ar
798802 mapM_ addErrRev ts
799803
804+processErrReduce :: Archive -> Idris ()
805+processErrReduce ar = do
806+ ts <- getEntry [] "ibc_errReduce" ar
807+ mapM_ addErrReduce ts
808+
800809processLineApps :: Archive -> Idris ()
801810processLineApps ar = do
802811 ls <- getEntry [] "ibc_lineapps" ar
@@ -1232,6 +1241,7 @@ instance Binary FnOpt where
12321241 UnfoldIface x ns -> do putWord8 19
12331242 put x
12341243 put ns
1244+ ErrorReduce -> putWord8 20
12351245 get
12361246 = do i <- getWord8
12371247 case i of
@@ -1259,6 +1269,7 @@ instance Binary FnOpt where
12591269 19 -> do x <- get
12601270 ns <- get
12611271 return (UnfoldIface x ns)
1272+ 20 -> return ErrorReduce
12621273 _ -> error "Corrupted binary data for FnOpt"
12631274
12641275instance Binary Fixity where
src/Idris/Parser.hs+2
@@ -688,6 +688,8 @@ fnOpt = do reservedHL "total"; return TotalFn
688688 return ErrorHandler
689689 <|> do try (lchar '%' *> reserved "error_reverse");
690690 return ErrorReverse
691+ <|> do try (lchar '%' *> reserved "error_reduce");
692+ return ErrorReduce
691693 <|> do try (lchar '%' *> reserved "reflection");
692694 return Reflection
693695 <|> do try (lchar '%' *> reserved "hint");