8c620dc · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

@@ -7,12 +7,16 @@ New in 0.9.11:

7 This is intended for field/effect disambiguation. "name" can be any

8 valid identifier. Two labels are definitionally equal if they have the

9 same name.

10+* General improvements in error messages, especially %error_reverse

11+ annotation, which allows a hint as to how to display a term in error

12+ messages

10

13

11Internal changes

14Internal changes

12

15

13* Faster elaboration

16* Faster elaboration

14* Smaller .ibc files

17* Smaller .ibc files

15

18

19+

16New in 0.9.10:

20New in 0.9.10:

17--------------

21--------------

18

22

contribs/lib/SimpleParser/simpleparser.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package simpleparser

2+

3+opts = "-i ../lib"

4+modules = SimpleParser

idris.cabal+1

@@ -380,6 +380,7 @@ Library

380 , Idris.ElabDecls

381 , Idris.ElabTerm

382 , Idris.Error

383+ , Idris.ErrReverse

383 , Idris.Help

384 , Idris.Help

384 , Idris.IBC

385 , Idris.IBC

385 , Idris.IdeSlave

386 , Idris.IdeSlave

libs/effects/Effects.idr+1

@@ -10,6 +10,7 @@ import Control.Catchable

10Effect : Type

11Effect = Type -> Type -> Type -> Type

12

13+%error_reverse

13data EFFECT : Type where

14data EFFECT : Type where

14 MkEff : Type -> Effect -> EFFECT

15 MkEff : Type -> Effect -> EFFECT

15

16

libs/neweffects/Effects.idr+1

@@ -11,6 +11,7 @@ import Effect.Default

11Effect : Type

12Effect = (x : Type) -> Type -> (x -> Type) -> Type

13

14+%error_reverse

14data EFFECT : Type where

15data EFFECT : Type where

15 MkEff : Type -> Effect -> EFFECT

16 MkEff : Type -> Effect -> EFFECT

16

17

libs/prelude/Decidable/Equality.idr+10−1

@@ -153,7 +153,7 @@ instance DecEq a => DecEq (List a) where

153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)

154 decEq (x :: xs) (y :: ys) with (decEq x y)

155 decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

156− decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -- maybe another yes refl

156+ decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl

157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)

158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)

159 decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)

@@ -215,3 +215,12 @@ instance DecEq Float where

215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

216 else No (really_believe_me _|_)

217

218+--------------------------------------------------------------------------------

219+-- String

220+--------------------------------------------------------------------------------

221+

222+instance DecEq String where

223+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

224+ else No (really_believe_me _|_)

225+

226+

src/Idris/AbsSyntax.hs+8−4

@@ -97,6 +97,10 @@ addTrans :: (Term, Term) -> Idris ()

97addTrans t = do i <- getIState

98 putIState $ i { idris_transforms = t : idris_transforms i }

99

100+addErrRev :: (Term, Term) -> Idris ()

101+addErrRev t = do i <- getIState

102+ putIState $ i { idris_errRev = t : idris_errRev i }

103+

100totcheck :: (FC, Name) -> Idris ()

104totcheck :: (FC, Name) -> Idris ()

101totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

105totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

102

106

@@ -1060,12 +1064,12 @@ addUsingConstraints syn fc t

1060 -- if all of args in ns, then add it

1064 -- if all of args in ns, then add it

1061 doAdd (UConstraint c args : cs) ns t

1065 doAdd (UConstraint c args : cs) ns t

1062 | all (\n -> elem n ns) args

1066 | all (\n -> elem n ns) args

1063− = PPi (Constraint False Dynamic "") (sMN 0 "cu")

1067+ = PPi (Constraint [] Dynamic "") (sMN 0 "cu")

1064 (mkConst c args) (doAdd cs ns t)

1068 (mkConst c args) (doAdd cs ns t)

1065 | otherwise = doAdd cs ns t

1069 | otherwise = doAdd cs ns t

1066

1070

1067 mkConst c args = PApp fc (PRef fc c)

1071 mkConst c args = PApp fc (PRef fc c)

1068− (map (\n -> PExp 0 False (PRef fc n) "") args)

1072+ (map (\n -> PExp 0 [] (PRef fc n) "") args)

1069

1073

1070 getConstraints (PPi (Constraint _ _ _) _ c sc)

1074 getConstraints (PPi (Constraint _ _ _) _ c sc)

1071 = getcapp c ++ getConstraints sc

1075 = getcapp c ++ getConstraints sc

@@ -1195,8 +1199,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1195 pibind using [] sc = sc

1199 pibind using [] sc = sc

1196 pibind using (n:ns) sc

1200 pibind using (n:ns) sc

1197 = case lookup n using of

1201 = case lookup n using of

1198− Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)

1202+ Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)

1199− Nothing -> PPi (Imp False Dynamic "" False) n Placeholder

1203+ Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder

1200 (pibind using ns sc)

1204 (pibind using ns sc)

1201

1205

1202-- Add implicit arguments in function calls

1206-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+43−22

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

111 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

112 idris_coercions :: [Name],

113 idris_transforms :: [(Term, Term)],

114+ idris_errRev :: [(Term, Term)],

114 syntax_rules :: [Syntax],

115 syntax_rules :: [Syntax],

115 syntax_keywords :: [String],

116 syntax_keywords :: [String],

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

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

@@ -187,6 +188,7 @@ data IBCWrite = IBCFix FixDecl

187 | IBCTotal Name Totality

188 | IBCTotal Name Totality

188 | IBCFlags Name [FnOpt]

189 | IBCFlags Name [FnOpt]

189 | IBCTrans (Term, Term)

190 | IBCTrans (Term, Term)

191+ | IBCErrRev (Term, Term)

190 | IBCCG Name

192 | IBCCG Name

191 | IBCDoc Name

193 | IBCDoc Name

192 | IBCCoercion Name

194 | IBCCoercion Name

@@ -203,7 +205,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

203 emptyContext emptyContext emptyContext emptyContext

205 emptyContext emptyContext emptyContext emptyContext

204 emptyContext emptyContext emptyContext emptyContext

206 emptyContext emptyContext emptyContext emptyContext

205 emptyContext

207 emptyContext

206− [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

208+ [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

207 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

209 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

208 True defaultTheme stdout [] (0, emptyContext) emptyContext

210 True defaultTheme stdout [] (0, emptyContext) emptyContext

209

211

@@ -357,33 +359,36 @@ deriving instance NFData Static

357!-}

359!-}

