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

CHANGELOG+3

compare with master

unifiedsplit

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

40 type classes. See the updated tutorial for details.

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

42 keyword.

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

44+ using the same syntax as record constructors.

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

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

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

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

45 desugaring.

47 desugaring.

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

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

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

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

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

49

51

52+

50New in 0.9.17:

53New in 0.9.17:

51--------------

54--------------

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

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

idris.cabal+5

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

357 test/bignum002/*.idr

358 test/bignum002/expected

359

360+ test/classes001/*.idr

361+ test/classes001/run

362+ test/classes001/expected

363+ test/classes001/input

364+

360 test/corecords001/*.idr

365 test/corecords001/*.idr

361 test/corecords001/run

366 test/corecords001/run

362 test/corecords001/expected

367 test/corecords001/expected

libs/prelude/Builtins.idr+1−1

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

63||| @ x the left side

64||| @ y the right side

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

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

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

67

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

69|||

src/Idris/AbsSyntax.hs+8−3

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

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

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

1103 = 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)

1105 = PClass doc info f

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

1107 n

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

1109 pDocs

1110 fds

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

1112+ cn

1113+ cd

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

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

1113 = PInstance doc argDocs info f

1115 = PInstance doc argDocs info f

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

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

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

1770 t' <- sl t

1772 t' <- sl t

1771 r' <- sl r

1773 r' <- sl r

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

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

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

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

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

1777+ PRef _ _ -> return fn

1778+ t -> sl t

1774 args' <- mapM slA args

1779 args' <- mapM slA args

1775− return $ PApp fc fn args'

1780+ return $ PApp fc fn' args'

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

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

1777 return $ PImp p m l n t'

1782 return $ PImp p m l n t'

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

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

src/Idris/AbsSyntaxTree.hs+13−11

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

612 -- ^ Record declaration

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

614 [(Name, t)] -- constraints

615− Name

615+ Name -- class name

616 [(Name, t)] -- parameters

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

618 [Name] -- determining parameters

619 [PDecl' t] -- declarations

620+ (Maybe Name) -- instance constructor name

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

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

622 -- ^ 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

622 | PInstance

624 | PInstance

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

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

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

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

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

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

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

740declared (PNamespace _ ds) = concatMap declared ds

742declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

744declared (PDSL n _) = [n]

746declared (PDSL n _) = [n]

745declared (PSyntax _ _) = []

747declared (PSyntax _ _) = []

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

759tldeclared (PParams _ _ ds) = []

761tldeclared (PParams _ _ ds) = []

760tldeclared (PMutual _ ds) = concatMap tldeclared ds

762tldeclared (PMutual _ ds) = concatMap tldeclared ds

761tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

764tldeclared _ = []

766tldeclared _ = []

765

767

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

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

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

776defined (PNamespace _ ds) = concatMap defined ds

778defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

780defined (PDSL n _) = [n]

782defined (PDSL n _) = [n]

781defined (PSyntax _ _) = []

783defined (PSyntax _ _) = []

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

1076

1078

1077-- Type class data

1079-- Type class data

1078

1080

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

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

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

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

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

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

1082 class_default_superclasses :: [PDecl],

1084 class_default_superclasses :: [PDecl],

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

1286

1288

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

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

1288

1290

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

1291+primNames = [inferTy, inferCon]

1290

1292

1291unitTy = sUN "Unit"

1293unitTy = sUN "Unit"

1292unitCon = sUN "MkUnit"

1294unitCon = sUN "MkUnit"

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

1350

1352

1351-- Defined in builtins.idr

1353-- Defined in builtins.idr

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

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

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

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

1354

1356

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

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

1356piBind = piBindp expl

1358piBind = piBindp expl

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

1601 annotated rparen

1603 annotated rparen

1602 where annotated = case pun of

1604 where annotated = case pun of

1603 IsType -> annName sigmaTy

1605 IsType -> annName sigmaTy

1604− IsTerm -> annName existsCon

1606+ IsTerm -> annName sigmaCon

1605 TypeOrTerm -> id

1607 TypeOrTerm -> id

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

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

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

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

1609 prettySe p bnd (PAlternative a as) =

1611 prettySe p bnd (PAlternative a as) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1796 = 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

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

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

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

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

60

61instance Apropos Def where

src/Idris/Coverage.hs+1−1

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

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

144 = let topx' = normalise ctxt [] topx

145 topy' = normalise ctxt [] topy in

146− checkRec topx' topy'

146+ r || checkRec topx' topy'

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

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

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

152 rnf x2 `seq`

153 rnf x3 `seq`

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

156 = rnf x1 `seq`

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

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

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

160 = rnf x1 `seq`

166 = rnf x1 `seq`

161 rnf x2 `seq`

167 rnf x2 `seq`

src/Idris/Delaborate.hs+4−4

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

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

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

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

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

113− | n == sUN "Sigma"

113+ | n == sigmaTy

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

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

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

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

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

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

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

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

121− (de env [] r)

121+ (de env [] r)

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

123 | n `elem` map snd env

124 = 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)

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

41 [PTerm] -- subclasses

42 [PTerm] -- superclasses

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

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

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

44 | ModDoc [String] -- Module name

45 | ModDoc [String] -- Module name

45 d

46 d

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

95 if null args then text "No constructors."

96 if null args then text "No constructors."

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

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

97 vsep (map (pprintFD ist) args))

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

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

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

100 if nullDocstring doc

101 if nullDocstring doc

101 then empty

102 then empty

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

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

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

107 vsep (map (pprintFD ist) meths))

108 vsep (map (pprintFD ist) meths))

108 <$>

109 <$>

110+ maybe empty

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

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

113+ pprintFD ist)

114+ ctor

115+ <>

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

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

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

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

111 else map pprintInstance normalInstances))

118 else map pprintInstance normalInstances))

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

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

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

252 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

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

260 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

254 return $ ClassDoc

265 return $ ClassDoc

255 n docstr mdocs params

266 n docstr mdocs params

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

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

268+ ctorDocs

257 where

269 where

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

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

259 namedInst n@(UN _) = Just n

271 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

54

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

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

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

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

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

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

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

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

61+ Idris ()

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

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

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

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

61 let tty = pibind ps (PType fc)

64 let tty = pibind ps (PType fc)

62 let constraint = PApp fc (PRef fc tn)

65 let constraint = PApp fc (PRef fc tn)

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

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

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

80 let cty = impbind ps $ conbind constraints

83 let cty = impbind ps $ conbind constraints

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

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

82 constraint

85 constraint

86+

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

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

84 let ddecl = PDatadecl tn NoFC tty cons

88 let ddecl = PDatadecl tn NoFC tty cons

89+

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

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

86 -- Elaborate the data declaration

91 -- Elaborate the data declaration

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

92 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

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

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

244 toExp ns e sc = sc

249 toExp ns e sc = sc

245

250

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+

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

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

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

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

248expandMethNS :: SyntaxInfo

262expandMethNS :: 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

130-- let lhs = PRef fc iname

131 let lhs = PApp fc (PRef fc iname)

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

134 (map (pexp . mkMethApp) mtys)

135

136 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

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

81 do focus n

82 g <- goal

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

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

84 (movelast n)) ivs

85 ivs <- get_instances

86 hs <- get_holes

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

89 do focus n

90 g <- goal

91 ptm <- get_term

92− resolveTC True True 7 g fn ist) ivs

92+ resolveTC True True 10 g fn ist) ivs

93 tm <- get_term

94 ctxt <- get_context

95 probs <- get_probs

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

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

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

349 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

351 elab' ina fc (PResolveTC fc')

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

353 instanceArg c

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

418 _ -> asType

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

420 [pexp t,

421+

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

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

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

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

423 -- semantic highlighting support. NoFC for now.

424 -- semantic highlighting support. NoFC for now.

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

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

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

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

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

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

428 pexp l, pexp r])

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

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

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

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

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

432 pexp l, pexp r])

433 pexp l, pexp r])

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

591 g <- goal

592 g <- goal

592 hs <- get_holes

593 hs <- get_holes

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

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

595 (movelast n)

596 (movelast n)

596 else movelast n)

597 else movelast n)

597 (ivs' \\ ivs)

598 (ivs' \\ ivs)

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

757 env <- get_env

758 env <- get_env

758 hs <- get_holes

759 hs <- get_holes

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

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

761 (movelast n)

762 (movelast n)

762 else movelast n)

763 else movelast n)

763 (ivs' \\ ivs)

764 (ivs' \\ ivs)

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

1494 try' (trivial' ist)

1495 try' (trivial' ist)

1495 (do t <- goal

1496 (do t <- goal

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

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

1497− scopeOnly <- needsDefault t tc ttypes

1498+ addDefault t tc ttypes

1498 let stk = elab_stack ist

1499 let stk = elab_stack ist

1499− let insts_in = findInstances ist t

1500+ let insts = findInstances ist t

1500− let insts = if scopeOnly then filter chaser insts_in

1501− else insts_in

1502 tm <- get_term

1501 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

1505 where

1503 where

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

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

1507 = True

1505 = True

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

1541

1539

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

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

1543

1541

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

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

1545 = do focus a

1543 = do focus a

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

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

1547 solve

1545 solve

1548− return False

1546+ addDefault t f as

1549− needsDefault t f as

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

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

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

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

1552

1549

1553 boundVar (P Bound _ _) = True

1550 boundVar (P Bound _ _) = True

1554 boundVar _ = False

1551 boundVar _ = False

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

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

80 ds <- checkAddDef True False fc iderr defer

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

82 -- things later (for solving metavariables)

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

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

84+ $ addTyInferred n

84

85

85 mapM_ (elabCaseBlock info opts) is

86 mapM_ (elabCaseBlock info opts) is

86 ctxt <- getContext

87 ctxt <- getContext

src/Idris/ElabDecls.hs+2−2

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

232 ninfo = case namespace info of

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

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

236 | what /= EDefns

237 = 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

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

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

241 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

1187 put x9

1188 put x10

1189 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

1191 -> do putWord8 7

1192 put x1

1193 put x2

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

1198 put x7

1199 put x8

1200 put x9

1201+ put x10

1202+ put x11

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

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

1202 do putWord8 8

1204 do putWord8 8

1203 put x1

1205 put x1

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

1301 x7 <- get

1303 x7 <- get

1302 x8 <- get

1304 x8 <- get

1303 x9 <- get

1305 x9 <- get

1306+ x10 <- get

1307+ x11 <- get

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

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

1305 8 -> do x1 <- get

1309 8 -> do x1 <- get

1306 x2 <- get

1310 x2 <- get

1307 x3 <- get

1311 x3 <- get

src/Idris/IdrisDoc.hs+13−13

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

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

167removeOrphans list =

168 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

170

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

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

172− names (Just (ClassDoc _ _ 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 _ = []

173+ names _ = []

174

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

176filterName :: Name -- ^ Name to check

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

218 names = concatMap (extractPTermNames) ts

219 in S.map getNs $ S.fromList names

220

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

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

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

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

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

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

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

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

225− getFunDocs (ModDoc _ _) = []

225+ getFunDocs (ModDoc _ _) = []

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

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

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

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

228

229

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

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

579 -> H.Html -- ^ Resulting HTML

580createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

581

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

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

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

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

585 H.span ! class_ "name type"

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

588 H.span ! class_ "signature" $ nbsp

589 H.dd $ do

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

592

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

594 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

109 constructor :: IdrisParser Name

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

111

112+

112 endPlicity :: Maybe Char -> IdrisParser Plicity

113 endPlicity :: Maybe Char -> IdrisParser Plicity

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

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

114 return impl

115 return impl

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

126 <|>

127 <|>

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

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

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

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

129−

130 where

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

132 namedTy syn =

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

636−collect (PClass doc f s cs n ps pdocs fds ds : 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) : collect ds'

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

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

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

640collect (d : ds) = d : collect ds

src/Idris/Parser.hs+19−5

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

626

627@

628ClassBlock ::=

629− 'where' OpenBlock MethodOrInstance* CloseBlock

629+ 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

630 ;

631@

632-}

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

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

634classBlock syn = do reserved "where"

635 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+

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

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

637 closeBlock

644 closeBlock

638− return (concat ds)

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

639 <?> "class block"

646 <?> "class block"

640

647

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+

641{-| Parses a type class declaration

655{-| Parses a type class declaration

642

656

643@

657@

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

666 let n = expandNS syn n_in

680 let n = expandNS syn n_in

667 cs <- many carg

681 cs <- many carg

668 fds <- option (map fst cs) fundeps

682 fds <- option (map fst cs) fundeps

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

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

670 accData acc n (concatMap declared ds)

684 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]

672 <?> "type-class declaration"

686 <?> "type-class declaration"

673 where

687 where

674 fundeps :: IdrisParser [Name]

688 fundeps :: IdrisParser [Name]

src/Idris/REPL.hs+1−1

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

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

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

793 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

795 getName _ = Nothing

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

797 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

77 sig HangmanRules Bool

78 (Hangman (Running (S g) (S w)))

79 (\inword =>

80− case inword of

80+ Hangman (case inword of

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

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

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

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

83

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

85

test/quasiquote004/Quasiquote004.idr+1−1

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

5%default total

6

7normPlus : 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

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

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

11 (normPlus ctxt m)

test/reg037/reg037.idr+3−3

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

1

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

3

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

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

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

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

6

7instance Foo (=) where

8− foo A B x y prf = prf

8+ foo x y prf = prf

9

test/reg047/reg047.idr+1−1

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

6data Nat = zero | succ Nat

7

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

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

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

10

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

12IdRefl A a = Refl {a}

test/totality006/totality006b.idr+2−2

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

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

8total

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

10−blargh [] [] Oh impossible

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

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

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

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

13

12

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)

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

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

26

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