@@ -26,6 +26,8 @@ import Idris.Core.Execute
2626import Idris.Core.Typecheck
2727import Idris.Core.CaseTree
2828
29+import Idris.Docstrings
30+
2931import Control.DeepSeq
3032import Control.Monad
3133import Control.Monad.State.Strict as State
@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
6365-- return (n, (i, top, t'))) ns
6466
6567-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
66−elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
68+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
6769 FC -> FnOpts -> Name -> PTerm -> Idris Type
6870elabType = elabType' False
6971
7072elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
7274 FC -> FnOpts -> Name -> PTerm -> Idris Type
7375elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
7476 n = liftname info n_in in -}
@@ -89,8 +91,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
8991 -- if the type is not complete, note that we'll need to infer
9092 -- things later (for solving metavariables)
9193 when (not (null ds)) $ addTyInferred n
92−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
93−-- addDeferred ds'
94+
9495 mapM_ (elabCaseBlock info opts) is
9596 ctxt <- getContext
9697 logLvl 5 $ "Rechecking"
@@ -106,8 +107,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
106107 -- Add normalised type to internals
107108 rep <- useREPL
108109 when rep $ do
109− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))
110− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
110+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
111+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))
111112
112113 let (t, _) = unApply (getRetTy nty')
113114 let corec = case t of
@@ -115,7 +116,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
115116 [TI _ True _ _] -> True
116117 _ -> False
117118 _ -> False
118− let opts' = if corec then (Coinductive : opts) else opts
119+ -- Productivity checking now via checking for guarded 'Delay'
120+ let opts' = opts -- if corec then (Coinductive : opts) else opts
119121 let usety = if norm then nty' else nty
120122 ds <- checkDef fc [(n, (-1, Nothing, usety))]
121123 addIBC (IBCDef n)
@@ -126,8 +128,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
126128 addDocStr n doc argDocs
127129 addIBC (IBCDoc n)
128130 addIBC (IBCFlags n opts')
129− when (Implicit `elem` opts) $ do addCoercion n
130− addIBC (IBCCoercion n)
131+ when (Implicit `elem` opts') $ do addCoercion n
132+ addIBC (IBCCoercion n)
131133 -- If the function is declared as an error handler and the language
132134 -- extension is enabled, then add it to the list of error handlers.
133135 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
@@ -142,8 +144,6 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
142144 addIBC (IBCErrorHandler n)
143145 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
144146 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
145− when corec $ do setAccessibility n Frozen
146− addIBC (IBCAccess n Frozen)
147147 return usety
148148 where
149149 -- for making an internalapp, we only want the explicit ones, and don't
@@ -171,7 +171,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
171171 tyIsHandler _ = False
172172
173173
174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
174+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
175175 FC -> FnOpts -> Name -> PTerm -> Idris ()
176176elabPostulate info syn doc fc opts n ty
177177 = do elabType info syn doc [] fc opts n ty
@@ -195,7 +195,7 @@ elabPostulate info syn doc fc opts n ty
195195 -- remove it from the deferred definitions list
196196 solveDeferred n
197197
198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()
198+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
199199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
200200 = do let codata = Codata `elem` opts
201201 iLOG (show (fc, doc))
@@ -253,12 +253,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
253253 let metainf = DataMI params
254254 addIBC (IBCMetaInformation n metainf)
255255 -- TMP HACK! Make this a data option
256− when (n /= sUN "Lazy") $ collapseCons n cons
256+ when (n /= sUN "Lazy'") $ collapseCons n cons
257257 updateContext (addDatatype (Data n ttag cty cons))
258258 updateContext (setMetaInformation n metainf)
259259 mapM_ (checkPositive n) cons
260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
261− else return ()
260+ if DefaultEliminator `elem` opts
261+ then evalStateT (elabEliminator params n t dcons info) Map.empty
262+ else return ()
262263 where
263264 checkDefinedAs fc n t ctxt
264265 = case lookupDef n ctxt of
@@ -322,7 +323,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris
322323
323324-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
324325elabEliminator :: [Int] -> Name -> PTerm ->
325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->
326+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
326327 ElabInfo -> EliminatorState ()
327328elabEliminator paramPos n ty cons info = do
328329 elimLog $ "Elaborating eliminator"
@@ -339,7 +340,7 @@ elabEliminator paramPos n ty cons info = do
339340 let motiveConstr = [(motiveName, expl, motive)]
340341 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
341342 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
342− let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
343+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
343344 let clauseConsElimArgs = map getPiName consTerms
344345 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
345346 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
@@ -488,7 +489,7 @@ elabEliminator paramPos n ty cons info = do
488489 splitArgPms _ = ([],[])
489490
490491
491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492493 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
493494 i <- State.lift getIState
494495 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -503,7 +504,7 @@ elabEliminator paramPos n ty cons info = do
503504 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
504505 _ -> return implargs
505506
506− extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
507+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
507508 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
508509 let cons' = replaceParams paramPos generalParameters ty
509510 let (args, resTy) = splitPi cons'
@@ -539,7 +540,7 @@ elabEliminator paramPos n ty cons info = do
539540 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
540541 convertImplPi _ = Nothing
541542
542− generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
543+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
543544 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
544545 let cons' = replaceParams paramPos generalParameters ty
545546 let (args, resTy) = splitPi cons'
@@ -561,7 +562,7 @@ elabEliminator paramPos n ty cons info = do
561562
562563elabPrims :: Idris ()
563564elabPrims = do mapM_ (elabDecl EAll toplevel)
564− (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)
565+ (map (\(opt, decl) -> PData emptyDocstring [] defaultSyntax (fileFC "builtin") opt decl)
565566 (zip
566567 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
567568 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
@@ -665,7 +666,7 @@ elabProvider info syn fc what n ty tm
665666 Provide tm
666667 | what `elem` [ProvTerm, ProvAny] ->
667668 do -- Finally add a top-level definition of the provided term
668− elabType info syn "" [] fc [] n ty
669+ elabType info syn emptyDocstring [] fc [] n ty
669670 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []] -- ipapp
670671 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671672 | otherwise ->
@@ -673,7 +674,7 @@ elabProvider info syn fc what n ty tm
673674 Postulate
674675 | what `elem` [ProvPostulate, ProvAny] ->
675676 do -- Add the postulate
676− elabPostulate info syn "Provided postulate" fc [] n ty
677+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty
677678 logLvl 3 $ "Elaborated provided postulate " ++ show n
678679 | otherwise ->
679680 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -690,7 +691,6 @@ elabProvider info syn fc what n ty tm
690691 , prov == txt "Provider" && provs == txt "Providers" = True
691692 isProviderOf _ _ = False
692693
693−-- | Elaborate a type provider
694694elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
695695elabTransform info fc safe lhs_in rhs_in
696696 = do ctxt <- getContext
@@ -724,8 +724,8 @@ elabTransform info fc safe lhs_in rhs_in
724724 addIBC (IBCTrans (clhs_tm, crhs_tm))
725725
726726
727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
728− PTerm -> String -> Name -> PTerm -> Idris ()
727+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
728+ PTerm -> Docstring -> Name -> PTerm -> Idris ()
729729elabRecord info syn doc fc tyn ty cdoc cn cty
730730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
731731 cty' <- implicit syn cn cty
@@ -797,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
797797
798798 mkProj recty substs cimp ((pn_in, pty), pos)
799799 = do let pn = expandNS syn pn_in
800− let pfnTy = PTy "" [] defaultSyntax fc [] pn
800+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
801801 (PPi expl rec recty
802802 (substMatches substs pty))
803803 let pls = repeat Placeholder
@@ -818,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
818818 let valname = sMN 0 "updateval"
819819 let pt = k (PPi expl pn pty
820820 (PPi expl rec recty recty))
821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt
821+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
822822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
823823 let lhsArgs = pls
824824 let rhsArgs = take pos pls ++ (PRef fc valname) :
@@ -834,7 +834,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
834834 return (pn, pfnTy, PClauses fc [] setname [pclause])
835835
836836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
837− (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
837+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
838838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
839839 = do checkUndefined fc n
840840 ctxt <- getContext
@@ -873,12 +873,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
873873
874874 mkLazy (PPi pl n ty sc)
875875 = let ty' = if getTyName ty
876− then PApp fc (PRef fc (sUN "Lazy")) [pexp ty] -- ipapp
876+ then PApp fc (PRef fc (sUN "Lazy'")) -- ipapp
877+ [pexp (PRef fc (sUN "LazyCodata")),
878+ pexp ty]
877879 else ty in
878880 PPi pl n ty' (mkLazy sc)
879881 mkLazy t = t
880882
881883 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
884+ getTyName (PRef _ n) = n == nsroot tn
882885 getTyName _ = False
883886
884887
@@ -988,7 +991,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
988991 simpleCase tcase False reflect CompileTime fc atys pdef
989992 cov <- coverage
990993 pmissing <-
991− if cov
994+ if cov && not (hasDefault cs)
992995 then do missing <- genClauses fc n (map getLHS pdef) cs
993996 -- missing <- genMissing n scargs sc
994997 missing' <- filterM (checkPossible info fc True n) missing
@@ -1017,6 +1020,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10171020 let tot = if pcover || AssertTotal `elem` opts
10181021 then Unchecked -- finish checking later
10191022 else Partial NotCovering -- already know it's not total
1023+
10201024 -- case lookupCtxt (namespace info) n (idris_flags ist) of
10211025 -- [fs] -> if TotalFn `elem` fs
10221026 -- then case tot of
@@ -1072,7 +1076,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10721076 return ()
10731077 -- addIBC (IBCTotal n tot)
10741078 [] -> return ()
1075− return ()
1079+ -- Check it's covering, if 'covering' option is used. Chase
1080+ -- all called functions, and fail if any of them are also
1081+ -- 'Partial NotCovering'
1082+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
10761083 where
10771084 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
10781085 Right _ -> False
@@ -1092,6 +1099,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10921099 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
10931100 depat acc x = (acc, x)
10941101
1102+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1103+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1104+ hasDefault _ = False
1105+
10951106 getLHS (_, l, _) = l
10961107
10971108 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
@@ -1162,7 +1173,7 @@ elabPE info fc caller r =
11621173 (map (\ (lhs, rhs) ->
11631174 (showTmImpls lhs ++ " = " ++
11641175 showTmImpls rhs)) pats)
1165− elabType info defaultSyntax "" [] fc opts newnm specTy
1176+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
11661177 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11671178 elabClauses info fc opts newnm def
11681179 logLvl 2 $ "Specialised " ++ show newnm)
@@ -1262,10 +1273,6 @@ checkPossible info fc tcgen fname lhs_in
12621273 case recheck ctxt [] (forget lhs_tm) lhs_tm of
12631274 OK _ -> return True
12641275 err -> return False
1265−
1266−-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1267−-- return (not b) -- then return (Just lhs_tm) else return Nothing
1268−-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
12691276 Error err -> if tcgen then return False
12701277 else return (impossibleError err)
12711278 where impossibleError (CantUnify _ topx topy e _ _)
@@ -1273,6 +1280,7 @@ checkPossible info fc tcgen fname lhs_in
12731280 impossibleError (CantConvert _ _ _) = False
12741281 impossibleError (At _ e) = impossibleError e
12751282 impossibleError (Elaborating _ _ e) = impossibleError e
1283+ impossibleError (ElaboratingArg _ _ _ e) = impossibleError e
12761284 impossibleError _ = True
12771285
12781286 sameFam topx topy
@@ -1382,7 +1390,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13821390 inj <- get_inj
13831391 return (res, probs, inj))
13841392
1385− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1393+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
13861394
13871395 let lhs_tm = orderPats (getInferTerm lhs')
13881396 let lhs_ty = getInferType lhs'
@@ -1401,8 +1409,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14011409
14021410 rep <- useREPL
14031411 when rep $ do
1404− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1405− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1412+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
1413+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
14061414
14071415 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
14081416 -- Elaborate where block
@@ -1446,14 +1454,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14461454 probs <- get_probs
14471455 return (tm, ds, is, probs))
14481456
1449− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1457+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
14501458
14511459 logLvl 5 "DONE CHECK"
14521460 logLvl 2 $ "---> " ++ show rhs'
1453− when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)
1461+ when (not (null defer)) $ iLOG $ "DEFERRED " ++
1462+ show (map (\ (n, (_,_,t)) -> (n, t)) defer)
14541463 def' <- checkDef fc defer
14551464 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
14561465 addDeferred def''
1466+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
14571467
14581468 when (not (null def')) $ do
14591469 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
@@ -1721,7 +1731,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17211731
17221732data MArgTy = IA | EA | CA deriving Show
17231733
1724−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1734+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
17251735 FC -> [PTerm] ->
17261736 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
17271737elabClass info syn doc fc constraints tn ps ds
@@ -1748,7 +1758,7 @@ elabClass info syn doc fc constraints tn ps ds
17481758 let cty = impbind ps $ conbind constraints
17491759 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
17501760 constraint
1751− let cons = [("", [], cn, cty, fc, [])]
1761+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
17521762 let ddecl = PDatadecl tn tty cons
17531763 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
17541764 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl
@@ -1803,7 +1813,7 @@ elabClass info syn doc fc constraints tn ps ds
18031813 case lookup n mtys of
18041814 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
18051815 let ds = map (decorateid defaultdec)
1806− [PTy "" [] syn fc [] n ty',
1816+ [PTy emptyDocstring [] syn fc [] n ty',
18071817 PClauses fc (o ++ opts) n cs]
18081818 iLOG (show ds)
18091819 return (n, ((defaultdec n, ds!!1), ds))
@@ -1841,7 +1851,7 @@ elabClass info syn doc fc constraints tn ps ds
18411851 addInstance False conn' cfn
18421852 addIBC (IBCInstance False conn' cfn)
18431853-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1844− return [PTy "" [] syn fc [] cfn ty,
1854+ return [PTy emptyDocstring [] syn fc [] cfn ty,
18451855 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
18461856
18471857 -- Generate a top level function which looks up a method in a given
@@ -1905,7 +1915,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19051915 let constraint = PApp fc (PRef fc n) (map pexp ps) -- ipapp
19061916 let iname = mkiname n ps expn
19071917 when (what /= EDefns) $ do
1908− nty <- elabType' True info syn "" [] fc [] iname t
1918+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
19091919 -- if the instance type matches any of the instances we have already,
19101920 -- and it's not a named instance, then it's overlapping, so report an error
19111921 case expn of
@@ -1970,10 +1980,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19701980 iLOG (show idecls)
19711981 mapM_ (elabDecl EAll info) idecls
19721982 addIBC (IBCInstance intInst n iname)
1973−-- -- for each constraint, build a top level function to chase it
1974−-- logLvl 5 $ "Building functions"
1975−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1976−-- mapM_ (elabDecl EAll info) (concat fns)
1983+
19771984 where
19781985 intInst = case ps of
19791986 [PConstant (AType (ATInt ITNative))] -> True
@@ -2057,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20572064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
20582065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
20592066
2060− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t
2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
20612068
20622069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
20632070 conbind [] x = x
@@ -2304,7 +2311,7 @@ inferredDiff fc inf user =
23042311-- | Check a PTerm against documentation and ensure that every documented
23052312-- argument actually exists. This must be run _after_ implicits have been
23062313-- found, or it will give spurious errors.
2307−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()
2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
23082315checkDocs fc args tm = cd (Map.fromList args) tm
23092316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
23102317 cd as _ | Map.null as = return ()