8464bc4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add field for documentation comments in abstract syntax

8464bc4Edwin Brady14 years ago

src/Core/CoreParser.hs+10−1

compare with master

unifiedsplit

@@ -1,7 +1,7 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,

4− idrisLexer, maybeWithNS) where

4+ idrisLexer, maybeWithNS, pDocComment) where

6import Core.TT

@@ -123,6 +123,15 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

123 (x, "") -> [x]

124 (x, '.':y) -> x : parseNS y

125

126+pDocComment :: Char -> CParser a String

127+pDocComment c

128+ = do string "--"

129+ char c

130+ i <- getInput

131+ let (doc, rest) = span (/='\n') i

132+ setInput rest

133+ return doc

134+

126pDef :: CParser a (Name, RDef)

135pDef :: CParser a (Name, RDef)

127pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

136pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

128 lchar '='

137 lchar '='

src/Idris/AbsSyntax.hs+52−42

@@ -68,8 +68,14 @@ getTotality n

68 _ -> return (Total [])

70addToCG :: Name -> CGInfo -> Idris ()

71−addToCG n cg = do i <- get

71+addToCG n cg

72+ = do i <- get

72− put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

73+ put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

74+

75+addDocStr :: Name -> String -> Idris ()

76+addDocStr n doc

77+ = do i <- get

78+ put (i { idris_docstrings = addDef n doc (idris_docstrings i) })

74addToCalledG :: Name -> [Name] -> Idris ()

80addToCalledG :: Name -> [Name] -> Idris ()

75addToCalledG n ns = return () -- TODO

81addToCalledG n ns = return () -- TODO

@@ -360,7 +366,7 @@ inferTy = MN 0 "__Infer"

360inferCon = MN 0 "__infer"

366inferCon = MN 0 "__infer"

361inferDecl = PDatadecl inferTy

367inferDecl = PDatadecl inferTy

362 PSet

368 PSet

363− [(inferCon, PPi impl (MN 0 "A") PSet (

369+ [("", inferCon, PPi impl (MN 0 "A") PSet (

364 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

370 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

365 (PRef bi inferTy)), bi)]

371 (PRef bi inferTy)), bi)]

366

372

