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

CHANGELOG+4

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

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

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

99 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

1013

1114Internal changes

1215

1316* Faster elaboration

1417* Smaller .ibc files

1518

19+

1620New in 0.9.10:

1721--------------

1822

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

380380 , Idris.ElabDecls

381381 , Idris.ElabTerm

382382 , Idris.Error

383+ , Idris.ErrReverse

383384 , Idris.Help

384385 , Idris.IBC

385386 , Idris.IdeSlave

libs/effects/Effects.idr+1

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

1010Effect : Type

1111Effect = Type -> Type -> Type -> Type

1212

13+%error_reverse

1314data EFFECT : Type where

1415 MkEff : Type -> Effect -> EFFECT

1516

libs/neweffects/Effects.idr+1

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

1111Effect : Type

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

1313

14+%error_reverse

1415data EFFECT : Type where

1516 MkEff : Type -> Effect -> EFFECT

1617

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

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

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

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

155155 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

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

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

159159 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

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

216216 else No (really_believe_me _|_)

217217

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

9797addTrans t = do i <- getIState

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

9999

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

101+addErrRev t = do i <- getIState

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

103+

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

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

102106

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

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

10611065 doAdd (UConstraint c args : cs) ns t

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

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

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

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

10651069 | otherwise = doAdd cs ns t

10661070

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

10691073

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

10711075 = getcapp c ++ getConstraints sc

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

11951199 pibind using [] sc = sc

11961200 pibind using (n:ns) sc

11971201 = case lookup n using of

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

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

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

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

12001204 (pibind using ns sc)

12011205

12021206-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+43−22

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

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

112112 idris_coercions :: [Name],

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

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

114115 syntax_rules :: [Syntax],

115116 syntax_keywords :: [String],

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

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

187188 | IBCTotal Name Totality

188189 | IBCFlags Name [FnOpt]

189190 | IBCTrans (Term, Term)

191+ | IBCErrRev (Term, Term)

190192 | IBCCG Name

191193 | IBCDoc Name

192194 | IBCCoercion Name

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

203205 emptyContext emptyContext emptyContext emptyContext

204206 emptyContext emptyContext emptyContext emptyContext

205207 emptyContext

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

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

207209 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

209211

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

357359!-}

358360

359361-- Mark bindings with their explicitness, and laziness

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

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

361363 pstatic :: Static,

362364 pdocstr :: String,

363365 pparam :: Bool }

364− | Exp { plazy :: Bool,

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

365367 pstatic :: Static,

366368 pdocstr :: String,

367369 pparam :: Bool }

368− | Constraint { plazy :: Bool,

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

369371 pstatic :: Static,

370372 pdocstr :: String }

371− | TacImp { plazy :: Bool,

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

372374 pstatic :: Static,

373375 pscript :: PTerm,

374376 pdocstr :: String }

375377 deriving (Show, Eq)

376378

379+plazy :: Plicity -> Bool

380+plazy tm = Lazy `elem` pargopts tm

381+

377382{-!

378383deriving instance Binary Plicity

379384deriving instance NFData Plicity

380385!-}

381386

382−impl = Imp False Dynamic "" False

383−expl = Exp False Dynamic "" False

384−expl_param = Exp False Dynamic "" True

385−constraint = Constraint False Dynamic ""

386−tacimpl t = TacImp False Dynamic t ""

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

388+expl = Exp [] Dynamic "" False

389+expl_param = Exp [] Dynamic "" True

390+constraint = Constraint [] Dynamic ""

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

387392

388393data FnOpt = Inlinable -- always evaluate when simplifying

389394 | TotalFn | PartialFn

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

393398 | Implicit -- implicit coercion

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

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

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

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

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

398404 deriving (Show, Eq)

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

413419-- | Data declaration options

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

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

422+ | DataErrRev

416423 deriving (Show, Eq)

417424

418425type DataOpts = [DataOpt]

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

729736

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

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

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

739+ argopts :: [ArgOpt],

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

733741 pargdoc :: String }

734742 | PExp { priority :: Int,

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

743+ argopts :: [ArgOpt],

744+ getTm :: t,

736745 pargdoc :: String }

737746 | PConstraint { priority :: Int,

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

747+ argopts :: [ArgOpt],

748+ getTm :: t,

739749 pargdoc :: String }

740750 | PTacImplicit { priority :: Int,

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

751+ argopts :: [ArgOpt],

752+ pname :: Name,

742753 getScript :: t,

743754 getTm :: t,

744755 pargdoc :: String }

