73b666b · Idris-dev · git.iko.soy

CHANGELOG+3

@@ -40,6 +40,8 @@ New in 0.9.18:

4040 type classes. See the updated tutorial for details.

4141* Records can be coinductive. Define coinductive records with the "corecord"

4242 keyword.

43+* Type class constructors can be assigned user-accessible names. This is done

44+ using the same syntax as record constructors.

4345* if ... then ... else ... is now built-in syntax instead of being defined in

4446 a library. It is shown in REPL output and error messages, rather than its

4547 desugaring.

@@ -47,6 +49,7 @@ New in 0.9.18:

4749 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and

4850 to reflect that if-notation makes sense with non-Bool datatypes.

4951

52+

5053New in 0.9.17:

5154--------------

5255* The --ideslave command line option has been replaced with a --ide-mode

idris.cabal+5

@@ -357,6 +357,11 @@ Extra-source-files:

357357 test/bignum002/*.idr

358358 test/bignum002/expected

359359

360+ test/classes001/*.idr

361+ test/classes001/run

362+ test/classes001/expected

363+ test/classes001/input

364+

360365 test/corecords001/*.idr

361366 test/corecords001/run

362367 test/corecords001/expected

libs/prelude/Builtins.idr+1−1

@@ -63,7 +63,7 @@ infix 5 ~=~

6363||| @ x the left side

6464||| @ y the right side

6565(~=~) : (x : a) -> (y : b) -> Type

66−(~=~) x y = (=) _ _ x y

66+(~=~) x y = (x = y)

6767

6868||| Perform substitution in a term according to some equality.

6969|||

src/Idris/AbsSyntax.hs+8−3

@@ -1101,7 +1101,7 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

11011101-- (map (expandParamsD ist dec ps ns) pds)

11021102expandParamsD rhs ist dec ps ns (PMutual f pds)

11031103 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1104−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

1104+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls cn cd)

11051105 = PClass doc info f

11061106 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

11071107 n

@@ -1109,6 +1109,8 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

11091109 pDocs

11101110 fds

11111111 (map (expandParamsD rhs ist dec ps ns) decls)

1112+ cn

1113+ cd

11121114expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

11131115 = PInstance doc argDocs info f

11141116 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

@@ -1770,9 +1772,12 @@ stripLinear i tm = evalState (sl tm) [] where

17701772 t' <- sl t

17711773 r' <- sl r

17721774 return (PDPair fc p l' t' r')

1773− sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1775+ sl (PApp fc fn args) = do fn' <- case fn of

1776+ -- Just the args, fn isn't matchable as a var

1777+ PRef _ _ -> return fn

1778+ t -> sl t

17741779 args' <- mapM slA args

1775− return $ PApp fc fn args'

1780+ return $ PApp fc fn' args'

17761781 where slA (PImp p m l n t) = do t' <- sl t

17771782 return $ PImp p m l n t'

17781783 slA (PExp p l n t) = do t' <- sl t

src/Idris/AbsSyntaxTree.hs+13−11

@@ -612,13 +612,15 @@ data PDecl' t

612612 -- ^ Record declaration

613613 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

614614 [(Name, t)] -- constraints

615− Name

615+ Name -- class name

616616 [(Name, t)] -- parameters

617617 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

618618 [Name] -- determining parameters

619619 [PDecl' t] -- declarations

620+ (Maybe Name) -- instance constructor name

621+ (Docstring (Either Err PTerm)) -- instance constructor docs

620622 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

621− -- class name, parameters, method declarations

623+ -- class name, parameters, method declarations, optional constructor name

622624 | PInstance

623625 (Docstring (Either Err PTerm)) -- Instance docs

624626 [(Name, Docstring (Either Err PTerm))] -- Parameter docs

@@ -739,7 +741,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

739741declared (PParams _ _ ds) = concatMap declared ds

740742declared (PNamespace _ ds) = concatMap declared ds

741743declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

742−declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms

744+declared (PClass _ _ _ _ n _ _ _ ms cn cd) = n : (maybeToList cn ++ concatMap declared ms)

743745declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

744746declared (PDSL n _) = [n]

745747declared (PSyntax _ _) = []

@@ -759,7 +761,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

759761tldeclared (PParams _ _ ds) = []

760762tldeclared (PMutual _ ds) = concatMap tldeclared ds

761763tldeclared (PNamespace _ ds) = concatMap tldeclared ds

762−tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms

764+tldeclared (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap tldeclared ms)

763765tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

764766tldeclared _ = []

765767

@@ -775,7 +777,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

775777defined (PParams _ _ ds) = concatMap defined ds

776778defined (PNamespace _ ds) = concatMap defined ds

777779defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

778−defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms

780+defined (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap defined ms)

779781defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

780782defined (PDSL n _) = [n]

781783defined (PSyntax _ _) = []

@@ -1076,7 +1078,7 @@ highestFC (PQuoteName _) = Nothing

10761078

10771079-- Type class data

10781080

1079−data ClassInfo = CI { instanceName :: Name,

1081+data ClassInfo = CI { instanceCtorName :: Name,

10801082 class_methods :: [(Name, (FnOpts, PTerm))],

10811083 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

10821084 class_default_superclasses :: [PDecl],

@@ -1286,7 +1288,7 @@ getInferType (App _ (App _ _ ty) _) = ty

12861288

12871289-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

12881290

1289−primNames = [eqTy, eqCon, inferTy, inferCon]

1291+primNames = [inferTy, inferCon]

12901292

12911293unitTy = sUN "Unit"

12921294unitCon = sUN "MkUnit"

@@ -1350,7 +1352,7 @@ modDocName = sMN 0 "ModuleDocs"

13501352

13511353-- Defined in builtins.idr

13521354sigmaTy = sNS (sUN "Sigma") ["Builtins"]

1353−existsCon = sNS (sUN "MkSigma") ["Builtins"]

1355+sigmaCon = sNS (sUN "MkSigma") ["Builtins"]

13541356

13551357piBind :: [(Name, PTerm)] -> PTerm -> PTerm

13561358piBind = piBindp expl

@@ -1601,10 +1603,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

16011603 annotated rparen

16021604 where annotated = case pun of

16031605 IsType -> annName sigmaTy

1604− IsTerm -> annName existsCon

1606+ IsTerm -> annName sigmaCon

16051607 TypeOrTerm -> id

16061608 (left, addBinding) = case (l, pun) of

1607− (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))

1609+ (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe startPrec bnd t, ((n, False) :))

16081610 _ -> (prettySe startPrec bnd l, id )

16091611 prettySe p bnd (PAlternative a as) =

16101612 lparen <> text "|" <> prettyAs <> text "|" <> rparen

@@ -1788,7 +1790,7 @@ showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

17881790showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

17891791showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

17901792showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1791−showDeclImp o (PClass _ _ _ cs n ps _ _ ds)

1793+showDeclImp o (PClass _ _ _ cs n ps _ _ ds _ _)

17921794 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

17931795showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

17941796 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

src/Idris/Apropos.hs+1−1

@@ -55,7 +55,7 @@ instance Apropos Name where

5555 | (n == pairTy || n == pairCon) && str == T.pack "," = True

5656 | n == eqTy && str == T.pack "=" = True

5757 | n == eqCon && (T.toLower str) == T.pack "Refl" = True

58− | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True

58+ | (n == sigmaTy || n == sigmaCon) && str == T.pack "**" = True

5959 isApropos _ _ = False -- we don't care about case blocks, MNs, etc

6060

6161instance Apropos Def where

src/Idris/Coverage.hs+1−1

@@ -143,7 +143,7 @@ recoverableCoverage :: Context -> Err -> Bool

143143recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

144144 = let topx' = normalise ctxt [] topx

145145 topy' = normalise ctxt [] topy in

146− checkRec topx' topy'

146+ r || checkRec topx' topy'

147147 where -- different notion of recoverable than in unification, since we

148148 -- have no metavars -- just looking to see if a constructor is failing

149149 -- to unify with a function that may be reduced later

src/Idris/DeepSeq.hs+8−2

@@ -152,10 +152,16 @@ instance (NFData t) => NFData (PDecl' t) where

152152 rnf x2 `seq`

153153 rnf x3 `seq`

154154 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

155− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)

155+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11)

156156 = rnf x1 `seq`

157157 rnf x2 `seq`

158− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

158+ rnf x3 `seq`

159+ rnf x4 `seq`

160+ rnf x5 `seq`

161+ rnf x6 `seq`

162+ rnf x7 `seq`

163+ rnf x8 `seq`

164+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

159165 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

160166 = rnf x1 `seq`

161167 rnf x2 `seq`

src/Idris/Delaborate.hs+4−4

@@ -108,17 +108,17 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

108108 deFn env (P _ n _) [l,r]

109109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

110110 | n == eqCon = PRefl un (de env [] r)

111− | n == sUN "lazy" = de env [] r

111+ | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

112112 deFn env (P _ n _) [ty, Bind x (Lam _) r]

113− | n == sUN "Sigma"

113+ | n == sigmaTy

114114 = PDPair un IsType (PRef un x) (de env [] ty)

115115 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

116116 deFn env (P _ n _) [lt,rt,l,r]

117117 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

118118 | n == eqTy = PEq un (de env [] lt) (de env [] rt)

119119 (de env [] l) (de env [] r)

120− | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

121− (de env [] r)

120+ | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder

121+ (de env [] r)

122122 deFn env f@(P _ n _) args

123123 | n `elem` map snd env

124124 = PApp un (de env [] f) (map pexp (map (de env []) args))

src/Idris/Docs.hs+13−1

@@ -40,6 +40,7 @@ data Docs' d = FunDoc (FunDoc' d)

4040 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs

4141 [PTerm] -- subclasses

4242 [PTerm] -- superclasses

43+ (Maybe (FunDoc' d)) -- explicit constructor

4344 | NamedInstanceDoc Name (FunDoc' d) -- name is class

4445 | ModDoc [String] -- Module name

4546 d

@@ -95,7 +96,7 @@ pprintDocs ist (DataDoc t args)

9596 if null args then text "No constructors."

9697 else nest 4 (text "Constructors:" <> line <>

9798 vsep (map (pprintFD ist) args))

98−pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

99+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)

99100 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

100101 if nullDocstring doc

101102 then empty

@@ -106,6 +107,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

106107 nest 4 (text "Methods:" <$>

107108 vsep (map (pprintFD ist) meths))

108109 <$>

110+ maybe empty

111+ ((<> line) . nest 4 .

112+ (text "Instance constructor:" <$>) .

113+ pprintFD ist)

114+ ctor

115+ <>

109116 nest 4 (text "Instances:" <$>

110117 vsep (if null instances then [text "<no instances>"]

111118 else map pprintInstance normalInstances))

@@ -251,9 +258,14 @@ docClass n ci

251258 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances

252259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

253260 mdocs <- mapM (docFun . fst) (class_methods ci)

261+ let ctorN = instanceCtorName ci

262+ ctorDocs <- case basename ctorN of

263+ SN _ -> return Nothing

264+ _ -> fmap Just $ docFun ctorN

254265 return $ ClassDoc

255266 n docstr mdocs params

256267 instances' (map (\(_,tm,_) -> tm) subclasses) superclasses

268+ ctorDocs

257269 where

258270 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

259271 namedInst n@(UN _) = Just n

src/Idris/Elab/Class.hs+19−5

@@ -54,10 +54,13 @@ data MArgTy = IA Name | EA Name | CA deriving Show

5454

5555elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

5656 FC -> [(Name, PTerm)] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58− [Name] -> [PDecl] -> Idris ()

59−elabClass info syn_in doc fc constraints tn ps pDocs fds ds

60− = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58+ [Name] -> [PDecl] ->

59+ Maybe Name {- ^ instance ctor name -} ->

60+ Docstring (Either Err PTerm) {- ^ instance ctor docs -} ->

61+ Idris ()

62+elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

63+ = do let cn = fromMaybe (SN (InstanceCtorN tn)) mcn

6164 let tty = pibind ps (PType fc)

6265 let constraint = PApp fc (PRef fc tn)

6366 (map (pexp . PRef fc) (map fst ps))

@@ -80,8 +83,10 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

8083 let cty = impbind ps $ conbind constraints

8184 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8285 constraint

83− let cons = [(emptyDocstring, [], cn, NoFC, cty, fc, [])]

86+

87+ let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

8488 let ddecl = PDatadecl tn NoFC tty cons

89+

8590 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

8691 -- Elaborate the data declaration

8792 elabData info (syn { no_imp = no_imp syn ++ mnames,

@@ -243,6 +248,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

243248 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

244249 toExp ns e sc = sc

245250

251+memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

252+memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

253+memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

254+memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)

255+memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ ) = Just (basename n, d)

256+memberDocs (PClass d _ _ _ n _ _ _ _ _ _) = Just (basename n, d)

257+memberDocs _ = Nothing

258+

259+

246260-- In a top level type for a method, expand all the method names namespaces

247261-- so that we don't have to disambiguate later

248262expandMethNS :: SyntaxInfo

src/Idris/Elab/Instance.hs+1−1

@@ -130,7 +130,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

130130-- let lhs = PRef fc iname

131131 let lhs = PApp fc (PRef fc iname)

132132 (map (\n -> pimp n (PRef fc n) True) headVars)

133− let rhs = PApp fc (PRef fc (instanceName ci))

133+ let rhs = PApp fc (PRef fc (instanceCtorName ci))

134134 (map (pexp . mkMethApp) mtys)

135135

136136 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

src/Idris/Elab/Term.hs+15−18

@@ -80,7 +80,7 @@ build ist info emode opts fn tm

8080 mapM_ (\n -> when (n `elem` hs) $

8181 do focus n

8282 g <- goal

83− try (resolveTC True False 7 g fn ist)

83+ try (resolveTC True False 10 g fn ist)

8484 (movelast n)) ivs

8585 ivs <- get_instances

8686 hs <- get_holes

@@ -89,7 +89,7 @@ build ist info emode opts fn tm

8989 do focus n

9090 g <- goal

9191 ptm <- get_term

92− resolveTC True True 7 g fn ist) ivs

92+ resolveTC True True 10 g fn ist) ivs

9393 tm <- get_term

9494 ctxt <- get_context

9595 probs <- get_probs

@@ -347,7 +347,7 @@ elab ist info emode opts fn tm

347347 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

348348 _ -> elab' ina (Just fc) (PRef fc unitCon)

349349 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

350− = do g <- goal; resolveTC False False 5 g fn ist

350+ = do g <- goal; resolveTC False False 10 g fn ist

351351 elab' ina fc (PResolveTC fc')

352352 = do c <- getNameFrom (sMN 0 "class")

353353 instanceArg c

@@ -418,15 +418,16 @@ elab ist info emode opts fn tm

418418 _ -> asType

419419 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)

420420 [pexp t,

421+

421422 -- TODO: save the FC from the dependent pair

422423 -- syntax and put it on this lambda for interactive

423424 -- semantic highlighting support. NoFC for now.

424425 pexp (PLam fc n NoFC Placeholder r)])

425− asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

426+ asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

426427 [pimp (sMN 0 "a") t False,

427428 pimp (sMN 0 "P") Placeholder True,

428429 pexp l, pexp r])

429− elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

430+ elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

430431 [pimp (sMN 0 "a") t False,

431432 pimp (sMN 0 "P") Placeholder True,

432433 pexp l, pexp r])

@@ -591,7 +592,7 @@ elab ist info emode opts fn tm

591592 g <- goal

592593 hs <- get_holes

593594 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

594− then try (resolveTC True False 7 g fn ist)

595+ then try (resolveTC True False 10 g fn ist)

595596 (movelast n)

596597 else movelast n)

597598 (ivs' \\ ivs)

@@ -757,7 +758,7 @@ elab ist info emode opts fn tm

757758 env <- get_env

758759 hs <- get_holes

759760 if all (\n -> not (n `elem` hs)) (freeNames g)

760− then try (resolveTC False False 7 g fn ist)

761+ then try (resolveTC False False 10 g fn ist)

761762 (movelast n)

762763 else movelast n)

763764 (ivs' \\ ivs)

@@ -1494,14 +1495,11 @@ resTC' tcs defaultOn topholes depth topg fn ist

14941495 try' (trivial' ist)

14951496 (do t <- goal

14961497 let (tc, ttypes) = unApply (getRetTy t)

1497− scopeOnly <- needsDefault t tc ttypes

1498+ addDefault t tc ttypes

14981499 let stk = elab_stack ist

1499− let insts_in = findInstances ist t

1500− let insts = if scopeOnly then filter chaser insts_in

1501− else insts_in

1500+ let insts = findInstances ist t

15021501 tm <- get_term

1503− let depth' = if scopeOnly then 2 else depth

1504− blunderbuss t depth' stk (stk ++ insts)) True

1502+ blunderbuss t depth stk (stk ++ insts)) True

15051503 where

15061504 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

15071505 = True

@@ -1541,14 +1539,13 @@ resTC' tcs defaultOn topholes depth topg fn ist

15411539

15421540 numclass = sNS (sUN "Num") ["Classes","Prelude"]

15431541

1544− needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

1542+ addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

15451543 = do focus a

15461544 fill (RConstant (AType (ATInt ITBig))) -- default Integer

15471545 solve

1548− return False

1549− needsDefault t f as

1550− | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

1551− needsDefault t f a = return False -- trace (show t) $ return ()

1546+ addDefault t f as

1547+ | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t

1548+ addDefault t f a = return () -- trace (show t) $ return ()

15521549

15531550 boundVar (P Bound _ _) = True

15541551 boundVar _ = False

src/Idris/Elab/Type.hs+2−1

@@ -80,7 +80,8 @@ buildType info syn fc opts n ty' = do

8080 ds <- checkAddDef True False fc iderr defer

8181 -- if the type is not complete, note that we'll need to infer

8282 -- things later (for solving metavariables)

83− when (not (null ds)) $ addTyInferred n

83+ when (length ds > length is) -- more deferred than case blocks

84+ $ addTyInferred n

8485

8586 mapM_ (elabCaseBlock info opts) is

8687 ctxt <- getContext

src/Idris/ElabDecls.hs+2−2

@@ -232,10 +232,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

232232 ninfo = case namespace info of

233233 Nothing -> info { namespace = Just [n] }

234234 Just ns -> info { namespace = Just (n:ns) }

235−elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

235+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds cn cd)

236236 | what /= EDefns

237237 = do iLOG $ "Elaborating class " ++ show n

238− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

238+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds cn cd

239239elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

240240 = do iLOG $ "Elaborating instance " ++ show n

241241 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/IBC.hs+6−2

@@ -1187,7 +1187,7 @@ instance (Binary t) => Binary (PDecl' t) where

11871187 put x9

11881188 put x10

11891189 put x11

1190− PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

1190+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11

11911191 -> do putWord8 7

11921192 put x1

11931193 put x2

@@ -1198,6 +1198,8 @@ instance (Binary t) => Binary (PDecl' t) where

11981198 put x7

11991199 put x8

12001200 put x9

1201+ put x10

1202+ put x11

12011203 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

12021204 do putWord8 8

12031205 put x1

@@ -1301,7 +1303,9 @@ instance (Binary t) => Binary (PDecl' t) where

13011303 x7 <- get

13021304 x8 <- get

13031305 x9 <- get

1304− return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

1306+ x10 <- get

1307+ x11 <- get

1308+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

13051309 8 -> do x1 <- get

13061310 x2 <- get

13071311 x3 <- get

src/Idris/IdrisDoc.hs+13−13

@@ -166,11 +166,11 @@ removeOrphans :: [NsItem] -- ^ List to remove orphans from

166166 -> [NsItem] -- ^ Orphan-free list

167167removeOrphans list =

168168 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

169− in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169+ in filter ((flip S.notMember children) . (\(n, _, _) -> n)) list

170170

171− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

172− names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

173− names _ = []

171+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

172+ names (Just (ClassDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

173+ names _ = []

174174

175175-- | Whether a Name names something which should be documented

176176filterName :: Name -- ^ Name to check

@@ -218,13 +218,13 @@ referredNss (n, Just d, _) =

218218 names = concatMap (extractPTermNames) ts

219219 in S.map getNs $ S.fromList names

220220

221− where getFunDocs (FunDoc f) = [f]

222− getFunDocs (DataDoc f fs) = f:fs

223− getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

224− getFunDocs (NamedInstanceDoc _ fd) = [fd]

225− getFunDocs (ModDoc _ _) = []

226− types (FD _ _ args t _) = t:(map second args)

227− second (_, x, _, _) = x

221+ where getFunDocs (FunDoc f) = [f]

222+ getFunDocs (DataDoc f fs) = f:fs

223+ getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

224+ getFunDocs (NamedInstanceDoc _ fd) = [fd]

225+ getFunDocs (ModDoc _ _) = []

226+ types (FD _ _ args t _) = t:(map second args)

227+ second (_, x, _, _) = x

228228

229229

230230-- | Returns an NsDict of containing all known namespaces and their contents

@@ -579,7 +579,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

579579 -> H.Html -- ^ Resulting HTML

580580createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

581581

582−createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

582+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do

583583 H.dt ! (A.id $ toValue $ show n) $ do

584584 H.span ! class_ "word" $ do "class"; nbsp

585585 H.span ! class_ "name type"

@@ -588,7 +588,7 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

588588 H.span ! class_ "signature" $ nbsp

589589 H.dd $ do

590590 (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)

591− H.dl ! class_ "decls" $ forM_ fds (createFunDoc ist)

591+ H.dl ! class_ "decls" $ (forM_ (maybeToList c ++ fds) (createFunDoc ist))

592592

593593 where name (NS n ns) = show (NS (sUN $ name n) ns)

594594 name n = let n' = show n

src/Idris/ParseData.hs+1−1

@@ -109,6 +109,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

109109 constructor :: IdrisParser Name

110110 constructor = (reserved "constructor") *> (fst <$> fnName)

111111

112+

112113 endPlicity :: Maybe Char -> IdrisParser Plicity

113114 endPlicity (Just _) = do lchar '}'

114115 return impl

@@ -126,7 +127,6 @@ recordParameter syn =

126127 <|>

127128 (do (n, nfc, pt) <- onlyName syn

128129 return (n, nfc, expl, pt))

129−

130130 where

131131 namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)

132132 namedTy syn =

src/Idris/ParseHelpers.hs+2−2

@@ -633,8 +633,8 @@ collect (c@(PClauses _ o _ _) : ds)

633633collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

634634collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

635635collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

636−collect (PClass doc f s cs n ps pdocs fds ds : ds')

637− = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

636+collect (PClass doc f s cs n ps pdocs fds ds cn cd : ds')

637+ = PClass doc f s cs n ps pdocs fds (collect ds) cn cd : collect ds'

638638collect (PInstance doc argDocs f s cs n ps t en ds : ds')

639639 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

640640collect (d : ds) = d : collect ds

src/Idris/Parser.hs+19−5

@@ -626,18 +626,32 @@ MethodOrInstance ::=

626626

627627@

628628ClassBlock ::=

629− 'where' OpenBlock MethodOrInstance* CloseBlock

629+ 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

630630 ;

631631@

632632-}

633−classBlock :: SyntaxInfo -> IdrisParser [PDecl]

633+classBlock :: SyntaxInfo -> IdrisParser (Maybe Name, Docstring (Either Err PTerm), [PDecl])

634634classBlock syn = do reserved "where"

635635 openBlock

636+ (cn, cd) <- option (Nothing, emptyDocstring) $

637+ try (do (doc, _) <- option noDocs docComment

638+ n <- constructor

639+ return (Just n, doc))

640+ ist <- get

641+ let cd' = annotate syn ist cd

642+

636643 ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

637644 closeBlock

638− return (concat ds)

645+ return (cn, cd', concat ds)

639646 <?> "class block"

640647

648+ where

649+ constructor :: IdrisParser Name

650+ constructor = reserved "constructor" *> (fst <$> fnName)

651+

652+ annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

653+ annotate syn ist = annotCode $ tryFullExpr syn ist

654+

641655{-| Parses a type class declaration

642656

643657@

@@ -666,9 +680,9 @@ class_ syn = do (doc, argDocs, acc)

666680 let n = expandNS syn n_in

667681 cs <- many carg

668682 fds <- option (map fst cs) fundeps

669− ds <- option [] (classBlock syn)

683+ (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)

670684 accData acc n (concatMap declared ds)

671− return [PClass doc syn fc cons' n cs argDocs fds ds]

685+ return [PClass doc syn fc cons' n cs argDocs fds ds cn cd]

672686 <?> "type-class declaration"

673687 where

674688 fundeps :: IdrisParser [Name]

src/Idris/REPL.hs+1−1

@@ -791,7 +791,7 @@ process fn (NewDefn decls) = do

791791 getName (PTy docs argdocs syn fc opts name _ ty) = Just name

792792 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

793793 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

794− getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

794+ getName (PClass doc syn fc constraints name parms parmdocs fds decls _ _) = Just name

795795 getName _ = Nothing

796796 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

797797 getClauseName (PClause fc name whole with rhs whereBlock) = name

test/basic001/reg005.dSYM/Contents/Info.plistdeleted−20

@@ -1,20 +0,0 @@

1−<?xml version="1.0" encoding="UTF-8"?>

2−<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">

3−<plist version="1.0">

4− <dict>

5− <key>CFBundleDevelopmentRegion</key>

6− <string>English</string>

7− <key>CFBundleIdentifier</key>

8− <string>com.apple.xcode.dsym.reg005</string>

9− <key>CFBundleInfoDictionaryVersion</key>

10− <string>6.0</string>

11− <key>CFBundlePackageType</key>

12− <string>dSYM</string>

13− <key>CFBundleSignature</key>

14− <string>????</string>

15− <key>CFBundleShortVersionString</key>

16− <string>1.0</string>

17− <key>CFBundleVersion</key>

18− <string>1</string>

19− </dict>

20−</plist>

test/basic001/reg005.dSYM/Contents/Resources/DWARF/reg005deleted

Binary file not shown.

test/classes001/ClassName.idrnew file+49

@@ -0,0 +1,49 @@

1+module ClassName

2+

3+||| A fancy shower with a constructor

4+||| @ a the thing to be shown

5+class MyShow a where

6+ ||| Build a MyShow

7+ constructor MkMyShow

8+ ||| The shower

9+ ||| @ x will become a string

10+ myShow : (x : a) -> String

11+

12+twiceAString : MyShow a => a -> String

13+twiceAString x = myShow x ++ myShow x

14+

15+instance MyShow Integer where

16+ myShow x = show x

17+

18+badShow : MyShow Integer

19+badShow = MkMyShow (const "hej")

20+

21+test1 : twiceAString 2 = "22"

22+test1 = Refl

23+

24+test2 : twiceAString @{badShow} 2 = "hejhej"

25+test2 = Refl

26+

27+

28+||| Superclass fun

29+class MyMagma a where

30+ constructor MkMyMagma

31+ total op : a -> a -> a

32+

33+||| Semigroup

34+class MyMagma a => MySemigroup a where

35+ constructor MkMySemigroup

36+ total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z

37+

38+instance [addition] MyMagma Nat where

39+ op = plus

40+

41+additionS : MySemigroup Nat

42+additionS = MkMySemigroup @{addition} plusAssociative

43+

44+doIt : MySemigroup a => a -> List a -> a

45+doIt x [] = x

46+doIt x (y :: xs) = doIt (x `op` y) xs

47+

48+test : Nat

49+test = doIt @{additionS} 22 [1,2,3,4]

test/classes001/expectednew file+27

@@ -0,0 +1,27 @@

1+Type class MyShow

2+ A fancy shower with a constructor

3+

4+Parameters:

5+ a -- the thing to be shown

6+

7+Methods:

8+ myShow : MyShow a => (x : a) -> String

9+ The shower

10+

11+Instance constructor:

12+ MkMyShow : (myShow : a -> String) -> MyShow a

13+ Build a MyShow

14+ Arguments:

15+ (implicit) a : Type -- the thing to be shown

16+

17+ myShow : a -> String -- The shower

18+

19+Instances:

20+ MyShow Integer

21+MkMyShow : (myShow : a -> String) -> MyShow a

22+ Build a MyShow

23+ Arguments:

24+ (implicit) a : Type -- the thing to be shown

25+

26+ myShow : a -> String -- The shower

27+

test/classes001/inputnew file+2

@@ -0,0 +1,2 @@

1+:doc MyShow

2+:doc MkMyShow

test/classes001/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input

3+rm -f bounded001 *.ibc

test/effects003/hangman.idr+3−3

@@ -77,9 +77,9 @@ data HangmanRules : Effect where

7777 sig HangmanRules Bool

7878 (Hangman (Running (S g) (S w)))

7979 (\inword =>

80− case inword of

81− True => Hangman (Running (S g) w)

82− False => Hangman (Running g (S w)))

80+ Hangman (case inword of

81+ True => (Running (S g) w)

82+ False => (Running g (S w))))

8383

8484-- The 'Won' operation requires that there are no missing letters

8585

test/quasiquote004/Quasiquote004.idr+1−1

@@ -5,7 +5,7 @@ import Language.Reflection

55%default total

66

77normPlus : List (TTName, Binder TT) -> TT -> Tactic

8−normPlus ctxt `((=) {Nat} {Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y

8+normPlus ctxt `((=) {A = Nat} {B = Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y

99normPlus ctxt `(S ~n) = normPlus ctxt n

1010normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))

1111 (normPlus ctxt m)

test/reg037/reg037.idr+3−3

@@ -1,9 +1,9 @@

11

22--- Parser regression for (=) as a function name (fnName)

33

4−class Foo (t : (A : Type) -> (B : Type) -> A -> B -> Type) where

5− foo : (A : Type) -> (B : Type) -> (x : A) -> (y : B) -> t A B x y -> t A B x y

4+class Foo (t : a -> b -> Type) where

5+ foo : (x : _) -> (y : _) -> t x y -> t x y

66

77instance Foo (=) where

8− foo A B x y prf = prf

8+ foo x y prf = prf

99

test/reg047/reg047.idr+1−1

@@ -6,7 +6,7 @@ data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

66data Nat = zero | succ Nat

77

88Id : (A : Type) -> A -> A -> Type

9−Id A = (=) {a0 = A} {b0 = A}

9+Id A = (=) {A = A} {B = A}

1010

1111IdRefl : (A : Type) -> (a : A) -> Id A a a

1212IdRefl A a = Refl {a}

test/totality006/totality006b.idr+2−2

@@ -7,8 +7,8 @@ import Data.So

77-- case but not on test006.idr, due to the extra computation.

88total

99blargh : (xs, ys : List a) -> So (length xs > length ys) -> GT (length xs) (length ys)

10−blargh [] [] Oh impossible

1110blargh [] (y :: xs) so = absurd so

1211blargh (y :: xs) [] Oh = LTESucc LTEZero

1312

14−-- Missing: blargh (y :: xs) (z :: ys) x = ?blargh_rhs_3

13+-- Missing: blargh (y :: xs) (z :: ys) p = ?blargh_rhs_3

14+-- blargh [] [] p = ?foo -- impossible

test/totality009/TestLambdaImpossible.idr−3

@@ -24,6 +24,3 @@ decElem x (y :: xs) with (decEq x y)

2424 decElem x (y :: xs) | (No notHere) | (Yes prf) = Yes (There prf)

2525 decElem x (y :: xs) | (No notHere) | (No notThere) = No $ notHereNotThere notHere notThere

2626

27−notEta : ((a : Type) -> (b : Type) -> (f : a -> b) -> f = (\x => f x)) -> Void

28−notEta eta = case eta Nat Nat id of

29− Refl impossible