@@ -384,7 +390,7 @@ primNames = [unitTy, unitCon,

384unitTy = MN 0 "__Unit"

390unitTy = MN 0 "__Unit"

385unitCon = MN 0 "__II"

391unitCon = MN 0 "__II"

386unitDecl = PDatadecl unitTy PSet

392unitDecl = PDatadecl unitTy PSet

387− [(unitCon, PRef bi unitTy, bi)]

393+ [("", unitCon, PRef bi unitTy, bi)]

388

394

389falseTy = MN 0 "__False"

395falseTy = MN 0 "__False"

390falseDecl = PDatadecl falseTy PSet []

396falseDecl = PDatadecl falseTy PSet []

@@ -392,7 +398,7 @@ falseDecl = PDatadecl falseTy PSet []

392pairTy = MN 0 "__Pair"

398pairTy = MN 0 "__Pair"

393pairCon = MN 0 "__MkPair"

399pairCon = MN 0 "__MkPair"

394pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

400pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

395− [(pairCon, PPi impl (n "A") PSet (

401+ [("", pairCon, PPi impl (n "A") PSet (

396 PPi impl (n "B") PSet (

402 PPi impl (n "B") PSet (

397 PPi expl (n "a") (PRef bi (n "A")) (

403 PPi expl (n "a") (PRef bi (n "A")) (

398 PPi expl (n "b") (PRef bi (n "B"))

404 PPi expl (n "b") (PRef bi (n "B"))

@@ -405,7 +411,7 @@ eqCon = UN "refl"

405eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

411eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

406 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

412 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

407 PSet)

413 PSet)

408− [(eqCon, PPi impl (n "a") PSet (

414+ [("", eqCon, PPi impl (n "a") PSet (

409 PPi impl (n "x") (PRef bi (n "a"))

415 PPi impl (n "x") (PRef bi (n "a"))

410 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,

416 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,

411 pimp (n "b") Placeholder,

417 pimp (n "b") Placeholder,

@@ -484,10 +490,10 @@ expandParams dec ps ns tm = en tm

484

490

485expandParamsD :: IState ->

491expandParamsD :: IState ->

486 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

492 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

487−expandParamsD ist dec ps ns (PTy syn fc o n ty)

493+expandParamsD ist dec ps ns (PTy doc syn fc o n ty)

488 = if n `elem` ns

494 = if n `elem` ns

489− then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

495+ then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

490− else PTy syn fc o n (expandParams dec ps ns ty)

496+ else PTy doc syn fc o n (expandParams dec ps ns ty)

491expandParamsD ist dec ps ns (PClauses fc opts n cs)

497expandParamsD ist dec ps ns (PClauses fc opts n cs)

492 = let n' = if n `elem` ns then dec n else n in

498 = let n' = if n `elem` ns then dec n else n in

493 PClauses fc opts n' (map expandParamsC cs)

499 PClauses fc opts n' (map expandParamsC cs)

@@ -512,7 +518,8 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)

512 updateps yn nm (((a, t), i):as)

518 updateps yn nm (((a, t), i):as)

513 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

519 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

514 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as

520 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as

515−expandParamsD ist dec ps ns (PData syn fc co pd) = PData syn fc co (expandPData pd)

521+expandParamsD ist dec ps ns (PData doc syn fc co pd)

522+ = PData doc syn fc co (expandPData pd)

516 where

523 where

517 -- just do the type decl, leave constructors alone (parameters will be

524 -- just do the type decl, leave constructors alone (parameters will be

518 -- added implicitly)

525 -- added implicitly)

@@ -520,12 +527,15 @@ expandParamsD ist dec ps ns (PData syn fc co pd) = PData syn fc co (expandPData

520 = if n `elem` ns

527 = if n `elem` ns

521 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)

528 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)

522 else PDatadecl n (expandParams dec ps ns ty) (map econ cons)

529 else PDatadecl n (expandParams dec ps ns ty) (map econ cons)

530+ econ (doc, n, t, fc)

523− econ (n, t, fc) = (dec n, piBindp expl ps (expandParams dec ps ns t), fc)

531+ = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)

524expandParamsD ist dec ps ns (PParams f params pds)

532expandParamsD ist dec ps ns (PParams f params pds)

525 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params) pds

533 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params) pds

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

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

527−expandParamsD ist dec ps ns (PClass info f cs n params decls)

535+expandParamsD ist dec ps ns (PMutual f pds)

536+ = PMutual f (map (expandParamsD ist dec ps ns) pds)

537+expandParamsD ist dec ps ns (PClass doc info f cs n params decls)

528− = PClass info f

538+ = PClass doc info f

529 (map (expandParams dec ps ns) cs)

539 (map (expandParams dec ps ns) cs)

530 n

540 n

531 (map (mapsnd (expandParams dec ps ns)) params)

541 (map (mapsnd (expandParams dec ps ns)) params)

@@ -638,34 +648,34 @@ implicitise syn ignore ist tm

638 = do (decls, ns) <- get

648 = do (decls, ns) <- get

639 let isn = concatMap (namesIn uvars ist) (map getTm as)

649 let isn = concatMap (namesIn uvars ist) (map getTm as)

640 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

650 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

641− imps top env (PPi (Imp l _) n ty sc)

651+ imps top env (PPi (Imp l _ doc) n ty sc)

642 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

652 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

643 (decls , ns) <- get

653 (decls , ns) <- get

644− put (PImp (getPriority ist ty) l n ty : decls,

654+ put (PImp (getPriority ist ty) l n ty doc : decls,

645 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

655 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

646 imps True (n:env) sc

656 imps True (n:env) sc

647− imps top env (PPi (Exp l _) n ty sc)

657+ imps top env (PPi (Exp l _ doc) n ty sc)

648 = do let isn = nub (namesIn uvars ist ty ++ case sc of

658 = do let isn = nub (namesIn uvars ist ty ++ case sc of

649 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

659 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

650 _ -> [])

660 _ -> [])

651 (decls, ns) <- get -- ignore decls in HO types

661 (decls, ns) <- get -- ignore decls in HO types

652− put (PExp (getPriority ist ty) l ty : decls,

662+ put (PExp (getPriority ist ty) l ty doc : decls,

653 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

663 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

654 imps True (n:env) sc

664 imps True (n:env) sc

655− imps top env (PPi (Constraint l _) n ty sc)

665+ imps top env (PPi (Constraint l _ doc) n ty sc)

656 = do let isn = nub (namesIn uvars ist ty ++ case sc of

666 = do let isn = nub (namesIn uvars ist ty ++ case sc of

657 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

667 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

658 _ -> [])

668 _ -> [])

659 (decls, ns) <- get -- ignore decls in HO types

669 (decls, ns) <- get -- ignore decls in HO types

660− put (PConstraint 10 l ty : decls,

670+ put (PConstraint 10 l ty doc : decls,

661 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

671 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

662 imps True (n:env) sc

672 imps True (n:env) sc

663− imps top env (PPi (TacImp l _ scr) n ty sc)

673+ imps top env (PPi (TacImp l _ scr doc) n ty sc)

664 = do let isn = nub (namesIn uvars ist ty ++ case sc of

674 = do let isn = nub (namesIn uvars ist ty ++ case sc of

665 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

675 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

666 _ -> [])

676 _ -> [])

667 (decls, ns) <- get -- ignore decls in HO types

677 (decls, ns) <- get -- ignore decls in HO types

668− put (PTacImplicit 10 l n scr ty : decls,

678+ put (PTacImplicit 10 l n scr ty doc : decls,

669 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

679 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

670 imps True (n:env) sc

680 imps True (n:env) sc

671 imps top env (PEq _ l r)

681 imps top env (PEq _ l r)

@@ -700,8 +710,8 @@ implicitise syn ignore ist tm

700 pibind using [] sc = sc

710 pibind using [] sc = sc

701 pibind using (n:ns) sc

711 pibind using (n:ns) sc

702 = case lookup n using of

712 = case lookup n using of

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

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

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

714+ Nothing -> PPi (Imp False Dynamic "") n Placeholder

705 (pibind using ns sc)

715 (pibind using ns sc)

706

716

707-- Add implicit arguments in function calls

717-- Add implicit arguments in function calls

@@ -781,7 +791,7 @@ aiFn inpat True ist fc f []

781 || any constructor alts || any allImp ialts)

791 || any constructor alts || any allImp ialts)

782 then aiFn inpat False ist fc f [] -- use it as a constructor

792 then aiFn inpat False ist fc f [] -- use it as a constructor

783 else Right $ PPatvar fc f

793 else Right $ PPatvar fc f

784− where imp (PExp _ _ _) = False

794+ where imp (PExp _ _ _ _) = False

785 imp _ = True

795 imp _ = True

786 allImp [] = False

796 allImp [] = False

787 allImp xs = all imp xs

797 allImp xs = all imp xs

@@ -806,29 +816,29 @@ aiFn inpat expat ist fc f as

806 (insertImpl ns as)) alts

816 (insertImpl ns as)) alts

807 where

817 where

808 insertImpl :: [PArg] -> [PArg] -> [PArg]

818 insertImpl :: [PArg] -> [PArg] -> [PArg]

809− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

819+ insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =

810− PExp p l tm : insertImpl ps given

820+ PExp p l tm d : insertImpl ps given

811− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

821+ insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =

812− PConstraint p l tm : insertImpl ps given

822+ PConstraint p l tm d : insertImpl ps given

813− insertImpl (PConstraint p l ty : ps) given =

823+ insertImpl (PConstraint p l ty d : ps) given =

814− PConstraint p l (PResolveTC fc) : insertImpl ps given

824+ PConstraint p l (PResolveTC fc) d : insertImpl ps given

815− insertImpl (PImp p l n ty : ps) given =

825+ insertImpl (PImp p l n ty d : ps) given =

816 case find n given [] of

826 case find n given [] of

817− Just (tm, given') -> PImp p l n tm : insertImpl ps given'

827+ Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'

818− Nothing -> PImp p l n Placeholder : insertImpl ps given

828+ Nothing -> PImp p l n Placeholder "" : insertImpl ps given

819− insertImpl (PTacImplicit p l n sc ty : ps) given =

829+ insertImpl (PTacImplicit p l n sc ty d : ps) given =

820 case find n given [] of

830 case find n given [] of

821− Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

831+ Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

822 Nothing -> if inpat

832 Nothing -> if inpat

823− then PTacImplicit p l n sc Placeholder : insertImpl ps given

833+ then PTacImplicit p l n sc Placeholder "" : insertImpl ps given

824− else PTacImplicit p l n sc sc : insertImpl ps given

834+ else PTacImplicit p l n sc sc "" : insertImpl ps given

825 insertImpl expected [] = []

835 insertImpl expected [] = []

826 insertImpl _ given = given

836 insertImpl _ given = given

827

837

828 find n [] acc = Nothing

838 find n [] acc = Nothing

829− find n (PImp _ _ n' t : gs) acc

839+ find n (PImp _ _ n' t _ : gs) acc

830 | n == n' = Just (t, reverse acc ++ gs)

840 | n == n' = Just (t, reverse acc ++ gs)

831− find n (PTacImplicit _ _ n' _ t : gs) acc

841+ find n (PTacImplicit _ _ n' _ t _ : gs) acc

832 | n == n' = Just (t, reverse acc ++ gs)

842 | n == n' = Just (t, reverse acc ++ gs)

833 find n (g : gs) acc = find n gs (g : acc)

843 find n (g : gs) acc = find n gs (g : acc)

834

844

@@ -876,13 +886,13 @@ dumpDecls [] = ""

876dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

886dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

877

887

878dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

888dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

879−dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

889+dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

880dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

890dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

881−dumpDecl (PData _ _ _ d) = showDImp True d

891+dumpDecl (PData _ _ _ _ d) = showDImp True d

882dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

892dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

883dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

893dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

884dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

894dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

885−dumpDecl (PClass _ _ cs n ps ds)

895+dumpDecl (PClass _ _ _ cs n ps ds)

886 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

896 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

887dumpDecl (PInstance _ _ cs n _ t _ ds)

897dumpDecl (PInstance _ _ cs n _ t _ ds)

888 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

898 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

src/Idris/AbsSyntaxTree.hs+68−54

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

57 idris_flags :: Ctxt [FnOpt],

58 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

59 idris_calledgraph :: Ctxt [Name],

60+ idris_docstrings :: Ctxt String,

60 idris_totcheck :: [(FC, Name)],

61 idris_totcheck :: [(FC, Name)],

61 idris_log :: String,

62 idris_log :: String,

62 idris_options :: IOption,

63 idris_options :: IOption,

@@ -120,12 +121,13 @@ data IBCWrite = IBCFix FixDecl

120 | IBCTotal Name Totality

121 | IBCTotal Name Totality

121 | IBCFlags Name [FnOpt]

122 | IBCFlags Name [FnOpt]

122 | IBCCG Name

123 | IBCCG Name

124+ | IBCDoc Name

123 | IBCDef Name -- i.e. main context

125 | IBCDef Name -- i.e. main context

124 deriving Show

126 deriving Show

125

127

126idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

128idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

127 emptyContext emptyContext emptyContext emptyContext

129 emptyContext emptyContext emptyContext emptyContext

128− emptyContext emptyContext emptyContext

130+ emptyContext emptyContext emptyContext emptyContext

129 [] "" defaultOpts 6 [] [] [] [] [] [] [] []

131 [] "" defaultOpts 6 [] [] [] [] [] [] [] []

130 [] Nothing Nothing [] [] [] Hidden False [] Nothing

132 [] Nothing Nothing [] [] [] Hidden False [] Nothing

131

133

@@ -241,24 +243,28 @@ deriving instance Binary Static

241

243

242-- Mark bindings with their explicitness, and laziness

244-- Mark bindings with their explicitness, and laziness

243data Plicity = Imp { plazy :: Bool,

245data Plicity = Imp { plazy :: Bool,

244− pstatic :: Static }

246+ pstatic :: Static,

247+ pdocstr :: String }

245 | Exp { plazy :: Bool,

248 | Exp { plazy :: Bool,

246− pstatic :: Static }

249+ pstatic :: Static,

250+ pdocstr :: String }

247 | Constraint { plazy :: Bool,

251 | Constraint { plazy :: Bool,

248− pstatic :: Static }

252+ pstatic :: Static,

253+ pdocstr :: String }

249 | TacImp { plazy :: Bool,

254 | TacImp { plazy :: Bool,

250 pstatic :: Static,

255 pstatic :: Static,

251− pscript :: PTerm }

256+ pscript :: PTerm,

257+ pdocstr :: String }

252 deriving (Show, Eq)

258 deriving (Show, Eq)

253

259

254{-!

260{-!

255deriving instance Binary Plicity

261deriving instance Binary Plicity

256!-}

262!-}

257

263

258−impl = Imp False Dynamic

264+impl = Imp False Dynamic ""

259−expl = Exp False Dynamic

265+expl = Exp False Dynamic ""

260−constraint = Constraint False Dynamic

266+constraint = Constraint False Dynamic ""

261−tacimpl = TacImp False Dynamic

267+tacimpl t = TacImp False Dynamic t ""

262

268

263data FnOpt = Inlinable | TotalFn | PartialFn

269data FnOpt = Inlinable | TotalFn | PartialFn

264 | Coinductive | AssertTotal | TCGen

270 | Coinductive | AssertTotal | TCGen

@@ -275,15 +281,15 @@ inlinable :: FnOpts -> Bool

275inlinable = elem Inlinable

281inlinable = elem Inlinable

276

282

277data PDecl' t = PFix FC Fixity [String] -- fixity declaration

283data PDecl' t = PFix FC Fixity [String] -- fixity declaration

278− | PTy SyntaxInfo FC FnOpts Name t -- type declaration

284+ | PTy String SyntaxInfo FC FnOpts Name t -- type declaration

279 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

285 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

280 | PCAF FC Name t -- top level constant

286 | PCAF FC Name t -- top level constant

281− | PData SyntaxInfo FC Bool -- codata

287+ | PData String SyntaxInfo FC Bool -- codata

282 (PData' t) -- data declaration

288 (PData' t) -- data declaration

283 | PParams FC [(Name, t)] [PDecl' t] -- params block

289 | PParams FC [(Name, t)] [PDecl' t] -- params block

284 | PNamespace String [PDecl' t] -- new namespace

290 | PNamespace String [PDecl' t] -- new namespace

285− | PRecord SyntaxInfo FC Name t Name t -- record declaration

291+ | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

286− | PClass SyntaxInfo FC

292+ | PClass String SyntaxInfo FC

287 [t] -- constraints

293 [t] -- constraints

288 Name

294 Name

289 [(Name, t)] -- parameters

295 [(Name, t)] -- parameters

@@ -314,7 +320,7 @@ deriving instance Binary PClause'

314

320

315data PData' t = PDatadecl { d_name :: Name,

321data PData' t = PDatadecl { d_name :: Name,

316 d_tcon :: t,

322 d_tcon :: t,

317− d_cons :: [(Name, t, FC)] }

323+ d_cons :: [(String, Name, t, FC)] }

318 | PLaterdecl { d_name :: Name, d_tcon :: t }

324 | PLaterdecl { d_name :: Name, d_tcon :: t }

319 deriving Functor

325 deriving Functor

320{-!

326{-!

@@ -332,21 +338,25 @@ type PClause = PClause' PTerm

332

338

333declared :: PDecl -> [Name]

339declared :: PDecl -> [Name]

334declared (PFix _ _ _) = []

340declared (PFix _ _ _) = []

335−declared (PTy _ _ _ n t) = [n]

341+declared (PTy _ _ _ _ n t) = [n]

336declared (PClauses _ _ n _) = [] -- not a declaration

342declared (PClauses _ _ n _) = [] -- not a declaration

343+declared (PRecord _ _ _ n _ _ c _) = [n, c]

337−declared (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

344+declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

338− where fstt (a, _, _) = a

345+ where fstt (_, a, _, _) = a

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

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

347+declared (PMutual _ ds) = concatMap declared ds

340declared (PNamespace _ ds) = concatMap declared ds

348declared (PNamespace _ ds) = concatMap declared ds

341-- declared (PImport _) = []

349-- declared (PImport _) = []

342

350

343defined :: PDecl -> [Name]

351defined :: PDecl -> [Name]

344defined (PFix _ _ _) = []

352defined (PFix _ _ _) = []

345−defined (PTy _ _ _ n t) = []

353+defined (PTy _ _ _ _ n t) = []

346defined (PClauses _ _ n _) = [n] -- not a declaration

354defined (PClauses _ _ n _) = [n] -- not a declaration

355+defined (PRecord _ _ _ n _ _ c _) = [n, c]

347−defined (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

356+defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

348− where fstt (a, _, _) = a

357+ where fstt (_, a, _, _) = a

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

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

359+defined (PMutual _ ds) = concatMap defined ds

350defined (PNamespace _ ds) = concatMap defined ds

360defined (PNamespace _ ds) = concatMap defined ds

351-- declared (PImport _) = []

361-- declared (PImport _) = []

352

362

@@ -486,31 +496,35 @@ type PDo = PDo' PTerm

486-- variables, e.g. a before (interpTy a).

496-- variables, e.g. a before (interpTy a).

487

497

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

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

489− lazyarg :: Bool, pname :: Name, getTm :: t }

499+ lazyarg :: Bool, pname :: Name, getTm :: t,

500+ pargdoc :: String }

490 | PExp { priority :: Int,

501 | PExp { priority :: Int,

491− lazyarg :: Bool, getTm :: t }

502+ lazyarg :: Bool, getTm :: t,

503+ pargdoc :: String }

492 | PConstraint { priority :: Int,

504 | PConstraint { priority :: Int,

493− lazyarg :: Bool, getTm :: t }

505+ lazyarg :: Bool, getTm :: t,

506+ pargdoc :: String }

494 | PTacImplicit { priority :: Int,

507 | PTacImplicit { priority :: Int,

495 lazyarg :: Bool, pname :: Name,

508 lazyarg :: Bool, pname :: Name,

496 getScript :: t,

509 getScript :: t,

497− getTm :: t }

510+ getTm :: t,

511+ pargdoc :: String }

498 deriving (Show, Eq, Functor)

512 deriving (Show, Eq, Functor)

499

513

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

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

501− size (PImp p l nm trm) = 1 + size nm + size trm

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

502− size (PExp p l trm) = 1 + size trm

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

503− size (PConstraint p l trm) = 1 + size trm

517+ size (PConstraint p l trm _) = 1 + size trm

504− size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

518+ size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

505

519

506{-!

520{-!

507deriving instance Binary PArg'

521deriving instance Binary PArg'

508!-}

522!-}

509

523

510−pimp = PImp 0 True

524+pimp n t = PImp 0 True n t ""

511−pexp = PExp 0 False

525+pexp t = PExp 0 False t ""

512−pconst = PConstraint 0 False

526+pconst t = PConstraint 0 False t ""

513−ptacimp = PTacImplicit 0 True

527+ptacimp n s t = PTacImplicit 0 True n s t ""

514

528

515type PArg = PArg' PTerm

529type PArg = PArg' PTerm

516

530

@@ -633,9 +647,9 @@ instance Show PData where

633 show d = showDImp False d

647 show d = showDImp False d

634

648

635showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

649showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

636−showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty

650+showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

637showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

651showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

638−showDeclImp _ (PData _ _ _ d) = show d

652+showDeclImp _ (PData _ _ _ _ d) = show d

639showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

653showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

640 showSep "\n" (map show ps)

654 showSep "\n" (map show ps)

641

655

@@ -659,21 +673,21 @@ showDImp :: Bool -> PData -> String

659showDImp impl (PDatadecl n ty cons)

673showDImp impl (PDatadecl n ty cons)

660 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

674 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

661 ++ showSep "\n\t| "

675 ++ showSep "\n\t| "

662− (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)

676+ (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)

663

677

664getImps :: [PArg] -> [(Name, PTerm)]

678getImps :: [PArg] -> [(Name, PTerm)]

665getImps [] = []

679getImps [] = []

666−getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs

680+getImps (PImp _ _ n tm _ : xs) = (n, tm) : getImps xs

667getImps (_ : xs) = getImps xs

681getImps (_ : xs) = getImps xs

668

682

669getExps :: [PArg] -> [PTerm]

683getExps :: [PArg] -> [PTerm]

670getExps [] = []

684getExps [] = []

671−getExps (PExp _ _ tm : xs) = tm : getExps xs

685+getExps (PExp _ _ tm _ : xs) = tm : getExps xs

672getExps (_ : xs) = getExps xs

686getExps (_ : xs) = getExps xs

673

687

674getConsts :: [PArg] -> [PTerm]

688getConsts :: [PArg] -> [PTerm]

675getConsts [] = []

689getConsts [] = []

676−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

690+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

677getConsts (_ : xs) = getConsts xs

691getConsts (_ : xs) = getConsts xs

678

692

679getAll :: [PArg] -> [PTerm]

693getAll :: [PArg] -> [PTerm]

@@ -711,7 +725,7 @@ prettyImp impl = prettySe 10

711 else

725 else

712 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

726 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

713 prettySe 10 sc

727 prettySe 10 sc

714− prettySe p (PPi (Exp l s) n ty sc)

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

715 | n `elem` allNamesIn sc || impl =

729 | n `elem` allNamesIn sc || impl =

716 let open = if l then text "|" <> lparen else lparen in

730 let open = if l then text "|" <> lparen else lparen in

717 bracket p 2 $

731 bracket p 2 $

@@ -732,7 +746,7 @@ prettyImp impl = prettySe 10

732 case s of

746 case s of

733 Static -> text "[static]"

747 Static -> text "[static]"

734 _ -> empty

748 _ -> empty

735− prettySe p (PPi (Imp l s) n ty sc)

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

736 | impl =

750 | impl =

737 let open = if l then text "|" <> lbrace else lbrace in

751 let open = if l then text "|" <> lbrace else lbrace in

738 bracket p 2 $

752 bracket p 2 $

@@ -748,13 +762,13 @@ prettyImp impl = prettySe 10

748 case s of

762 case s of

749 Static -> text $ "[static]"

763 Static -> text $ "[static]"

750 _ -> empty

764 _ -> empty

751− prettySe p (PPi (Constraint _ _) n ty sc) =

765+ prettySe p (PPi (Constraint _ _ _) n ty sc) =

752 bracket p 2 $

766 bracket p 2 $

753 if size sc > breakingSize then

767 if size sc > breakingSize then

754 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

768 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

755 else

769 else

756 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc

770 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc

757− prettySe p (PPi (TacImp _ _ s) n ty sc) =

771+ prettySe p (PPi (TacImp _ _ s _) n ty sc) =

758 bracket p 2 $

772 bracket p 2 $

759 if size sc > breakingSize then

773 if size sc > breakingSize then

760 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

774 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

@@ -846,10 +860,10 @@ prettyImp impl = prettySe 10

846

860

847 prettySe p _ = text "test"

861 prettySe p _ = text "test"

848

862

849− prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)

863+ prettyArgS (PImp _ _ n tm _) = prettyArgSi (n, tm)

850− prettyArgS (PExp _ _ tm) = prettyArgSe tm

864+ prettyArgS (PExp _ _ tm _) = prettyArgSe tm

851− prettyArgS (PConstraint _ _ tm) = prettyArgSc tm

865+ prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm

852− prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)

866+ prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)

853

867

854 prettyArgSe arg = prettySe 0 arg

868 prettyArgSe arg = prettySe 0 arg

855 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

869 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

@@ -874,7 +888,7 @@ showImp impl tm = se 10 tm where

874 ++ se 10 sc

888 ++ se 10 sc

875 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

889 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

876 " in " ++ se 10 sc

890 " in " ++ se 10 sc

877− se p (PPi (Exp l s) n ty sc)

891+ se p (PPi (Exp l s _) n ty sc)

878 | n `elem` allNamesIn sc || impl

892 | n `elem` allNamesIn sc || impl

879 = bracket p 2 $

893 = bracket p 2 $

880 if l then "|(" else "(" ++

894 if l then "|(" else "(" ++

@@ -885,7 +899,7 @@ showImp impl tm = se 10 tm where

885 where st = case s of

899 where st = case s of

886 Static -> "[static] "

900 Static -> "[static] "

887 _ -> ""

901 _ -> ""

888− se p (PPi (Imp l s) n ty sc)

902+ se p (PPi (Imp l s _) n ty sc)

889 | impl = bracket p 2 $ if l then "|{" else "{" ++

903 | impl = bracket p 2 $ if l then "|{" else "{" ++

890 show n ++ " : " ++ se 10 ty ++

904 show n ++ " : " ++ se 10 ty ++

891 "} " ++ st ++ "-> " ++ se 10 sc

905 "} " ++ st ++ "-> " ++ se 10 sc

@@ -893,9 +907,9 @@ showImp impl tm = se 10 tm where

893 where st = case s of

907 where st = case s of

894 Static -> "[static] "

908 Static -> "[static] "

895 _ -> ""

909 _ -> ""

896− se p (PPi (Constraint _ _) n ty sc)

910+ se p (PPi (Constraint _ _ _) n ty sc)

897 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

911 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

898− se p (PPi (TacImp _ _ s) n ty sc)

912+ se p (PPi (TacImp _ _ s _) n ty sc)

899 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc

913 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc

900 se p (PApp _ (PRef _ f) [])

914 se p (PApp _ (PRef _ f) [])

901 | not impl = show f

915 | not impl = show f

@@ -933,10 +947,10 @@ showImp impl tm = se 10 tm where

933 se p (PElabError s) = show s

947 se p (PElabError s) = show s

934-- se p x = "Not implemented"

948-- se p x = "Not implemented"

935

949

936− sArg (PImp _ _ n tm) = siArg (n, tm)

950+ sArg (PImp _ _ n tm _) = siArg (n, tm)

937− sArg (PExp _ _ tm) = seArg tm

951+ sArg (PExp _ _ tm _) = seArg tm

938− sArg (PConstraint _ _ tm) = scArg tm

952+ sArg (PConstraint _ _ tm _) = scArg tm

939− sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)

953+ sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)

940

954

941 seArg arg = " " ++ se 0 arg

955 seArg arg = " " ++ se 0 arg

942 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

956 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

src/Idris/Delaborate.hs+4−4

@@ -66,10 +66,10 @@ delab' ist tm fullname = de [] tm

66 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

67 | otherwise = PApp un (PRef un n) (map pexp args)

69− imp (PImp p l n _) arg = PImp p l n arg

69+ imp (PImp p l n _ d) arg = PImp p l n arg d

70− imp (PExp p l _) arg = PExp p l arg

70+ imp (PExp p l _ d) arg = PExp p l arg d

71− imp (PConstraint p l _) arg = PConstraint p l arg

71+ imp (PConstraint p l _ d) arg = PConstraint p l arg d

72− imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

72+ imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

74pshow :: IState -> Err -> String

75pshow i (Msg s) = s

src/Idris/ElabDecls.hs+69−62

@@ -38,8 +38,9 @@ checkDef fc ns = do ctxt <- getContext

38 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

39 return (n, t')) ns

41−elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()

41+elabType :: ElabInfo -> SyntaxInfo -> String ->

42+ FC -> FnOpts -> Name -> PTerm -> Idris ()

42−elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

43+elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

43 n = liftname info n_in in -}

44 n = liftname info n_in in -}

44 do checkUndefined fc n

45 do checkUndefined fc n

45 ctxt <- getContext

46 ctxt <- getContext

@@ -75,8 +76,8 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

75 when corec $ do setAccessibility n Frozen

76 when corec $ do setAccessibility n Frozen

76 addIBC (IBCAccess n Frozen)

77 addIBC (IBCAccess n Frozen)

78−elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()

79+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

79−elabData info syn fc codata (PLaterdecl n t_in)

80+elabData info syn doc fc codata (PLaterdecl n t_in)

80 = do iLOG (show fc)

81 = do iLOG (show fc)

81 checkUndefined fc n

82 checkUndefined fc n

82 ctxt <- getContext

83 ctxt <- getContext

@@ -92,7 +93,7 @@ elabData info syn fc codata (PLaterdecl n t_in)

92 logLvl 2 $ "---> " ++ show cty

93 logLvl 2 $ "---> " ++ show cty

93 updateContext (addTyDecl n cty) -- temporary, to check cons

94 updateContext (addTyDecl n cty) -- temporary, to check cons

95−elabData info syn fc codata (PDatadecl n t_in dcons)

96+elabData info syn doc fc codata (PDatadecl n t_in dcons)

96 = do iLOG (show fc)

97 = do iLOG (show fc)

97 undef <- isUndefined fc n

98 undef <- isUndefined fc n

98 ctxt <- getContext

99 ctxt <- getContext

@@ -119,10 +120,10 @@ elabData info syn fc codata (PDatadecl n t_in dcons)

119 updateContext (addDatatype (Data n ttag cty cons))

120 updateContext (addDatatype (Data n ttag cty cons))

120 mapM_ (checkPositive n) cons

121 mapM_ (checkPositive n) cons

121

122

122−elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

123+elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

123− PTerm -> Name -> PTerm -> Idris ()

124+ PTerm -> String -> Name -> PTerm -> Idris ()

124−elabRecord info syn fc tyn ty cn cty

125+elabRecord info syn doc fc tyn ty cdoc cn cty

125− = do elabData info syn fc False (PDatadecl tyn ty [(cn, cty, fc)])

126+ = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

126 cty' <- implicit syn cn cty

127 cty' <- implicit syn cn cty

127 i <- get

128 i <- get

128 cty <- case lookupTy Nothing cn (tt_ctxt i) of

129 cty <- case lookupTy Nothing cn (tt_ctxt i) of

@@ -145,7 +146,7 @@ elabRecord info syn fc tyn ty cn cty

145 where

146 where

146-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

147-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

147

148

148− isNonImp (PExp _ _ _, a) = Just a

149+ isNonImp (PExp _ _ _ _, a) = Just a

149 isNonImp _ = Nothing

150 isNonImp _ = Nothing

150

151

151 tryElabDecl info (fn, ty, val)

152 tryElabDecl info (fn, ty, val)

@@ -157,15 +158,15 @@ elabRecord info syn fc tyn ty cn cty

157 show fn ++ " (" ++ show ty ++ ")"

158 show fn ++ " (" ++ show ty ++ ")"

158 put i)

159 put i)

159

160

160− getImplB k (PPi (Imp l s) n Placeholder sc)

161+ getImplB k (PPi (Imp l s _) n Placeholder sc)

161 = getImplB k sc

162 = getImplB k sc

162− getImplB k (PPi (Imp l s) n ty sc)

163+ getImplB k (PPi (Imp l s d) n ty sc)

163− = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc

164+ = getImplB (\x -> k (PPi (Imp l s d) n ty x)) sc

164 getImplB k (PPi _ n ty sc)

165 getImplB k (PPi _ n ty sc)

165 = getImplB k sc

166 = getImplB k sc

166 getImplB k _ = k

167 getImplB k _ = k

167

168

168− renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)

169+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

169 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

170 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

170 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

171 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

171 renameBs _ t = t

172 renameBs _ t = t

@@ -192,7 +193,7 @@ elabRecord info syn fc tyn ty cn cty

192

193

193 mkProj recty substs cimp ((pn_in, pty), pos)

194 mkProj recty substs cimp ((pn_in, pty), pos)

194 = do let pn = expandNS syn pn_in

195 = do let pn = expandNS syn pn_in

195− let pfnTy = PTy defaultSyntax fc [] pn

196+ let pfnTy = PTy "" defaultSyntax fc [] pn

196 (PPi expl rec recty

197 (PPi expl rec recty

197 (substMatches substs pty))

198 (substMatches substs pty))

198 let pls = repeat Placeholder

199 let pls = repeat Placeholder

@@ -213,7 +214,7 @@ elabRecord info syn fc tyn ty cn cty

213 let valname = MN 0 "updateval"

214 let valname = MN 0 "updateval"

214 let pt = k (PPi expl pn pty

215 let pt = k (PPi expl pn pty

215 (PPi expl rec recty recty))

216 (PPi expl rec recty recty))

216− let pfnTy = PTy defaultSyntax fc [] setname pt

217+ let pfnTy = PTy "" defaultSyntax fc [] setname pt

217 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]

218 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]

218 let lhsArgs = pls

219 let lhsArgs = pls

219 let rhsArgs = take pos pls ++ (PRef fc valname) :

220 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -228,8 +229,9 @@ elabRecord info syn fc tyn ty cn cty

228 (map pexp rhsArgs)) []

229 (map pexp rhsArgs)) []

229 return (pn, pfnTy, PClauses fc [] setname [pclause])

230 return (pn, pfnTy, PClauses fc [] setname [pclause])

230

231

231−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (Name, PTerm, FC) -> Idris (Name, Type)

232+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

233+ (String, Name, PTerm, FC) -> Idris (Name, Type)

232−elabCon info syn tn codata (n, t_in, fc)

234+elabCon info syn tn codata (doc, n, t_in, fc)

233 = do checkUndefined fc n

235 = do checkUndefined fc n

234 ctxt <- getContext

236 ctxt <- getContext

235 i <- get

237 i <- get

@@ -620,10 +622,10 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

620

622

621data MArgTy = IA | EA | CA deriving Show

623data MArgTy = IA | EA | CA deriving Show

622

624

623−elabClass :: ElabInfo -> SyntaxInfo ->

625+elabClass :: ElabInfo -> SyntaxInfo -> String ->

624 FC -> [PTerm] ->

626 FC -> [PTerm] ->

625 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

627 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

626−elabClass info syn fc constraints tn ps ds

628+elabClass info syn doc fc constraints tn ps ds

627 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

629 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

628 let tty = pibind ps PSet

630 let tty = pibind ps PSet

629 let constraint = PApp fc (PRef fc tn)

631 let constraint = PApp fc (PRef fc tn)

@@ -635,12 +637,14 @@ elabClass info syn fc constraints tn ps ds

635 ims <- mapM (tdecl mnames) mdecls

637 ims <- mapM (tdecl mnames) mdecls

636 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

638 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

637 (filter clause ds)

639 (filter clause ds)

638− let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)

640+ let (methods, imethods)

641+ = unzip (map (\ ( x,y,z) -> (x, y)) ims)

639− let cty = impbind ps $ conbind constraints $ pibind methods constraint

642+ let cty = impbind ps $ conbind constraints

643+ $ pibind methods constraint

640− let cons = [(cn, cty, fc)]

644+ let cons = [("", cn, cty, fc)]

641 let ddecl = PDatadecl tn tty cons

645 let ddecl = PDatadecl tn tty cons

642 logLvl 5 $ "Class data " ++ showDImp True ddecl

646 logLvl 5 $ "Class data " ++ showDImp True ddecl

643− elabData info (syn { no_imp = no_imp syn ++ mnames }) fc False ddecl

647+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl

644 -- for each constraint, build a top level function to chase it

648 -- for each constraint, build a top level function to chase it

645 logLvl 5 $ "Building functions"

649 logLvl 5 $ "Building functions"

646 let usyn = syn { using = ps ++ using syn }

650 let usyn = syn { using = ps ++ using syn }

@@ -653,9 +657,10 @@ elabClass info syn fc constraints tn ps ds

653 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

657 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

654 i <- get

658 i <- get

655 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

659 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

656− addClass tn (CI cn imethods defaults (map fst ps) [])

660+ addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])

657 addIBC (IBCClass tn)

661 addIBC (IBCClass tn)

658 where

662 where

663+ nodoc (n, (_, o, t)) = (n, (o, t))

659 pibind [] x = x

664 pibind [] x = x

660 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

665 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

661 impbind [] x = x

666 impbind [] x = x

@@ -663,12 +668,12 @@ elabClass info syn fc constraints tn ps ds

663 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

668 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

664 conbind [] x = x

669 conbind [] x = x

665

670

666− getMName (PTy _ _ _ n _) = nsroot n

671+ getMName (PTy _ _ _ _ n _) = nsroot n

667− tdecl allmeths (PTy syn _ o n t)

672+ tdecl allmeths (PTy doc syn _ o n t)

668 = do t' <- implicit' syn allmeths n t

673 = do t' <- implicit' syn allmeths n t

669 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'

674 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'

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

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

671− (n, (o, (toExp (map fst ps) Imp t'))),

676+ (n, (doc, o, (toExp (map fst ps) Imp t'))),

672 (n, (syn, o, t) ) )

677 (n, (syn, o, t) ) )

673 tdecl _ _ = fail "Not allowed in a class declaration"

678 tdecl _ _ = fail "Not allowed in a class declaration"

674

679

@@ -677,7 +682,7 @@ elabClass info syn fc constraints tn ps ds

677 case lookup n mtys of

682 case lookup n mtys of

678 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

683 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

679 let ds = map (decorateid defaultdec)

684 let ds = map (decorateid defaultdec)

680− [PTy syn fc [] n ty',

685+ [PTy "" syn fc [] n ty',

681 PClauses fc (TCGen:o ++ opts) n cs]

686 PClauses fc (TCGen:o ++ opts) n cs]

682 iLOG (show ds)

687 iLOG (show ds)

683 return (n, ((defaultdec n, ds!!1), ds))

688 return (n, ((defaultdec n, ds!!1), ds))

@@ -687,7 +692,7 @@ elabClass info syn fc constraints tn ps ds

687 defaultdec (UN n) = UN ("default#" ++ n)

692 defaultdec (UN n) = UN ("default#" ++ n)

688 defaultdec (NS n ns) = NS (defaultdec n) ns

693 defaultdec (NS n ns) = NS (defaultdec n) ns

689

694

690− tydecl (PTy _ _ _ _ _) = True

695+ tydecl (PTy _ _ _ _ _ _) = True

691 tydecl _ = False

696 tydecl _ = False

692 clause (PClauses _ _ _ _) = True

697 clause (PClauses _ _ _ _) = True

693 clause _ = False

698 clause _ = False

@@ -711,10 +716,10 @@ elabClass info syn fc constraints tn ps ds

711 addInstance False conn' cfn

716 addInstance False conn' cfn

712 addIBC (IBCInstance False conn' cfn)

717 addIBC (IBCInstance False conn' cfn)

713-- iputStrLn ("Added " ++ show (conn, cfn, ty))

718-- iputStrLn ("Added " ++ show (conn, cfn, ty))

714− return [PTy syn fc [] cfn ty,

719+ return [PTy "" syn fc [] cfn ty,

715 PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

720 PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

716

721

717− tfun cn c syn all (m, (o, ty))

722+ tfun cn c syn all (m, (doc, o, ty))

718 = do let ty' = insertConstraint c ty

723 = do let ty' = insertConstraint c ty

719 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

724 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

720 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

725 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

@@ -725,12 +730,12 @@ elabClass info syn fc constraints tn ps ds

725 iLOG (showImp True ty)

730 iLOG (showImp True ty)

726 iLOG (show (m, ty', capp, margs))

731 iLOG (show (m, ty', capp, margs))

727 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

732 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

728− return [PTy syn fc o m ty',

733+ return [PTy doc syn fc o m ty',

729 PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]

734 PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]

730

735

731− getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

736+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

732− getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

737+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

733− getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

738+ getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

734 getMArgs _ = []

739 getMArgs _ = []

735

740

736 getMeth (m:ms) (a:as) x | x == a = PRef fc m

741 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -746,14 +751,14 @@ elabClass info syn fc constraints tn ps ds

746 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

751 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

747 rhsArgs [] _ = []

752 rhsArgs [] _ = []

748

753

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

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

750 = PPi p n ty (insertConstraint c sc)

755 = PPi p n ty (insertConstraint c sc)

751 insertConstraint c sc = PPi constraint (MN 0 "c") c sc

756 insertConstraint c sc = PPi constraint (MN 0 "c") c sc

752

757

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

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

754− toExp ns e (PPi (Imp l s) n ty sc)

759+ toExp ns e (PPi (Imp l s _) n ty sc)

755 | n `elem` ns = toExp ns e sc

760 | n `elem` ns = toExp ns e sc

756− | otherwise = PPi (e l s) n ty (toExp ns e sc)

761+ | otherwise = PPi (e l s "") n ty (toExp ns e sc)

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

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

758 toExp ns e sc = sc

763 toExp ns e sc = sc

759

764

@@ -778,7 +783,7 @@ elabInstance info syn fc cs n ps t expn ds

778 Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)

783 Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)

779 addInstance intInst n iname

784 addInstance intInst n iname

780 Just _ -> addInstance intInst n iname

785 Just _ -> addInstance intInst n iname

781− elabType info syn fc [] iname t

786+ elabType info syn "" fc [] iname t

782 let ips = zip (class_params ci) ps

787 let ips = zip (class_params ci) ps

783 let ns = case n of

788 let ns = case n of

784 NS n ns' -> ns'

789 NS n ns' -> ns'

@@ -836,17 +841,19 @@ elabInstance info syn fc cs n ps t expn ds

836 getRetType (PPi _ _ _ sc) = getRetType sc

841 getRetType (PPi _ _ _ sc) = getRetType sc

837 getRetType t = t

842 getRetType t = t

838

843

844+ mkMethApp (n, _, _, ty)

839− mkMethApp (n, _, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

845+ = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

840− lamBind i (PPi (Constraint _ _) _ _ sc) sc'

846+ lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'

841− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

847+ = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

848+ lamBind i (PPi _ n ty sc) sc'

842− lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

849+ = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

843 lamBind i _ sc = sc

850 lamBind i _ sc = sc

844− methArgs i (PPi (Imp _ _) n ty sc)

851+ methArgs i (PPi (Imp _ _ _) n ty sc)

845− = PImp 0 False n (PRef fc (MN i "meth")) : methArgs (i+1) sc

852+ = PImp 0 False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

846− methArgs i (PPi (Exp _ _) n ty sc)

853+ methArgs i (PPi (Exp _ _ _) n ty sc)

847− = PExp 0 False (PRef fc (MN i "meth")) : methArgs (i+1) sc

854+ = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

848− methArgs i (PPi (Constraint _ _) n ty sc)

855+ methArgs i (PPi (Constraint _ _ _) n ty sc)

849− = PConstraint 0 False (PResolveTC fc) : methArgs (i+1) sc

856+ = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

850 methArgs i _ = []

857 methArgs i _ = []

851

858

852 papp fc f [] = f

859 papp fc f [] = f

@@ -865,12 +872,12 @@ elabInstance info syn fc cs n ps t expn ds

865 decorate ns iname (UN n) = NS (UN ('!':n)) ns

872 decorate ns iname (UN n) = NS (UN ('!':n)) ns

866 decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns

873 decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns

867

874

868− mkTyDecl (n, op, t, _) = PTy syn fc op n t

875+ mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

869

876

870 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

877 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

871 conbind [] x = x

878 conbind [] x = x

872

879

873− coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc)

880+ coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

874 coninsert cs sc = conbind cs sc

881 coninsert cs sc = conbind cs sc

875

882

876 insertDefaults :: IState -> Name ->

883 insertDefaults :: IState -> Name ->

@@ -903,7 +910,7 @@ elabInstance info syn fc cs n ps t expn ds

903 = decorate ns iname m == decorate ns iname m'

910 = decorate ns iname m == decorate ns iname m'

904 clauseFor m iname ns _ = False

911 clauseFor m iname ns _ = False

905

912

906−decorateid decorate (PTy s f o n t) = PTy s f o (decorate n) t

913+decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

907decorateid decorate (PClauses f o n cs)

914decorateid decorate (PClauses f o n cs)

908 = PClauses f o (decorate n) (map dc cs)

915 = PClauses f o (decorate n) (map dc cs)

909 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

916 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

@@ -947,17 +954,17 @@ elabDecl' _ info (PFix _ _ _)

947 = return () -- nothing to elaborate

954 = return () -- nothing to elaborate

948elabDecl' _ info (PSyntax _ p)

955elabDecl' _ info (PSyntax _ p)

949 = return () -- nothing to elaborate

956 = return () -- nothing to elaborate

950−elabDecl' what info (PTy s f o n ty)

957+elabDecl' what info (PTy doc s f o n ty)

951 | what /= EDefns

958 | what /= EDefns

952 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

959 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

953− elabType info s f o n ty

960+ elabType info s doc f o n ty

954−elabDecl' what info (PData s f co d)

961+elabDecl' what info (PData doc s f co d)

955 | what /= ETypes

962 | what /= ETypes

956 = do iLOG $ "Elaborating " ++ show (d_name d)

963 = do iLOG $ "Elaborating " ++ show (d_name d)

957− elabData info s f co d

964+ elabData info s doc f co d

958 | otherwise

965 | otherwise

959 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

966 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

960− elabData info s f co (PLaterdecl (d_name d) (d_tcon d))

967+ elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))

961elabDecl' what info d@(PClauses f o n ps)

968elabDecl' what info d@(PClauses f o n ps)

962 | what /= ETypes

969 | what /= ETypes

963 = do iLOG $ "Elaborating clause " ++ show n

970 = do iLOG $ "Elaborating clause " ++ show n

@@ -988,18 +995,18 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

988 ninfo = case namespace info of

995 ninfo = case namespace info of

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

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

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

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

991−elabDecl' what info (PClass s f cs n ps ds)

998+elabDecl' what info (PClass doc s f cs n ps ds)

992 | what /= EDefns

999 | what /= EDefns

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

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

994− elabClass info s f cs n ps ds

1001+ elabClass info s doc f cs n ps ds

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

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

996 | what /= ETypes

1003 | what /= ETypes

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

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

998 elabInstance info s f cs n ps t expn ds

1005 elabInstance info s f cs n ps t expn ds

999−elabDecl' what info (PRecord s f tyn ty cn cty)

1006+elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

1000 | what /= EDefns

1007 | what /= EDefns

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

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

1002− elabRecord info s f tyn ty cn cty

1009+ elabRecord info s doc f tyn ty cdoc cn cty

1003elabDecl' _ info (PDSL n dsl)

1010elabDecl' _ info (PDSL n dsl)

1004 = do i <- get

1011 = do i <- get

1005 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

1012 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

src/Idris/ElabTerm.hs+3−3

@@ -262,7 +262,7 @@ elab ist info pattern tcgen fn tm

262 mapM_ (\n -> do focus n

263 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

264 resolveTC 7 fn ist) (ivs' \\ ivs)

265− where tcArg (n, PConstraint _ _ Placeholder) = True

265+ where tcArg (n, PConstraint _ _ Placeholder _) = True

266 tcArg _ = False

267

268 elab' ina@(_, a) (PApp fc f [arg])

@@ -469,7 +469,7 @@ resolveTC depth fn ist

469 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

470 -- if there's any arguments left, we've failed to resolve

471 solve

472− where isImp (PImp p _ _ _) = (True, p)

472+ where isImp (PImp p _ _ _ _) = (True, p)

473 isImp arg = (False, priority arg)

474

475collectDeferred :: Term -> State [(Name, Type)] Term

@@ -515,7 +515,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

515 [(n, args)] -> return $ (n, map isImp args)

516 ns <- apply (Var fn') (map (\x -> (x, 0)) imps)

517 when autoSolve solveAll

518− where isImp (PImp _ _ _ _) = True

518+ where isImp (PImp _ _ _ _ _) = True

519 isImp _ = False

520 envArgs n = do e <- get_env

521 case lookup n e of

src/Idris/IBC.hs+78−29

@@ -21,7 +21,7 @@ import System.Directory

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 22

24+ibcVersion = 23

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -43,13 +43,15 @@ data IBCFile = IBCFile { ver :: Word8,

43 ibc_total :: [(Name, Totality)],

44 ibc_flags :: [(Name, [FnOpt])],

45 ibc_cg :: [(Name, CGInfo)],

46− ibc_defs :: [(Name, Def)] }

46+ ibc_defs :: [(Name, Def)],

47+ ibc_docstrings :: [(Name, String)]

48+ }

47{-!

49{-!

48deriving instance Binary IBCFile

50deriving instance Binary IBCFile

49!-}

51!-}

51initIBC :: IBCFile

53initIBC :: IBCFile

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

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

54loadIBC :: FilePath -> Idris ()

56loadIBC :: FilePath -> Idris ()

55loadIBC fp = do iLOG $ "Loading ibc " ++ fp

57loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -111,6 +113,9 @@ ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

111ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

113ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

112 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

114 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

113 _ -> fail "IBC write failed"

115 _ -> fail "IBC write failed"

116+ibc i (IBCDoc n) f = case lookupCtxt Nothing n (idris_docstrings i) of

117+ [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

118+ _ -> fail "IBC write failed"

114ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of

119ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of

115 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

120 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

116 _ -> fail "IBC write failed"

121 _ -> fail "IBC write failed"

@@ -145,6 +150,7 @@ process i fn

145 pAccess (ibc_access i)

150 pAccess (ibc_access i)

146 pTotal (ibc_total i)

151 pTotal (ibc_total i)

147 pCG (ibc_cg i)

152 pCG (ibc_cg i)

153+ pDocs (ibc_docstrings i)

148

154

149timestampOlder :: FilePath -> FilePath -> IO ()

155timestampOlder :: FilePath -> FilePath -> IO ()

150timestampOlder src ibc = do srct <- getModificationTime src

156timestampOlder src ibc = do srct <- getModificationTime src

@@ -243,6 +249,9 @@ pDefs ds = mapM_ (\ (n, d) ->

243 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

249 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

244 ds

250 ds

245

251

252+pDocs :: [(Name, String)] -> Idris ()

253+pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

254+

246pAccess :: [(Name, Accessibility)] -> Idris ()

255pAccess :: [(Name, Accessibility)] -> Idris ()

247pAccess ds = mapM_ (\ (n, a) ->

256pAccess ds = mapM_ (\ (n, a) ->

248 do i <- getIState

257 do i <- getIState

@@ -707,7 +716,7 @@ instance Binary Totality where

707 _ -> error "Corrupted binary data for Totality"

716 _ -> error "Corrupted binary data for Totality"

708

717

709instance Binary IBCFile where

718instance Binary IBCFile where

710− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21)

719+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22)

711 = do put x1

720 = do put x1

712 put x2

721 put x2

713 put x3

722 put x3

@@ -729,6 +738,7 @@ instance Binary IBCFile where

729 put x19

738 put x19

730 put x20

739 put x20

731 put x21

740 put x21

741+ put x22

732 get

742 get

733 = do x1 <- get

743 = do x1 <- get

734 if x1 == ibcVersion then

744 if x1 == ibcVersion then

@@ -752,7 +762,8 @@ instance Binary IBCFile where

752 x19 <- get

762 x19 <- get

753 x20 <- get

763 x20 <- get

754 x21 <- get

764 x21 <- get

765+ x22 <- get

755− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21)

766+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22)

756 else return (initIBC { ver = x1 })

767 else return (initIBC { ver = x1 })

757

768

758instance Binary FnOpt where

769instance Binary FnOpt where

@@ -830,35 +841,47 @@ instance Binary Static where

830instance Binary Plicity where

841instance Binary Plicity where

831 put x

842 put x

832 = case x of

843 = case x of

844+ Imp x1 x2 x3 ->

833− Imp x1 x2 -> do putWord8 0

845+ do putWord8 0

834 put x1

846 put x1

835 put x2

847 put x2

848+ put x3

849+ Exp x1 x2 x3 ->

836− Exp x1 x2 -> do putWord8 1

850+ do putWord8 1

837 put x1

851 put x1

838 put x2

852 put x2

853+ put x3

839− Constraint x1 x2 -> do putWord8 2

854+ Constraint x1 x2 x3 ->

855+ do putWord8 2

840 put x1

856 put x1

841 put x2

857 put x2

858+ put x3

842− TacImp x1 x2 x3 -> do putWord8 3

859+ TacImp x1 x2 x3 x4 ->

860+ do putWord8 3

843 put x1

861 put x1

844 put x2

862 put x2

845 put x3

863 put x3

864+ put x4

846 get

865 get

847 = do i <- getWord8

866 = do i <- getWord8

848 case i of

867 case i of

849 0 -> do x1 <- get

868 0 -> do x1 <- get

850 x2 <- get

869 x2 <- get

870+ x3 <- get

851− return (Imp x1 x2)

871+ return (Imp x1 x2 x3)

852 1 -> do x1 <- get

872 1 -> do x1 <- get

853 x2 <- get

873 x2 <- get

874+ x3 <- get

854− return (Exp x1 x2)

875+ return (Exp x1 x2 x3)

855 2 -> do x1 <- get

876 2 -> do x1 <- get

856 x2 <- get

877 x2 <- get

878+ x3 <- get

857− return (Constraint x1 x2)

879+ return (Constraint x1 x2 x3)

858 3 -> do x1 <- get

880 3 -> do x1 <- get

859 x2 <- get

881 x2 <- get

860 x3 <- get

882 x3 <- get

883+ x4 <- get

861− return (TacImp x1 x2 x3)

884+ return (TacImp x1 x2 x3 x4)

862 _ -> error "Corrupted binary data for Plicity"

885 _ -> error "Corrupted binary data for Plicity"

863

886

864

887

@@ -869,22 +892,26 @@ instance (Binary t) => Binary (PDecl' t) where

869 put x1

892 put x1

870 put x2

893 put x2

871 put x3

894 put x3

872− PTy x1 x2 x3 x4 x5 -> do putWord8 1

895+ PTy x1 x2 x3 x4 x5 x6

896+ -> do putWord8 1

873 put x1

897 put x1

874 put x2

898 put x2

875 put x3

899 put x3

876 put x4

900 put x4

877 put x5

901 put x5

902+ put x6

878 PClauses x1 x2 x3 x4 -> do putWord8 2

903 PClauses x1 x2 x3 x4 -> do putWord8 2

879 put x1

904 put x1

880 put x2

905 put x2

881 put x3

906 put x3

882 put x4

907 put x4

883− PData x1 x2 x3 x4 -> do putWord8 3

908+ PData x1 x2 x3 x4 x5 ->

909+ do putWord8 3

884 put x1

910 put x1

885 put x2

911 put x2

886 put x3

912 put x3

887 put x4

913 put x4

914+ put x5

888 PParams x1 x2 x3 -> do putWord8 4

915 PParams x1 x2 x3 -> do putWord8 4

889 put x1

916 put x1

890 put x2

917 put x2

@@ -892,20 +919,25 @@ instance (Binary t) => Binary (PDecl' t) where

892 PNamespace x1 x2 -> do putWord8 5

919 PNamespace x1 x2 -> do putWord8 5

893 put x1

920 put x1

894 put x2

921 put x2

895− PRecord x1 x2 x3 x4 x5 x6 -> do putWord8 6

922+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 ->

923+ do putWord8 6

896 put x1

924 put x1

897 put x2

925 put x2

898 put x3

926 put x3

899 put x4

927 put x4

900 put x5

928 put x5

901 put x6

929 put x6

930+ put x7

931+ put x8

902− PClass x1 x2 x3 x4 x5 x6 -> do putWord8 7

932+ PClass x1 x2 x3 x4 x5 x6 x7

933+ -> do putWord8 7

903 put x1

934 put x1

904 put x2

935 put x2

905 put x3

936 put x3

906 put x4

937 put x4

907 put x5

938 put x5

908 put x6

939 put x6

940+ put x7

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

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

910 put x1

942 put x1

911 put x2

943 put x2

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

937 x3 <- get

969 x3 <- get

938 x4 <- get

970 x4 <- get

939 x5 <- get

971 x5 <- get

972+ x6 <- get

940− return (PTy x1 x2 x3 x4 x5)

973+ return (PTy x1 x2 x3 x4 x5 x6)

941 2 -> do x1 <- get

974 2 -> do x1 <- get

942 x2 <- get

975 x2 <- get

943 x3 <- get

976 x3 <- get

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

947 x2 <- get

980 x2 <- get

948 x3 <- get

981 x3 <- get

949 x4 <- get

982 x4 <- get

983+ x5 <- get

950− return (PData x1 x2 x3 x4)

984+ return (PData x1 x2 x3 x4 x5)

951 4 -> do x1 <- get

985 4 -> do x1 <- get

952 x2 <- get

986 x2 <- get

953 x3 <- get

987 x3 <- get

@@ -961,14 +995,17 @@ instance (Binary t) => Binary (PDecl' t) where

961 x4 <- get

995 x4 <- get

962 x5 <- get

996 x5 <- get

963 x6 <- get

997 x6 <- get

998+ x7 <- get

999+ x8 <- get

964− return (PRecord x1 x2 x3 x4 x5 x6)

1000+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

965 7 -> do x1 <- get

1001 7 -> do x1 <- get

966 x2 <- get

1002 x2 <- get

967 x3 <- get

1003 x3 <- get

968 x4 <- get

1004 x4 <- get

969 x5 <- get

1005 x5 <- get

970 x6 <- get

1006 x6 <- get

1007+ x7 <- get

971− return (PClass x1 x2 x3 x4 x5 x6)

1008+ return (PClass x1 x2 x3 x4 x5 x6 x7)

972 8 -> do x1 <- get

1009 8 -> do x1 <- get

973 x2 <- get

1010 x2 <- get

974 x3 <- get

1011 x3 <- get

@@ -1370,25 +1407,33 @@ instance (Binary t) => Binary (PDo' t) where

1370instance (Binary t) => Binary (PArg' t) where

1407instance (Binary t) => Binary (PArg' t) where

1371 put x

1408 put x

1372 = case x of

1409 = case x of

1373− PImp x1 x2 x3 x4 -> do putWord8 0

1410+ PImp x1 x2 x3 x4 x5 ->

1411+ do putWord8 0

1374 put x1

1412 put x1

1375 put x2

1413 put x2

1376 put x3

1414 put x3

1377 put x4

1415 put x4

1416+ put x5

1417+ PExp x1 x2 x3 x4 ->

1378− PExp x1 x2 x3 -> do putWord8 1

1418+ do putWord8 1

1379 put x1

1419 put x1

1380 put x2

1420 put x2

1381 put x3

1421 put x3

1422+ put x4

1382− PConstraint x1 x2 x3 -> do putWord8 2

1423+ PConstraint x1 x2 x3 x4 ->

1424+ do putWord8 2

1383 put x1

1425 put x1

1384 put x2

1426 put x2

1385 put x3

1427 put x3

1428+ put x4

1386− PTacImplicit x1 x2 x3 x4 x5 -> do putWord8 3

1429+ PTacImplicit x1 x2 x3 x4 x5 x6 ->

1430+ do putWord8 3

1387 put x1

1431 put x1

1388 put x2

1432 put x2

1389 put x3

1433 put x3

1390 put x4

1434 put x4

1391 put x5

1435 put x5

1436+ put x6

1392 get

1437 get

1393 = do i <- getWord8

1438 = do i <- getWord8

1394 case i of

1439 case i of

@@ -1396,21 +1441,25 @@ instance (Binary t) => Binary (PArg' t) where

1396 x2 <- get

1441 x2 <- get

1397 x3 <- get

1442 x3 <- get

1398 x4 <- get

1443 x4 <- get

1444+ x5 <- get

1399− return (PImp x1 x2 x3 x4)

1445+ return (PImp x1 x2 x3 x4 x5)

1400 1 -> do x1 <- get

1446 1 -> do x1 <- get

1401 x2 <- get

1447 x2 <- get

1402 x3 <- get

1448 x3 <- get

1449+ x4 <- get

1403− return (PExp x1 x2 x3)

1450+ return (PExp x1 x2 x3 x4)

1404 2 -> do x1 <- get

1451 2 -> do x1 <- get

1405 x2 <- get

1452 x2 <- get

1406 x3 <- get

1453 x3 <- get

1454+ x4 <- get

1407− return (PConstraint x1 x2 x3)

1455+ return (PConstraint x1 x2 x3 x4)

1408 3 -> do x1 <- get

1456 3 -> do x1 <- get

1409 x2 <- get

1457 x2 <- get

1410 x3 <- get

1458 x3 <- get

1411 x4 <- get

1459 x4 <- get

1412 x5 <- get

1460 x5 <- get

1461+ x6 <- get

1413− return (PTacImplicit x1 x2 x3 x4 x5)

1462+ return (PTacImplicit x1 x2 x3 x4 x5 x6)

1414 _ -> error "Corrupted binary data for PArg'"

1463 _ -> error "Corrupted binary data for PArg'"

1415

1464

1416

1465

src/Idris/Parser.hs+29−23

@@ -273,7 +273,11 @@ pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

273 where dot '.' = '/'

274 dot c = c

275

276+-- a program is a list of declarations, possibly with associated

277+-- documentation strings

278+

276−parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]

279+parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->

280+ Idris [PDecl]

277parseProg syn fname input pos

281parseProg syn fname input pos

278 = do i <- get

282 = do i <- get

279 case runParser (do setPosition pos

283 case runParser (do setPosition pos

@@ -308,7 +312,8 @@ collect (c@(PClauses _ o _ _) : ds)

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

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

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

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

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

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

315+collect (PClass doc f s cs n ps ds : ds')

311−collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

316+ = PClass doc f s cs n ps (collect ds) : collect ds'

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

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

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

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

314collect (d : ds) = d : collect ds

319collect (d : ds) = d : collect ds

@@ -433,7 +438,7 @@ pFunDecl' syn = try (do pushIndent

433 pTerminator

438 pTerminator

434-- ty' <- implicit syn n ty

439-- ty' <- implicit syn n ty

435 addAcc n acc

440 addAcc n acc

436− return (PTy syn fc opts' n ty))

441+ return (PTy "" syn fc opts' n ty))

437 <|> try (pPattern syn)

442 <|> try (pPattern syn)

438 <|> try (pCAF syn)

443 <|> try (pCAF syn)

439

444

@@ -507,7 +512,7 @@ pClass syn = do acc <- pAccessibility

507 closeBlock

512 closeBlock

508 let allDs = concat ds

513 let allDs = concat ds

509 accData acc n (concatMap declared allDs)

514 accData acc n (concatMap declared allDs)

510− return [PClass syn fc cons n cs allDs]

515+ return [PClass "" syn fc cons n cs allDs]

511 where

516 where

512 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

517 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

513 return (i, ty)

518 return (i, ty)

@@ -902,7 +907,7 @@ pPi syn =

902 lchar '('; xt <- tyDeclList syn; lchar ')'

907 lchar '('; xt <- tyDeclList syn; lchar ')'

903 symbol "->"

908 symbol "->"

904 sc <- pExpr syn

909 sc <- pExpr syn

905− return (bindList (PPi (Exp lazy st)) xt sc))

910+ return (bindList (PPi (Exp lazy st "")) xt sc))

906 <|> try (if implicitAllowed syn

911 <|> try (if implicitAllowed syn

907 then do lazy <- option False (do lchar '|'

912 then do lazy <- option False (do lchar '|'

908 return True)

913 return True)

@@ -912,7 +917,7 @@ pPi syn =

912 lchar '}'

917 lchar '}'

913 symbol "->"

918 symbol "->"

914 sc <- pExpr syn

919 sc <- pExpr syn

915− return (bindList (PPi (Imp lazy st)) xt sc)

920+ return (bindList (PPi (Imp lazy st "")) xt sc)

916 else fail "No implicit arguments allowed here")

921 else fail "No implicit arguments allowed here")

917 <|> try (do lchar '{'

922 <|> try (do lchar '{'

918 reserved "auto"

923 reserved "auto"

@@ -920,7 +925,8 @@ pPi syn =

920 lchar '}'

925 lchar '}'

921 symbol "->"

926 symbol "->"

922 sc <- pExpr syn

927 sc <- pExpr syn

928+ return (bindList (PPi

923− return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))

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

924 <|> try (do lchar '{'

930 <|> try (do lchar '{'

925 reserved "default"

931 reserved "default"

926 script <- pSimpleExpr syn

932 script <- pSimpleExpr syn

@@ -928,7 +934,7 @@ pPi syn =

928 lchar '}'

934 lchar '}'

929 symbol "->"

935 symbol "->"

930 sc <- pExpr syn

936 sc <- pExpr syn

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

937+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

932 <|> do --lazy <- option False (do lchar '|'; return True)

938 <|> do --lazy <- option False (do lchar '|'; return True)

933 lchar '{'

939 lchar '{'

934 reserved "static"

940 reserved "static"

@@ -936,7 +942,7 @@ pPi syn =

936 t <- pExpr' syn

942 t <- pExpr' syn

937 symbol "->"

943 symbol "->"

938 sc <- pExpr syn

944 sc <- pExpr syn

939− return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)

945+ return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)

940

946

941pConstList :: SyntaxInfo -> IParser [PTerm]

947pConstList :: SyntaxInfo -> IParser [PTerm]

942pConstList syn = try (do lchar '('

948pConstList syn = try (do lchar '('

@@ -1096,7 +1102,7 @@ pRecord syn = do acc <- pAccessibility

1096 reserved "where"

1102 reserved "where"

1097 openBlock

1103 openBlock

1098 pushIndent

1104 pushIndent

1099− (cn, cty, _) <- pConstructor syn

1105+ (cdoc, cn, cty, _) <- pConstructor syn

1100 pKeepTerminator

1106 pKeepTerminator

1101 popIndent

1107 popIndent

1102 closeBlock

1108 closeBlock

@@ -1105,7 +1111,7 @@ pRecord syn = do acc <- pAccessibility

1105 syn_namespace syn }

1111 syn_namespace syn }

1106 let fns = getRecNames rsyn cty

1112 let fns = getRecNames rsyn cty

1107 mapM_ (\n -> addAcc n (toFreeze acc)) fns

1113 mapM_ (\n -> addAcc n (toFreeze acc)) fns

1108− return $ PRecord rsyn fc tyn ty cn cty

1114+ return $ PRecord "" rsyn fc tyn ty cdoc cn cty

1109 where

1115 where

1110 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]

1116 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]

1111 ++ getRecNames syn sc

1117 ++ getRecNames syn sc

@@ -1124,7 +1130,7 @@ pData syn = try (do acc <- pAccessibility

1124 tyn_in <- pfName

1130 tyn_in <- pfName

1125 ty <- pTSig (impOK syn)

1131 ty <- pTSig (impOK syn)

1126 let tyn = expandNS syn tyn_in

1132 let tyn = expandNS syn tyn_in

1127− option (PData syn fc co (PLaterdecl tyn ty)) (do

1133+ option (PData "" syn fc co (PLaterdecl tyn ty)) (do

1128 reserved "where"

1134 reserved "where"

1129 openBlock

1135 openBlock

1130 pushIndent

1136 pushIndent

@@ -1134,8 +1140,8 @@ pData syn = try (do acc <- pAccessibility

1134 return c) -- (lchar '|')

1140 return c) -- (lchar '|')

1135 popIndent

1141 popIndent

1136 closeBlock

1142 closeBlock

1137− accData acc tyn (map (\ (n, _, _) -> n) cons)

1143+ accData acc tyn (map (\ (_, n, _, _) -> n) cons)

1138− return $ PData syn fc co (PDatadecl tyn ty cons)))

1144+ return $ PData "" syn fc co (PDatadecl tyn ty cons)))

1139 <|> try (do pushIndent

1145 <|> try (do pushIndent

1140 acc <- pAccessibility

1146 acc <- pAccessibility

1141 co <- pDataI

1147 co <- pDataI

@@ -1144,16 +1150,16 @@ pData syn = try (do acc <- pAccessibility

1144 args <- many pName

1150 args <- many pName

1145 let ty = bindArgs (map (const PSet) args) PSet

1151 let ty = bindArgs (map (const PSet) args) PSet

1146 let tyn = expandNS syn tyn_in

1152 let tyn = expandNS syn tyn_in

1147− option (PData syn fc co (PLaterdecl tyn ty)) (do

1153+ option (PData "" syn fc co (PLaterdecl tyn ty)) (do

1148 lchar '='

1154 lchar '='

1149 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1155 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1150 pTerminator

1156 pTerminator

1151 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

1157 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

1152− cons' <- mapM (\ (x, cargs, cfc) ->

1158+ cons' <- mapM (\ (doc, x, cargs, cfc) ->

1153 do let cty = bindArgs cargs conty

1159 do let cty = bindArgs cargs conty

1154− return (x, cty, cfc)) cons

1160+ return (doc, x, cty, cfc)) cons

1155− accData acc tyn (map (\ (n, _, _) -> n) cons')

1161+ accData acc tyn (map (\ (_, n, _, _) -> n) cons')

1156− return $ PData syn fc co (PDatadecl tyn ty cons')))

1162+ return $ PData "" syn fc co (PDatadecl tyn ty cons')))

1157 where

1163 where

1158 mkPApp fc t [] = t

1164 mkPApp fc t [] = t

1159 mkPApp fc t xs = PApp fc t (map pexp xs)

1165 mkPApp fc t xs = PApp fc t (map pexp xs)

@@ -1161,23 +1167,23 @@ pData syn = try (do acc <- pAccessibility

1161bindArgs :: [PTerm] -> PTerm -> PTerm

1167bindArgs :: [PTerm] -> PTerm -> PTerm

1162bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

1168bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

1163

1169

1164−pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1170+pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)

1165pConstructor syn

1171pConstructor syn

1166 = do cn_in <- pfName; fc <- pfc

1172 = do cn_in <- pfName; fc <- pfc

1167 let cn = expandNS syn cn_in

1173 let cn = expandNS syn cn_in

1168 ty <- pTSig (impOK syn)

1174 ty <- pTSig (impOK syn)

1169-- ty' <- implicit syn cn ty

1175-- ty' <- implicit syn cn ty

1170− return (cn, ty, fc)

1176+ return ("", cn, ty, fc)

1171

1177

1172

1178

1173−pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

1179+pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)

1174pSimpleCon syn

1180pSimpleCon syn

1175 = do cn_in <- pfName

1181 = do cn_in <- pfName

1176 let cn = expandNS syn cn_in

1182 let cn = expandNS syn cn_in

1177 fc <- pfc

1183 fc <- pfc

1178 args <- many (do notEndApp

1184 args <- many (do notEndApp

1179 pSimpleExpr syn)

1185 pSimpleExpr syn)

1180− return (cn, args, fc)

1186+ return ("", cn, args, fc)

1181

1187

1182--------- DSL syntax overloading ---------

1188--------- DSL syntax overloading ---------

1183

1189

src/Idris/Primitives.hs+1−1

@@ -281,7 +281,7 @@ elabPrim (Prim n ty i def sc tot)

281

282elabPrims :: Idris ()

283elabPrims = do mapM_ (elabDecl EAll toplevel)

284− (map (PData defaultSyntax (FC "builtin" 0) False)

284+ (map (PData "" defaultSyntax (FC "builtin" 0) False)

285 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

286 mapM_ elabPrim primitives

287

test/test018/expected−100

@@ -14,502 +14,402 @@ Received

14Hello to you too!

15Finished

16100

17−Waiting for message

18Sent ping

17Sent ping

19Received Hello!

18Received Hello!

20Reply: Hello back!

19Reply: Hello back!

2199

2099

22−Waiting for message

23Sent ping

21Sent ping

24Received Hello!

22Received Hello!

25Reply: Hello back!

23Reply: Hello back!

2698

2498

27−Waiting for message

28Sent ping

25Sent ping

29Received Hello!

26Received Hello!

30Reply: Hello back!

27Reply: Hello back!

3197

2897

32−Waiting for message

33Sent ping

29Sent ping

34Received Hello!

30Received Hello!

35Reply: Hello back!

31Reply: Hello back!

3696

3296

37−Waiting for message

38Sent ping

33Sent ping

39Received Hello!

34Received Hello!

40Reply: Hello back!

35Reply: Hello back!

4195

3695

42−Waiting for message

43Sent ping

37Sent ping

44Received Hello!

38Received Hello!

45Reply: Hello back!

39Reply: Hello back!

4694

4094

47−Waiting for message

48Sent ping

41Sent ping

49Received Hello!

42Received Hello!

50Reply: Hello back!

43Reply: Hello back!

5193

4493

52−Waiting for message

53Sent ping

45Sent ping

54Received Hello!

46Received Hello!

55Reply: Hello back!

47Reply: Hello back!

5692

4892

57−Waiting for message

58Sent ping

49Sent ping

59Received Hello!

50Received Hello!

60Reply: Hello back!

51Reply: Hello back!

6191

5291

62−Waiting for message

63Sent ping

53Sent ping

64Received Hello!

54Received Hello!

65Reply: Hello back!

55Reply: Hello back!

6690

5690

67−Waiting for message

68Sent ping

57Sent ping

69Received Hello!

58Received Hello!

70Reply: Hello back!

59Reply: Hello back!

7189

6089

72−Waiting for message

73Sent ping

61Sent ping

74Received Hello!

62Received Hello!

75Reply: Hello back!

63Reply: Hello back!

7688

6488

77−Waiting for message

78Sent ping

65Sent ping

79Received Hello!

66Received Hello!

80Reply: Hello back!

67Reply: Hello back!

8187

6887

82−Waiting for message

83Sent ping

69Sent ping

84Received Hello!

70Received Hello!

85Reply: Hello back!

71Reply: Hello back!

8686

7286

87−Waiting for message

88Sent ping

73Sent ping

89Received Hello!

74Received Hello!

90Reply: Hello back!

75Reply: Hello back!

9185

7685

92−Waiting for message

93Sent ping

77Sent ping

94Received Hello!

78Received Hello!

95Reply: Hello back!

79Reply: Hello back!

9684

8084

97−Waiting for message

98Sent ping

81Sent ping

99Received Hello!

82Received Hello!

100Reply: Hello back!

83Reply: Hello back!

10183

8483

102−Waiting for message

103Sent ping

85Sent ping

104Received Hello!

86Received Hello!

105Reply: Hello back!

87Reply: Hello back!

10682

8882

107−Waiting for message

108Sent ping

89Sent ping

109Received Hello!

90Received Hello!

110Reply: Hello back!

91Reply: Hello back!

11181

9281

112−Waiting for message

113Sent ping

93Sent ping

114Received Hello!

94Received Hello!

115Reply: Hello back!

95Reply: Hello back!

11680

9680

117−Waiting for message

118Sent ping

97Sent ping

119Received Hello!

98Received Hello!

120Reply: Hello back!

99Reply: Hello back!

12179

10079

122−Waiting for message

123Sent ping

101Sent ping

124Received Hello!

102Received Hello!

125Reply: Hello back!

103Reply: Hello back!

12678

10478

127−Waiting for message

128Sent ping

105Sent ping

129Received Hello!

106Received Hello!

130Reply: Hello back!

107Reply: Hello back!

13177

10877

132−Waiting for message

133Sent ping

109Sent ping

134Received Hello!

110Received Hello!

135Reply: Hello back!

111Reply: Hello back!

13676

11276

137−Waiting for message

138Sent ping

113Sent ping

139Received Hello!

114Received Hello!

140Reply: Hello back!

115Reply: Hello back!

14175

11675

142−Waiting for message

143Sent ping

117Sent ping

144Received Hello!

118Received Hello!

145Reply: Hello back!

119Reply: Hello back!

14674

12074

147−Waiting for message

148Sent ping

121Sent ping

149Received Hello!

122Received Hello!

150Reply: Hello back!

123Reply: Hello back!

15173

12473

152−Waiting for message

153Sent ping

125Sent ping

154Received Hello!

126Received Hello!

155Reply: Hello back!

127Reply: Hello back!

15672

12872

157−Waiting for message

158Sent ping

129Sent ping

159Received Hello!

130Received Hello!

160Reply: Hello back!

131Reply: Hello back!

16171

13271

162−Waiting for message

163Sent ping

133Sent ping

164Received Hello!

134Received Hello!

165Reply: Hello back!

135Reply: Hello back!

16670

13670

167−Waiting for message

168Sent ping

137Sent ping

169Received Hello!

138Received Hello!

170Reply: Hello back!

139Reply: Hello back!

17169

14069

172−Waiting for message

173Sent ping

141Sent ping

174Received Hello!

142Received Hello!

175Reply: Hello back!

143Reply: Hello back!

17668

14468

177−Waiting for message

178Sent ping

145Sent ping

179Received Hello!

146Received Hello!

180Reply: Hello back!

147Reply: Hello back!

18167

14867

182−Waiting for message

183Sent ping

149Sent ping

184Received Hello!

150Received Hello!

185Reply: Hello back!

151Reply: Hello back!

18666

15266

187−Waiting for message

188Sent ping

153Sent ping

189Received Hello!

154Received Hello!

190Reply: Hello back!

155Reply: Hello back!

19165

15665

192−Waiting for message

193Sent ping

157Sent ping

194Received Hello!

158Received Hello!

195Reply: Hello back!

159Reply: Hello back!

19664

16064

197−Waiting for message

198Sent ping

161Sent ping

199Received Hello!

162Received Hello!

200Reply: Hello back!

163Reply: Hello back!

20163

16463

202−Waiting for message

203Sent ping

165Sent ping

204Received Hello!

166Received Hello!

205Reply: Hello back!

167Reply: Hello back!

20662

16862

207−Waiting for message

208Sent ping

169Sent ping

209Received Hello!

170Received Hello!

210Reply: Hello back!

171Reply: Hello back!

21161

17261

212−Waiting for message

213Sent ping

173Sent ping

214Received Hello!

174Received Hello!

215Reply: Hello back!

175Reply: Hello back!

21660

17660

217−Waiting for message

218Sent ping

177Sent ping

219Received Hello!

178Received Hello!

220Reply: Hello back!

179Reply: Hello back!

22159

18059

222−Waiting for message

223Sent ping

181Sent ping

224Received Hello!

182Received Hello!

225Reply: Hello back!

183Reply: Hello back!

22658

18458

227−Waiting for message

228Sent ping

185Sent ping

229Received Hello!

186Received Hello!

230Reply: Hello back!

187Reply: Hello back!

23157

18857

232−Waiting for message

233Sent ping

189Sent ping

234Received Hello!

190Received Hello!

235Reply: Hello back!

191Reply: Hello back!

23656

19256

237−Waiting for message

238Sent ping

193Sent ping

239Received Hello!

194Received Hello!

240Reply: Hello back!

195Reply: Hello back!

24155

19655

242−Waiting for message

243Sent ping

197Sent ping

244Received Hello!

198Received Hello!

245Reply: Hello back!

199Reply: Hello back!

24654

20054

247−Waiting for message

248Sent ping

201Sent ping

249Received Hello!

202Received Hello!

250Reply: Hello back!

203Reply: Hello back!

25153

20453

252−Waiting for message

253Sent ping

205Sent ping

254Received Hello!

206Received Hello!

255Reply: Hello back!

207Reply: Hello back!

25652

20852

257−Waiting for message

258Sent ping

209Sent ping

259Received Hello!

210Received Hello!

260Reply: Hello back!

211Reply: Hello back!

26151

21251

262−Waiting for message

263Sent ping

213Sent ping

264Received Hello!

214Received Hello!

265Reply: Hello back!

215Reply: Hello back!

26650

21650

267−Waiting for message

268Sent ping

217Sent ping

269Received Hello!

218Received Hello!

270Reply: Hello back!

219Reply: Hello back!

27149

22049

272−Waiting for message

273Sent ping

221Sent ping

274Received Hello!

222Received Hello!

275Reply: Hello back!

223Reply: Hello back!

27648

22448

277−Waiting for message

278Sent ping

225Sent ping

279Received Hello!

226Received Hello!

280Reply: Hello back!

227Reply: Hello back!

28147

22847

282−Waiting for message

283Sent ping

229Sent ping

284Received Hello!

230Received Hello!

285Reply: Hello back!

231Reply: Hello back!

28646

23246

287−Waiting for message

288Sent ping

233Sent ping

289Received Hello!

234Received Hello!

290Reply: Hello back!

235Reply: Hello back!

29145

23645

292−Waiting for message

293Sent ping

237Sent ping

294Received Hello!

238Received Hello!

295Reply: Hello back!

239Reply: Hello back!

29644

24044

297−Waiting for message

298Sent ping

241Sent ping

299Received Hello!

242Received Hello!

300Reply: Hello back!

243Reply: Hello back!

30143

24443

302−Waiting for message

303Sent ping

245Sent ping

304Received Hello!

246Received Hello!

305Reply: Hello back!

247Reply: Hello back!

30642

24842

307−Waiting for message

308Sent ping

249Sent ping

309Received Hello!

250Received Hello!

310Reply: Hello back!

251Reply: Hello back!

31141

25241

312−Waiting for message

313Sent ping

253Sent ping

314Received Hello!

254Received Hello!

315Reply: Hello back!

255Reply: Hello back!

31640

25640

317−Waiting for message

318Sent ping

257Sent ping

319Received Hello!

258Received Hello!

320Reply: Hello back!

259Reply: Hello back!

32139

26039

322−Waiting for message

323Sent ping

261Sent ping

324Received Hello!

262Received Hello!

325Reply: Hello back!

263Reply: Hello back!

32638

26438

327−Waiting for message

328Sent ping

265Sent ping

329Received Hello!

266Received Hello!

330Reply: Hello back!

267Reply: Hello back!

33137

26837

332−Waiting for message

333Sent ping

269Sent ping

334Received Hello!

270Received Hello!

335Reply: Hello back!

271Reply: Hello back!

33636

27236

337−Waiting for message

338Sent ping

273Sent ping

339Received Hello!

274Received Hello!

340Reply: Hello back!

275Reply: Hello back!

34135

27635

342−Waiting for message

343Sent ping

277Sent ping

344Received Hello!

278Received Hello!

345Reply: Hello back!

279Reply: Hello back!

34634

28034

347−Waiting for message

348Sent ping

281Sent ping

349Received Hello!

282Received Hello!

350Reply: Hello back!

283Reply: Hello back!

35133

28433

352−Waiting for message

353Sent ping

285Sent ping

354Received Hello!

286Received Hello!

355Reply: Hello back!

287Reply: Hello back!

35632

28832

357−Waiting for message

358Sent ping

289Sent ping

359Received Hello!

290Received Hello!

360Reply: Hello back!

291Reply: Hello back!

36131

29231

362−Waiting for message

363Sent ping

293Sent ping

364Received Hello!

294Received Hello!

365Reply: Hello back!

295Reply: Hello back!

36630

29630

367−Waiting for message

368Sent ping

297Sent ping

369Received Hello!

298Received Hello!

370Reply: Hello back!

299Reply: Hello back!

37129

30029

372−Waiting for message

373Sent ping

301Sent ping

374Received Hello!

302Received Hello!

375Reply: Hello back!

303Reply: Hello back!

37628

30428

377−Waiting for message

378Sent ping

305Sent ping

379Received Hello!

306Received Hello!

380Reply: Hello back!

307Reply: Hello back!

38127

30827

382−Waiting for message

383Sent ping

309Sent ping

384Received Hello!

310Received Hello!

385Reply: Hello back!

311Reply: Hello back!

38626

31226

387−Waiting for message

388Sent ping

313Sent ping

389Received Hello!

314Received Hello!

390Reply: Hello back!

315Reply: Hello back!

39125

31625

392−Waiting for message

393Sent ping

317Sent ping

394Received Hello!

318Received Hello!

395Reply: Hello back!

319Reply: Hello back!

39624

32024

397−Waiting for message

398Sent ping

321Sent ping

399Received Hello!

322Received Hello!

400Reply: Hello back!

323Reply: Hello back!

40123

32423

402−Waiting for message

403Sent ping

325Sent ping

404Received Hello!

326Received Hello!

405Reply: Hello back!

327Reply: Hello back!

40622

32822

407−Waiting for message

408Sent ping

329Sent ping

409Received Hello!

330Received Hello!

410Reply: Hello back!

331Reply: Hello back!

41121

33221

412−Waiting for message

413Sent ping

333Sent ping

414Received Hello!

334Received Hello!

415Reply: Hello back!

335Reply: Hello back!

41620

33620

417−Waiting for message

418Sent ping

337Sent ping

419Received Hello!

338Received Hello!

420Reply: Hello back!

339Reply: Hello back!

42119

34019

422−Waiting for message

423Sent ping

341Sent ping

424Received Hello!

342Received Hello!

425Reply: Hello back!

343Reply: Hello back!

42618

34418

427−Waiting for message

428Sent ping

345Sent ping

429Received Hello!

346Received Hello!

430Reply: Hello back!

347Reply: Hello back!

43117

34817

432−Waiting for message

433Sent ping

349Sent ping

434Received Hello!

350Received Hello!

435Reply: Hello back!

351Reply: Hello back!

43616

35216

437−Waiting for message

438Sent ping

353Sent ping

439Received Hello!

354Received Hello!

440Reply: Hello back!

355Reply: Hello back!

44115

35615

442−Waiting for message

443Sent ping

357Sent ping

444Received Hello!

358Received Hello!

445Reply: Hello back!

359Reply: Hello back!

44614

36014

447−Waiting for message

448Sent ping

361Sent ping

449Received Hello!

362Received Hello!

450Reply: Hello back!

363Reply: Hello back!

45113

36413

452−Waiting for message

453Sent ping

365Sent ping

454Received Hello!

366Received Hello!

455Reply: Hello back!

367Reply: Hello back!

45612

36812

457−Waiting for message

458Sent ping

369Sent ping

459Received Hello!

370Received Hello!

460Reply: Hello back!

371Reply: Hello back!

46111

37211

462−Waiting for message

463Sent ping

373Sent ping

464Received Hello!

374Received Hello!

465Reply: Hello back!

375Reply: Hello back!

46610

37610

467−Waiting for message

468Sent ping

377Sent ping

469Received Hello!

378Received Hello!

470Reply: Hello back!

379Reply: Hello back!

4719

3809

472−Waiting for message

473Sent ping

381Sent ping

474Received Hello!

382Received Hello!

475Reply: Hello back!

383Reply: Hello back!

4768

3848

477−Waiting for message

478Sent ping

385Sent ping

479Received Hello!

386Received Hello!

480Reply: Hello back!

387Reply: Hello back!

4817

3887

482−Waiting for message

483Sent ping

389Sent ping

484Received Hello!

390Received Hello!

485Reply: Hello back!

391Reply: Hello back!

4866

3926

487−Waiting for message

488Sent ping

393Sent ping

489Received Hello!

394Received Hello!

490Reply: Hello back!

395Reply: Hello back!

4915

3965

492−Waiting for message

493Sent ping

397Sent ping

494Received Hello!

398Received Hello!

495Reply: Hello back!

399Reply: Hello back!

4964

4004

497−Waiting for message

498Sent ping

401Sent ping

499Received Hello!

402Received Hello!

500Reply: Hello back!

403Reply: Hello back!

5013

4043

502−Waiting for message

503Sent ping

405Sent ping

504Received Hello!

406Received Hello!

505Reply: Hello back!

407Reply: Hello back!

5062

4082

507−Waiting for message

508Sent ping

409Sent ping

509Received Hello!

410Received Hello!

510Reply: Hello back!

411Reply: Hello back!

5111

4121

512−Waiting for message

513Sent ping

413Sent ping

514Received Hello!

414Received Hello!

515Reply: Hello back!

415Reply: Hello back!