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

git.iko.soy/Idris-dev

Instance docs: basic plumbing of types and parsing

commit2d205a610d5c439262c48715b219d5a3a218d2cc authorAdam Sandberg Eriksson <adam@sandbergericsson.se> dateThu 5 Mar 2015, 00:44 (12 years ago) parente9c96d4

11 files changed+102−98

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+10−10 src/Idris/AbsSyntaxTree.hs+28−25 src/Idris/DeepSeq.hs+3−5 src/Idris/Docs.hs+1−1 src/Idris/Elab/Class.hs+7−9 src/Idris/Elab/Instance.hs+5−4 src/Idris/ElabDecls.hs+4−5 src/Idris/IBC.hs+28−27 src/Idris/ParseHelpers.hs+2−2 src/Idris/Parser.hs+12−8 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntax.hs+10−10

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

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

9797

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

99−addImported pub f

99+addImported pub f

100100 = do i <- getIState

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

102102

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

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

135135

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

137−addUsedName fc n arg

137+addUsedName fc n arg

138138 = do ist <- getIState

139139 case lookupTyName n (tt_ctxt ist) of

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

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

10831083 pDocs

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

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

1086− = PInstance info f

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

1086+ = PInstance doc info f

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

10881088 n

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

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

15521552 PLam fc n ty' sc'

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

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

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

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

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

15571557 = case lookupDef n (tt_ctxt ist) of

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

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

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

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

17281728 t' <- sl t

1729− r' <- sl r

1729+ r' <- sl r

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

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

17321732 args' <- mapM slA args

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

19251925 match (PHidden x) (PHidden y)

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

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

1928− match (PHidden x) y

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

1928+ match (PHidden x) y

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

19301930 | otherwise = return []

1931− match x (PHidden y)

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

1931+ match x (PHidden y)

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

19331933 | otherwise = return []

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

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

src/Idris/AbsSyntaxTree.hs+28−25

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

5757 liftname :: Name -> Name,

5858 namespace :: Maybe [String],

5959 elabFC :: Maybe FC,

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

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

6161 Idris () }

6262

6363toplevel :: ElabInfo

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

