git.iko.soy/Idris-dev
on master help sign in
Add field for documentation comments in abstract syntax
commit8464bc4566d166785b9ce607ca897fde13d749d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Nov 2012, 16:31 (14 years ago) parent96f3b9e
10 files changed+314−319
compare with master
unifiedsplit
src/Core/CoreParser.hs+10−1 src/Idris/AbsSyntax.hs+52−42 src/Idris/AbsSyntaxTree.hs+68−54 src/Idris/Delaborate.hs+4−4 src/Idris/ElabDecls.hs+69−62 src/Idris/ElabTerm.hs+3−3 src/Idris/IBC.hs+78−29 src/Idris/Parser.hs+29−23 src/Idris/Primitives.hs+1−1 test/test018/expected−100
src/Core/CoreParser.hs+10−1
@@ -1,7 +1,7 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
22
33module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4− idrisLexer, maybeWithNS) where
4+ idrisLexer, maybeWithNS, pDocComment) where
55
66import Core.TT
77
@@ -123,6 +123,15 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
123123 (x, "") -> [x]
124124 (x, '.':y) -> x : parseNS y
125125
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+
126135pDef :: CParser a (Name, RDef)
127136pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
128137 lchar '='
src/Idris/AbsSyntax.hs+52−42
@@ -68,8 +68,14 @@ getTotality n
6868 _ -> return (Total [])
6969
7070addToCG :: Name -> CGInfo -> Idris ()
71−addToCG n cg = do i <- get
72− put (i { idris_callgraph = addDef n cg (idris_callgraph i) })
71+addToCG n cg
72+ = do i <- get
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) })
7379
7480addToCalledG :: Name -> [Name] -> Idris ()
7581addToCalledG n ns = return () -- TODO
@@ -360,7 +366,7 @@ inferTy = MN 0 "__Infer"
360366inferCon = MN 0 "__infer"
361367inferDecl = PDatadecl inferTy
362368 PSet
363− [(inferCon, PPi impl (MN 0 "A") PSet (
369+ [("", inferCon, PPi impl (MN 0 "A") PSet (
364370 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
365371 (PRef bi inferTy)), bi)]
366372
@@ -384,7 +390,7 @@ primNames = [unitTy, unitCon,
384390unitTy = MN 0 "__Unit"
385391unitCon = MN 0 "__II"
386392unitDecl = PDatadecl unitTy PSet
387− [(unitCon, PRef bi unitTy, bi)]
393+ [("", unitCon, PRef bi unitTy, bi)]
388394
389395falseTy = MN 0 "__False"
390396falseDecl = PDatadecl falseTy PSet []
@@ -392,7 +398,7 @@ falseDecl = PDatadecl falseTy PSet []
392398pairTy = MN 0 "__Pair"
393399pairCon = MN 0 "__MkPair"
394400pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
395− [(pairCon, PPi impl (n "A") PSet (
401+ [("", pairCon, PPi impl (n "A") PSet (
396402 PPi impl (n "B") PSet (
397403 PPi expl (n "a") (PRef bi (n "A")) (
398404 PPi expl (n "b") (PRef bi (n "B"))
@@ -405,7 +411,7 @@ eqCon = UN "refl"
405411eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
406412 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
407413 PSet)
408− [(eqCon, PPi impl (n "a") PSet (
414+ [("", eqCon, PPi impl (n "a") PSet (
409415 PPi impl (n "x") (PRef bi (n "a"))
410416 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
411417 pimp (n "b") Placeholder,
@@ -484,10 +490,10 @@ expandParams dec ps ns tm = en tm
484490
485491expandParamsD :: IState ->
486492 (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)
488494 = if n `elem` ns
489− then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
490− else PTy syn fc o n (expandParams dec ps ns ty)
495+ then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
496+ else PTy doc syn fc o n (expandParams dec ps ns ty)
491497expandParamsD ist dec ps ns (PClauses fc opts n cs)
492498 = let n' = if n `elem` ns then dec n else n in
493499 PClauses fc opts n' (map expandParamsC cs)
@@ -512,7 +518,8 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
512518 updateps yn nm (((a, t), i):as)
513519 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
514520 | 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)
516523 where
517524 -- just do the type decl, leave constructors alone (parameters will be
518525 -- added implicitly)
@@ -520,12 +527,15 @@ expandParamsD ist dec ps ns (PData syn fc co pd) = PData syn fc co (expandPData
520527 = if n `elem` ns
521528 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)
522529 else PDatadecl n (expandParams dec ps ns ty) (map econ cons)
523− econ (n, t, fc) = (dec n, piBindp expl ps (expandParams dec ps ns t), fc)
530+ econ (doc, n, t, fc)
531+ = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)
524532expandParamsD ist dec ps ns (PParams f params pds)
525533 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params) pds
526534-- (map (expandParamsD ist dec ps ns) pds)
527−expandParamsD ist dec ps ns (PClass info f cs n params decls)
528− = PClass info f
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)
538+ = PClass doc info f
529539 (map (expandParams dec ps ns) cs)
530540 n
531541 (map (mapsnd (expandParams dec ps ns)) params)
@@ -638,34 +648,34 @@ implicitise syn ignore ist tm
638648 = do (decls, ns) <- get
639649 let isn = concatMap (namesIn uvars ist) (map getTm as)
640650 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)
642652 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
643653 (decls , ns) <- get
644− put (PImp (getPriority ist ty) l n ty : decls,
654+ put (PImp (getPriority ist ty) l n ty doc : decls,
645655 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
646656 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)
648658 = do let isn = nub (namesIn uvars ist ty ++ case sc of
649659 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
650660 _ -> [])
651661 (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,
653663 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
654664 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)
656666 = do let isn = nub (namesIn uvars ist ty ++ case sc of
657667 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
658668 _ -> [])
659669 (decls, ns) <- get -- ignore decls in HO types
660− put (PConstraint 10 l ty : decls,
670+ put (PConstraint 10 l ty doc : decls,
661671 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
662672 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)
664674 = do let isn = nub (namesIn uvars ist ty ++ case sc of
665675 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
666676 _ -> [])
667677 (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,
669679 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
670680 imps True (n:env) sc
671681 imps top env (PEq _ l r)
@@ -700,8 +710,8 @@ implicitise syn ignore ist tm
700710 pibind using [] sc = sc
701711 pibind using (n:ns) sc
702712 = case lookup n using of
703− Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
704− Nothing -> PPi (Imp False Dynamic) n Placeholder
713+ Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
714+ Nothing -> PPi (Imp False Dynamic "") n Placeholder
705715 (pibind using ns sc)
706716
707717-- Add implicit arguments in function calls
@@ -781,7 +791,7 @@ aiFn inpat True ist fc f []
781791 || any constructor alts || any allImp ialts)
782792 then aiFn inpat False ist fc f [] -- use it as a constructor
783793 else Right $ PPatvar fc f
784− where imp (PExp _ _ _) = False
794+ where imp (PExp _ _ _ _) = False
785795 imp _ = True
786796 allImp [] = False
787797 allImp xs = all imp xs
@@ -806,29 +816,29 @@ aiFn inpat expat ist fc f as
806816 (insertImpl ns as)) alts
807817 where
808818 insertImpl :: [PArg] -> [PArg] -> [PArg]
809− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
810− PExp p l tm : insertImpl ps given
811− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
812− PConstraint p l tm : insertImpl ps given
813− insertImpl (PConstraint p l ty : ps) given =
814− PConstraint p l (PResolveTC fc) : insertImpl ps given
815− insertImpl (PImp p l n ty : ps) given =
819+ insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
820+ PExp p l tm d : insertImpl ps given
821+ insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
822+ PConstraint p l tm d : insertImpl ps given
823+ insertImpl (PConstraint p l ty d : ps) given =
824+ PConstraint p l (PResolveTC fc) d : insertImpl ps given
825+ insertImpl (PImp p l n ty d : ps) given =
816826 case find n given [] of
817− Just (tm, given') -> PImp p l n tm : insertImpl ps given'
818− Nothing -> PImp p l n Placeholder : insertImpl ps given
819− insertImpl (PTacImplicit p l n sc ty : ps) given =
827+ Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
828+ Nothing -> PImp p l n Placeholder "" : insertImpl ps given
829+ insertImpl (PTacImplicit p l n sc ty d : ps) given =
820830 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'
822832 Nothing -> if inpat
823− then PTacImplicit p l n sc Placeholder : insertImpl ps given
824− else PTacImplicit p l n sc sc : insertImpl ps given
833+ then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
834+ else PTacImplicit p l n sc sc "" : insertImpl ps given
825835 insertImpl expected [] = []
826836 insertImpl _ given = given
827837
828838 find n [] acc = Nothing
829− find n (PImp _ _ n' t : gs) acc
839+ find n (PImp _ _ n' t _ : gs) acc
830840 | n == n' = Just (t, reverse acc ++ gs)
831− find n (PTacImplicit _ _ n' _ t : gs) acc
841+ find n (PTacImplicit _ _ n' _ t _ : gs) acc
832842 | n == n' = Just (t, reverse acc ++ gs)
833843 find n (g : gs) acc = find n gs (g : acc)
834844
@@ -876,13 +886,13 @@ dumpDecls [] = ""
876886dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
877887
878888dumpDecl (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
880890dumpDecl (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
882892dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
883893dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
884894dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
885−dumpDecl (PClass _ _ cs n ps ds)
895+dumpDecl (PClass _ _ _ cs n ps ds)
886896 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
887897dumpDecl (PInstance _ _ cs n _ t _ ds)
888898 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
src/Idris/AbsSyntaxTree.hs+68−54
@@ -57,6 +57,7 @@ data IState = IState {
5757 idris_flags :: Ctxt [FnOpt],
5858 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
5959 idris_calledgraph :: Ctxt [Name],
60+ idris_docstrings :: Ctxt String,
6061 idris_totcheck :: [(FC, Name)],
6162 idris_log :: String,
6263 idris_options :: IOption,
@@ -120,12 +121,13 @@ data IBCWrite = IBCFix FixDecl
120121 | IBCTotal Name Totality
121122 | IBCFlags Name [FnOpt]
122123 | IBCCG Name
124+ | IBCDoc Name
123125 | IBCDef Name -- i.e. main context
124126 deriving Show
125127
126128idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
127129 emptyContext emptyContext emptyContext emptyContext
128− emptyContext emptyContext emptyContext
130+ emptyContext emptyContext emptyContext emptyContext
129131 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
130132 [] Nothing Nothing [] [] [] Hidden False [] Nothing
131133
@@ -241,24 +243,28 @@ deriving instance Binary Static
241243
242244-- Mark bindings with their explicitness, and laziness
243245data Plicity = Imp { plazy :: Bool,
244− pstatic :: Static }
246+ pstatic :: Static,
247+ pdocstr :: String }
245248 | Exp { plazy :: Bool,
246− pstatic :: Static }
249+ pstatic :: Static,
250+ pdocstr :: String }
247251 | Constraint { plazy :: Bool,
248− pstatic :: Static }
252+ pstatic :: Static,
253+ pdocstr :: String }
249254 | TacImp { plazy :: Bool,
250255 pstatic :: Static,
251− pscript :: PTerm }
256+ pscript :: PTerm,
257+ pdocstr :: String }
252258 deriving (Show, Eq)
253259
254260{-!
255261deriving instance Binary Plicity
256262!-}
257263
258−impl = Imp False Dynamic
259−expl = Exp False Dynamic
260−constraint = Constraint False Dynamic
261−tacimpl = TacImp False Dynamic
264+impl = Imp False Dynamic ""
265+expl = Exp False Dynamic ""
266+constraint = Constraint False Dynamic ""
267+tacimpl t = TacImp False Dynamic t ""
262268
263269data FnOpt = Inlinable | TotalFn | PartialFn
264270 | Coinductive | AssertTotal | TCGen
@@ -275,15 +281,15 @@ inlinable :: FnOpts -> Bool
275281inlinable = elem Inlinable
276282
277283data 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
279285 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
280286 | PCAF FC Name t -- top level constant
281− | PData SyntaxInfo FC Bool -- codata
287+ | PData String SyntaxInfo FC Bool -- codata
282288 (PData' t) -- data declaration
283289 | PParams FC [(Name, t)] [PDecl' t] -- params block
284290 | PNamespace String [PDecl' t] -- new namespace
285− | PRecord SyntaxInfo FC Name t Name t -- record declaration
286− | PClass SyntaxInfo FC
291+ | PRecord String SyntaxInfo FC Name t String Name t -- record declaration
292+ | PClass String SyntaxInfo FC
287293 [t] -- constraints
288294 Name
289295 [(Name, t)] -- parameters
@@ -314,7 +320,7 @@ deriving instance Binary PClause'
314320
315321data PData' t = PDatadecl { d_name :: Name,
316322 d_tcon :: t,
317− d_cons :: [(Name, t, FC)] }
323+ d_cons :: [(String, Name, t, FC)] }
318324 | PLaterdecl { d_name :: Name, d_tcon :: t }
319325 deriving Functor
320326{-!
@@ -332,21 +338,25 @@ type PClause = PClause' PTerm
332338
333339declared :: PDecl -> [Name]
334340declared (PFix _ _ _) = []
335−declared (PTy _ _ _ n t) = [n]
341+declared (PTy _ _ _ _ n t) = [n]
336342declared (PClauses _ _ n _) = [] -- not a declaration
337−declared (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
338− where fstt (a, _, _) = a
343+declared (PRecord _ _ _ n _ _ c _) = [n, c]
344+declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
345+ where fstt (_, a, _, _) = a
339346declared (PParams _ _ ds) = concatMap declared ds
347+declared (PMutual _ ds) = concatMap declared ds
340348declared (PNamespace _ ds) = concatMap declared ds
341349-- declared (PImport _) = []
342350
343351defined :: PDecl -> [Name]
344352defined (PFix _ _ _) = []
345−defined (PTy _ _ _ n t) = []
353+defined (PTy _ _ _ _ n t) = []
346354defined (PClauses _ _ n _) = [n] -- not a declaration
347−defined (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
348− where fstt (a, _, _) = a
355+defined (PRecord _ _ _ n _ _ c _) = [n, c]
356+defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
357+ where fstt (_, a, _, _) = a
349358defined (PParams _ _ ds) = concatMap defined ds
359+defined (PMutual _ ds) = concatMap defined ds
350360defined (PNamespace _ ds) = concatMap defined ds
351361-- declared (PImport _) = []
352362
@@ -486,31 +496,35 @@ type PDo = PDo' PTerm
486496-- variables, e.g. a before (interpTy a).
487497
488498data PArg' t = PImp { priority :: Int,
489− lazyarg :: Bool, pname :: Name, getTm :: t }
499+ lazyarg :: Bool, pname :: Name, getTm :: t,
500+ pargdoc :: String }
490501 | PExp { priority :: Int,
491− lazyarg :: Bool, getTm :: t }
502+ lazyarg :: Bool, getTm :: t,
503+ pargdoc :: String }
492504 | PConstraint { priority :: Int,
493− lazyarg :: Bool, getTm :: t }
505+ lazyarg :: Bool, getTm :: t,
506+ pargdoc :: String }
494507 | PTacImplicit { priority :: Int,
495508 lazyarg :: Bool, pname :: Name,
496509 getScript :: t,
497− getTm :: t }
510+ getTm :: t,
511+ pargdoc :: String }
498512 deriving (Show, Eq, Functor)
499513
500514instance Sized a => Sized (PArg' a) where
501− size (PImp p l nm trm) = 1 + size nm + size trm
502− size (PExp p l trm) = 1 + size trm
503− size (PConstraint p l trm) = 1 + size trm
504− size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
515+ size (PImp p l nm trm _) = 1 + size nm + size trm
516+ size (PExp p l trm _) = 1 + size trm
517+ size (PConstraint p l trm _) = 1 + size trm
518+ size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm
505519
506520{-!
507521deriving instance Binary PArg'
508522!-}
509523
510−pimp = PImp 0 True
511−pexp = PExp 0 False
512−pconst = PConstraint 0 False
513−ptacimp = PTacImplicit 0 True
524+pimp n t = PImp 0 True n t ""
525+pexp t = PExp 0 False t ""
526+pconst t = PConstraint 0 False t ""
527+ptacimp n s t = PTacImplicit 0 True n s t ""
514528
515529type PArg = PArg' PTerm
516530
@@ -633,9 +647,9 @@ instance Show PData where
633647 show d = showDImp False d
634648
635649showDeclImp _ (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
637651showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
638−showDeclImp _ (PData _ _ _ d) = show d
652+showDeclImp _ (PData _ _ _ _ d) = show d
639653showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
640654 showSep "\n" (map show ps)
641655
@@ -659,21 +673,21 @@ showDImp :: Bool -> PData -> String
659673showDImp impl (PDatadecl n ty cons)
660674 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
661675 ++ showSep "\n\t| "
662− (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
676+ (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
663677
664678getImps :: [PArg] -> [(Name, PTerm)]
665679getImps [] = []
666−getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
680+getImps (PImp _ _ n tm _ : xs) = (n, tm) : getImps xs
667681getImps (_ : xs) = getImps xs
668682
669683getExps :: [PArg] -> [PTerm]
670684getExps [] = []
671−getExps (PExp _ _ tm : xs) = tm : getExps xs
685+getExps (PExp _ _ tm _ : xs) = tm : getExps xs
672686getExps (_ : xs) = getExps xs
673687
674688getConsts :: [PArg] -> [PTerm]
675689getConsts [] = []
676−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
690+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
677691getConsts (_ : xs) = getConsts xs
678692
679693getAll :: [PArg] -> [PTerm]
@@ -711,7 +725,7 @@ prettyImp impl = prettySe 10
711725 else
712726 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
713727 prettySe 10 sc
714− prettySe p (PPi (Exp l s) n ty sc)
728+ prettySe p (PPi (Exp l s _) n ty sc)
715729 | n `elem` allNamesIn sc || impl =
716730 let open = if l then text "|" <> lparen else lparen in
717731 bracket p 2 $
@@ -732,7 +746,7 @@ prettyImp impl = prettySe 10
732746 case s of
733747 Static -> text "[static]"
734748 _ -> empty
735− prettySe p (PPi (Imp l s) n ty sc)
749+ prettySe p (PPi (Imp l s _) n ty sc)
736750 | impl =
737751 let open = if l then text "|" <> lbrace else lbrace in
738752 bracket p 2 $
@@ -748,13 +762,13 @@ prettyImp impl = prettySe 10
748762 case s of
749763 Static -> text $ "[static]"
750764 _ -> empty
751− prettySe p (PPi (Constraint _ _) n ty sc) =
765+ prettySe p (PPi (Constraint _ _ _) n ty sc) =
752766 bracket p 2 $
753767 if size sc > breakingSize then
754768 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
755769 else
756770 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) =
758772 bracket p 2 $
759773 if size sc > breakingSize then
760774 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
@@ -846,10 +860,10 @@ prettyImp impl = prettySe 10
846860
847861 prettySe p _ = text "test"
848862
849− prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
850− prettyArgS (PExp _ _ tm) = prettyArgSe tm
851− prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
852− prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
863+ prettyArgS (PImp _ _ n tm _) = prettyArgSi (n, tm)
864+ prettyArgS (PExp _ _ tm _) = prettyArgSe tm
865+ prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
866+ prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
853867
854868 prettyArgSe arg = prettySe 0 arg
855869 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
@@ -874,7 +888,7 @@ showImp impl tm = se 10 tm where
874888 ++ se 10 sc
875889 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
876890 " in " ++ se 10 sc
877− se p (PPi (Exp l s) n ty sc)
891+ se p (PPi (Exp l s _) n ty sc)
878892 | n `elem` allNamesIn sc || impl
879893 = bracket p 2 $
880894 if l then "|(" else "(" ++
@@ -885,7 +899,7 @@ showImp impl tm = se 10 tm where
885899 where st = case s of
886900 Static -> "[static] "
887901 _ -> ""
888− se p (PPi (Imp l s) n ty sc)
902+ se p (PPi (Imp l s _) n ty sc)
889903 | impl = bracket p 2 $ if l then "|{" else "{" ++
890904 show n ++ " : " ++ se 10 ty ++
891905 "} " ++ st ++ "-> " ++ se 10 sc
@@ -893,9 +907,9 @@ showImp impl tm = se 10 tm where
893907 where st = case s of
894908 Static -> "[static] "
895909 _ -> ""
896− se p (PPi (Constraint _ _) n ty sc)
910+ se p (PPi (Constraint _ _ _) n ty sc)
897911 = 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)
899913 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
900914 se p (PApp _ (PRef _ f) [])
901915 | not impl = show f
@@ -933,10 +947,10 @@ showImp impl tm = se 10 tm where
933947 se p (PElabError s) = show s
934948-- se p x = "Not implemented"
935949
936− sArg (PImp _ _ n tm) = siArg (n, tm)
937− sArg (PExp _ _ tm) = seArg tm
938− sArg (PConstraint _ _ tm) = scArg tm
939− sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
950+ sArg (PImp _ _ n tm _) = siArg (n, tm)
951+ sArg (PExp _ _ tm _) = seArg tm
952+ sArg (PConstraint _ _ tm _) = scArg tm
953+ sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
940954
941955 seArg arg = " " ++ se 0 arg
942956 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
src/Idris/Delaborate.hs+4−4
@@ -66,10 +66,10 @@ delab' ist tm fullname = de [] tm
6666 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
6767 | otherwise = PApp un (PRef un n) (map pexp args)
6868
69− imp (PImp p l n _) arg = PImp p l n arg
70− imp (PExp p l _) arg = PExp p l arg
71− imp (PConstraint p l _) arg = PConstraint p l arg
72− imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg
69+ imp (PImp p l n _ d) arg = PImp p l n arg d
70+ imp (PExp p l _ d) arg = PExp p l arg d
71+ imp (PConstraint p l _ d) arg = PConstraint p l arg d
72+ imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
7373
7474pshow :: IState -> Err -> String
7575pshow i (Msg s) = s
src/Idris/ElabDecls.hs+69−62
@@ -38,8 +38,9 @@ checkDef fc ns = do ctxt <- getContext
3838 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t
3939 return (n, t')) ns
4040
41−elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()
42−elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
41+elabType :: ElabInfo -> SyntaxInfo -> String ->
42+ FC -> FnOpts -> Name -> PTerm -> Idris ()
43+elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
4344 n = liftname info n_in in -}
4445 do checkUndefined fc n
4546 ctxt <- getContext
@@ -75,8 +76,8 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
7576 when corec $ do setAccessibility n Frozen
7677 addIBC (IBCAccess n Frozen)
7778
78−elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()
79−elabData info syn fc codata (PLaterdecl n t_in)
79+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()
80+elabData info syn doc fc codata (PLaterdecl n t_in)
8081 = do iLOG (show fc)
8182 checkUndefined fc n
8283 ctxt <- getContext
@@ -92,7 +93,7 @@ elabData info syn fc codata (PLaterdecl n t_in)
9293 logLvl 2 $ "---> " ++ show cty
9394 updateContext (addTyDecl n cty) -- temporary, to check cons
9495
95−elabData info syn fc codata (PDatadecl n t_in dcons)
96+elabData info syn doc fc codata (PDatadecl n t_in dcons)
9697 = do iLOG (show fc)
9798 undef <- isUndefined fc n
9899 ctxt <- getContext
@@ -119,10 +120,10 @@ elabData info syn fc codata (PDatadecl n t_in dcons)
119120 updateContext (addDatatype (Data n ttag cty cons))
120121 mapM_ (checkPositive n) cons
121122
122−elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
123− PTerm -> Name -> PTerm -> Idris ()
124−elabRecord info syn fc tyn ty cn cty
125− = do elabData info syn fc False (PDatadecl tyn ty [(cn, cty, fc)])
123+elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
124+ PTerm -> String -> Name -> PTerm -> Idris ()
125+elabRecord info syn doc fc tyn ty cdoc cn cty
126+ = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
126127 cty' <- implicit syn cn cty
127128 i <- get
128129 cty <- case lookupTy Nothing cn (tt_ctxt i) of
@@ -145,7 +146,7 @@ elabRecord info syn fc tyn ty cn cty
145146 where
146147-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
147148
148− isNonImp (PExp _ _ _, a) = Just a
149+ isNonImp (PExp _ _ _ _, a) = Just a
149150 isNonImp _ = Nothing
150151
151152 tryElabDecl info (fn, ty, val)
@@ -157,15 +158,15 @@ elabRecord info syn fc tyn ty cn cty
157158 show fn ++ " (" ++ show ty ++ ")"
158159 put i)
159160
160− getImplB k (PPi (Imp l s) n Placeholder sc)
161+ getImplB k (PPi (Imp l s _) n Placeholder sc)
161162 = getImplB k sc
162− getImplB k (PPi (Imp l s) n ty sc)
163− = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc
163+ getImplB k (PPi (Imp l s d) n ty sc)
164+ = getImplB (\x -> k (PPi (Imp l s d) n ty x)) sc
164165 getImplB k (PPi _ n ty sc)
165166 = getImplB k sc
166167 getImplB k _ = k
167168
168− renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
169+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
169170 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
170171 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
171172 renameBs _ t = t
@@ -192,7 +193,7 @@ elabRecord info syn fc tyn ty cn cty
192193
193194 mkProj recty substs cimp ((pn_in, pty), pos)
194195 = do let pn = expandNS syn pn_in
195− let pfnTy = PTy defaultSyntax fc [] pn
196+ let pfnTy = PTy "" defaultSyntax fc [] pn
196197 (PPi expl rec recty
197198 (substMatches substs pty))
198199 let pls = repeat Placeholder
@@ -213,7 +214,7 @@ elabRecord info syn fc tyn ty cn cty
213214 let valname = MN 0 "updateval"
214215 let pt = k (PPi expl pn pty
215216 (PPi expl rec recty recty))
216− let pfnTy = PTy defaultSyntax fc [] setname pt
217+ let pfnTy = PTy "" defaultSyntax fc [] setname pt
217218 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
218219 let lhsArgs = pls
219220 let rhsArgs = take pos pls ++ (PRef fc valname) :
@@ -228,8 +229,9 @@ elabRecord info syn fc tyn ty cn cty
228229 (map pexp rhsArgs)) []
229230 return (pn, pfnTy, PClauses fc [] setname [pclause])
230231
231−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (Name, PTerm, FC) -> Idris (Name, Type)
232−elabCon info syn tn codata (n, t_in, fc)
232+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
233+ (String, Name, PTerm, FC) -> Idris (Name, Type)
234+elabCon info syn tn codata (doc, n, t_in, fc)
233235 = do checkUndefined fc n
234236 ctxt <- getContext
235237 i <- get
@@ -620,10 +622,10 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)
620622
621623data MArgTy = IA | EA | CA deriving Show
622624
623−elabClass :: ElabInfo -> SyntaxInfo ->
625+elabClass :: ElabInfo -> SyntaxInfo -> String ->
624626 FC -> [PTerm] ->
625627 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
626−elabClass info syn fc constraints tn ps ds
628+elabClass info syn doc fc constraints tn ps ds
627629 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
628630 let tty = pibind ps PSet
629631 let constraint = PApp fc (PRef fc tn)
@@ -635,12 +637,14 @@ elabClass info syn fc constraints tn ps ds
635637 ims <- mapM (tdecl mnames) mdecls
636638 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
637639 (filter clause ds)
638− let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)
639− let cty = impbind ps $ conbind constraints $ pibind methods constraint
640− let cons = [(cn, cty, fc)]
640+ let (methods, imethods)
641+ = unzip (map (\ ( x,y,z) -> (x, y)) ims)
642+ let cty = impbind ps $ conbind constraints
643+ $ pibind methods constraint
644+ let cons = [("", cn, cty, fc)]
641645 let ddecl = PDatadecl tn tty cons
642646 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
644648 -- for each constraint, build a top level function to chase it
645649 logLvl 5 $ "Building functions"
646650 let usyn = syn { using = ps ++ using syn }
@@ -653,9 +657,10 @@ elabClass info syn fc constraints tn ps ds
653657 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
654658 i <- get
655659 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) [])
657661 addIBC (IBCClass tn)
658662 where
663+ nodoc (n, (_, o, t)) = (n, (o, t))
659664 pibind [] x = x
660665 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
661666 impbind [] x = x
@@ -663,12 +668,12 @@ elabClass info syn fc constraints tn ps ds
663668 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
664669 conbind [] x = x
665670
666− getMName (PTy _ _ _ n _) = nsroot n
667− tdecl allmeths (PTy syn _ o n t)
671+ getMName (PTy _ _ _ _ n _) = nsroot n
672+ tdecl allmeths (PTy doc syn _ o n t)
668673 = do t' <- implicit' syn allmeths n t
669674 logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'
670675 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'))),
672677 (n, (syn, o, t) ) )
673678 tdecl _ _ = fail "Not allowed in a class declaration"
674679
@@ -677,7 +682,7 @@ elabClass info syn fc constraints tn ps ds
677682 case lookup n mtys of
678683 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
679684 let ds = map (decorateid defaultdec)
680− [PTy syn fc [] n ty',
685+ [PTy "" syn fc [] n ty',
681686 PClauses fc (TCGen:o ++ opts) n cs]
682687 iLOG (show ds)
683688 return (n, ((defaultdec n, ds!!1), ds))
@@ -687,7 +692,7 @@ elabClass info syn fc constraints tn ps ds
687692 defaultdec (UN n) = UN ("default#" ++ n)
688693 defaultdec (NS n ns) = NS (defaultdec n) ns
689694
690− tydecl (PTy _ _ _ _ _) = True
695+ tydecl (PTy _ _ _ _ _ _) = True
691696 tydecl _ = False
692697 clause (PClauses _ _ _ _) = True
693698 clause _ = False
@@ -711,10 +716,10 @@ elabClass info syn fc constraints tn ps ds
711716 addInstance False conn' cfn
712717 addIBC (IBCInstance False conn' cfn)
713718-- iputStrLn ("Added " ++ show (conn, cfn, ty))
714− return [PTy syn fc [] cfn ty,
719+ return [PTy "" syn fc [] cfn ty,
715720 PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]
716721
717− tfun cn c syn all (m, (o, ty))
722+ tfun cn c syn all (m, (doc, o, ty))
718723 = do let ty' = insertConstraint c ty
719724 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
720725 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
@@ -725,12 +730,12 @@ elabClass info syn fc constraints tn ps ds
725730 iLOG (showImp True ty)
726731 iLOG (show (m, ty', capp, margs))
727732 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
728− return [PTy syn fc o m ty',
733+ return [PTy doc syn fc o m ty',
729734 PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]
730735
731− getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc
732− getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc
733− getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc
736+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc
737+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc
738+ getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc
734739 getMArgs _ = []
735740
736741 getMeth (m:ms) (a:as) x | x == a = PRef fc m
@@ -746,14 +751,14 @@ elabClass info syn fc constraints tn ps ds
746751 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
747752 rhsArgs [] _ = []
748753
749− insertConstraint c (PPi p@(Imp _ _) n ty sc)
754+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)
750755 = PPi p n ty (insertConstraint c sc)
751756 insertConstraint c sc = PPi constraint (MN 0 "c") c sc
752757
753758 -- 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)
755760 | 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)
757762 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
758763 toExp ns e sc = sc
759764
@@ -778,7 +783,7 @@ elabInstance info syn fc cs n ps t expn ds
778783 Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)
779784 addInstance intInst n iname
780785 Just _ -> addInstance intInst n iname
781− elabType info syn fc [] iname t
786+ elabType info syn "" fc [] iname t
782787 let ips = zip (class_params ci) ps
783788 let ns = case n of
784789 NS n ns' -> ns'
@@ -836,17 +841,19 @@ elabInstance info syn fc cs n ps t expn ds
836841 getRetType (PPi _ _ _ sc) = getRetType sc
837842 getRetType t = t
838843
839− mkMethApp (n, _, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
840− lamBind i (PPi (Constraint _ _) _ _ sc) sc'
841− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
842− lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
844+ mkMethApp (n, _, _, ty)
845+ = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
846+ lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
847+ = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
848+ lamBind i (PPi _ n ty sc) sc'
849+ = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')
843850 lamBind i _ sc = sc
844− methArgs i (PPi (Imp _ _) n ty sc)
845− = PImp 0 False n (PRef fc (MN i "meth")) : methArgs (i+1) sc
846− methArgs i (PPi (Exp _ _) n ty sc)
847− = PExp 0 False (PRef fc (MN i "meth")) : methArgs (i+1) sc
848− methArgs i (PPi (Constraint _ _) n ty sc)
849− = PConstraint 0 False (PResolveTC fc) : methArgs (i+1) sc
851+ methArgs i (PPi (Imp _ _ _) n ty sc)
852+ = PImp 0 False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
853+ methArgs i (PPi (Exp _ _ _) n ty sc)
854+ = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc
855+ methArgs i (PPi (Constraint _ _ _) n ty sc)
856+ = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc
850857 methArgs i _ = []
851858
852859 papp fc f [] = f
@@ -865,12 +872,12 @@ elabInstance info syn fc cs n ps t expn ds
865872 decorate ns iname (UN n) = NS (UN ('!':n)) ns
866873 decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns
867874
868− mkTyDecl (n, op, t, _) = PTy syn fc op n t
875+ mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
869876
870877 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
871878 conbind [] x = x
872879
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)
874881 coninsert cs sc = conbind cs sc
875882
876883 insertDefaults :: IState -> Name ->
@@ -903,7 +910,7 @@ elabInstance info syn fc cs n ps t expn ds
903910 = decorate ns iname m == decorate ns iname m'
904911 clauseFor m iname ns _ = False
905912
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
907914decorateid decorate (PClauses f o n cs)
908915 = PClauses f o (decorate n) (map dc cs)
909916 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 _ _ _)
947954 = return () -- nothing to elaborate
948955elabDecl' _ info (PSyntax _ p)
949956 = 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)
951958 | what /= EDefns
952959 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
953− elabType info s f o n ty
954−elabDecl' what info (PData s f co d)
960+ elabType info s doc f o n ty
961+elabDecl' what info (PData doc s f co d)
955962 | what /= ETypes
956963 = do iLOG $ "Elaborating " ++ show (d_name d)
957− elabData info s f co d
964+ elabData info s doc f co d
958965 | otherwise
959966 = 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))
961968elabDecl' what info d@(PClauses f o n ps)
962969 | what /= ETypes
963970 = do iLOG $ "Elaborating clause " ++ show n
@@ -988,18 +995,18 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
988995 ninfo = case namespace info of
989996 Nothing -> info { namespace = Just [n] }
990997 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)
992999 | what /= EDefns
9931000 = 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
9951002elabDecl' what info (PInstance s f cs n ps t expn ds)
9961003 | what /= ETypes
9971004 = do iLOG $ "Elaborating instance " ++ show n
9981005 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)
10001007 | what /= EDefns
10011008 = 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
10031010elabDecl' _ info (PDSL n dsl)
10041011 = do i <- get
10051012 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
262262 mapM_ (\n -> do focus n
263263 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
264264 resolveTC 7 fn ist) (ivs' \\ ivs)
265− where tcArg (n, PConstraint _ _ Placeholder) = True
265+ where tcArg (n, PConstraint _ _ Placeholder _) = True
266266 tcArg _ = False
267267
268268 elab' ina@(_, a) (PApp fc f [arg])
@@ -469,7 +469,7 @@ resolveTC depth fn ist
469469 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
470470 -- if there's any arguments left, we've failed to resolve
471471 solve
472− where isImp (PImp p _ _ _) = (True, p)
472+ where isImp (PImp p _ _ _ _) = (True, p)
473473 isImp arg = (False, priority arg)
474474
475475collectDeferred :: Term -> State [(Name, Type)] Term
@@ -515,7 +515,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
515515 [(n, args)] -> return $ (n, map isImp args)
516516 ns <- apply (Var fn') (map (\x -> (x, 0)) imps)
517517 when autoSolve solveAll
518− where isImp (PImp _ _ _ _) = True
518+ where isImp (PImp _ _ _ _ _) = True
519519 isImp _ = False
520520 envArgs n = do e <- get_env
521521 case lookup n e of
src/Idris/IBC.hs+78−29
@@ -21,7 +21,7 @@ import System.Directory
2121import Paths_idris
2222
2323ibcVersion :: Word8
24−ibcVersion = 22
24+ibcVersion = 23
2525
2626data IBCFile = IBCFile { ver :: Word8,
2727 sourcefile :: FilePath,
@@ -43,13 +43,15 @@ data IBCFile = IBCFile { ver :: Word8,
4343 ibc_total :: [(Name, Totality)],
4444 ibc_flags :: [(Name, [FnOpt])],
4545 ibc_cg :: [(Name, CGInfo)],
46− ibc_defs :: [(Name, Def)] }
46+ ibc_defs :: [(Name, Def)],
47+ ibc_docstrings :: [(Name, String)]
48+ }
4749{-!
4850deriving instance Binary IBCFile
4951!-}
5052
5153initIBC :: IBCFile
52−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
54+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
5355
5456loadIBC :: FilePath -> Idris ()
5557loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -111,6 +113,9 @@ ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }
111113ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of
112114 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }
113115 _ -> 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"
114119ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of
115120 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }
116121 _ -> fail "IBC write failed"
@@ -145,6 +150,7 @@ process i fn
145150 pAccess (ibc_access i)
146151 pTotal (ibc_total i)
147152 pCG (ibc_cg i)
153+ pDocs (ibc_docstrings i)
148154
149155timestampOlder :: FilePath -> FilePath -> IO ()
150156timestampOlder src ibc = do srct <- getModificationTime src
@@ -243,6 +249,9 @@ pDefs ds = mapM_ (\ (n, d) ->
243249 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))
244250 ds
245251
252+pDocs :: [(Name, String)] -> Idris ()
253+pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds
254+
246255pAccess :: [(Name, Accessibility)] -> Idris ()
247256pAccess ds = mapM_ (\ (n, a) ->
248257 do i <- getIState
@@ -707,7 +716,7 @@ instance Binary Totality where
707716 _ -> error "Corrupted binary data for Totality"
708717
709718instance 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)
711720 = do put x1
712721 put x2
713722 put x3
@@ -729,6 +738,7 @@ instance Binary IBCFile where
729738 put x19
730739 put x20
731740 put x21
741+ put x22
732742 get
733743 = do x1 <- get
734744 if x1 == ibcVersion then
@@ -752,7 +762,8 @@ instance Binary IBCFile where
752762 x19 <- get
753763 x20 <- get
754764 x21 <- 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)
765+ x22 <- get
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)
756767 else return (initIBC { ver = x1 })
757768
758769instance Binary FnOpt where
@@ -830,35 +841,47 @@ instance Binary Static where
830841instance Binary Plicity where
831842 put x
832843 = case x of
833− Imp x1 x2 -> do putWord8 0
844+ Imp x1 x2 x3 ->
845+ do putWord8 0
834846 put x1
835847 put x2
836− Exp x1 x2 -> do putWord8 1
848+ put x3
849+ Exp x1 x2 x3 ->
850+ do putWord8 1
837851 put x1
838852 put x2
839− Constraint x1 x2 -> do putWord8 2
853+ put x3
854+ Constraint x1 x2 x3 ->
855+ do putWord8 2
840856 put x1
841857 put x2
842− TacImp x1 x2 x3 -> do putWord8 3
858+ put x3
859+ TacImp x1 x2 x3 x4 ->
860+ do putWord8 3
843861 put x1
844862 put x2
845863 put x3
864+ put x4
846865 get
847866 = do i <- getWord8
848867 case i of
849868 0 -> do x1 <- get
850869 x2 <- get
851− return (Imp x1 x2)
870+ x3 <- get
871+ return (Imp x1 x2 x3)
852872 1 -> do x1 <- get
853873 x2 <- get
854− return (Exp x1 x2)
874+ x3 <- get
875+ return (Exp x1 x2 x3)
855876 2 -> do x1 <- get
856877 x2 <- get
857− return (Constraint x1 x2)
878+ x3 <- get
879+ return (Constraint x1 x2 x3)
858880 3 -> do x1 <- get
859881 x2 <- get
860882 x3 <- get
861− return (TacImp x1 x2 x3)
883+ x4 <- get
884+ return (TacImp x1 x2 x3 x4)
862885 _ -> error "Corrupted binary data for Plicity"
863886
864887
@@ -869,22 +892,26 @@ instance (Binary t) => Binary (PDecl' t) where
869892 put x1
870893 put x2
871894 put x3
872− PTy x1 x2 x3 x4 x5 -> do putWord8 1
895+ PTy x1 x2 x3 x4 x5 x6
896+ -> do putWord8 1
873897 put x1
874898 put x2
875899 put x3
876900 put x4
877901 put x5
902+ put x6
878903 PClauses x1 x2 x3 x4 -> do putWord8 2
879904 put x1
880905 put x2
881906 put x3
882907 put x4
883− PData x1 x2 x3 x4 -> do putWord8 3
908+ PData x1 x2 x3 x4 x5 ->
909+ do putWord8 3
884910 put x1
885911 put x2
886912 put x3
887913 put x4
914+ put x5
888915 PParams x1 x2 x3 -> do putWord8 4
889916 put x1
890917 put x2
@@ -892,20 +919,25 @@ instance (Binary t) => Binary (PDecl' t) where
892919 PNamespace x1 x2 -> do putWord8 5
893920 put x1
894921 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
896924 put x1
897925 put x2
898926 put x3
899927 put x4
900928 put x5
901929 put x6
902− PClass x1 x2 x3 x4 x5 x6 -> do putWord8 7
930+ put x7
931+ put x8
932+ PClass x1 x2 x3 x4 x5 x6 x7
933+ -> do putWord8 7
903934 put x1
904935 put x2
905936 put x3
906937 put x4
907938 put x5
908939 put x6
940+ put x7
909941 PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8
910942 put x1
911943 put x2
@@ -937,7 +969,8 @@ instance (Binary t) => Binary (PDecl' t) where
937969 x3 <- get
938970 x4 <- get
939971 x5 <- get
940− return (PTy x1 x2 x3 x4 x5)
972+ x6 <- get
973+ return (PTy x1 x2 x3 x4 x5 x6)
941974 2 -> do x1 <- get
942975 x2 <- get
943976 x3 <- get
@@ -947,7 +980,8 @@ instance (Binary t) => Binary (PDecl' t) where
947980 x2 <- get
948981 x3 <- get
949982 x4 <- get
950− return (PData x1 x2 x3 x4)
983+ x5 <- get
984+ return (PData x1 x2 x3 x4 x5)
951985 4 -> do x1 <- get
952986 x2 <- get
953987 x3 <- get
@@ -961,14 +995,17 @@ instance (Binary t) => Binary (PDecl' t) where
961995 x4 <- get
962996 x5 <- get
963997 x6 <- get
964− return (PRecord x1 x2 x3 x4 x5 x6)
998+ x7 <- get
999+ x8 <- get
1000+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8)
9651001 7 -> do x1 <- get
9661002 x2 <- get
9671003 x3 <- get
9681004 x4 <- get
9691005 x5 <- get
9701006 x6 <- get
971− return (PClass x1 x2 x3 x4 x5 x6)
1007+ x7 <- get
1008+ return (PClass x1 x2 x3 x4 x5 x6 x7)
9721009 8 -> do x1 <- get
9731010 x2 <- get
9741011 x3 <- get
@@ -1370,25 +1407,33 @@ instance (Binary t) => Binary (PDo' t) where
13701407instance (Binary t) => Binary (PArg' t) where
13711408 put x
13721409 = case x of
1373− PImp x1 x2 x3 x4 -> do putWord8 0
1410+ PImp x1 x2 x3 x4 x5 ->
1411+ do putWord8 0
13741412 put x1
13751413 put x2
13761414 put x3
13771415 put x4
1378− PExp x1 x2 x3 -> do putWord8 1
1416+ put x5
1417+ PExp x1 x2 x3 x4 ->
1418+ do putWord8 1
13791419 put x1
13801420 put x2
13811421 put x3
1382− PConstraint x1 x2 x3 -> do putWord8 2
1422+ put x4
1423+ PConstraint x1 x2 x3 x4 ->
1424+ do putWord8 2
13831425 put x1
13841426 put x2
13851427 put x3
1386− PTacImplicit x1 x2 x3 x4 x5 -> do putWord8 3
1428+ put x4
1429+ PTacImplicit x1 x2 x3 x4 x5 x6 ->
1430+ do putWord8 3
13871431 put x1
13881432 put x2
13891433 put x3
13901434 put x4
13911435 put x5
1436+ put x6
13921437 get
13931438 = do i <- getWord8
13941439 case i of
@@ -1396,21 +1441,25 @@ instance (Binary t) => Binary (PArg' t) where
13961441 x2 <- get
13971442 x3 <- get
13981443 x4 <- get
1399− return (PImp x1 x2 x3 x4)
1444+ x5 <- get
1445+ return (PImp x1 x2 x3 x4 x5)
14001446 1 -> do x1 <- get
14011447 x2 <- get
14021448 x3 <- get
1403− return (PExp x1 x2 x3)
1449+ x4 <- get
1450+ return (PExp x1 x2 x3 x4)
14041451 2 -> do x1 <- get
14051452 x2 <- get
14061453 x3 <- get
1407− return (PConstraint x1 x2 x3)
1454+ x4 <- get
1455+ return (PConstraint x1 x2 x3 x4)
14081456 3 -> do x1 <- get
14091457 x2 <- get
14101458 x3 <- get
14111459 x4 <- get
14121460 x5 <- get
1413− return (PTacImplicit x1 x2 x3 x4 x5)
1461+ x6 <- get
1462+ return (PTacImplicit x1 x2 x3 x4 x5 x6)
14141463 _ -> error "Corrupted binary data for PArg'"
14151464
14161465
src/Idris/Parser.hs+29−23
@@ -273,7 +273,11 @@ pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
273273 where dot '.' = '/'
274274 dot c = c
275275
276−parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
276+-- a program is a list of declarations, possibly with associated
277+-- documentation strings
278+
279+parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
280+ Idris [PDecl]
277281parseProg syn fname input pos
278282 = do i <- get
279283 case runParser (do setPosition pos
@@ -308,7 +312,8 @@ collect (c@(PClauses _ o _ _) : ds)
308312collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
309313collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
310314collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
311−collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
315+collect (PClass doc f s cs n ps ds : ds')
316+ = PClass doc f s cs n ps (collect ds) : collect ds'
312317collect (PInstance f s cs n ps t en ds : ds')
313318 = PInstance f s cs n ps t en (collect ds) : collect ds'
314319collect (d : ds) = d : collect ds
@@ -433,7 +438,7 @@ pFunDecl' syn = try (do pushIndent
433438 pTerminator
434439-- ty' <- implicit syn n ty
435440 addAcc n acc
436− return (PTy syn fc opts' n ty))
441+ return (PTy "" syn fc opts' n ty))
437442 <|> try (pPattern syn)
438443 <|> try (pCAF syn)
439444
@@ -507,7 +512,7 @@ pClass syn = do acc <- pAccessibility
507512 closeBlock
508513 let allDs = concat ds
509514 accData acc n (concatMap declared allDs)
510− return [PClass syn fc cons n cs allDs]
515+ return [PClass "" syn fc cons n cs allDs]
511516 where
512517 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
513518 return (i, ty)
@@ -902,7 +907,7 @@ pPi syn =
902907 lchar '('; xt <- tyDeclList syn; lchar ')'
903908 symbol "->"
904909 sc <- pExpr syn
905− return (bindList (PPi (Exp lazy st)) xt sc))
910+ return (bindList (PPi (Exp lazy st "")) xt sc))
906911 <|> try (if implicitAllowed syn
907912 then do lazy <- option False (do lchar '|'
908913 return True)
@@ -912,7 +917,7 @@ pPi syn =
912917 lchar '}'
913918 symbol "->"
914919 sc <- pExpr syn
915− return (bindList (PPi (Imp lazy st)) xt sc)
920+ return (bindList (PPi (Imp lazy st "")) xt sc)
916921 else fail "No implicit arguments allowed here")
917922 <|> try (do lchar '{'
918923 reserved "auto"
@@ -920,7 +925,8 @@ pPi syn =
920925 lchar '}'
921926 symbol "->"
922927 sc <- pExpr syn
923− return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
928+ return (bindList (PPi
929+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
924930 <|> try (do lchar '{'
925931 reserved "default"
926932 script <- pSimpleExpr syn
@@ -928,7 +934,7 @@ pPi syn =
928934 lchar '}'
929935 symbol "->"
930936 sc <- pExpr syn
931− return (bindList (PPi (TacImp False Dynamic script)) xt sc))
937+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
932938 <|> do --lazy <- option False (do lchar '|'; return True)
933939 lchar '{'
934940 reserved "static"
@@ -936,7 +942,7 @@ pPi syn =
936942 t <- pExpr' syn
937943 symbol "->"
938944 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)
940946
941947pConstList :: SyntaxInfo -> IParser [PTerm]
942948pConstList syn = try (do lchar '('
@@ -1096,7 +1102,7 @@ pRecord syn = do acc <- pAccessibility
10961102 reserved "where"
10971103 openBlock
10981104 pushIndent
1099− (cn, cty, _) <- pConstructor syn
1105+ (cdoc, cn, cty, _) <- pConstructor syn
11001106 pKeepTerminator
11011107 popIndent
11021108 closeBlock
@@ -1105,7 +1111,7 @@ pRecord syn = do acc <- pAccessibility
11051111 syn_namespace syn }
11061112 let fns = getRecNames rsyn cty
11071113 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
11091115 where
11101116 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]
11111117 ++ getRecNames syn sc
@@ -1124,7 +1130,7 @@ pData syn = try (do acc <- pAccessibility
11241130 tyn_in <- pfName
11251131 ty <- pTSig (impOK syn)
11261132 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
11281134 reserved "where"
11291135 openBlock
11301136 pushIndent
@@ -1134,8 +1140,8 @@ pData syn = try (do acc <- pAccessibility
11341140 return c) -- (lchar '|')
11351141 popIndent
11361142 closeBlock
1137− accData acc tyn (map (\ (n, _, _) -> n) cons)
1138− return $ PData syn fc co (PDatadecl tyn ty cons)))
1143+ accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1144+ return $ PData "" syn fc co (PDatadecl tyn ty cons)))
11391145 <|> try (do pushIndent
11401146 acc <- pAccessibility
11411147 co <- pDataI
@@ -1144,16 +1150,16 @@ pData syn = try (do acc <- pAccessibility
11441150 args <- many pName
11451151 let ty = bindArgs (map (const PSet) args) PSet
11461152 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
11481154 lchar '='
11491155 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
11501156 pTerminator
11511157 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1152− cons' <- mapM (\ (x, cargs, cfc) ->
1158+ cons' <- mapM (\ (doc, x, cargs, cfc) ->
11531159 do let cty = bindArgs cargs conty
1154− return (x, cty, cfc)) cons
1155− accData acc tyn (map (\ (n, _, _) -> n) cons')
1156− return $ PData syn fc co (PDatadecl tyn ty cons')))
1160+ return (doc, x, cty, cfc)) cons
1161+ accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1162+ return $ PData "" syn fc co (PDatadecl tyn ty cons')))
11571163 where
11581164 mkPApp fc t [] = t
11591165 mkPApp fc t xs = PApp fc t (map pexp xs)
@@ -1161,23 +1167,23 @@ pData syn = try (do acc <- pAccessibility
11611167bindArgs :: [PTerm] -> PTerm -> PTerm
11621168bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
11631169
1164−pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1170+pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
11651171pConstructor syn
11661172 = do cn_in <- pfName; fc <- pfc
11671173 let cn = expandNS syn cn_in
11681174 ty <- pTSig (impOK syn)
11691175-- ty' <- implicit syn cn ty
1170− return (cn, ty, fc)
1176+ return ("", cn, ty, fc)
11711177
11721178
1173−pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
1179+pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
11741180pSimpleCon syn
11751181 = do cn_in <- pfName
11761182 let cn = expandNS syn cn_in
11771183 fc <- pfc
11781184 args <- many (do notEndApp
11791185 pSimpleExpr syn)
1180− return (cn, args, fc)
1186+ return ("", cn, args, fc)
11811187
11821188--------- DSL syntax overloading ---------
11831189
src/Idris/Primitives.hs+1−1
@@ -281,7 +281,7 @@ elabPrim (Prim n ty i def sc tot)
281281
282282elabPrims :: Idris ()
283283elabPrims = do mapM_ (elabDecl EAll toplevel)
284− (map (PData defaultSyntax (FC "builtin" 0) False)
284+ (map (PData "" defaultSyntax (FC "builtin" 0) False)
285285 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
286286 mapM_ elabPrim primitives
287287
test/test018/expected−100
@@ -14,502 +14,402 @@ Received
1414Hello to you too!
1515Finished
1616100
17−Waiting for message
1817Sent ping
1918Received Hello!
2019Reply: Hello back!
212099
22−Waiting for message
2321Sent ping
2422Received Hello!
2523Reply: Hello back!
262498
27−Waiting for message
2825Sent ping
2926Received Hello!
3027Reply: Hello back!
312897
32−Waiting for message
3329Sent ping
3430Received Hello!
3531Reply: Hello back!
363296
37−Waiting for message
3833Sent ping
3934Received Hello!
4035Reply: Hello back!
413695
42−Waiting for message
4337Sent ping
4438Received Hello!
4539Reply: Hello back!
464094
47−Waiting for message
4841Sent ping
4942Received Hello!
5043Reply: Hello back!
514493
52−Waiting for message
5345Sent ping
5446Received Hello!
5547Reply: Hello back!
564892
57−Waiting for message
5849Sent ping
5950Received Hello!
6051Reply: Hello back!
615291
62−Waiting for message
6353Sent ping
6454Received Hello!
6555Reply: Hello back!
665690
67−Waiting for message
6857Sent ping
6958Received Hello!
7059Reply: Hello back!
716089
72−Waiting for message
7361Sent ping
7462Received Hello!
7563Reply: Hello back!
766488
77−Waiting for message
7865Sent ping
7966Received Hello!
8067Reply: Hello back!
816887
82−Waiting for message
8369Sent ping
8470Received Hello!
8571Reply: Hello back!
867286
87−Waiting for message
8873Sent ping
8974Received Hello!
9075Reply: Hello back!
917685
92−Waiting for message
9377Sent ping
9478Received Hello!
9579Reply: Hello back!
968084
97−Waiting for message
9881Sent ping
9982Received Hello!
10083Reply: Hello back!
1018483
102−Waiting for message
10385Sent ping
10486Received Hello!
10587Reply: Hello back!
1068882
107−Waiting for message
10889Sent ping
10990Received Hello!
11091Reply: Hello back!
1119281
112−Waiting for message
11393Sent ping
11494Received Hello!
11595Reply: Hello back!
1169680
117−Waiting for message
11897Sent ping
11998Received Hello!
12099Reply: Hello back!
12110079
122−Waiting for message
123101Sent ping
124102Received Hello!
125103Reply: Hello back!
12610478
127−Waiting for message
128105Sent ping
129106Received Hello!
130107Reply: Hello back!
13110877
132−Waiting for message
133109Sent ping
134110Received Hello!
135111Reply: Hello back!
13611276
137−Waiting for message
138113Sent ping
139114Received Hello!
140115Reply: Hello back!
14111675
142−Waiting for message
143117Sent ping
144118Received Hello!
145119Reply: Hello back!
14612074
147−Waiting for message
148121Sent ping
149122Received Hello!
150123Reply: Hello back!
15112473
152−Waiting for message
153125Sent ping
154126Received Hello!
155127Reply: Hello back!
15612872
157−Waiting for message
158129Sent ping
159130Received Hello!
160131Reply: Hello back!
16113271
162−Waiting for message
163133Sent ping
164134Received Hello!
165135Reply: Hello back!
16613670
167−Waiting for message
168137Sent ping
169138Received Hello!
170139Reply: Hello back!
17114069
172−Waiting for message
173141Sent ping
174142Received Hello!
175143Reply: Hello back!
17614468
177−Waiting for message
178145Sent ping
179146Received Hello!
180147Reply: Hello back!
18114867
182−Waiting for message
183149Sent ping
184150Received Hello!
185151Reply: Hello back!
18615266
187−Waiting for message
188153Sent ping
189154Received Hello!
190155Reply: Hello back!
19115665
192−Waiting for message
193157Sent ping
194158Received Hello!
195159Reply: Hello back!
19616064
197−Waiting for message
198161Sent ping
199162Received Hello!
200163Reply: Hello back!
20116463
202−Waiting for message
203165Sent ping
204166Received Hello!
205167Reply: Hello back!
20616862
207−Waiting for message
208169Sent ping
209170Received Hello!
210171Reply: Hello back!
21117261
212−Waiting for message
213173Sent ping
214174Received Hello!
215175Reply: Hello back!
21617660
217−Waiting for message
218177Sent ping
219178Received Hello!
220179Reply: Hello back!
22118059
222−Waiting for message
223181Sent ping
224182Received Hello!
225183Reply: Hello back!
22618458
227−Waiting for message
228185Sent ping
229186Received Hello!
230187Reply: Hello back!
23118857
232−Waiting for message
233189Sent ping
234190Received Hello!
235191Reply: Hello back!
23619256
237−Waiting for message
238193Sent ping
239194Received Hello!
240195Reply: Hello back!
24119655
242−Waiting for message
243197Sent ping
244198Received Hello!
245199Reply: Hello back!
24620054
247−Waiting for message
248201Sent ping
249202Received Hello!
250203Reply: Hello back!
25120453
252−Waiting for message
253205Sent ping
254206Received Hello!
255207Reply: Hello back!
25620852
257−Waiting for message
258209Sent ping
259210Received Hello!
260211Reply: Hello back!
26121251
262−Waiting for message
263213Sent ping
264214Received Hello!
265215Reply: Hello back!
26621650
267−Waiting for message
268217Sent ping
269218Received Hello!
270219Reply: Hello back!
27122049
272−Waiting for message
273221Sent ping
274222Received Hello!
275223Reply: Hello back!
27622448
277−Waiting for message
278225Sent ping
279226Received Hello!
280227Reply: Hello back!
28122847
282−Waiting for message
283229Sent ping
284230Received Hello!
285231Reply: Hello back!
28623246
287−Waiting for message
288233Sent ping
289234Received Hello!
290235Reply: Hello back!
29123645
292−Waiting for message
293237Sent ping
294238Received Hello!
295239Reply: Hello back!
29624044
297−Waiting for message
298241Sent ping
299242Received Hello!
300243Reply: Hello back!
30124443
302−Waiting for message
303245Sent ping
304246Received Hello!
305247Reply: Hello back!
30624842
307−Waiting for message
308249Sent ping
309250Received Hello!
310251Reply: Hello back!
31125241
312−Waiting for message
313253Sent ping
314254Received Hello!
315255Reply: Hello back!
31625640
317−Waiting for message
318257Sent ping
319258Received Hello!
320259Reply: Hello back!
32126039
322−Waiting for message
323261Sent ping
324262Received Hello!
325263Reply: Hello back!
32626438
327−Waiting for message
328265Sent ping
329266Received Hello!
330267Reply: Hello back!
33126837
332−Waiting for message
333269Sent ping
334270Received Hello!
335271Reply: Hello back!
33627236
337−Waiting for message
338273Sent ping
339274Received Hello!
340275Reply: Hello back!
34127635
342−Waiting for message
343277Sent ping
344278Received Hello!
345279Reply: Hello back!
34628034
347−Waiting for message
348281Sent ping
349282Received Hello!
350283Reply: Hello back!
35128433
352−Waiting for message
353285Sent ping
354286Received Hello!
355287Reply: Hello back!
35628832
357−Waiting for message
358289Sent ping
359290Received Hello!
360291Reply: Hello back!
36129231
362−Waiting for message
363293Sent ping
364294Received Hello!
365295Reply: Hello back!
36629630
367−Waiting for message
368297Sent ping
369298Received Hello!
370299Reply: Hello back!
37130029
372−Waiting for message
373301Sent ping
374302Received Hello!
375303Reply: Hello back!
37630428
377−Waiting for message
378305Sent ping
379306Received Hello!
380307Reply: Hello back!
38130827
382−Waiting for message
383309Sent ping
384310Received Hello!
385311Reply: Hello back!
38631226
387−Waiting for message
388313Sent ping
389314Received Hello!
390315Reply: Hello back!
39131625
392−Waiting for message
393317Sent ping
394318Received Hello!
395319Reply: Hello back!
39632024
397−Waiting for message
398321Sent ping
399322Received Hello!
400323Reply: Hello back!
40132423
402−Waiting for message
403325Sent ping
404326Received Hello!
405327Reply: Hello back!
40632822
407−Waiting for message
408329Sent ping
409330Received Hello!
410331Reply: Hello back!
41133221
412−Waiting for message
413333Sent ping
414334Received Hello!
415335Reply: Hello back!
41633620
417−Waiting for message
418337Sent ping
419338Received Hello!
420339Reply: Hello back!
42134019
422−Waiting for message
423341Sent ping
424342Received Hello!
425343Reply: Hello back!
42634418
427−Waiting for message
428345Sent ping
429346Received Hello!
430347Reply: Hello back!
43134817
432−Waiting for message
433349Sent ping
434350Received Hello!
435351Reply: Hello back!
43635216
437−Waiting for message
438353Sent ping
439354Received Hello!
440355Reply: Hello back!
44135615
442−Waiting for message
443357Sent ping
444358Received Hello!
445359Reply: Hello back!
44636014
447−Waiting for message
448361Sent ping
449362Received Hello!
450363Reply: Hello back!
45136413
452−Waiting for message
453365Sent ping
454366Received Hello!
455367Reply: Hello back!
45636812
457−Waiting for message
458369Sent ping
459370Received Hello!
460371Reply: Hello back!
46137211
462−Waiting for message
463373Sent ping
464374Received Hello!
465375Reply: Hello back!
46637610
467−Waiting for message
468377Sent ping
469378Received Hello!
470379Reply: Hello back!
4713809
472−Waiting for message
473381Sent ping
474382Received Hello!
475383Reply: Hello back!
4763848
477−Waiting for message
478385Sent ping
479386Received Hello!
480387Reply: Hello back!
4813887
482−Waiting for message
483389Sent ping
484390Received Hello!
485391Reply: Hello back!
4863926
487−Waiting for message
488393Sent ping
489394Received Hello!
490395Reply: Hello back!
4913965
492−Waiting for message
493397Sent ping
494398Received Hello!
495399Reply: Hello back!
4964004
497−Waiting for message
498401Sent ping
499402Received Hello!
500403Reply: Hello back!
5014043
502−Waiting for message
503405Sent ping
504406Received Hello!
505407Reply: Hello back!
5064082
507−Waiting for message
508409Sent ping
509410Received Hello!
510411Reply: Hello back!
5114121
512−Waiting for message
513413Sent ping
514414Received Hello!
515415Reply: Hello back!