745756 deriving (Show, Eq, Functor)

746757

758+data ArgOpt = Lazy | HideDisplay

759+ deriving (Show, Eq)

760+

761+lazyarg :: PArg' t -> Bool

762+lazyarg tm = Lazy `elem` argopts tm

763+

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

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

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

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

755772deriving instance NFData PArg'

756773!-}

757774

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

759−pexp t = PExp 1 False t ""

760−pconst t = PConstraint 1 False t ""

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

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

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

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

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

762779

763780type PArg = PArg' PTerm

764781

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

801818

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

803820 codata :: Bool,

821+ data_opts :: DataOpts,

804822 param_pos :: [Int] }

805823 deriving Show

806824{-!

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

10081026 prettySe 10 sc

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

10101028 | 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

10121030 bracket p 2 $

10131031 if size sc > breakingSize then

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

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

10291047 _ -> empty

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

10311049 | 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

10331051 bracket p 2 $

10341052 if size sc > breakingSize then

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

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

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

12231241 | n `elem` allNamesIn sc || impl

12241242 = bracket p 2 $

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

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

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

12271245 ") " ++

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

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

12331251 Static -> "[static] "

12341252 _ -> ""

12351253 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 "{") ++

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

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

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

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

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

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

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

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

12511272 | not impl = se p bnd hd

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

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

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

9191

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

9393-- if they reach the top level.

94−data Err = Msg String

94+data Err' t

95+ = Msg String

9596 | InternalMsg String

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

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

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

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

99100 -- unification succeed

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

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

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

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

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

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

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

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

104105 | CantInferType String

105− | NonFunctionType Term Term

106− | NotEquality Term Term

106+ | NonFunctionType t t

107+ | NotEquality t t

107108 | TooManyArguments Name

108− | CantIntroduce Term

109+ | CantIntroduce t

109110 | NoSuchVariable Name

110111 | NoTypeDecl Name

111− | NotInjective Term Term Term

112− | CantResolve Term

112+ | NotInjective t t t

113+ | CantResolve t

113114 | CantResolveAlts [String]

114− | IncompleteTerm Term

115+ | IncompleteTerm t

115116 | UniverseError

116117 | ProgramLineComment

117118 | Inaccessible Name

118119 | NonCollapsiblePostulate Name

119120 | AlreadyDefined Name

120− | ProofSearchFail Err

121− | NoRewriting Term

122− | At FC Err

123− | Elaborating String Name Err

