2d205a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Instance docs: basic plumbing of types and parsing

2d205a6Adam Sandberg Eriksson12 years ago

src/Idris/AbsSyntax.hs+10−10

compare with master

unifiedsplit

@@ -96,7 +96,7 @@ addHdr :: Codegen -> String -> Idris ()

96addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

98addImported :: Bool -> FilePath -> Idris ()

99−addImported pub f

99+addImported pub f

100 = do i <- getIState

101 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

102

@@ -134,7 +134,7 @@ addExport n = do ist <- getIState

134 putIState $ ist { idris_exports = n : idris_exports ist }

135

136addUsedName :: FC -> Name -> Name -> Idris ()

137−addUsedName fc n arg

137+addUsedName fc n arg

138 = do ist <- getIState

139 case lookupTyName n (tt_ctxt ist) of

140 [(n', ty)] -> addUsage n' 0 ty

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

1082 (map (mapsnd (expandParams dec ps ns [])) params)

1083 pDocs

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

1085−expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

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

1086− = PInstance info f

1086+ = PInstance doc info f

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

1088 n

1089 (map (expandParams dec ps ns []) params)

@@ -1552,7 +1552,7 @@ addImpl' inpat env infns ist ptm

1552 PLam fc n ty' sc'

1553 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty

1554 (PCase fc (PRef fc (sMN 0 "lamp") )

1555− [(PRef fc n, sc)]))

1555+ [(PRef fc n, sc)]))

1556 ai qq env ds (PLet fc n ty val sc)

1557 = case lookupDef n (tt_ctxt ist) of

1558 [] -> let ty' = ai qq env ds ty

@@ -1726,7 +1726,7 @@ stripLinear i tm = evalState (sl tm) [] where

1726 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1727 sl (PDPair fc p l t r) = do l' <- sl l

1728 t' <- sl t

1729− r' <- sl r

1729+ r' <- sl r

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

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

1732 args' <- mapM slA args

@@ -1925,11 +1925,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1925 match (PHidden x) (PHidden y)

1926 | RightOK xs <- match x y = return xs -- to collect variables

1927 | otherwise = return [] -- Otherwise hidden things are unmatchable

1928− match (PHidden x) y

1928+ match (PHidden x) y

1929− | RightOK xs <- match x y = return xs

1929+ | RightOK xs <- match x y = return xs

1930 | otherwise = return []

1931− match x (PHidden y)

1931+ match x (PHidden y)

1932− | RightOK xs <- match x y = return xs

1932+ | RightOK xs <- match x y = return xs

1933 | otherwise = return []

1934 match (PUnifyLog x) y = match' x y

1935 match x (PUnifyLog y) = match' x y

src/Idris/AbsSyntaxTree.hs+28−25

@@ -57,7 +57,7 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

57 liftname :: Name -> Name,

58 namespace :: Maybe [String],

59 elabFC :: Maybe FC,

60− rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

60+ rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

61 Idris () }

63toplevel :: ElabInfo

@@ -601,14 +601,18 @@ data PDecl' t

