ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 20:04:36 +03:00
Code Issues Projects Releases Wiki Activity

Added %error_reverse annotation

Browse Source 
On a function, %error_reverse hints that the function should be run "in
reverse", i.e. as a rewrite rule from right to left, before displaying
an error message.

On a data declaration, %error_reverse means that all functions with that
type will be implicitly set as %error_reverse functions.

EFFECT is now set as %error_reverse. So in the Effects library, this
leads to much nicer messages, e.g.:

Can't solve goal
    SubList [(FILE_IO (OpenFile m))] [(FILE_IO ()),STDIO,
    ('Count ::: (STATE Int))]

...rather than the fully normalised versions we used to see.
This commit is contained in:
Edwin Brady 2014-01-26 23:52:04 +00:00
parent 803194f5d7
commit fe3f03f272
15 changed files with 212 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
CHANGELOG
View File

@ -7,12 +7,16 @@ New in 0.9.11:
This is intended for field/effect disambiguation. "name" can be any
valid identifier. Two labels are definitionally equal if they have the
same name.
* General improvements in error messages, especially %error_reverse
annotation, which allows a hint as to how to display a term in error
messages
Internal changes
* Faster elaboration
* Smaller .ibc files
New in 0.9.10:
--------------

1
idris.cabal
View File

@ -377,6 +377,7 @@ Library
, Idris.ElabDecls
, Idris.ElabTerm
, Idris.Error
, Idris.ErrReverse
, Idris.Help
, Idris.IBC
, Idris.IdeSlave

1
libs/effects/Effects.idr
View File

@ -10,6 +10,7 @@ import Control.Catchable
Effect : Type
Effect = Type -> Type -> Type -> Type
%error_reverse
data EFFECT : Type where
MkEff : Type -> Effect -> EFFECT

1
libs/neweffects/Effects.idr
View File

@ -11,6 +11,7 @@ import Effect.Default
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type
%error_reverse
data EFFECT : Type where
MkEff : Type -> Effect -> EFFECT

4
src/Idris/AbsSyntax.hs
View File

@ -95,6 +95,10 @@ addTrans :: (Term, Term) -> Idris ()
addTrans t = do i <- getIState
putIState $ i { idris_transforms = t : idris_transforms i }
addErrRev :: (Term, Term) -> Idris ()
addErrRev t = do i <- getIState
putIState $ i { idris_errRev = t : idris_errRev i }
totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

10
src/Idris/AbsSyntaxTree.hs
View File

@ -109,6 +109,7 @@ data IState = IState {
idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
idris_coercions :: [Name],
idris_transforms :: [(Term, Term)],
idris_errRev :: [(Term, Term)],
syntax_rules :: [Syntax],
syntax_keywords :: [String],
imported :: [FilePath], -- ^ The imported modules
@ -184,6 +185,7 @@ data IBCWrite = IBCFix FixDecl
| IBCTotal Name Totality
| IBCFlags Name [FnOpt]
| IBCTrans (Term, Term)
| IBCErrRev (Term, Term)
| IBCCG Name
| IBCDoc Name
| IBCCoercion Name
@ -198,7 +200,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
emptyContext
[] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
[] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
[] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
True defaultTheme stdout [] (0, emptyContext)
@ -391,6 +393,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
| Implicit -- implicit coercion
| CExport String -- export, with a C name
| ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
| ErrorReverse -- ^^ attempt to reverse normalise before showing in error
| Reflection -- a reflecting function, compile-time only
| Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
deriving (Show, Eq)
@ -411,6 +414,7 @@ dictionary = elem Dictionary
-- | Data declaration options
data DataOpt = Codata -- Set if the the data-type is coinductive
| DefaultEliminator -- Set if an eliminator should be generated for data type
| DataErrRev
deriving (Show, Eq)
type DataOpts = [DataOpt]
@ -809,6 +813,7 @@ deriving instance NFData OptInfo
data TypeInfo = TI { con_names :: [Name],
codata :: Bool,
data_opts :: DataOpts,
param_pos :: [Int] }
deriving Show
{-!
@ -1255,6 +1260,9 @@ showImp ist impl colour tm = se 10 [] tm where
"{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
se 10 ((n, False):bnd) sc
se p bnd (PMatchApp _ f) = "match " ++ show f
se p bnd (PApp _ hd@(PRef fc f) [tm])
| PConstant (Idris.Core.TT.Str str) <- getTm tm,
f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))
se p bnd (PApp _ hd@(PRef _ f) [])
| not impl = se p bnd hd
se p bnd (PAppBind _ hd@(PRef _ f) [])

44
src/Idris/Core/TT.hs
View File

@ -90,41 +90,45 @@ data ErrorReportPart = TextPart String
-- | Idris errors. Used as exceptions in the compiler, but reported to users
-- if they reach the top level.
data Err = Msg String
data Err' t
= Msg String
| InternalMsg String
| CantUnify Bool Term Term Err [(Name, Type)] Int
| CantUnify Bool t t (Err' t) [(Name, t)] Int
-- Int is 'score' - how much we did unify
-- Bool indicates recoverability, True indicates more info may make
-- unification succeed
| InfiniteUnify Name Term [(Name, Type)]
| CantConvert Term Term [(Name, Type)]
| CantSolveGoal Term [(Name, Type)]
| UnifyScope Name Name Term [(Name, Type)]
| InfiniteUnify Name t [(Name, t)]
| CantConvert t t [(Name, t)]
| CantSolveGoal t [(Name, t)]
| UnifyScope Name Name t [(Name, t)]
| CantInferType String
| NonFunctionType Term Term
| NotEquality Term Term
| NonFunctionType t t
| NotEquality t t
| TooManyArguments Name
| CantIntroduce Term
| CantIntroduce t
| NoSuchVariable Name
| NoTypeDecl Name
| NotInjective Term Term Term
| CantResolve Term
| NotInjective t t t
| CantResolve t
| CantResolveAlts [String]
| IncompleteTerm Term
| IncompleteTerm t
| UniverseError
| ProgramLineComment
| Inaccessible Name
| NonCollapsiblePostulate Name
| AlreadyDefined Name
| ProofSearchFail Err
| NoRewriting Term
| At FC Err
| Elaborating String Name Err
| ProofSearchFail (Err' t)
| NoRewriting t
| At FC (Err' t)
| Elaborating String Name (Err' t)
| ProviderError String
| LoadingFailed String Err
| ReflectionError [[ErrorReportPart]] Err
| ReflectionFailed String Err
deriving Eq
| LoadingFailed String (Err' t)
| ReflectionError [[ErrorReportPart]] (Err' t)
| ReflectionFailed String (Err' t)
deriving (Eq, Functor)
type Err = Err' Term
{-!
deriving instance NFData Err
!-}

8
src/Idris/Coverage.hs
View File

@ -183,7 +183,7 @@ genAll i args
let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
let tyn = getTy n (tt_ctxt i)
case lookupCtxt tyn (idris_datatypes i) of
(TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
(TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
_ -> [p]
ops fc n arg o = return Placeholder
@ -289,7 +289,7 @@ calcProd i fc topn pats
cotype (DCon _ _) n ty
| (P _ t _, _) <- unApply (getRetTy ty)
= case lookupCtxt t (idris_datatypes i) of
[TI _ True _] -> True
[TI _ True _ _] -> True
_ -> False
cotype nt n ty = False
@ -466,7 +466,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
isInductive (P _ nty _) (P _ nty' _) =
let co = case lookupCtxt nty (idris_datatypes ist) of
[TI _ x _] -> x
[TI _ x _ _] -> x
_ -> False in
nty == nty' && not co
isInductive _ _ = False
@ -507,7 +507,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
[ty] = lookupTy n ctxt -- must exist!
P _ nty _ = fst (unApply (getRetTy ty))
co = case lookupCtxt nty (idris_datatypes ist) of
[TI _ x _] -> x
[TI _ x _ _] -> x
_ -> False
args = map snd (getArgTys ty) in
map (getRel co nty) (map (fst . unApply . getRetTy) args)

2
src/Idris/DeepSeq.hs
View File

@ -243,7 +243,7 @@ instance NFData OptInfo where
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
instance NFData TypeInfo where
rnf (TI x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
instance (NFData t) => NFData (DSL' t) where
rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

77
src/Idris/Delaborate.hs
View File

@ -8,6 +8,7 @@ module Idris.Delaborate where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.ErrReverse
import Data.List (intersperse)
@ -121,11 +122,13 @@ indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
else [c]
pshow :: IState -> Err -> String
pshow i (Msg s) = s
pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
pshow i err = pshow' i (fmap (errReverse i) err)
pshow' i (Msg s) = s
pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
"\nThis is probably a bug, or a missing error message.\n" ++
"Please consider reporting at " ++ bugaddr
pshow i (CantUnify _ x y e sc s)
pshow' i (CantUnify _ x y e sc s)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
"Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
@ -134,72 +137,72 @@ pshow i (CantUnify _ x y e sc s)
case e of
Msg "" -> ""
_ -> "\nSpecifically:" ++
indented (pshow i e) ++
indented (pshow' i e) ++
if (opt_errContext (idris_options i)) then showSc i sc else ""
pshow i (CantConvert x y env)
pshow' i (CantConvert x y env)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
"Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
++ indented (showImp (Just i) imps colour (delab i y)) ++
if (opt_errContext (idris_options i)) then showSc i env else ""
pshow i (CantSolveGoal x env)
pshow' i (CantSolveGoal x env)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
"Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++
if (opt_errContext (idris_options i)) then showSc i env else ""
pshow i (UnifyScope n out tm env)
pshow' i (UnifyScope n out tm env)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
"Can't unify" ++ indented (show n) ++ "with"
++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
indented (show out) ++ "is not in scope" ++
if (opt_errContext (idris_options i)) then showSc i env else ""
pshow i (CantInferType t)
pshow' i (CantInferType t)
= "Can't infer type for " ++ t
pshow i (NonFunctionType f ty)
pshow' i (NonFunctionType f ty)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
++ showImp (Just i) imps colour (delab i ty) ++ ")"
pshow i (NotEquality tm ty)
pshow' i (NotEquality tm ty)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
++ showImp (Just i) imps colour (delab i ty) ++ ")"
pshow i (TooManyArguments f)
pshow' i (TooManyArguments f)
= "Too many arguments for " ++ show f
pshow i (CantIntroduce ty)
pshow' i (CantIntroduce ty)
= let imps = opt_showimp (idris_options i) in
let colour = idris_colourRepl i in
"Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
pshow i (InfiniteUnify x tm env)
pshow' i (InfiniteUnify x tm env)
= "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
" would lead to infinite value" ++
if (opt_errContext (idris_options i)) then showSc i env else ""
pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
" when unifying " ++ show (delab i x) ++ " and " ++
show (delab i y)
pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
pshow i (NoTypeDecl n) = "No type declaration for " ++ show n
pshow i (NoSuchVariable n) = "No such variable " ++ show n
pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
pshow i UniverseError = "Universe inconsistency"
pshow i ProgramLineComment = "Program line next to comment"
pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
pshow i (NonCollapsiblePostulate n)
pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
" when unifying " ++ show (delab i x) ++ " and " ++
show (delab i y)
pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n
pshow' i (NoSuchVariable n) = "No such variable " ++ show n
pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
pshow' i UniverseError = "Universe inconsistency"
pshow' i ProgramLineComment = "Program line next to comment"
pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
pshow' i (NonCollapsiblePostulate n)
= "The return type of postulate " ++ show n ++ " is not collapsible"
pshow i (AlreadyDefined n) = show n ++ " is already defined"
pshow i (ProofSearchFail e) = pshow i e
pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
pshow i (At f e) = show f ++ ":" ++ pshow i e
pshow i (Elaborating s n e) = "When elaborating " ++ s ++
showqual i n ++ ":\n" ++ pshow i e
pshow i (ProviderError msg) = "Type provider error: " ++ msg
pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e
pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
pshow' i (AlreadyDefined n) = show n ++ " is already defined"
pshow' i (ProofSearchFail e) = pshow' i e
pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
pshow' i (At f e) = show f ++ ":" ++ pshow' i e
pshow' i (Elaborating s n e) = "When elaborating " ++ s ++
showqual i n ++ ":\n" ++ pshow' i e
pshow' i (ProviderError msg) = "Type provider error: " ++ msg
pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e
pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
concat (intersperse "\n" parts') ++
"\nOriginal error:\n" ++ indented (pshow i orig)
"\nOriginal error:\n" ++ indented (pshow' i orig)
where showPart :: ErrorReportPart -> String
showPart (TextPart str) = str
showPart (NamePart n) = let colour = idris_colourRepl i in
@ -207,8 +210,8 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "
showPart (TermPart tm) = let colour = idris_colourRepl i
in showImp (Just i) False colour (delab i tm)
showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
indented (pshow i err) ++
pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
indented (pshow' i err) ++
"\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

19
src/Idris/ElabDecls.hs
View File

@ -100,7 +100,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
let (t, _) = unApply (getRetTy nty')
let corec = case t of
P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
[TI _ True _] -> True
[TI _ True _ _] -> True
_ -> False
_ -> False
let opts' = if corec then (Coinductive : opts) else opts
@ -228,7 +228,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
let as = map (const Nothing) (getArgTys cty)
let params = findParams (map snd cons)
logLvl 2 $ "Parameters : " ++ show params
putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
putIState (i { idris_datatypes =
addDef n (TI (map fst cons) codata opts params)
(idris_datatypes i) })
addIBC (IBCDef n)
addIBC (IBCData n)
@ -1357,6 +1358,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
i <- getIState
checkInferred fc (delab' i crhs True True) rhs
-- if the function is declared '%error_reverse', or its type,
-- then we'll try running it in reverse to improve error messages
let (ret_fam, _) = unApply (getRetTy crhsty)
rev <- case ret_fam of
P _ rfamn _ ->
case lookupCtxt rfamn (idris_datatypes i) of
[TI _ _ dopts _] ->
return (DataErrRev `elem` dopts)
_ -> return False
_ -> return False
when (rev || ErrorReverse `elem` opts) $ do
addIBC (IBCErrRev (crhs, clhs))
addErrRev (crhs, clhs)
return $ Right (clhs, crhs)
where
decorate (NS x ns)

72
src/Idris/ErrReverse.hs Normal file
View File

@ -0,0 +1,72 @@
{-# LANGUAGE PatternGuards #-}
module Idris.ErrReverse where
import Idris.AbsSyntax
import Idris.Core.TT
import Util.Pretty
import Data.List
import Debug.Trace
-- For display purposes, apply any 'error reversal' transformations so that
-- errors will be more readable
errReverse :: IState -> Term -> Term
errReverse ist t = rewrite 5 (elideLambdas t)
where
rewrite 0 t = t
rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in
if t == t' then t
else rewrite (n - 1) t'
applyRule :: Term -> (Term, Term) -> Term
applyRule t (l, r) = applyNames [] t l r
-- Assume pattern bindings match in l and r (if they don't just treat
-- the rule as invalid and return t)
applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)
| n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)
(instantiate (P Ref n' ty') scr)
| otherwise = t
applyNames ns t l r = matchTerm ns l r t
matchTerm ns l r t
| Just nmap <- match ns l t = substNames nmap r
matchTerm ns l r (App f a) = let f' = matchTerm ns l r f
a' = matchTerm ns l r a in
App f' a'
matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b
sc' = matchTerm ns l r sc in
Bind n b' sc'
matchTerm ns l r t = t
match ns l t = do ms <- match' ns l t
combine (nub ms)
-- If any duplicate mappings, it's a failure
combine [] = Just []
combine ((x, t) : xs)
| Just _ <- lookup x xs = Nothing
| otherwise = do xs' <- combine xs
Just ((x, t) : xs')
match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]
match' ns (App f a) (App f' a') = do fs <- match' ns f f'
as <- match' ns a a'
Just (fs ++ as)
-- no matching Binds, for now...
match' ns x y = if x == y then Just [] else Nothing
-- if the term under a lambda is huge, there's no much point in showing
-- it as it won't be very enlightening.
elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)
elideLambdas (Bind n (Lam t) sc)
| size sc > 100 = P Ref (sUN "...") Erased
elideLambdas (Bind n b sc)
= Bind n (fmap elideLambdas b) (elideLambdas sc)
elideLambdas t = t

30
src/Idris/IBC.hs
View File

@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)
ibcVersion :: Word8
ibcVersion = 54
ibcVersion = 56
data IBCFile = IBCFile { ver :: Word8,
sourcefile :: FilePath,
@ -54,6 +54,7 @@ data IBCFile = IBCFile { ver :: Word8,
ibc_defs :: [(Name, Def)],
ibc_docstrings :: [(Name, String)],
ibc_transforms :: [(Term, Term)],
ibc_errRev :: [(Term, Term)],
ibc_coercions :: [Name],
ibc_lineapps :: [(FilePath, Int, PTerm)],
ibc_namehints :: [(Name, Name)],
@ -65,7 +66,7 @@ deriving instance Binary IBCFile
!-}
initIBC :: IBCFile
initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
loadIBC :: FilePath -> Idris ()
loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@ -208,6 +209,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }
ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }
ibc i (IBCLineApp fp l t) f
= return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
ibc i (IBCNameHint (n, ty)) f
@ -247,6 +249,7 @@ process i fn
pDocs (ibc_docstrings i)
pCoercions (ibc_coercions i)
pTrans (ibc_transforms i)
pErrRev (ibc_errRev i)
pLineApps (ibc_lineapps i)
pNameHints (ibc_namehints i)
pMetaInformation (ibc_metainformation i)
@ -416,6 +419,9 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns
pTrans :: [(Term, Term)] -> Idris ()
pTrans ts = mapM_ addTrans ts
pErrRev :: [(Term, Term)] -> Idris ()
pErrRev ts = mapM_ addErrRev ts
pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
@ -1012,7 +1018,7 @@ instance Binary MetaInformation where
return (DataMI x1)
instance Binary IBCFile where
put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)
put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31)
= {-# SCC "putIBCFile" #-}
do put x1
put x2
@ -1044,6 +1050,7 @@ instance Binary IBCFile where
put x28
put x29
put x30
put x31
get
= do x1 <- get
if x1 == ibcVersion then
@ -1076,17 +1083,20 @@ instance Binary IBCFile where
x28 <- get
x29 <- get
x30 <- get
return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)
x31 <- get
return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31)
else return (initIBC { ver = x1 })
instance Binary DataOpt where
put x = case x of
Codata -> putWord8 0
DefaultEliminator -> putWord8 1
DataErrRev -> putWord8 2
get = do i <- getWord8
case i of
0 -> return Codata
1 -> return DefaultEliminator
2 -> return DataErrRev
instance Binary FnOpt where
put x
@ -1102,6 +1112,7 @@ instance Binary FnOpt where
Implicit -> putWord8 7
Reflection -> putWord8 8
ErrorHandler -> putWord8 9
ErrorReverse -> putWord8 10
get
= do i <- getWord8
case i of
@ -1116,6 +1127,7 @@ instance Binary FnOpt where
7 -> return Implicit
8 -> return Reflection
9 -> return ErrorHandler
10 -> return ErrorReverse
_ -> error "Corrupted binary data for FnOpt"
instance Binary Fixity where
@ -1932,13 +1944,15 @@ instance Binary OptInfo where
return (Optimise x1 x2 x3 x4)
instance Binary TypeInfo where
put (TI x1 x2 x3) = do put x1
put x2
put x3
put (TI x1 x2 x3 x4) = do put x1
put x2
put x3
put x4
get = do x1 <- get
x2 <- get
x3 <- get
return (TI x1 x2 x3)
x4 <- get
return (TI x1 x2 x3 x4)
instance Binary SynContext where
put x

14
src/Idris/ParseData.hs
View File

@ -77,8 +77,12 @@ dataI = do reserved "data"; return []
{- | Parses if a data should not have a default eliminator
DefaultEliminator ::= 'noelim'?
-}
defaultEliminator :: IdrisParser DataOpts
defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])
dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts opts
= do reserved "%elim"; dataOpts (DefaultEliminator : opts)
<|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
<|> return opts
<?> "data options"
{- | Parses a data type declaration
Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
@ -100,7 +104,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do
doc <- option "" (docComment '|')
pushIndent
acc <- optional accessibility
elim <- defaultEliminator
elim <- dataOpts []
co <- dataI
let dataOpts = combineDataOpts(elim ++ co)
return (doc, acc, dataOpts))
@ -146,7 +150,9 @@ data_ syn = do (doc, acc, dataOpts) <- try (do
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs
combineDataOpts :: DataOpts -> DataOpts
combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts
combineDataOpts opts = if Codata `elem` opts
then delete DefaultEliminator opts
else opts
{- | Parses a type constructor declaration

2
src/Idris/Parser.hs
View File

@ -337,6 +337,8 @@ fnOpts opts
fnOpts (AssertTotal : opts)
<|> do try (lchar '%' *> reserved "error_handler");
fnOpts (ErrorHandler : opts)
<|> do try (lchar '%' *> reserved "error_reverse");
fnOpts (ErrorReverse : opts)
<|> do try (lchar '%' *> reserved "reflection");
fnOpts (Reflection : opts)
<|> do lchar '%'; reserved "specialise";