121+ | ProofSearchFail (Err' t)

122+ | NoRewriting t

123+ | At FC (Err' t)

124+ | Elaborating String Name (Err' t)

124125 | ProviderError String

125− | LoadingFailed String Err

126− | ReflectionError [[ErrorReportPart]] Err

127− | ReflectionFailed String Err

128− deriving Eq

126+ | LoadingFailed String (Err' t)

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

128+ | ReflectionFailed String (Err' t)

129+ deriving (Eq, Functor)

130+

131+type Err = Err' Term

132+

129133{-!

130134deriving instance NFData Err

131135!-}

src/Idris/Coverage.hs+5−5

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

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

5757 -- suggests)

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

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

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

6060 _ -> repeat (pexp Placeholder)

6161 let tryclauses = mkClauses parg all_args

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

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

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

184184 let tyn = getTy n (tt_ctxt i)

185185 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])

187187 _ -> [p]

188188 ops fc n arg o = return Placeholder

189189

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

289289 cotype (DCon _ _) n ty

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

291291 = case lookupCtxt t (idris_datatypes i) of

292− [TI _ True _] -> True

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

293293 _ -> False

294294 cotype nt n ty = False

295295

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

466466

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

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

469− [TI _ x _] -> x

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

470470 _ -> False in

471471 nty == nty' && not co

472472 isInductive _ _ = False

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

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

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

509509 co = case lookupCtxt nty (idris_datatypes ist) of

510− [TI _ x _] -> x

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

511511 _ -> False

512512 args = map snd (getArgTys ty) in

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

src/Idris/DeepSeq.hs+4−1

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

5353 rnf Static = ()

5454 rnf Dynamic = ()

5555

56+instance NFData ArgOpt where

57+ rnf _ = ()

58+

5659instance NFData Plicity where

5760 rnf (Imp x1 x2 x3 x4)

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

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

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

241244

242245instance 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` ()

244247

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

246249 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

88import Idris.AbsSyntax

99import Idris.Core.TT

1010import Idris.Core.Evaluate

11+import Idris.ErrReverse

1112

1213import Data.List (intersperse)

1314

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

121122 else [c]

122123

123124pshow :: IState -> Err -> String

124−pshow i (Msg s) = s

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

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

126+

127+pshow' i (Msg s) = s

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

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

127130 "Please consider reporting at " ++ bugaddr

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

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

129132 = let imps = opt_showimp (idris_options i) in

130133 let colour = idris_colourRepl i in

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

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

134137 case e of

135138 Msg "" -> ""

136139 _ -> "\nSpecifically:" ++

137− indented (pshow i e) ++

140+ indented (pshow' i e) ++

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

140143 = let imps = opt_showimp (idris_options i) in

141144 let colour = idris_colourRepl i in

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

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

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

145−pshow i (CantSolveGoal x env)

148+pshow' i (CantSolveGoal x env)

146149 = let imps = opt_showimp (idris_options i) in

147150 let colour = idris_colourRepl i in

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

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

151154 = let imps = opt_showimp (idris_options i) in

152155 let colour = idris_colourRepl i in

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

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

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

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

157−pshow i (CantInferType t)

160+pshow' i (CantInferType t)

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

159−pshow i (NonFunctionType f ty)

162+pshow' i (NonFunctionType f ty)

160163 = let imps = opt_showimp (idris_options i) in

161164 let colour = idris_colourRepl i in

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

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

164−pshow i (NotEquality tm ty)

167+pshow' i (NotEquality tm ty)

165168 = let imps = opt_showimp (idris_options i) in

166169 let colour = idris_colourRepl i in

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

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

169−pshow i (TooManyArguments f)

172+pshow' i (TooManyArguments f)

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

171−pshow i (CantIntroduce ty)

174+pshow' i (CantIntroduce ty)

172175 = let imps = opt_showimp (idris_options i) in

173176 let colour = idris_colourRepl i in

174177 "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)

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

177180 " would lead to infinite value" ++

178181 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) ++

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

181− show (delab i y)

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

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

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

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

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

187−pshow i UniverseError = "Universe inconsistency"

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

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

190−pshow i (NonCollapsiblePostulate n)

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

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

184+ show (delab i y)

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

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

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

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

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

190+pshow' i UniverseError = "Universe inconsistency"

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

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

193+pshow' i (NonCollapsiblePostulate n)

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

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

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

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

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

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

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

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

199−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

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

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

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

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

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

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

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

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

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

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

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

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

203206 where showPart :: ErrorReportPart -> String

204207 showPart (TextPart str) = str

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

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

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

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

209212 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" ++

211− indented (pshow i err) ++

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

214+ indented (pshow' i err) ++

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

213216

214217

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

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

101101 let corec = case t of

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

103− [TI _ True _] -> True

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

104104 _ -> False

105105 _ -> False

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

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

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

230230 let params = findParams (map snd cons)

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

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

232+ putIState (i { idris_datatypes =

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

233234 (idris_datatypes i) })

234235 addIBC (IBCDef n)

235236 addIBC (IBCData n)

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

843844 else return ()

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

845846

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)

847849 mkLazy t = t

848850

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

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

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

13581360 i <- getIState

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

13601376 return $ Right (clhs, crhs)

13611377 where

13621378 decorate (NS x ns)

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

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

19101926 lamBind i _ sc = sc

19111927 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

19131929 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

19151931 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

19171933 methArgs i _ = []

19181934

19191935 papp fc f [] = f

src/Idris/ElabTerm.hs−6

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

231231 ctxt <- get_context

232232 let (tc, _) = unApply ty

233233 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') $

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

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

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

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 55

29+ibcVersion = 56

30+

3031

3132data IBCFile = IBCFile { ver :: Word8,

3233 sourcefile :: FilePath,

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

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

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

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

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

5759 ibc_coercions :: [Name],

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

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

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

6769!-}

6870

6971initIBC :: IBCFile

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

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

73+

7174

7275loadIBC :: FilePath -> Idris ()

7376loadIBC 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 }

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

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

212215ibc 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 }

213217ibc i (IBCLineApp fp l t) f

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

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

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

252256 pDocs (ibc_docstrings i)

253257 pCoercions (ibc_coercions i)

254258 pTrans (ibc_transforms i)

259+ pErrRev (ibc_errRev i)

255260 pLineApps (ibc_lineapps i)

256261 pNameHints (ibc_namehints i)

257262 pMetaInformation (ibc_metainformation i)

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

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

424429pTrans ts = mapM_ addTrans ts

425430

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

432+pErrRev ts = mapM_ addErrRev ts

433+

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

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

428436

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

10271035 return (DataMI x1)

10281036

10291037instance 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)

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

10321040 do put x1

10331041 put x2

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

10611069 put x30

10621070 put x31

10631071 put x32

1072+ put x33

1073+

10641074 get

10651075 = do x1 <- get

10661076 if x1 == ibcVersion then

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

10951105 x30 <- get

10961106 x31 <- get

10971107 x32 <- 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)

1108+ x33 <- get

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)

10991110 else return (initIBC { ver = x1 })

11001111

11011112instance Binary DataOpt where

11021113 put x = case x of

11031114 Codata -> putWord8 0

11041115 DefaultEliminator -> putWord8 1

1116+ DataErrRev -> putWord8 2

11051117 get = do i <- getWord8

11061118 case i of

11071119 0 -> return Codata

11081120 1 -> return DefaultEliminator

1121+ 2 -> return DataErrRev

11091122

11101123instance Binary FnOpt where

11111124 put x

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

11211134 Implicit -> putWord8 7

11221135 Reflection -> putWord8 8

11231136 ErrorHandler -> putWord8 9

1137+ ErrorReverse -> putWord8 10

11241138 get

11251139 = do i <- getWord8

11261140 case i of

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

11351149 7 -> return Implicit

11361150 8 -> return Reflection

11371151 9 -> return ErrorHandler

1152+ 10 -> return ErrorReverse

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

11391154

11401155instance Binary Fixity where

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

11721187 return (Fix x1 x2)

11731188

11741189

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+

11751202instance Binary Static where

11761203 put x

11771204 = case x of

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

19391966 return (Optimise x1 x2 x3 x4)

19401967

19411968instance Binary TypeInfo where

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

1943− put x2

1944− put x3

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

1970+ put x2

1971+ put x3

1972+ put x4

19451973 get = do x1 <- get

19461974 x2 <- get

19471975 x3 <- get

1948− return (TI x1 x2 x3)

1976+ x4 <- get

1977+ return (TI x1 x2 x3 x4)

19491978

19501979instance Binary SynContext where

19511980 put x

src/Idris/ParseData.hs+10−4

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

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

7878DefaultEliminator ::= 'noelim'?

7979 -}

80−defaultEliminator :: IdrisParser DataOpts

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

80+dataOpts :: DataOpts -> IdrisParser DataOpts

81+dataOpts opts

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

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

84+ <|> return opts

85+ <?> "data options"

8286

8387{- | Parses a data type declaration

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

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

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

101105 pushIndent

102106 acc <- optional accessibility

103− elim <- defaultEliminator

107+ elim <- dataOpts []

104108 co <- dataI

105109 let dataOpts = combineDataOpts(elim ++ co)

106110 return (doc, acc, dataOpts))

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

146150 bindArgs :: [PTerm] -> PTerm -> PTerm

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

148152 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

150156

151157

152158{- | Parses a type constructor declaration

src/Idris/ParseExpr.hs+9−9

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

769769

770770pi :: SyntaxInfo -> IdrisParser PTerm

771771pi syn =

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

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

774− else return False

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

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

774+ else return []

775775 st <- static

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

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

778778 symbol "->"

779779 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

781781 lchar '{'

782782 (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"

784784 xt <- typeDeclList syn

785785 lchar '}'

786786 symbol "->"

787787 sc <- expr syn

788788 return (bindList (PPi

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

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

790790 <|> (do

791791 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"

793793 script <- simpleExpr syn

794794 xt <- typeDeclList syn

795795 lchar '}'

796796 symbol "->"

797797 sc <- expr syn

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

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

799799 <|> (if implicitAllowed syn then do

800800 xt <- typeDeclList syn

801801 lchar '}'

802802 symbol "->"

803803 sc <- expr syn

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

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

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

806806 <?> "dependent type signature"

807807

src/Idris/Parser.hs+2

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

338338 fnOpts (AssertTotal : opts)

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

340340 fnOpts (ErrorHandler : opts)

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

342+ fnOpts (ErrorReverse : opts)

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

342344 fnOpts (Reflection : opts)

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

src/Idris/Providers.hs+1−1

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

1111

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

1313providerTy :: 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 ""]

1515

1616ioret = sUN "prim_io_return"

1717ermod = 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 @@

11#!/usr/bin/env bash

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

3−rm -f *.ibc

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

3+./test038

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