@@ -26,6 +26,8 @@ import Idris.Core.Execute
26import Idris.Core.Typecheck
26import Idris.Core.Typecheck
27import Idris.Core.CaseTree
27import Idris.Core.CaseTree
29+import Idris.Docstrings
29import Control.DeepSeq
31import Control.DeepSeq
30import Control.Monad
32import Control.Monad
31import Control.Monad.State.Strict as State
33import Control.Monad.State.Strict as State
@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
63-- return (n, (i, top, t'))) ns
65-- return (n, (i, top, t'))) ns
65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
67-- | 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)] ->
67 FC -> FnOpts -> Name -> PTerm -> Idris Type
69 FC -> FnOpts -> Name -> PTerm -> Idris Type
68elabType = elabType' False
70elabType = elabType' False
70elabType' :: Bool -> -- normalise it
72elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
72 FC -> FnOpts -> Name -> PTerm -> Idris Type
74 FC -> FnOpts -> Name -> PTerm -> Idris Type
73elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
75elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
74 n = liftname info n_in in -}
76 n = liftname info n_in in -}
@@ -89,8 +91,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
89 -- if the type is not complete, note that we'll need to infer
91 -- if the type is not complete, note that we'll need to infer
90 -- things later (for solving metavariables)
92 -- things later (for solving metavariables)
91 when (not (null ds)) $ addTyInferred n
93 when (not (null ds)) $ addTyInferred n
92−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
94+
94 mapM_ (elabCaseBlock info opts) is
95 mapM_ (elabCaseBlock info opts) is
95 ctxt <- getContext
96 ctxt <- getContext
96 logLvl 5 $ "Rechecking"
97 logLvl 5 $ "Rechecking"
@@ -106,8 +107,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
106 -- Add normalised type to internals
107 -- Add normalised type to internals
107 rep <- useREPL
108 rep <- useREPL
108 when rep $ do
109 when rep $ do
109− addInternalApp (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?
110− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
111+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))
112 let (t, _) = unApply (getRetTy nty')
113 let (t, _) = unApply (getRetTy nty')
113 let corec = case t of
114 let corec = case t of
@@ -115,7 +116,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
115 [TI _ True _ _] -> True
116 [TI _ True _ _] -> True
116 _ -> False
117 _ -> False
117 _ -> False
118 _ -> False
119+ -- Productivity checking now via checking for guarded 'Delay'
118− let opts' = if corec then (Coinductive : opts) else opts
120+ let opts' = opts -- if corec then (Coinductive : opts) else opts
119 let usety = if norm then nty' else nty
121 let usety = if norm then nty' else nty
120 ds <- checkDef fc [(n, (-1, Nothing, usety))]
122 ds <- checkDef fc [(n, (-1, Nothing, usety))]
121 addIBC (IBCDef n)
123 addIBC (IBCDef n)
@@ -126,8 +128,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
126 addDocStr n doc argDocs
128 addDocStr n doc argDocs
127 addIBC (IBCDoc n)
129 addIBC (IBCDoc n)
128 addIBC (IBCFlags n opts')
130 addIBC (IBCFlags n opts')
129− when (Implicit `elem` opts) $ do addCoercion n
131+ when (Implicit `elem` opts') $ do addCoercion n
130− addIBC (IBCCoercion n)
132+ addIBC (IBCCoercion n)
131 -- If the function is declared as an error handler and the language
133 -- If the function is declared as an error handler and the language
132 -- extension is enabled, then add it to the list of error handlers.
134 -- extension is enabled, then add it to the list of error handlers.
133 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
135 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
142 addIBC (IBCErrorHandler n)
144 addIBC (IBCErrorHandler n)
143 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
145 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
144 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
146 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)
147 return usety
147 return usety
149 -- for making an internalapp, we only want the explicit ones, and don't
149 -- 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
171 tyIsHandler _ = False
171 tyIsHandler _ = False
174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
174+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
175 FC -> FnOpts -> Name -> PTerm -> Idris ()
175 FC -> FnOpts -> Name -> PTerm -> Idris ()
176elabPostulate info syn doc fc opts n ty
176elabPostulate info syn doc fc opts n ty
177 = do elabType info syn doc [] fc opts n ty
177 = do elabType info syn doc [] fc opts n ty
@@ -195,7 +195,7 @@ elabPostulate info syn doc fc opts n ty
195 -- remove it from the deferred definitions list
195 -- remove it from the deferred definitions list
196 solveDeferred n
196 solveDeferred n
198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()
198+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
200 = do let codata = Codata `elem` opts
200 = do let codata = Codata `elem` opts
201 iLOG (show (fc, doc))
201 iLOG (show (fc, doc))
@@ -253,12 +253,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
253 let metainf = DataMI params
253 let metainf = DataMI params
254 addIBC (IBCMetaInformation n metainf)
254 addIBC (IBCMetaInformation n metainf)
255 -- TMP HACK! Make this a data option
255 -- TMP HACK! Make this a data option
256− when (n /= sUN "Lazy") $ collapseCons n cons
256+ when (n /= sUN "Lazy'") $ collapseCons n cons
257 updateContext (addDatatype (Data n ttag cty cons))
257 updateContext (addDatatype (Data n ttag cty cons))
258 updateContext (setMetaInformation n metainf)
258 updateContext (setMetaInformation n metainf)
259 mapM_ (checkPositive n) cons
259 mapM_ (checkPositive n) cons
260+ if DefaultEliminator `elem` opts
260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
261+ then evalStateT (elabEliminator params n t dcons info) Map.empty
261− else return ()
262+ else return ()
263 checkDefinedAs fc n t ctxt
264 checkDefinedAs fc n t ctxt
264 = case lookupDef n ctxt of
265 = case lookupDef n ctxt of
@@ -322,7 +323,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris
323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
324-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
324elabEliminator :: [Int] -> Name -> PTerm ->
325elabEliminator :: [Int] -> Name -> PTerm ->
325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->
326+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
326 ElabInfo -> EliminatorState ()
327 ElabInfo -> EliminatorState ()
327elabEliminator paramPos n ty cons info = do
328elabEliminator paramPos n ty cons info = do
328 elimLog $ "Elaborating eliminator"
329 elimLog $ "Elaborating eliminator"
@@ -339,7 +340,7 @@ elabEliminator paramPos n ty cons info = do
339 let motiveConstr = [(motiveName, expl, motive)]
340 let motiveConstr = [(motiveName, expl, motive)]
340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
341 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
342 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
343 let clauseConsElimArgs = map getPiName consTerms
344 let clauseConsElimArgs = map getPiName consTerms
344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
345 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
346 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
@@ -488,7 +489,7 @@ elabEliminator paramPos n ty cons info = do
488 splitArgPms _ = ([],[])
489 splitArgPms _ = ([],[])
491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
493 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
493 i <- State.lift getIState
494 i <- State.lift getIState
494 implargs' <- case lookupCtxt cnm (idris_implicits i) of
495 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -503,7 +504,7 @@ elabEliminator paramPos n ty cons info = do
503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
504 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
504 _ -> return implargs
505 _ -> return implargs
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
507 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
508 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
508 let cons' = replaceParams paramPos generalParameters ty
509 let cons' = replaceParams paramPos generalParameters ty
509 let (args, resTy) = splitPi cons'
510 let (args, resTy) = splitPi cons'
@@ -539,7 +540,7 @@ elabEliminator paramPos n ty cons info = do
539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
540 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
540 convertImplPi _ = Nothing
541 convertImplPi _ = Nothing
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
543 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
544 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
544 let cons' = replaceParams paramPos generalParameters ty
545 let cons' = replaceParams paramPos generalParameters ty
545 let (args, resTy) = splitPi cons'
546 let (args, resTy) = splitPi cons'
@@ -561,7 +562,7 @@ elabEliminator paramPos n ty cons info = do
562elabPrims :: Idris ()
563elabPrims :: Idris ()
563elabPrims = do mapM_ (elabDecl EAll toplevel)
564elabPrims = 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)
566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
567 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
568 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
@@ -665,7 +666,7 @@ elabProvider info syn fc what n ty tm
665 Provide tm
666 Provide tm
666 | what `elem` [ProvTerm, ProvAny] ->
667 | what `elem` [ProvTerm, ProvAny] ->
667 do -- Finally add a top-level definition of the provided term
668 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
669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []] -- ipapp
670 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []] -- ipapp
670 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671 | otherwise ->
672 | otherwise ->
@@ -673,7 +674,7 @@ elabProvider info syn fc what n ty tm
673 Postulate
674 Postulate
674 | what `elem` [ProvPostulate, ProvAny] ->
675 | what `elem` [ProvPostulate, ProvAny] ->
675 do -- Add the postulate
676 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
677 logLvl 3 $ "Elaborated provided postulate " ++ show n
678 logLvl 3 $ "Elaborated provided postulate " ++ show n
678 | otherwise ->
679 | otherwise ->
679 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
680 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -690,7 +691,6 @@ elabProvider info syn fc what n ty tm
690 , prov == txt "Provider" && provs == txt "Providers" = True
691 , prov == txt "Provider" && provs == txt "Providers" = True
691 isProviderOf _ _ = False
692 isProviderOf _ _ = False
693−-- | Elaborate a type provider
694elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
694elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
695elabTransform info fc safe lhs_in rhs_in
695elabTransform info fc safe lhs_in rhs_in
696 = do ctxt <- getContext
696 = do ctxt <- getContext
@@ -724,8 +724,8 @@ elabTransform info fc safe lhs_in rhs_in
724 addIBC (IBCTrans (clhs_tm, crhs_tm))
724 addIBC (IBCTrans (clhs_tm, crhs_tm))
727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
727+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
728− PTerm -> String -> Name -> PTerm -> Idris ()
728+ PTerm -> Docstring -> Name -> PTerm -> Idris ()
729elabRecord info syn doc fc tyn ty cdoc cn cty
729elabRecord info syn doc fc tyn ty cdoc cn cty
730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
731 cty' <- implicit syn cn cty
731 cty' <- implicit syn cn cty
@@ -797,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
798 mkProj recty substs cimp ((pn_in, pty), pos)
798 mkProj recty substs cimp ((pn_in, pty), pos)
799 = do let pn = expandNS syn pn_in
799 = do let pn = expandNS syn pn_in
800− let pfnTy = PTy "" [] defaultSyntax fc [] pn
800+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
801 (PPi expl rec recty
801 (PPi expl rec recty
802 (substMatches substs pty))
802 (substMatches substs pty))
803 let pls = repeat Placeholder
803 let pls = repeat Placeholder
@@ -818,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
818 let valname = sMN 0 "updateval"
818 let valname = sMN 0 "updateval"
819 let pt = k (PPi expl pn pty
819 let pt = k (PPi expl pn pty
820 (PPi expl rec recty recty))
820 (PPi expl rec recty recty))
821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt
821+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
823 let lhsArgs = pls
823 let lhsArgs = pls
824 let rhsArgs = take pos pls ++ (PRef fc valname) :
824 let rhsArgs = take pos pls ++ (PRef fc valname) :
@@ -834,7 +834,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
834 return (pn, pfnTy, PClauses fc [] setname [pclause])
834 return (pn, pfnTy, PClauses fc [] setname [pclause])
836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
836elabCon :: 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)
838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
839 = do checkUndefined fc n
839 = do checkUndefined fc n
840 ctxt <- getContext
840 ctxt <- getContext
@@ -873,12 +873,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
874 mkLazy (PPi pl n ty sc)
874 mkLazy (PPi pl n ty sc)
875 = let ty' = if getTyName ty
875 = 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")),
877 else ty in
879 else ty in
878 PPi pl n ty' (mkLazy sc)
880 PPi pl n ty' (mkLazy sc)
879 mkLazy t = t
881 mkLazy t = t
881 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
883 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
884+ getTyName (PRef _ n) = n == nsroot tn
882 getTyName _ = False
885 getTyName _ = False
@@ -988,7 +991,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
988 simpleCase tcase False reflect CompileTime fc atys pdef
991 simpleCase tcase False reflect CompileTime fc atys pdef
989 cov <- coverage
992 cov <- coverage
990 pmissing <-
993 pmissing <-
991− if cov
994+ if cov && not (hasDefault cs)
992 then do missing <- genClauses fc n (map getLHS pdef) cs
995 then do missing <- genClauses fc n (map getLHS pdef) cs
993 -- missing <- genMissing n scargs sc
996 -- missing <- genMissing n scargs sc
994 missing' <- filterM (checkPossible info fc True n) missing
997 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
1017 let tot = if pcover || AssertTotal `elem` opts
1020 let tot = if pcover || AssertTotal `elem` opts
1018 then Unchecked -- finish checking later
1021 then Unchecked -- finish checking later
1019 else Partial NotCovering -- already know it's not total
1022 else Partial NotCovering -- already know it's not total
1020 -- case lookupCtxt (namespace info) n (idris_flags ist) of
1024 -- case lookupCtxt (namespace info) n (idris_flags ist) of
1021 -- [fs] -> if TotalFn `elem` fs
1025 -- [fs] -> if TotalFn `elem` fs
1022 -- then case tot of
1026 -- then case tot of
@@ -1072,7 +1076,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1072 return ()
1076 return ()
1073 -- addIBC (IBCTotal n tot)
1077 -- addIBC (IBCTotal n tot)
1074 [] -> return ()
1078 [] -> 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
1077 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
1084 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
1078 Right _ -> False
1085 Right _ -> False
@@ -1092,6 +1099,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1092 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1099 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1093 depat acc x = (acc, x)
1100 depat acc x = (acc, x)
1102+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1103+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1104+ hasDefault _ = False
1095 getLHS (_, l, _) = l
1106 getLHS (_, l, _) = l
1097 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
1108 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
@@ -1162,7 +1173,7 @@ elabPE info fc caller r =
1162 (map (\ (lhs, rhs) ->
1173 (map (\ (lhs, rhs) ->
1163 (showTmImpls lhs ++ " = " ++
1174 (showTmImpls lhs ++ " = " ++
1164 showTmImpls rhs)) pats)
1175 showTmImpls rhs)) pats)
1165− elabType info defaultSyntax "" [] fc opts newnm specTy
1176+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
1166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1177 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1167 elabClauses info fc opts newnm def
1178 elabClauses info fc opts newnm def
1168 logLvl 2 $ "Specialised " ++ show newnm)
1179 logLvl 2 $ "Specialised " ++ show newnm)
@@ -1262,10 +1273,6 @@ checkPossible info fc tcgen fname lhs_in
1262 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1273 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1263 OK _ -> return True
1274 OK _ -> return True
1264 err -> return False
1275 err -> return False
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)
1269 Error err -> if tcgen then return False
1276 Error err -> if tcgen then return False
1270 else return (impossibleError err)
1277 else return (impossibleError err)
1271 where impossibleError (CantUnify _ topx topy e _ _)
1278 where impossibleError (CantUnify _ topx topy e _ _)
@@ -1273,6 +1280,7 @@ checkPossible info fc tcgen fname lhs_in
1273 impossibleError (CantConvert _ _ _) = False
1280 impossibleError (CantConvert _ _ _) = False
1274 impossibleError (At _ e) = impossibleError e
1281 impossibleError (At _ e) = impossibleError e
1275 impossibleError (Elaborating _ _ e) = impossibleError e
1282 impossibleError (Elaborating _ _ e) = impossibleError e
1283+ impossibleError (ElaboratingArg _ _ _ e) = impossibleError e
1276 impossibleError _ = True
1284 impossibleError _ = True
1278 sameFam topx topy
1286 sameFam topx topy
@@ -1382,7 +1390,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1382 inj <- get_inj
1390 inj <- get_inj
1383 return (res, probs, inj))
1391 return (res, probs, inj))
1385− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1393+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1387 let lhs_tm = orderPats (getInferTerm lhs')
1395 let lhs_tm = orderPats (getInferTerm lhs')
1388 let lhs_ty = getInferType lhs'
1396 let lhs_ty = getInferType lhs'
@@ -1401,8 +1409,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1402 rep <- useREPL
1410 rep <- useREPL
1403 when rep $ do
1411 when rep $ do
1404− addInternalApp (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?
1405− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1413+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
1407 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1415 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1408 -- Elaborate where block
1416 -- Elaborate where block
@@ -1446,14 +1454,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1446 probs <- get_probs
1454 probs <- get_probs
1447 return (tm, ds, is, probs))
1455 return (tm, ds, is, probs))
1449− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1457+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1451 logLvl 5 "DONE CHECK"
1459 logLvl 5 "DONE CHECK"
1452 logLvl 2 $ "---> " ++ show rhs'
1460 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)
1454 def' <- checkDef fc defer
1463 def' <- checkDef fc defer
1455 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1464 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1456 addDeferred def''
1465 addDeferred def''
1466+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
1458 when (not (null def')) $ do
1468 when (not (null def')) $ do
1459 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
1469 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)
1722data MArgTy = IA | EA | CA deriving Show
1732data MArgTy = IA | EA | CA deriving Show
1724−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1734+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
1725 FC -> [PTerm] ->
1735 FC -> [PTerm] ->
1726 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1736 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1727elabClass info syn doc fc constraints tn ps ds
1737elabClass info syn doc fc constraints tn ps ds
@@ -1748,7 +1758,7 @@ elabClass info syn doc fc constraints tn ps ds
1748 let cty = impbind ps $ conbind constraints
1758 let cty = impbind ps $ conbind constraints
1749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1759 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1750 constraint
1760 constraint
1751− let cons = [("", [], cn, cty, fc, [])]
1761+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
1752 let ddecl = PDatadecl tn tty cons
1762 let ddecl = PDatadecl tn tty cons
1753 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1763 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1754 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl
1764 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
1803 case lookup n mtys of
1813 case lookup n mtys of
1804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1814 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1805 let ds = map (decorateid defaultdec)
1815 let ds = map (decorateid defaultdec)
1806− [PTy "" [] syn fc [] n ty',
1816+ [PTy emptyDocstring [] syn fc [] n ty',
1807 PClauses fc (o ++ opts) n cs]
1817 PClauses fc (o ++ opts) n cs]
1808 iLOG (show ds)
1818 iLOG (show ds)
1809 return (n, ((defaultdec n, ds!!1), ds))
1819 return (n, ((defaultdec n, ds!!1), ds))
@@ -1841,7 +1851,7 @@ elabClass info syn doc fc constraints tn ps ds
1841 addInstance False conn' cfn
1851 addInstance False conn' cfn
1842 addIBC (IBCInstance False conn' cfn)
1852 addIBC (IBCInstance False conn' cfn)
1843-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1853-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1844− return [PTy "" [] syn fc [] cfn ty,
1854+ return [PTy emptyDocstring [] syn fc [] cfn ty,
1845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1855 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1847 -- Generate a top level function which looks up a method in a given
1857 -- 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
1905 let constraint = PApp fc (PRef fc n) (map pexp ps) -- ipapp
1915 let constraint = PApp fc (PRef fc n) (map pexp ps) -- ipapp
1906 let iname = mkiname n ps expn
1916 let iname = mkiname n ps expn
1907 when (what /= EDefns) $ do
1917 when (what /= EDefns) $ do
1908− nty <- elabType' True info syn "" [] fc [] iname t
1918+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
1909 -- if the instance type matches any of the instances we have already,
1919 -- if the instance type matches any of the instances we have already,
1910 -- and it's not a named instance, then it's overlapping, so report an error
1920 -- and it's not a named instance, then it's overlapping, so report an error
1911 case expn of
1921 case expn of
@@ -1970,10 +1980,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
1970 iLOG (show idecls)
1980 iLOG (show idecls)
1971 mapM_ (elabDecl EAll info) idecls
1981 mapM_ (elabDecl EAll info) idecls
1972 addIBC (IBCInstance intInst n iname)
1982 addIBC (IBCInstance intInst n iname)
1973−-- -- for each constraint, build a top level function to chase it
1983+
1974−-- logLvl 5 $ "Building functions"
1975−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1976−-- mapM_ (elabDecl EAll info) (concat fns)
1978 intInst = case ps of
1985 intInst = case ps of
1979 [PConstant (AType (ATInt ITNative))] -> True
1986 [PConstant (AType (ATInt ITNative))] -> True
@@ -2057,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
2057 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2058 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2060− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t
2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
2062 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2063 conbind [] x = x
2070 conbind [] x = x
@@ -2304,7 +2311,7 @@ inferredDiff fc inf user =
2304-- | Check a PTerm against documentation and ensure that every documented
2311-- | Check a PTerm against documentation and ensure that every documented
2305-- argument actually exists. This must be run _after_ implicits have been
2312-- argument actually exists. This must be run _after_ implicits have been
2306-- found, or it will give spurious errors.
2313-- found, or it will give spurious errors.
2307−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()
2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
2308checkDocs fc args tm = cd (Map.fromList args) tm
2315checkDocs fc args tm = cd (Map.fromList args) tm
2309 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2310 cd as _ | Map.null as = return ()
2317 cd as _ | Map.null as = return ()