601601 [PDecl' t] -- declarations

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

603603 -- class name, parameters, method declarations

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

605− Name -- class

606− [t] -- parameters

607− t -- full instance type

608− (Maybe Name) -- explicit name

609− [PDecl' t]

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

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

604+ | PInstance

605+ (Docstring (Either Err PTerm))

606+ SyntaxInfo

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

608+ Name -- class

609+ [t] -- parameters

610+ t -- full instance type

611+ (Maybe Name) -- explicit name

612+ [PDecl' t]

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

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

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

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

613617 | PSyntax FC Syntax -- ^ Syntax definition

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

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

688692declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

692696declared (PDSL n _) = [n]

693697declared (PSyntax _ _) = []

694698declared (PMutual _ ds) = concatMap declared ds

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

707711tldeclared (PMutual _ ds) = concatMap tldeclared ds

708712tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

711715tldeclared _ = []

712716

713717defined :: PDecl -> [Name]

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

723727defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

727731defined (PDSL n _) = [n]

728732defined (PSyntax _ _) = []

729733defined (PMutual _ ds) = concatMap defined ds

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

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

779783 | PHidden PTerm -- ^ Irrelevant or hidden pattern

780784 | PType -- ^ 'Type' type

781− | PUniverse Universe -- ^ Some universe

785+ | PUniverse Universe -- ^ Some universe

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

783787 | PConstant Const -- ^ Builtin types

784788 | Placeholder -- ^ Underscore

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

11131117 | Expr Name

11141118 | SimpleExpr Name

11151119 deriving (Show, Eq)

1116−

1120+

11171121

11181122{-!

11191123deriving instance Binary SSymbol

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

13881392 where

13891393 startPrec = 0

13901394 funcAppPrec = 10

1391−

1395+

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

13931397 prettySe p bnd (PQuote r) =

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

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

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

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

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

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

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

14551459 bracket p funcAppPrec $

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

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

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

14671471 Just (Infixr p') -> p'

14681472 Just f' -> prec f' + 1

14691473 inFix l r = align . group $

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

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

14711475 group (prettySe right bnd r)

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

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

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

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

14871491 indent 2 (vsep (map ppcase cases))

14881492 where

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

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

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

14911495 in nest nestingSize $

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

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

15571561 prettyAs =

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

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

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

15621566 -- XXX: add pretty for tactics

15631567 prettySe p bnd (PProof ts) =

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

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

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

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

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

17341738showDeclImp _ _ = text "..."

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

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

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

19061910 where

19071911 ni env (PRef _ n)

1908− | not (n `elem` env)

1912+ | not (n `elem` env)

19091913 = case lookupTy n (tt_ctxt ist) of

19101914 [] -> [n]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

20032007 case lookupCtxtExact n (idris_optimisation ist) of

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

20052009 Nothing -> []

2006−

src/Idris/DeepSeq.hs+3−5

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

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

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

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

159159 rnf x3 `seq`

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

160+ rnf x4 `seq`

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

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

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

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

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

357358 rnf x4 `seq`

358359 rnf x5 `seq`

359360 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

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

192192 return $ ClassDoc n docstr mdocs params instances superclasses

193193 where

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

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

195195 getDInst _ = Nothing

196196

197197docFun :: 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

109109 mdec x = x

110110

111111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

116116 i <- getIState

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

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

121121 return ()

122122

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

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

124124 impbind [] x = x

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

126126

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

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

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

129129 conbind [] x = x

130130

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

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

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

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

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

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

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

138138 (n, (syn, o, t) ) )

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

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

155155

156156 tydecl (PTy _ _ _ _ _ _ _) = True

157157 tydecl _ = False

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

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

159159 instdecl _ = False

160160 clause (PClauses _ _ _ _) = True

161161 clause _ = False

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

221221

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

223223 = PPi p n ty (insertConstraint c sc)

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

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

225225 (sMN 0 "class") c sc

226226

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

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

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

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

232232 toExp ns e sc = sc

233−

234−

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

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

5151import Util.Pretty(pretty, text)

5252

5353elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

5455 ElabWhat -> -- phase

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

5657 Name -> -- the class

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

5859 PTerm -> -- full instance type

5960 Maybe Name -> -- explicit name

6061 [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

6263 i <- getIState

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

6465 [c] -> return c

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

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

148149 Just nm -> nm

149150

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

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

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

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

152153

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

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

154155 = case lookupCtxtName n (idris_classes i) of

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

156157 case lookupTy iname (tt_ctxt i) of

src/Idris/ElabDecls.hs+4−5

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

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

201201 isDataDecl _ = False

202202

203− setMutData ns n

203+ setMutData ns n

204204 = do i <- getIState

205205 case lookupCtxt n (idris_datatypes i) of

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

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208208 = addDef n x' (idris_datatypes i) }

209209 _ -> return ()

210210

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

233233 | what /= EDefns

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

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

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

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

240240 | what /= ETypes

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

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

257257 = do elabTransform info fc safety old new

258258 return ()

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

260−

src/Idris/IBC.hs+28−27

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

9191initIBC :: IBCFile

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

9393

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

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

9595 -> FilePath -> Idris ()

96−loadIBC reexport fp

96+loadIBC reexport fp

9797 = do imps <- getImported

9898 let redo = case lookup fp imps of

9999 Nothing -> True

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

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

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

196196ibc 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

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

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

200200 _ -> ifail "IBC write failed"

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

239239process :: Bool -- ^ Reexporting

240240 -> IBCFile -> FilePath -> Idris ()

241241process reexp i fn

242− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

243243 = do iLOG "ibc out of date"

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

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

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

247247 "Please clean and rebuild."

248−

248+

249249 --- please rebuild"

250250 | otherwise =

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

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

323323

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

325325pImports fs

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

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

327327 do i <- getIState

328328 ibcsd <- valIBCSubDir i

329329 ids <- allImportDirs

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

427427pHdrs hs = mapM_ (uncurry addHdr) hs

428428

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

430−pPatdefs ds

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

430+pPatdefs ds

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

432432 do i <- getIState

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

434434 ds

435435

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

437−pDefs reexp syms ds

437+pDefs reexp syms ds

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

439439 do d' <- updateDef d

440440 case d' of

441− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

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

443− solveDeferred n

443+ solveDeferred n

444444 i <- getIState

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

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

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

509509

510510pAccess :: Bool -- ^ Reexporting?

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

512−pAccess reexp ds

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

512+pAccess reexp ds

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

514514 do let a = if reexp then a_in else Hidden

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

516516 i <- getIState

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

568568

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

570570pMetavars ns = do i <- getIState

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

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

572572 ++ idris_metavars i }

573573

574574----- For Cheapskate and docstrings

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

862862safeToEnum label x' = result

863863 where

864864 x = fromIntegral x'

865− result

865+ result

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

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

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

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

12481248 put x6

12491249 put x7

12501250 put x8

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

1252− put x1

1253− put x2

1254− put x3

1255− put x4

1256− put x5

1257− put x6

1258− put x7

1259− put x8

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

1252+ put x1

1253+ put x2

1254+ put x3

1255+ put x4

1256+ put x5

1257+ put x6

1258+ put x7

1259+ put x8

1260+ put x9

12601261 PDSL x1 x2 -> do putWord8 9

12611262 put x1

12621263 put x2

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

12881289 put x1

12891290 put x2

12901291 put x3

1291− put x4

1292+ put x4

12921293 get

12931294 = do i <- getWord8

12941295 case i of

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

13501351 x6 <- get

13511352 x7 <- get

13521353 x8 <- get

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

1354+ x9 <- get

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

13541356 9 -> do x1 <- get

13551357 x2 <- get

13561358 return (PDSL x1 x2)

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

21982200 return (Via x1)

21992201 1 -> return Bytecode

22002202 _ -> 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

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

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

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

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

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

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

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

592592collect (d : ds) = d : collect ds

593593collect [] = []

src/Idris/Parser.hs+12−8

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

178178 <|> params syn

179179 <|> mutual syn

180180 <|> namespace syn

181− <|> class_ syn

182− <|> instance_ syn

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

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

184183 <|> directive syn

185184 <|> provider syn

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

291290

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

293292 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

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

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

297296 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

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

587586classBlock :: SyntaxInfo -> IdrisParser [PDecl]

588587classBlock syn = do reserved "where"

589588 openBlock

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

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

591590 closeBlock

592591 return (concat ds)

593592 <?> "class block"

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

634633

635634@

636635 Instance ::=

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

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

638637 ;

639638@

640639

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

643642@

644643-}

645644instance_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

650+ reserved "instance"; fc <- getFC

647651 en <- optional instanceName

648652 cs <- constraintList syn

649653 cn <- fnName

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

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

652656 let t = bindList (PPi constraint) cs sc

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

655659 <?> "instance declaration"

656660 where instanceName :: IdrisParser Name

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

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

14051409 case x of

14061410 PClauses _ _ _ _ -> r

14071411 PClass _ _ _ _ _ _ _ _ -> r

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

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

14091413 _ -> x

14101414

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

src/Idris/REPL.hs+2−2

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

811811 fixClauses :: PDecl' t -> PDecl' t

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

813813 PClauses fc opts (getClauseName clause) css

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

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

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

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

816816 fixClauses decl = decl

817817

818818process fn (Undefine names) = undefine names