358

360

359-- Mark bindings with their explicitness, and laziness

361-- Mark bindings with their explicitness, and laziness

360−data Plicity = Imp { plazy :: Bool,

362+data Plicity = Imp { pargopts :: [ArgOpt],

361 pstatic :: Static,

363 pstatic :: Static,

362 pdocstr :: String,

364 pdocstr :: String,

363 pparam :: Bool }

365 pparam :: Bool }

364− | Exp { plazy :: Bool,

366+ | Exp { pargopts :: [ArgOpt],

365 pstatic :: Static,

367 pstatic :: Static,

366 pdocstr :: String,

368 pdocstr :: String,

367 pparam :: Bool }

369 pparam :: Bool }

368− | Constraint { plazy :: Bool,

370+ | Constraint { pargopts :: [ArgOpt],

369 pstatic :: Static,

371 pstatic :: Static,

370 pdocstr :: String }

372 pdocstr :: String }

371− | TacImp { plazy :: Bool,

373+ | TacImp { pargopts :: [ArgOpt],

372 pstatic :: Static,

374 pstatic :: Static,

373 pscript :: PTerm,

375 pscript :: PTerm,

374 pdocstr :: String }

376 pdocstr :: String }

375 deriving (Show, Eq)

377 deriving (Show, Eq)

376

378

379+plazy :: Plicity -> Bool

380+plazy tm = Lazy `elem` pargopts tm

381+

377{-!

382{-!

378deriving instance Binary Plicity

383deriving instance Binary Plicity

379deriving instance NFData Plicity

384deriving instance NFData Plicity

380!-}

385!-}

381

386

382−impl = Imp False Dynamic "" False

387+impl = Imp [Lazy] Dynamic "" False

383−expl = Exp False Dynamic "" False

388+expl = Exp [] Dynamic "" False

384−expl_param = Exp False Dynamic "" True

389+expl_param = Exp [] Dynamic "" True

385−constraint = Constraint False Dynamic ""

390+constraint = Constraint [] Dynamic ""

386−tacimpl t = TacImp False Dynamic t ""

391+tacimpl t = TacImp [] Dynamic t ""

387

392

388data FnOpt = Inlinable -- always evaluate when simplifying

393data FnOpt = Inlinable -- always evaluate when simplifying

389 | TotalFn | PartialFn

394 | TotalFn | PartialFn

@@ -393,6 +398,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

393 | Implicit -- implicit coercion

398 | Implicit -- implicit coercion

394 | CExport String -- export, with a C name

399 | CExport String -- export, with a C name

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

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

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

396 | Reflection -- a reflecting function, compile-time only

402 | Reflection -- a reflecting function, compile-time only

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

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

398 deriving (Show, Eq)

404 deriving (Show, Eq)

@@ -413,6 +419,7 @@ dictionary = elem Dictionary

413-- | Data declaration options

419-- | Data declaration options

414data DataOpt = Codata -- Set if the the data-type is coinductive

420data DataOpt = Codata -- Set if the the data-type is coinductive

415 | DefaultEliminator -- Set if an eliminator should be generated for data type

421 | DefaultEliminator -- Set if an eliminator should be generated for data type

422+ | DataErrRev

416 deriving (Show, Eq)

423 deriving (Show, Eq)

417

424

418type DataOpts = [DataOpt]

425type DataOpts = [DataOpt]

@@ -729,21 +736,31 @@ type PDo = PDo' PTerm

729

736

730data PArg' t = PImp { priority :: Int,

737data PArg' t = PImp { priority :: Int,

731 machine_inf :: Bool, -- true if the machine inferred it

738 machine_inf :: Bool, -- true if the machine inferred it

739+ argopts :: [ArgOpt],

732− lazyarg :: Bool, pname :: Name, getTm :: t,

740+ pname :: Name, getTm :: t,

733 pargdoc :: String }

741 pargdoc :: String }

734 | PExp { priority :: Int,

742 | PExp { priority :: Int,

743+ argopts :: [ArgOpt],

735− lazyarg :: Bool, getTm :: t,

744+ getTm :: t,

736 pargdoc :: String }

745 pargdoc :: String }

737 | PConstraint { priority :: Int,

746 | PConstraint { priority :: Int,

747+ argopts :: [ArgOpt],

738− lazyarg :: Bool, getTm :: t,

748+ getTm :: t,

739 pargdoc :: String }

749 pargdoc :: String }

740 | PTacImplicit { priority :: Int,

750 | PTacImplicit { priority :: Int,

751+ argopts :: [ArgOpt],

741− lazyarg :: Bool, pname :: Name,

752+ pname :: Name,

742 getScript :: t,

753 getScript :: t,

743 getTm :: t,

754 getTm :: t,

744 pargdoc :: String }

755 pargdoc :: String }

745 deriving (Show, Eq, Functor)

756 deriving (Show, Eq, Functor)

746

757

758+data ArgOpt = Lazy | HideDisplay

759+ deriving (Show, Eq)

760+

761+lazyarg :: PArg' t -> Bool

762+lazyarg tm = Lazy `elem` argopts tm

763+

747instance Sized a => Sized (PArg' a) where

764instance Sized a => Sized (PArg' a) where

748 size (PImp p _ l nm trm _) = 1 + size nm + size trm

765 size (PImp p _ l nm trm _) = 1 + size nm + size trm

749 size (PExp p l trm _) = 1 + size trm

766 size (PExp p l trm _) = 1 + size trm

@@ -755,10 +772,10 @@ deriving instance Binary PArg'

755deriving instance NFData PArg'

772deriving instance NFData PArg'

756!-}

773!-}

757

774

758−pimp n t mach = PImp 1 mach True n t ""

775+pimp n t mach = PImp 1 mach [Lazy] n t ""

759−pexp t = PExp 1 False t ""

776+pexp t = PExp 1 [] t ""

760−pconst t = PConstraint 1 False t ""

777+pconst t = PConstraint 1 [] t ""

761−ptacimp n s t = PTacImplicit 2 True n s t ""

778+ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

762

779

763type PArg = PArg' PTerm

780type PArg = PArg' PTerm

764

781

@@ -801,6 +818,7 @@ deriving instance NFData OptInfo

801

818

802data TypeInfo = TI { con_names :: [Name],

819data TypeInfo = TI { con_names :: [Name],

803 codata :: Bool,

820 codata :: Bool,

821+ data_opts :: DataOpts,

804 param_pos :: [Int] }

822 param_pos :: [Int] }