601 [PDecl' t] -- declarations

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

603 -- class name, parameters, method declarations

604+ | PInstance

605+ (Docstring (Either Err PTerm))

606+ SyntaxInfo

604− | PInstance SyntaxInfo FC [(Name, t)] -- constraints

607+ FC [(Name, t)] -- constraints

605− Name -- class

608+ Name -- class

606− [t] -- parameters

609+ [t] -- parameters

607− t -- full instance type

610+ t -- full instance type

608− (Maybe Name) -- explicit name

611+ (Maybe Name) -- explicit name

609− [PDecl' t]

612+ [PDecl' t]

610− -- ^ Instance declaration: arguments are syntax info, source location, constraints,

613+ -- ^ Instance declaration: documentation, arguments are syntax info, source

614+ -- location, constraints, class name, parameters, full instance

611− -- class name, parameters, full instance type, optional explicit name, and definitions

615+ -- type, optional explicit name, and definitions

612 | PDSL Name (DSL' t) -- ^ DSL declaration

616 | PDSL Name (DSL' t) -- ^ DSL declaration

613 | PSyntax FC Syntax -- ^ Syntax definition

617 | PSyntax FC Syntax -- ^ Syntax definition

614 | PMutual FC [PDecl' t] -- ^ Mutual block

618 | PMutual FC [PDecl' t] -- ^ Mutual block

@@ -688,7 +692,7 @@ declared (PParams _ _ ds) = concatMap declared ds

688declared (PNamespace _ ds) = concatMap declared ds

692declared (PNamespace _ ds) = concatMap declared ds

689declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

693declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

690declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

694declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

691−declared (PInstance _ _ _ _ _ _ _ _) = []

695+declared (PInstance _ _ _ _ _ _ _ _ _) = []

692declared (PDSL n _) = [n]

696declared (PDSL n _) = [n]

693declared (PSyntax _ _) = []

697declared (PSyntax _ _) = []

694declared (PMutual _ ds) = concatMap declared ds

698declared (PMutual _ ds) = concatMap declared ds

@@ -707,7 +711,7 @@ tldeclared (PParams _ _ ds) = []

707tldeclared (PMutual _ ds) = concatMap tldeclared ds

711tldeclared (PMutual _ ds) = concatMap tldeclared ds

708tldeclared (PNamespace _ ds) = concatMap tldeclared ds

712tldeclared (PNamespace _ ds) = concatMap tldeclared ds

709tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

713tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

710−tldeclared (PInstance _ _ _ _ _ _ _ _) = []

714+tldeclared (PInstance _ _ _ _ _ _ _ _ _) = []

711tldeclared _ = []

715tldeclared _ = []

712

716

713defined :: PDecl -> [Name]

717defined :: PDecl -> [Name]

@@ -723,7 +727,7 @@ defined (PParams _ _ ds) = concatMap defined ds

723defined (PNamespace _ ds) = concatMap defined ds

727defined (PNamespace _ ds) = concatMap defined ds

724defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

728defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

725defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

729defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

726−defined (PInstance _ _ _ _ _ _ _ _) = []

730+defined (PInstance _ _ _ _ _ _ _ _ _) = []

727defined (PDSL n _) = [n]

731defined (PDSL n _) = [n]

728defined (PSyntax _ _) = []

732defined (PSyntax _ _) = []

729defined (PMutual _ ds) = concatMap defined ds

733defined (PMutual _ ds) = concatMap defined ds

@@ -778,7 +782,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

778 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

782 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

779 | PHidden PTerm -- ^ Irrelevant or hidden pattern

783 | PHidden PTerm -- ^ Irrelevant or hidden pattern

780 | PType -- ^ 'Type' type

784 | PType -- ^ 'Type' type

781− | PUniverse Universe -- ^ Some universe

785+ | PUniverse Universe -- ^ Some universe

782 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

786 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

783 | PConstant Const -- ^ Builtin types

787 | PConstant Const -- ^ Builtin types

784 | Placeholder -- ^ Underscore

788 | Placeholder -- ^ Underscore

@@ -1113,7 +1117,7 @@ data SSymbol = Keyword Name

1113 | Expr Name

1117 | Expr Name

1114 | SimpleExpr Name

1118 | SimpleExpr Name

1115 deriving (Show, Eq)

1119 deriving (Show, Eq)

1116−

1120+

1117

1121

1118{-!

1122{-!

1119deriving instance Binary SSymbol

1123deriving instance Binary SSymbol

@@ -1388,7 +1392,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1388 where

1392 where

1389 startPrec = 0

1393 startPrec = 0

1390 funcAppPrec = 10

1394 funcAppPrec = 10

1391−

1395+

1392 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1396 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1393 prettySe p bnd (PQuote r) =

1397 prettySe p bnd (PQuote r) =

1394 text "![" <> pretty r <> text "]"

1398 text "![" <> pretty r <> text "]"

@@ -1451,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1451 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1455 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1452 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1456 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1453 in bracket p precedence $ inFix (getTm l) (getTm r)

1457 in bracket p precedence $ inFix (getTm l) (getTm r)

1454− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1458+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1455 bracket p funcAppPrec $

1459 bracket p funcAppPrec $

1456 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1460 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1457 align (group (vsep (map (prettyArgS bnd) rest)))

1461 align (group (vsep (map (prettyArgS bnd) rest)))

@@ -1467,7 +1471,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1467 Just (Infixr p') -> p'

1471 Just (Infixr p') -> p'

1468 Just f' -> prec f' + 1

1472 Just f' -> prec f' + 1

1469 inFix l r = align . group $

1473 inFix l r = align . group $

1470− (prettySe left bnd l <+> opName False) <$>

1474+ (prettySe left bnd l <+> opName False) <$>

1471 group (prettySe right bnd r)

1475 group (prettySe right bnd r)

1472 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1476 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

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

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

@@ -1486,7 +1490,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1486 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1490 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1487 indent 2 (vsep (map ppcase cases))

1491 indent 2 (vsep (map ppcase cases))

1488 where

1492 where

1489− ppcase (l, r) = let prettyCase = prettySe startPrec

1493+ ppcase (l, r) = let prettyCase = prettySe startPrec

1490 ([(n, False) | n <- vars l] ++ bnd)

1494 ([(n, False) | n <- vars l] ++ bnd)

1491 in nest nestingSize $

1495 in nest nestingSize $

1492 prettyCase l <+> text "=>" <+> prettyCase r

1496 prettyCase l <+> text "=>" <+> prettyCase r

@@ -1557,7 +1561,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1557 prettyAs =

1561 prettyAs =

1558 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1562 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1559 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1563 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1560− prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1564+ prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1561 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1565 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1562 -- XXX: add pretty for tactics

1566 -- XXX: add pretty for tactics

1563 prettySe p bnd (PProof ts) =

1567 prettySe p bnd (PProof ts) =

@@ -1729,7 +1733,7 @@ showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <>

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

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

1730showDeclImp o (PClass _ _ _ cs n ps _ ds)

1734showDeclImp o (PClass _ _ _ cs n ps _ ds)

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

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

1732−showDeclImp o (PInstance _ _ cs n _ t _ ds)

1736+showDeclImp o (PInstance _ _ _ cs n _ t _ ds)

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

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

1734showDeclImp _ _ = text "..."

1738showDeclImp _ _ = text "..."

1735-- showDeclImp (PImport o) = "import " ++ o

1739-- showDeclImp (PImport o) = "import " ++ o

@@ -1905,16 +1909,16 @@ implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1905implicitNamesIn uvars ist tm = nub $ ni [] tm

1909implicitNamesIn uvars ist tm = nub $ ni [] tm

1906 where

1910 where

1907 ni env (PRef _ n)

1911 ni env (PRef _ n)

1908− | not (n `elem` env)

1912+ | not (n `elem` env)

1909 = case lookupTy n (tt_ctxt ist) of

1913 = case lookupTy n (tt_ctxt ist) of

1910 [] -> [n]

1914 [] -> [n]

1911 _ -> if n `elem` uvars then [n] else []

1915 _ -> if n `elem` uvars then [n] else []

1912− ni env (PApp _ f@(PRef _ n) as)

1916+ ni env (PApp _ f@(PRef _ n) as)

1913 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1917 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1914 | otherwise = concatMap (ni env) (map getTm as)

1918 | otherwise = concatMap (ni env) (map getTm as)

1915 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1919 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1916 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1920 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1917− ni env (PCase _ c os) = ni env c ++

1921+ ni env (PCase _ c os) = ni env c ++

1918 -- names in 'os', not counting the names bound in the cases

1922 -- names in 'os', not counting the names bound in the cases

1919 (nub (concatMap (ni env) (map snd os))

1923 (nub (concatMap (ni env) (map snd os))

1920 \\ nub (concatMap (ni env) (map fst os)))

1924 \\ nub (concatMap (ni env) (map fst os)))

@@ -1944,7 +1948,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1944 _ -> if n `elem` (map fst uvars) then [n] else []

1948 _ -> if n `elem` (map fst uvars) then [n] else []

1945 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1949 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1946 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1950 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1947− ni env (PCase _ c os) = ni env c ++

1951+ ni env (PCase _ c os) = ni env c ++

1948 -- names in 'os', not counting the names bound in the cases

1952 -- names in 'os', not counting the names bound in the cases

1949 (nub (concatMap (ni env) (map snd os))

1953 (nub (concatMap (ni env) (map snd os))

1950 \\ nub (concatMap (ni env) (map fst os)))

1954 \\ nub (concatMap (ni env) (map fst os)))

@@ -2003,4 +2007,3 @@ getErasureInfo ist n =

2003 case lookupCtxtExact n (idris_optimisation ist) of

2007 case lookupCtxtExact n (idris_optimisation ist) of

2004 Just (Optimise inacc detagg) -> map fst inacc

2008 Just (Optimise inacc detagg) -> map fst inacc

2005 Nothing -> []

2009 Nothing -> []

2006−

src/Idris/DeepSeq.hs+3−5

@@ -153,11 +153,12 @@ instance (NFData t) => NFData (PDecl' t) where

153 = rnf x1 `seq`

154 rnf x2 `seq`

155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

156− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

156+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9)

157 = rnf x1 `seq`

158 rnf x2 `seq`

159 rnf x3 `seq`

160+ rnf x4 `seq`

160− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

161+ rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

161 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

162 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

162 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

@@ -357,6 +358,3 @@ instance NFData SyntaxInfo where

357 rnf x4 `seq`

358 rnf x4 `seq`

358 rnf x5 `seq`

359 rnf x5 `seq`

359 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

360 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

360−

361−

362−

src/Idris/Docs.hs+1−1

@@ -191,7 +191,7 @@ docClass n ci

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

192 return $ ClassDoc n docstr mdocs params instances superclasses

193 where

194− getDInst (PInstance _ _ _ _ _ t _ _) = Just t

194+ getDInst (PInstance _ _ _ _ _ _ t _ _) = Just t

195 getDInst _ = Nothing

196

197docFun :: Name -> Idris FunDoc

src/Idris/Elab/Class.hs+7−9

@@ -109,8 +109,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

109 mdec x = x

110

111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

113− checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

113+ checkDefaultSuperclassInstance (PInstance _ _ fc cs n ps _ _ _)

114 = do when (not $ null cs) . tclift

115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116 i <- getIState

@@ -120,11 +120,11 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

121 return ()

122

123− impbind :: [(Name, PTerm)] -> PTerm -> PTerm

123+ impbind :: [(Name, PTerm)] -> PTerm -> PTerm

124 impbind [] x = x

125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126

127− conbind :: [(Name, PTerm)] -> PTerm -> PTerm

127+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

128 conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

129 conbind [] x = x

130

@@ -133,7 +133,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133 = do t' <- implicit' info syn allmeths n t

134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps)

136+ (n, (doc, o, (toExp (map fst ps)

137 (\ l s p -> Imp l s p Nothing) t'))),

138 (n, (syn, o, t) ) )

139 tdecl _ _ = ifail "Not allowed in a class declaration"

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155

156 tydecl (PTy _ _ _ _ _ _ _) = True

157 tydecl _ = False

158− instdecl (PInstance _ _ _ _ _ _ _ _) = True

158+ instdecl (PInstance _ _ _ _ _ _ _ _ _) = True

159 instdecl _ = False

160 clause (PClauses _ _ _ _) = True

161 clause _ = False

@@ -221,7 +221,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

221

222 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

223 = PPi p n ty (insertConstraint c sc)

224− insertConstraint c sc = PPi (constraint { pstatic = Static })

224+ insertConstraint c sc = PPi (constraint { pstatic = Static })

225 (sMN 0 "class") c sc

226

227 -- make arguments explicit and don't bind class parameters

@@ -230,5 +230,3 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

232 toExp ns e sc = sc

233−

234−

src/Idris/Elab/Instance.hs+5−4

@@ -51,6 +51,7 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

53elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

54 ElabWhat -> -- phase

55 ElabWhat -> -- phase

55 FC -> [(Name, PTerm)] -> -- constraints

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

56 Name -> -- the class

57 Name -> -- the class

@@ -58,7 +59,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

58 PTerm -> -- full instance type

59 PTerm -> -- full instance type

59 Maybe Name -> -- explicit name

60 Maybe Name -> -- explicit name

60 [PDecl] -> Idris ()

61 [PDecl] -> Idris ()

61−elabInstance info syn what fc cs n ps t expn ds = do

62+elabInstance info syn doc what fc cs n ps t expn ds = do

62 i <- getIState

63 i <- getIState

63 (n, ci) <- case lookupCtxtName n (idris_classes i) of

64 (n, ci) <- case lookupCtxtName n (idris_classes i) of

64 [c] -> return c

65 [c] -> return c

@@ -147,10 +148,10 @@ elabInstance info syn what fc cs n ps t expn ds = do

147 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

148 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

148 Just nm -> nm

149 Just nm -> nm

149

150

150− substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

151+ substInstance ips pnames (PInstance doc syn _ cs n ps t expn ds)

151− = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152+ = PInstance doc syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152

153

153− isOverlapping i (PInstance syn _ _ n ps t expn _)

154+ isOverlapping i (PInstance doc syn _ _ n ps t expn _)

154 = case lookupCtxtName n (idris_classes i) of

155 = case lookupCtxtName n (idris_classes i) of

155 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

156 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

156 case lookupTy iname (tt_ctxt i) of

157 case lookupTy iname (tt_ctxt i) of

src/Idris/ElabDecls.hs+4−5

@@ -200,11 +200,11 @@ elabDecl' what info (PMutual f ps)

200 where isDataDecl (PData _ _ _ _ _ _) = True

201 isDataDecl _ = False

202

203− setMutData ns n

203+ setMutData ns n

204 = do i <- getIState

205 case lookupCtxt n (idris_datatypes i) of

206 [x] -> do let x' = x { mutual_types = ns }

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208 = addDef n x' (idris_datatypes i) }

209 _ -> return ()

210

@@ -233,9 +233,9 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

233 | what /= EDefns

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

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

236−elabDecl' what info (PInstance s f cs n ps t expn ds)

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

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

238− elabInstance info s what f cs n ps t expn ds

238+ elabInstance info s doc what f cs n ps t expn ds

239elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

240 | what /= ETypes

241 = do iLOG $ "Elaborating record " ++ show tyn

@@ -257,4 +257,3 @@ elabDecl' what info (PTransform fc safety old new)

257 = do elabTransform info fc safety old new

258 return ()

259elabDecl' _ _ _ = return () -- skipped this time

260−

src/Idris/IBC.hs+28−27

@@ -91,9 +91,9 @@ deriving instance Binary IBCFile

91initIBC :: IBCFile

92initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

94−loadIBC :: Bool -- ^ True = reexport, False = make everything private

94+loadIBC :: Bool -- ^ True = reexport, False = make everything private

95 -> FilePath -> Idris ()

96−loadIBC reexport fp

96+loadIBC reexport fp

97 = do imps <- getImported

98 let redo = case lookup fp imps of

99 Nothing -> True

@@ -194,7 +194,7 @@ ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

194ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

195ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

196ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

197−ibc i (IBCDef n) f

197+ibc i (IBCDef n) f

198 = do f' <- case lookupDefExact n (tt_ctxt i) of

199 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

200 _ -> ifail "IBC write failed"

@@ -239,13 +239,13 @@ ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

239process :: Bool -- ^ Reexporting

240 -> IBCFile -> FilePath -> Idris ()

241process reexp i fn

242− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

243 = do iLOG "ibc out of date"

244 let e = if ver i < ibcVersion then " an earlier " else " a later "

245 ifail $ "Incompatible ibc version.\nThis library was built with"

246 ++ e ++ "version of Idris.\n" ++

247 "Please clean and rebuild."

248−

248+

249 --- please rebuild"

250 | otherwise =

251 do srcok <- runIO $ doesFileExist (sourcefile i)

@@ -323,7 +323,7 @@ pImportDirs fs = mapM_ addImportDir fs

323

324pImports :: [(Bool, FilePath)] -> Idris ()

325pImports fs

326− = do mapM_ (\(re, f) ->

326+ = do mapM_ (\(re, f) ->

327 do i <- getIState

328 ibcsd <- valIBCSubDir i

329 ids <- allImportDirs

@@ -427,20 +427,20 @@ pHdrs :: [(Codegen, String)] -> Idris ()

427pHdrs hs = mapM_ (uncurry addHdr) hs

428

429pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

430−pPatdefs ds

430+pPatdefs ds

431− = mapM_ (\ (n, d) ->

431+ = mapM_ (\ (n, d) ->

432 do i <- getIState

433 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

434 ds

435

436pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

437−pDefs reexp syms ds

437+pDefs reexp syms ds

438 = mapM_ (\ (n, d) ->

439 do d' <- updateDef d

440 case d' of

441− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

442 _ -> do iLOG $ "SOLVING " ++ show n

443− solveDeferred n

443+ solveDeferred n

444 i <- getIState

445-- logLvl 1 $ "Added " ++ show (n, d')

446 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

@@ -509,8 +509,8 @@ pMDocs ds = mapM_ addMDocStr ds

509

510pAccess :: Bool -- ^ Reexporting?

511 -> [(Name, Accessibility)] -> Idris ()

512−pAccess reexp ds

512+pAccess reexp ds

513− = mapM_ (\ (n, a_in) ->

513+ = mapM_ (\ (n, a_in) ->

514 do let a = if reexp then a_in else Hidden

515 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

516 i <- getIState

@@ -568,7 +568,7 @@ pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn

568

569pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

570pMetavars ns = do i <- getIState

571− putIState $ i { idris_metavars = Data.List.reverse ns

571+ putIState $ i { idris_metavars = Data.List.reverse ns

572 ++ idris_metavars i }

573

574----- For Cheapskate and docstrings

@@ -862,7 +862,7 @@ safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

862safeToEnum label x' = result

863 where

864 x = fromIntegral x'

865− result

865+ result

866 | x < fromEnum (minBound `asTypeOf` result)

867 || x > fromEnum (maxBound `asTypeOf` result)

868 = error $ label ++ ": corrupted binary representation in IBC"

@@ -1248,15 +1248,16 @@ instance (Binary t) => Binary (PDecl' t) where

1248 put x6

1249 put x7

1250 put x8

1251− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1251+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 -> do putWord8 8

1252− put x1

1252+ put x1

1253− put x2

1253+ put x2

1254− put x3

1254+ put x3

1255− put x4

1255+ put x4

1256− put x5

1256+ put x5

1257− put x6

1257+ put x6

1258− put x7

1258+ put x7

1259− put x8

1259+ put x8

1260+ put x9

1260 PDSL x1 x2 -> do putWord8 9

1261 PDSL x1 x2 -> do putWord8 9

1261 put x1

1262 put x1

1262 put x2

1263 put x2

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

1288 put x1

1289 put x1

1289 put x2

1290 put x2

1290 put x3

1291 put x3

1291− put x4

1292+ put x4

1292 get

1293 get

1293 = do i <- getWord8

1294 = do i <- getWord8

1294 case i of

1295 case i of

@@ -1350,7 +1351,8 @@ instance (Binary t) => Binary (PDecl' t) where

1350 x6 <- get

1351 x6 <- get

1351 x7 <- get

1352 x7 <- get

1352 x8 <- get

1353 x8 <- get

1354+ x9 <- get

1353− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1355+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9)

1354 9 -> do x1 <- get

1356 9 -> do x1 <- get

1355 x2 <- get

1357 x2 <- get

1356 return (PDSL x1 x2)

1358 return (PDSL x1 x2)

@@ -2198,4 +2200,3 @@ instance Binary Codegen where

2198 return (Via x1)

2200 return (Via x1)

2199 1 -> return Bytecode

2201 1 -> return Bytecode

2200 _ -> error "Corrupted binary data for Codegen"

2202 _ -> error "Corrupted binary data for Codegen"

2201−

src/Idris/ParseHelpers.hs+2−2

@@ -587,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

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

588collect (PClass doc f s cs n ps pdocs ds : ds')

589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

590−collect (PInstance f s cs n ps t en ds : ds')

590+collect (PInstance doc f s cs n ps t en ds : ds')

591− = PInstance f s cs n ps t en (collect ds) : collect ds'

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

592collect (d : ds) = d : collect ds

593collect [] = []

src/Idris/Parser.hs+12−8

@@ -178,8 +178,7 @@ decl syn = do fc <- getFC

178 <|> params syn

179 <|> mutual syn

180 <|> namespace syn

181− <|> class_ syn

182− <|> instance_ syn

181+ <|> (try (class_ syn) <|> instance_ syn)

183 <|> do d <- dsl syn; return [d]

182 <|> do d <- dsl syn; return [d]

184 <|> directive syn

183 <|> directive syn

185 <|> provider syn

184 <|> provider syn

@@ -291,7 +290,7 @@ syntaxRule syn

291

290

292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

291 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293 mkSimple es

292 mkSimple es

294− -- Can't parse a full expression followed by operator like characters due to ambiguity

293+ -- Can't parse a full expression followed by operator like characters due to ambiguity

295 mkSimple' (Expr e : Symbol s : es)

294 mkSimple' (Expr e : Symbol s : es)

296 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

295 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

296 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

@@ -587,7 +586,7 @@ ClassBlock ::=

587classBlock :: SyntaxInfo -> IdrisParser [PDecl]

586classBlock :: SyntaxInfo -> IdrisParser [PDecl]

588classBlock syn = do reserved "where"

587classBlock syn = do reserved "where"

589 openBlock

588 openBlock

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

589+ ds <- many (try (notEndBlock >> instance_ syn) <|> fnDecl syn)

591 closeBlock

590 closeBlock

592 return (concat ds)

591 return (concat ds)

593 <?> "class block"

592 <?> "class block"

@@ -634,7 +633,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

634

633

635@

634@

636 Instance ::=

635 Instance ::=

637− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

636+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

638 ;

637 ;

639@

638@

640

639

@@ -643,7 +642,12 @@ InstanceName ::= '[' Name ']';

643@

642@

644-}

643-}

645instance_ :: SyntaxInfo -> IdrisParser [PDecl]

644instance_ :: SyntaxInfo -> IdrisParser [PDecl]

645+instance_ syn = do doc <- try (do

646+ (doc, _) <- option noDocs docComment

647+ ist <- get

648+ let doc' = annotCode (tryFullExpr syn ist) doc

649+ return doc')

646−instance_ syn = do reserved "instance"; fc <- getFC

650+ reserved "instance"; fc <- getFC

647 en <- optional instanceName

651 en <- optional instanceName

648 cs <- constraintList syn

652 cs <- constraintList syn

649 cn <- fnName

653 cn <- fnName

@@ -651,7 +655,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

651 let sc = PApp fc (PRef fc cn) (map pexp args)

655 let sc = PApp fc (PRef fc cn) (map pexp args)

652 let t = bindList (PPi constraint) cs sc

656 let t = bindList (PPi constraint) cs sc

653 ds <- option [] (instanceBlock syn)

657 ds <- option [] (instanceBlock syn)

654− return [PInstance syn fc cs cn args t en ds]

658+ return [PInstance doc syn fc cs cn args t en ds]

655 <?> "instance declaration"

659 <?> "instance declaration"

656 where instanceName :: IdrisParser Name

660 where instanceName :: IdrisParser Name

657 instanceName = do lchar '['; n_in <- fnName; lchar ']'

661 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -1405,7 +1409,7 @@ loadSource lidr f toline

1405 case x of

1409 case x of

1406 PClauses _ _ _ _ -> r

1410 PClauses _ _ _ _ -> r

1407 PClass _ _ _ _ _ _ _ _ -> r

1411 PClass _ _ _ _ _ _ _ _ -> r

1408− PInstance _ _ _ _ _ _ _ _ -> r

1412+ PInstance _ _ _ _ _ _ _ _ _ -> r

1409 _ -> x

1413 _ -> x

1410

1414

1411 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

1415 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/REPL.hs+2−2

@@ -811,8 +811,8 @@ process fn (NewDefn decls) = do

811 fixClauses :: PDecl' t -> PDecl' t

812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

813 PClauses fc opts (getClauseName clause) css

814− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

814+ fixClauses (PInstance doc syn fc constraints cls parms ty instName decls) =

815− PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

815+ PInstance doc syn fc constraints cls parms ty instName (map fixClauses decls)

816 fixClauses decl = decl

817

818process fn (Undefine names) = undefine names