805 deriving Show

823 deriving Show

806{-!

824{-!

@@ -1008,7 +1026,7 @@ prettyImp impl = prettySe 10

1008 prettySe 10 sc

1026 prettySe 10 sc

1009 prettySe p (PPi (Exp l s _ _) n ty sc)

1027 prettySe p (PPi (Exp l s _ _) n ty sc)

1010 | n `elem` allNamesIn sc || impl =

1028 | n `elem` allNamesIn sc || impl =

1011− let open = if l then text "|" <> lparen else lparen in

1029+ let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1012 bracket p 2 $

1030 bracket p 2 $

1013 if size sc > breakingSize then

1031 if size sc > breakingSize then

1014 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1032 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

@@ -1029,7 +1047,7 @@ prettyImp impl = prettySe 10

1029 _ -> empty

1047 _ -> empty

1030 prettySe p (PPi (Imp l s _ _) n ty sc)

1048 prettySe p (PPi (Imp l s _ _) n ty sc)

1031 | impl =

1049 | impl =

1032− let open = if l then text "|" <> lbrace else lbrace in

1050+ let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1033 bracket p 2 $

1051 bracket p 2 $

1034 if size sc > breakingSize then

1052 if size sc > breakingSize then

1035 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1053 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

@@ -1222,7 +1240,7 @@ showImp ist impl colour tm = se 10 [] tm where

1222 se p bnd (PPi (Exp l s _ param) n ty sc)

1240 se p bnd (PPi (Exp l s _ param) n ty sc)

1223 | n `elem` allNamesIn sc || impl

1241 | n `elem` allNamesIn sc || impl

1224 = bracket p 2 $

1242 = bracket p 2 $

1225− (if l then "|(" else "(") ++

1243+ (if Lazy `elem` l then "|(" else "(") ++

1226 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1244 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1227 ") " ++

1245 ") " ++

1228 (if (impl && param) then "P" else "") ++

1246 (if (impl && param) then "P" else "") ++

@@ -1233,7 +1251,7 @@ showImp ist impl colour tm = se 10 [] tm where

1233 Static -> "[static] "

1251 Static -> "[static] "

1234 _ -> ""

1252 _ -> ""

1235 se p bnd (PPi (Imp l s _ _) n ty sc)

1253 se p bnd (PPi (Imp l s _ _) n ty sc)

1236− | impl = bracket p 2 $ (if l then "|{" else "{") ++

1254+ | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++

1237 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1255 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1238 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1256 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1239 | otherwise = se 10 ((n, True):bnd) sc

1257 | otherwise = se 10 ((n, True):bnd) sc

@@ -1247,6 +1265,9 @@ showImp ist impl colour tm = se 10 [] tm where

1247 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1265 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1248 se 10 ((n, False):bnd) sc

1266 se 10 ((n, False):bnd) sc

1249 se p bnd (PMatchApp _ f) = "match " ++ show f

1267 se p bnd (PMatchApp _ f) = "match " ++ show f

1268+ se p bnd (PApp _ hd@(PRef fc f) [tm])

1269+ | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1270+ f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))

1250 se p bnd (PApp _ hd@(PRef _ f) [])

1271 se p bnd (PApp _ hd@(PRef _ f) [])

1251 | not impl = se p bnd hd

1272 | not impl = se p bnd hd

1252 se p bnd (PAppBind _ hd@(PRef _ f) [])

1273 se p bnd (PAppBind _ hd@(PRef _ f) [])

src/Idris/Core/TT.hs+24−20

@@ -91,41 +91,45 @@ data ErrorReportPart = TextPart String

91

92-- | Idris errors. Used as exceptions in the compiler, but reported to users

93-- if they reach the top level.

94+data Err' t

94−data Err = Msg String

95+ = Msg String

95 | InternalMsg String

96 | InternalMsg String

96− | CantUnify Bool Term Term Err [(Name, Type)] Int

97+ | CantUnify Bool t t (Err' t) [(Name, t)] Int

97 -- Int is 'score' - how much we did unify

98 -- Int is 'score' - how much we did unify

98 -- Bool indicates recoverability, True indicates more info may make

99 -- Bool indicates recoverability, True indicates more info may make

99 -- unification succeed

100 -- unification succeed

100− | InfiniteUnify Name Term [(Name, Type)]

101+ | InfiniteUnify Name t [(Name, t)]

101− | CantConvert Term Term [(Name, Type)]

102+ | CantConvert t t [(Name, t)]

102− | CantSolveGoal Term [(Name, Type)]

103+ | CantSolveGoal t [(Name, t)]

103− | UnifyScope Name Name Term [(Name, Type)]

104+ | UnifyScope Name Name t [(Name, t)]

104 | CantInferType String

105 | CantInferType String

105− | NonFunctionType Term Term

106+ | NonFunctionType t t

106− | NotEquality Term Term

107+ | NotEquality t t

107 | TooManyArguments Name

108 | TooManyArguments Name

108− | CantIntroduce Term

109+ | CantIntroduce t

109 | NoSuchVariable Name

110 | NoSuchVariable Name

110 | NoTypeDecl Name

111 | NoTypeDecl Name

111− | NotInjective Term Term Term

112+ | NotInjective t t t

112− | CantResolve Term

113+ | CantResolve t

113 | CantResolveAlts [String]

114 | CantResolveAlts [String]

114− | IncompleteTerm Term

115+ | IncompleteTerm t

115 | UniverseError

116 | UniverseError

116 | ProgramLineComment

117 | ProgramLineComment

117 | Inaccessible Name

118 | Inaccessible Name

118 | NonCollapsiblePostulate Name

119 | NonCollapsiblePostulate Name

119 | AlreadyDefined Name

120 | AlreadyDefined Name

120− | ProofSearchFail Err

121+ | ProofSearchFail (Err' t)

121− | NoRewriting Term

122+ | NoRewriting t

122− | At FC Err

123+ | At FC (Err' t)

123− | Elaborating String Name Err

124+ | Elaborating String Name (Err' t)

124 | ProviderError String

125 | ProviderError String

125− | LoadingFailed String Err

126+ | LoadingFailed String (Err' t)

126− | ReflectionError [[ErrorReportPart]] Err

127+ | ReflectionError [[ErrorReportPart]] (Err' t)

127− | ReflectionFailed String Err

128+ | ReflectionFailed String (Err' t)

128− deriving Eq

129+ deriving (Eq, Functor)

130+

131+type Err = Err' Term

132+

129{-!

133{-!

130deriving instance NFData Err

134deriving instance NFData Err

131!-}

135!-}

src/Idris/Coverage.hs+5−5

@@ -56,7 +56,7 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 False Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

@@ -183,7 +183,7 @@ genAll i args

183 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

184 let tyn = getTy n (tt_ctxt i)

185 case lookupCtxt tyn (idris_datatypes i) of

186− (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

186+ (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

187 _ -> [p]

188 ops fc n arg o = return Placeholder

189

@@ -289,7 +289,7 @@ calcProd i fc topn pats

289 cotype (DCon _ _) n ty

290 | (P _ t _, _) <- unApply (getRetTy ty)

291 = case lookupCtxt t (idris_datatypes i) of

292− [TI _ True _] -> True

292+ [TI _ True _ _] -> True

293 _ -> False

294 cotype nt n ty = False

295

@@ -466,7 +466,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

466

467 isInductive (P _ nty _) (P _ nty' _) =

468 let co = case lookupCtxt nty (idris_datatypes ist) of

469− [TI _ x _] -> x

469+ [TI _ x _ _] -> x

470 _ -> False in

471 nty == nty' && not co

472 isInductive _ _ = False

@@ -507,7 +507,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

507 [ty] = lookupTy n ctxt -- must exist!

508 P _ nty _ = fst (unApply (getRetTy ty))

509 co = case lookupCtxt nty (idris_datatypes ist) of

510− [TI _ x _] -> x

510+ [TI _ x _ _] -> x

511 _ -> False

512 args = map snd (getArgTys ty) in

513 map (getRel co nty) (map (fst . unApply . getRetTy) args)

src/Idris/DeepSeq.hs+4−1

@@ -53,6 +53,9 @@ instance NFData Static where

53 rnf Static = ()

54 rnf Dynamic = ()

55

56+instance NFData ArgOpt where

57+ rnf _ = ()

58+

56instance NFData Plicity where

59instance NFData Plicity where

57 rnf (Imp x1 x2 x3 x4)

60 rnf (Imp x1 x2 x3 x4)

58 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

61 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

@@ -240,7 +243,7 @@ instance NFData OptInfo where

240 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

243 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

241

244

242instance NFData TypeInfo where

245instance NFData TypeInfo where

243− rnf (TI x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

246+ rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

244

247

245instance (NFData t) => NFData (DSL' t) where

248instance (NFData t) => NFData (DSL' t) where

246 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

249 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

src/Idris/Delaborate.hs+40−37

@@ -8,6 +8,7 @@ module Idris.Delaborate where

8import Idris.AbsSyntax

9import Idris.Core.TT

10import Idris.Core.Evaluate

11+import Idris.ErrReverse

11

12

12import Data.List (intersperse)

13import Data.List (intersperse)

13

14

@@ -121,11 +122,13 @@ indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where

121 else [c]

122 else [c]

122

123

123pshow :: IState -> Err -> String

124pshow :: IState -> Err -> String

125+pshow i err = pshow' i (fmap (errReverse i) err)

126+

124−pshow i (Msg s) = s

127+pshow' i (Msg s) = s

125−pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

128+pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

126 "\nThis is probably a bug, or a missing error message.\n" ++

129 "\nThis is probably a bug, or a missing error message.\n" ++

127 "Please consider reporting at " ++ bugaddr

130 "Please consider reporting at " ++ bugaddr

128−pshow i (CantUnify _ x y e sc s)

131+pshow' i (CantUnify _ x y e sc s)

129 = let imps = opt_showimp (idris_options i) in

132 = let imps = opt_showimp (idris_options i) in

130 let colour = idris_colourRepl i in

133 let colour = idris_colourRepl i in

131 "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))

134 "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))

@@ -134,72 +137,72 @@ pshow i (CantUnify _ x y e sc s)

134 case e of

137 case e of

135 Msg "" -> ""

138 Msg "" -> ""

136 _ -> "\nSpecifically:" ++

139 _ -> "\nSpecifically:" ++

137− indented (pshow i e) ++

140+ indented (pshow' i e) ++

138 if (opt_errContext (idris_options i)) then showSc i sc else ""

141 if (opt_errContext (idris_options i)) then showSc i sc else ""

139−pshow i (CantConvert x y env)

142+pshow' i (CantConvert x y env)

140 = let imps = opt_showimp (idris_options i) in

143 = let imps = opt_showimp (idris_options i) in

141 let colour = idris_colourRepl i in

144 let colour = idris_colourRepl i in

142 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

145 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

143 ++ indented (showImp (Just i) imps colour (delab i y)) ++

146 ++ indented (showImp (Just i) imps colour (delab i y)) ++

144 if (opt_errContext (idris_options i)) then showSc i env else ""

147 if (opt_errContext (idris_options i)) then showSc i env else ""

145−pshow i (CantSolveGoal x env)

148+pshow' i (CantSolveGoal x env)

146 = let imps = opt_showimp (idris_options i) in

149 = let imps = opt_showimp (idris_options i) in

147 let colour = idris_colourRepl i in

150 let colour = idris_colourRepl i in

148 "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

151 "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

149 if (opt_errContext (idris_options i)) then showSc i env else ""

152 if (opt_errContext (idris_options i)) then showSc i env else ""

150−pshow i (UnifyScope n out tm env)

153+pshow' i (UnifyScope n out tm env)

151 = let imps = opt_showimp (idris_options i) in

154 = let imps = opt_showimp (idris_options i) in

152 let colour = idris_colourRepl i in

155 let colour = idris_colourRepl i in

153 "Can't unify" ++ indented (show n) ++ "with"

156 "Can't unify" ++ indented (show n) ++ "with"

154 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

157 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

155 indented (show out) ++ "is not in scope" ++

158 indented (show out) ++ "is not in scope" ++

156 if (opt_errContext (idris_options i)) then showSc i env else ""

159 if (opt_errContext (idris_options i)) then showSc i env else ""

157−pshow i (CantInferType t)

160+pshow' i (CantInferType t)

158 = "Can't infer type for " ++ t

161 = "Can't infer type for " ++ t

159−pshow i (NonFunctionType f ty)

162+pshow' i (NonFunctionType f ty)

160 = let imps = opt_showimp (idris_options i) in

163 = let imps = opt_showimp (idris_options i) in

161 let colour = idris_colourRepl i in

164 let colour = idris_colourRepl i in

162 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

165 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

163 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

166 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

164−pshow i (NotEquality tm ty)

167+pshow' i (NotEquality tm ty)

165 = let imps = opt_showimp (idris_options i) in

168 = let imps = opt_showimp (idris_options i) in

166 let colour = idris_colourRepl i in

169 let colour = idris_colourRepl i in

167 showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

170 showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

168 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

171 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

169−pshow i (TooManyArguments f)

172+pshow' i (TooManyArguments f)

170 = "Too many arguments for " ++ show f

173 = "Too many arguments for " ++ show f

171−pshow i (CantIntroduce ty)

174+pshow' i (CantIntroduce ty)

172 = let imps = opt_showimp (idris_options i) in

175 = let imps = opt_showimp (idris_options i) in

173 let colour = idris_colourRepl i in

176 let colour = idris_colourRepl i in

174 "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)

177 "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)

175−pshow i (InfiniteUnify x tm env)

178+pshow' i (InfiniteUnify x tm env)

176 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

179 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

177 " would lead to infinite value" ++

180 " would lead to infinite value" ++

178 if (opt_errContext (idris_options i)) then showSc i env else ""

181 if (opt_errContext (idris_options i)) then showSc i env else ""

179−pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

182+pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

180− " when unifying " ++ show (delab i x) ++ " and " ++

183+ " when unifying " ++ show (delab i x) ++ " and " ++

181− show (delab i y)

184+ show (delab i y)

182−pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

185+pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

183−pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

186+pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

184−pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

187+pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n

185−pshow i (NoSuchVariable n) = "No such variable " ++ show n

188+pshow' i (NoSuchVariable n) = "No such variable " ++ show n

186−pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

189+pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

187−pshow i UniverseError = "Universe inconsistency"

190+pshow' i UniverseError = "Universe inconsistency"

188−pshow i ProgramLineComment = "Program line next to comment"

191+pshow' i ProgramLineComment = "Program line next to comment"

189−pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

192+pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

190−pshow i (NonCollapsiblePostulate n)

193+pshow' i (NonCollapsiblePostulate n)

191 = "The return type of postulate " ++ show n ++ " is not collapsible"

194 = "The return type of postulate " ++ show n ++ " is not collapsible"

192−pshow i (AlreadyDefined n) = show n ++ " is already defined"

195+pshow' i (AlreadyDefined n) = show n ++ " is already defined"

193−pshow i (ProofSearchFail e) = pshow i e

196+pshow' i (ProofSearchFail e) = pshow' i e

194−pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

197+pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

195−pshow i (At f e) = show f ++ ":" ++ pshow i e

198+pshow' i (At f e) = show f ++ ":" ++ pshow' i e

196−pshow i (Elaborating s n e) = "When elaborating " ++ s ++

199+pshow' i (Elaborating s n e) = "When elaborating " ++ s ++

197− showqual i n ++ ":\n" ++ pshow i e

200+ showqual i n ++ ":\n" ++ pshow' i e

198−pshow i (ProviderError msg) = "Type provider error: " ++ msg

201+pshow' i (ProviderError msg) = "Type provider error: " ++ msg

199−pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e

202+pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e

200−pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

203+pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

201 concat (intersperse "\n" parts') ++

204 concat (intersperse "\n" parts') ++

202− "\nOriginal error:\n" ++ indented (pshow i orig)

205+ "\nOriginal error:\n" ++ indented (pshow' i orig)

203 where showPart :: ErrorReportPart -> String

206 where showPart :: ErrorReportPart -> String

204 showPart (TextPart str) = str

207 showPart (TextPart str) = str

205 showPart (NamePart n) = let colour = idris_colourRepl i in

208 showPart (NamePart n) = let colour = idris_colourRepl i in

@@ -207,8 +210,8 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "

207 showPart (TermPart tm) = let colour = idris_colourRepl i

210 showPart (TermPart tm) = let colour = idris_colourRepl i

208 in showImp (Just i) False colour (delab i tm)

211 in showImp (Just i) False colour (delab i tm)

209 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

212 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

210−pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

213+pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

211− indented (pshow i err) ++

214+ indented (pshow' i err) ++

212 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

215 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

213

216

214

217

src/Idris/ElabDecls.hs+22−6

@@ -100,7 +100,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

100 let (t, _) = unApply (getRetTy nty')

101 let corec = case t of

102 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

103− [TI _ True _] -> True

103+ [TI _ True _ _] -> True

104 _ -> False

105 _ -> False

106 let opts' = if corec then (Coinductive : opts) else opts

@@ -229,7 +229,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

229 let as = map (const Nothing) (getArgTys cty)

230 let params = findParams (map snd cons)

231 logLvl 2 $ "Parameters : " ++ show params

232+ putIState (i { idris_datatypes =

232− putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

233+ addDef n (TI (map fst cons) codata opts params)

233 (idris_datatypes i) })

234 (idris_datatypes i) })

234 addIBC (IBCDef n)

235 addIBC (IBCDef n)

235 addIBC (IBCData n)

236 addIBC (IBCData n)

@@ -843,7 +844,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

843 else return ()

844 else return ()

844 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

845 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

845

846

846− mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

847+ mkLazy (PPi pl n ty sc)

848+ = PPi (pl { pargopts = nub (Lazy : pargopts pl) }) n ty (mkLazy sc)

847 mkLazy t = t

849 mkLazy t = t

848

850

849 getNamePos :: Int -> PTerm -> Name -> Maybe Int

851 getNamePos :: Int -> PTerm -> Name -> Maybe Int

@@ -1357,6 +1359,20 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1357 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

1359 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

1358 i <- getIState

1360 i <- getIState

1359 checkInferred fc (delab' i crhs True True) rhs

1361 checkInferred fc (delab' i crhs True True) rhs

1362+ -- if the function is declared '%error_reverse', or its type,

1363+ -- then we'll try running it in reverse to improve error messages

1364+ let (ret_fam, _) = unApply (getRetTy crhsty)

1365+ rev <- case ret_fam of

1366+ P _ rfamn _ ->

1367+ case lookupCtxt rfamn (idris_datatypes i) of

1368+ [TI _ _ dopts _] ->

1369+ return (DataErrRev `elem` dopts)

1370+ _ -> return False

1371+ _ -> return False

1372+

1373+ when (rev || ErrorReverse `elem` opts) $ do

1374+ addIBC (IBCErrRev (crhs, clhs))

1375+ addErrRev (crhs, clhs)

1360 return $ Right (clhs, crhs)

1376 return $ Right (clhs, crhs)

1361 where

1377 where

1362 decorate (NS x ns)

1378 decorate (NS x ns)

@@ -1909,11 +1925,11 @@ elabInstance info syn what fc cs n ps t expn ds = do

1909 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

1925 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

1910 lamBind i _ sc = sc

1926 lamBind i _ sc = sc

1911 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1927 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1912− = PImp 0 True False n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1928+ = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1913 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1929 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1914− = PExp 0 False (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1930+ = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1915 methArgs i (PPi (Constraint _ _ _) n ty sc)

1931 methArgs i (PPi (Constraint _ _ _) n ty sc)

1916− = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

1932+ = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

1917 methArgs i _ = []

1933 methArgs i _ = []

1918

1934

1919 papp fc f [] = f

1935 papp fc f [] = f

src/Idris/ElabTerm.hs−6

@@ -231,12 +231,6 @@ elab ist info pattern opts fn tm

231 ctxt <- get_context

232 let (tc, _) = unApply ty

233 let as' = pruneByType tc ctxt as

234−-- case as' of

235−-- [a] -> elab' ina a

236−-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

237−-- trace ("Original " ++ show (length as, as) ++ "\n" ++

238−-- "New " ++ show (length as', as)) $

239−-- traceWhen (length as' > 1) (show as') $

240 tryAll (zip (map (elab' ina) as') (map showHd as'))

234 tryAll (zip (map (elab' ina) as') (map showHd as'))

241 where showHd (PApp _ h _) = show h

235 where showHd (PApp _ h _) = show h

242 showHd x = show x

236 showHd x = show x

src/Idris/ErrReverse.hsnew file+72

@@ -0,0 +1,72 @@

1+{-# LANGUAGE PatternGuards #-}

2+

3+module Idris.ErrReverse where

4+

5+import Idris.AbsSyntax

6+import Idris.Core.TT

7+import Util.Pretty

8+

9+import Data.List

10+import Debug.Trace

11+

12+-- For display purposes, apply any 'error reversal' transformations so that

13+-- errors will be more readable

14+

15+errReverse :: IState -> Term -> Term

16+errReverse ist t = rewrite 5 (elideLambdas t)

17+ where

18+

19+ rewrite 0 t = t

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

21+ if t == t' then t

22+ else rewrite (n - 1) t'

23+

24+ applyRule :: Term -> (Term, Term) -> Term

25+ applyRule t (l, r) = applyNames [] t l r

26+

27+ -- Assume pattern bindings match in l and r (if they don't just treat

28+ -- the rule as invalid and return t)

29+

30+ applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)

31+ | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)

32+ (instantiate (P Ref n' ty') scr)

33+ | otherwise = t

34+ applyNames ns t l r = matchTerm ns l r t

35+

36+ matchTerm ns l r t

37+ | Just nmap <- match ns l t = substNames nmap r

38+ matchTerm ns l r (App f a) = let f' = matchTerm ns l r f

39+ a' = matchTerm ns l r a in

40+ App f' a'

41+ matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

42+ sc' = matchTerm ns l r sc in

43+ Bind n b' sc'

44+ matchTerm ns l r t = t

45+

46+ match ns l t = do ms <- match' ns l t

47+ combine (nub ms)

48+

49+ -- If any duplicate mappings, it's a failure

50+ combine [] = Just []

51+ combine ((x, t) : xs)

52+ | Just _ <- lookup x xs = Nothing

53+ | otherwise = do xs' <- combine xs

54+ Just ((x, t) : xs')

55+

56+ match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]

57+ match' ns (App f a) (App f' a') = do fs <- match' ns f f'

58+ as <- match' ns a a'

59+ Just (fs ++ as)

60+ -- no matching Binds, for now...

61+ match' ns x y = if x == y then Just [] else Nothing

62+

63+ -- if the term under a lambda is huge, there's no much point in showing

64+ -- it as it won't be very enlightening.

65+

66+ elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

67+ elideLambdas (Bind n (Lam t) sc)

68+ | size sc > 100 = P Ref (sUN "...") Erased

69+ elideLambdas (Bind n b sc)

70+ = Bind n (fmap elideLambdas b) (elideLambdas sc)

71+ elideLambdas t = t

72+

src/Idris/IBC.hs+37−8

@@ -26,7 +26,8 @@ import Util.Zlib (decompressEither)

26

27

28ibcVersion :: Word8

29−ibcVersion = 55

29+ibcVersion = 56

30+

30

31

31data IBCFile = IBCFile { ver :: Word8,

32data IBCFile = IBCFile { ver :: Word8,

32 sourcefile :: FilePath,

33 sourcefile :: FilePath,

@@ -54,6 +55,7 @@ data IBCFile = IBCFile { ver :: Word8,

54 ibc_defs :: [(Name, Def)],

55 ibc_defs :: [(Name, Def)],

55 ibc_docstrings :: [(Name, String)],

56 ibc_docstrings :: [(Name, String)],

56 ibc_transforms :: [(Term, Term)],

57 ibc_transforms :: [(Term, Term)],

58+ ibc_errRev :: [(Term, Term)],

57 ibc_coercions :: [Name],

59 ibc_coercions :: [Name],

58 ibc_lineapps :: [(FilePath, Int, PTerm)],

60 ibc_lineapps :: [(FilePath, Int, PTerm)],

59 ibc_namehints :: [(Name, Name)],

61 ibc_namehints :: [(Name, Name)],

@@ -67,7 +69,8 @@ deriving instance Binary IBCFile

67!-}

69!-}

68

70

69initIBC :: IBCFile

71initIBC :: IBCFile

70−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

72+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

73+

71

74

72loadIBC :: FilePath -> Idris ()

75loadIBC :: FilePath -> Idris ()

73loadIBC fp = do iLOG $ "Loading ibc " ++ fp

76loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -210,6 +213,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

210ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

213ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

211ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

214ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

212ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

215ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

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

213ibc i (IBCLineApp fp l t) f

217ibc i (IBCLineApp fp l t) f

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

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

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

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

@@ -252,6 +256,7 @@ process i fn

252 pDocs (ibc_docstrings i)

256 pDocs (ibc_docstrings i)

253 pCoercions (ibc_coercions i)

257 pCoercions (ibc_coercions i)

254 pTrans (ibc_transforms i)

258 pTrans (ibc_transforms i)

259+ pErrRev (ibc_errRev i)

255 pLineApps (ibc_lineapps i)

260 pLineApps (ibc_lineapps i)

256 pNameHints (ibc_namehints i)

261 pNameHints (ibc_namehints i)

257 pMetaInformation (ibc_metainformation i)

262 pMetaInformation (ibc_metainformation i)

@@ -423,6 +428,9 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns

423pTrans :: [(Term, Term)] -> Idris ()

428pTrans :: [(Term, Term)] -> Idris ()

424pTrans ts = mapM_ addTrans ts

429pTrans ts = mapM_ addTrans ts

425

430

431+pErrRev :: [(Term, Term)] -> Idris ()

432+pErrRev ts = mapM_ addErrRev ts

433+

426pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

434pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

427pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

435pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

428

436

@@ -1027,7 +1035,7 @@ instance Binary MetaInformation where

1027 return (DataMI x1)

1035 return (DataMI x1)

1028

1036

1029instance Binary IBCFile where

1037instance Binary IBCFile where

1030− 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 x32)

1038+ 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 x32 x33)

1031 = {-# SCC "putIBCFile" #-}

1039 = {-# SCC "putIBCFile" #-}

1032 do put x1

1040 do put x1

1033 put x2

1041 put x2

@@ -1061,6 +1069,8 @@ instance Binary IBCFile where

1061 put x30

1069 put x30

1062 put x31

1070 put x31

1063 put x32

1071 put x32

1072+ put x33

1073+

1064 get

1074 get

1065 = do x1 <- get

1075 = do x1 <- get

1066 if x1 == ibcVersion then

1076 if x1 == ibcVersion then

@@ -1095,17 +1105,20 @@ instance Binary IBCFile where

1095 x30 <- get

1105 x30 <- get

1096 x31 <- get

1106 x31 <- get

1097 x32 <- get

1107 x32 <- get

1108+ x33 <- get

1098− 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 x32)

1109+ 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 x32 x33)

1099 else return (initIBC { ver = x1 })

1110 else return (initIBC { ver = x1 })

1100

1111

1101instance Binary DataOpt where

1112instance Binary DataOpt where

1102 put x = case x of

1113 put x = case x of

1103 Codata -> putWord8 0

1114 Codata -> putWord8 0

1104 DefaultEliminator -> putWord8 1

1115 DefaultEliminator -> putWord8 1

1116+ DataErrRev -> putWord8 2

1105 get = do i <- getWord8

1117 get = do i <- getWord8

1106 case i of

1118 case i of

1107 0 -> return Codata

1119 0 -> return Codata

1108 1 -> return DefaultEliminator

1120 1 -> return DefaultEliminator

1121+ 2 -> return DataErrRev

1109

1122

1110instance Binary FnOpt where

1123instance Binary FnOpt where

1111 put x

1124 put x

@@ -1121,6 +1134,7 @@ instance Binary FnOpt where

1121 Implicit -> putWord8 7

1134 Implicit -> putWord8 7

1122 Reflection -> putWord8 8

1135 Reflection -> putWord8 8

1123 ErrorHandler -> putWord8 9

1136 ErrorHandler -> putWord8 9

1137+ ErrorReverse -> putWord8 10

1124 get

1138 get

1125 = do i <- getWord8

1139 = do i <- getWord8

1126 case i of

1140 case i of

@@ -1135,6 +1149,7 @@ instance Binary FnOpt where

1135 7 -> return Implicit

1149 7 -> return Implicit

1136 8 -> return Reflection

1150 8 -> return Reflection

1137 9 -> return ErrorHandler

1151 9 -> return ErrorHandler

1152+ 10 -> return ErrorReverse

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

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

1139

1154

1140instance Binary Fixity where

1155instance Binary Fixity where

@@ -1172,6 +1187,18 @@ instance Binary FixDecl where

1172 return (Fix x1 x2)

1187 return (Fix x1 x2)

1173

1188

1174

1189

1190+instance Binary ArgOpt where

1191+ put x

1192+ = case x of

1193+ Lazy -> putWord8 0

1194+ HideDisplay -> putWord8 1

1195+ get

1196+ = do i <- getWord8

1197+ case i of

1198+ 0 -> return Lazy

1199+ 1 -> return HideDisplay

1200+ _ -> error "Corrupted binary data for Static"

1201+

1175instance Binary Static where

1202instance Binary Static where

1176 put x

1203 put x

1177 = case x of

1204 = case x of

@@ -1939,13 +1966,15 @@ instance Binary OptInfo where

1939 return (Optimise x1 x2 x3 x4)

1966 return (Optimise x1 x2 x3 x4)

1940

1967

1941instance Binary TypeInfo where

1968instance Binary TypeInfo where

1942− put (TI x1 x2 x3) = do put x1

1969+ put (TI x1 x2 x3 x4) = do put x1

1943− put x2

1970+ put x2

1944− put x3

1971+ put x3

1972+ put x4

1945 get = do x1 <- get

1973 get = do x1 <- get

1946 x2 <- get

1974 x2 <- get

1947 x3 <- get

1975 x3 <- get

1976+ x4 <- get

1948− return (TI x1 x2 x3)

1977+ return (TI x1 x2 x3 x4)

1949

1978

1950instance Binary SynContext where

1979instance Binary SynContext where

1951 put x

1980 put x

src/Idris/ParseData.hs+10−4

@@ -77,8 +77,12 @@ dataI = do reserved "data"; return []

77{- | Parses if a data should not have a default eliminator

78DefaultEliminator ::= 'noelim'?

79 -}

80−defaultEliminator :: IdrisParser DataOpts

80+dataOpts :: DataOpts -> IdrisParser DataOpts

81−defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])

81+dataOpts opts

82+ = do reserved "%elim"; dataOpts (DefaultEliminator : opts)

83+ <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

84+ <|> return opts

85+ <?> "data options"

82

86

83{- | Parses a data type declaration

87{- | Parses a data type declaration

84Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

88Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

@@ -100,7 +104,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

100 doc <- option "" (docComment '|')

104 doc <- option "" (docComment '|')

101 pushIndent

105 pushIndent

102 acc <- optional accessibility

106 acc <- optional accessibility

103− elim <- defaultEliminator

107+ elim <- dataOpts []

104 co <- dataI

108 co <- dataI

105 let dataOpts = combineDataOpts(elim ++ co)

109 let dataOpts = combineDataOpts(elim ++ co)

106 return (doc, acc, dataOpts))

110 return (doc, acc, dataOpts))

@@ -146,7 +150,9 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

146 bindArgs :: [PTerm] -> PTerm -> PTerm

150 bindArgs :: [PTerm] -> PTerm -> PTerm

147 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

151 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

148 combineDataOpts :: DataOpts -> DataOpts

152 combineDataOpts :: DataOpts -> DataOpts

149− combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

153+ combineDataOpts opts = if Codata `elem` opts

154+ then delete DefaultEliminator opts

155+ else opts

150

156

151

157

152{- | Parses a type constructor declaration

158{- | Parses a type constructor declaration

src/Idris/ParseExpr.hs+9−9

@@ -769,39 +769,39 @@ Pi ::=

769

770pi :: SyntaxInfo -> IdrisParser PTerm

771pi syn =

772− do lazy <- if implicitAllowed syn -- laziness is top level only

772+ do opts <- if implicitAllowed syn -- laziness is top level only

773− then option False (do lchar '|'; return True)

773+ then option [] (do lchar '|'; return [Lazy])

774− else return False

774+ else return []

775 st <- static

776 (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

777 doc <- option "" (docComment '^')

778 symbol "->"

779 sc <- expr syn

780− return (bindList (PPi (Exp lazy st doc False)) xt sc)) <|> (do

780+ return (bindList (PPi (Exp opts st doc False)) xt sc)) <|> (do

781 lchar '{'

782 (do reserved "auto"

783− when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

783+ when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

784 xt <- typeDeclList syn

785 lchar '}'

786 symbol "->"

787 sc <- expr syn

788 return (bindList (PPi

789− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))

789+ (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

790 <|> (do

791 reserved "default"

792− when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

792+ when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

793 script <- simpleExpr syn

794 xt <- typeDeclList syn

795 lchar '}'

796 symbol "->"

797 sc <- expr syn

798− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

798+ return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

799 <|> (if implicitAllowed syn then do

800 xt <- typeDeclList syn

801 lchar '}'

802 symbol "->"

803 sc <- expr syn

804− return (bindList (PPi (Imp lazy st "" False)) xt sc)

804+ return (bindList (PPi (Imp opts st "" False)) xt sc)

805 else do fail "no implicit arguments allowed here"))

806 <?> "dependent type signature"

807

src/Idris/Parser.hs+2

@@ -338,6 +338,8 @@ fnOpts opts

338 fnOpts (AssertTotal : opts)

339 <|> do try (lchar '%' *> reserved "error_handler");

340 fnOpts (ErrorHandler : opts)

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

342+ fnOpts (ErrorReverse : opts)

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

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

342 fnOpts (Reflection : opts)

344 fnOpts (Reflection : opts)

343 <|> do lchar '%'; reserved "specialise";

345 <|> do lchar '%'; reserved "specialise";

src/Idris/Providers.hs+1−1

@@ -11,7 +11,7 @@ import Debug.Trace

11

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 False tm ""]

14+providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm ""]

15

16ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]

test/test038/expected+29

@@ -0,0 +1,29 @@

1+True

2+False

3+True

4+False

5+True

6+False

7+True

8+False

9+True

10+False

11+False

12+True

13+False

14+True

15+True

16+False

17+True

18+False

19+True

20+False

21+False

22+True

23+False

24+False

25+False

26+True

27+False

28+True

29+False

test/test038/run+4−2

@@ -1,3 +1,5 @@

1#!/usr/bin/env bash

2−idris $@ FunErrTest.idr --nocolour --check

2+idris $@ -o test038 test038.idr --nocolour

3+./test038

3−rm -f *.ibc

4+rm -f test038 *.ibc

5+

test/test038/test038.idrnew file+62

@@ -0,0 +1,62 @@

1+module Main

2+

3+test : DecEq a => a -> a -> Bool

4+test i1 i2 with (decEq i1 i2)

5+ test i1 i1 | Yes refl = True

6+ test i1 i2 | No p = False

7+

8+main : IO ()

9+main = do

10+-- Primitives

11+ putStrLn . show $ test (the Int 3) (the Int 3)

12+ putStrLn . show $ test (the Integer 3) (the Integer 4)

13+ putStrLn . show $ test "hello" "hello"

14+ putStrLn . show $ test "hello" "world"

15+ putStrLn . show $ test (the Char '\0') (the Char '\0')

16+ putStrLn . show $ test (the Char '\1') (the Char '\2')

17+-- Non-primitives

18+ -- Vect

19+ putStrLn . show $

20+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])

21+ putStrLn . show $

22+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])

23+ -- List

24+ putStrLn . show $

25+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])

26+ putStrLn . show $

27+ test (the (List Int) [1,2,3]) (the (List Int) [1,2])

28+ putStrLn . show $

29+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])

30+ -- Tuple

31+ putStrLn . show $

32+ test (the (Int, Int) (1, 1)) (the (Int, Int) (1, 1))

33+ putStrLn . show $

34+ test (the (Int, Int) (1, 2)) (the (Int, Int) (1, 1))

35+ -- Unit

36+ putStrLn . show $ test () ()

37+ -- Booleans

38+ putStrLn . show $ test True True

39+ putStrLn . show $ test True False

40+ -- Float

41+ putStrLn . show $ test 1.0 1.0

42+ putStrLn . show $ test 1.0 2.0

43+ -- Maybe

44+ putStrLn . show $ test (Just "hello") (Just "hello")

45+ putStrLn . show $ test (Just "hello") (Just "world")

46+ putStrLn . show $ test (Just "hello") Nothing

47+ -- Either

48+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))

49+ (the (Either String Bool) (Left "hello"))

50+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))

51+ (the (Either String Bool) (Left "world"))

52+ putStrLn . show $ test (Left "hello") (Right "world")

53+ putStrLn . show $ test (Left "hello") (Right False)

54+ -- Fin

55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

56+ (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

58+ (the (Fin (S (S (S (Z))))) (fS (fZ)))

59+ -- Nat

60+ putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))

61+ putStrLn . show $ test (S (S (S Z))) (S (S Z))

62+

test/test038/FunErrTest.idr → test/test039/FunErrTest.idrrenamed

The content is the same.

test/test039/expectednew file

No changes to the content.

test/test039/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ FunErrTest.idr --nocolour --check

3+rm -f *.ibc