@@ -4,6 +4,7 @@
44module Idris.ElabDecls where
55
66import Idris.AbsSyntax
7+import Idris.ASTUtils
78import Idris.DSL
89import Idris.Error
910import Idris.Delaborate
@@ -16,6 +17,7 @@ import Idris.Primitives
1617import Idris.Inliner
1718import Idris.PartialEval
1819import Idris.DeepSeq
20+import Idris.Output (iputStrLn, pshow, iWarn)
1921import IRTS.Lang
2022import Paths_idris
2123
@@ -26,6 +28,12 @@ import Idris.Core.Execute
2628import Idris.Core.Typecheck
2729import Idris.Core.CaseTree
2830
31+import Idris.Docstrings
32+
33+import Prelude hiding (id, (.))
34+import Control.Category
35+
36+import Control.Applicative hiding (Const)
2937import Control.DeepSeq
3038import Control.Monad
3139import Control.Monad.State.Strict as State
@@ -34,6 +42,7 @@ import Data.Maybe
3442import Debug.Trace
3543
3644import qualified Data.Map as Map
45+import qualified Data.Set as S
3746import qualified Data.Text as T
3847import Data.Char(isLetter, toLower)
3948import Data.List.Split (splitOn)
@@ -56,32 +65,37 @@ checkAddDef add toplvl fc [] = return []
5665checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
5766 = do ctxt <- getContext
5867 (t', _) <- recheckC fc [] t
59− when add $ addDeferred [(n, (i, top, t, toplvl))]
68+ when add $ do addDeferred [(n, (i, top, t, toplvl))]
69+ addIBC (IBCDef n)
6070 ns' <- checkAddDef add toplvl fc ns
6171 return ((n, (i, top, t')) : ns')
6272-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
6373-- return (n, (i, top, t'))) ns
6474
6575-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
66−elabType :: ElabInfo -> SyntaxInfo -> String ->
76+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
6777 FC -> FnOpts -> Name -> PTerm -> Idris Type
6878elabType = elabType' False
6979
7080elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String ->
81+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
7282 FC -> FnOpts -> Name -> PTerm -> Idris Type
73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
74− n = liftname info n_in in -}
83+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
84+ n = liftname info n_in in -}
7585 do checkUndefined fc n
7686 ctxt <- getContext
7787 i <- getIState
7888
79− logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'
89+ logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'
8090 ty' <- addUsingConstraints syn fc ty'
81− ty' <- implicit syn n ty'
91+ ty' <- implicit info syn n ty'
92+
93+ let ty = addImpl i ty'
94+ inacc = inaccessibleArgs 0 ty
95+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
96+ logLvl 5 $ show n ++ " type " ++ showTmImpls ty
97+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc
8298
83− let ty = addImpl i ty'
84− logLvl 1 $ show n ++ " type " ++ showTmImpls ty
8599 ((tyT, defer, is), log) <-
86100 tclift $ elaborate ctxt n (TType (UVal 0)) []
87101 (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -89,8 +103,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
89103 -- if the type is not complete, note that we'll need to infer
90104 -- things later (for solving metavariables)
91105 when (not (null ds)) $ addTyInferred n
92−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
93−-- addDeferred ds'
106+
94107 mapM_ (elabCaseBlock info opts) is
95108 ctxt <- getContext
96109 logLvl 5 $ "Rechecking"
@@ -106,27 +119,32 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
106119 -- Add normalised type to internals
107120 rep <- useREPL
108121 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')))
122+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
123+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))
111124
112125 let (t, _) = unApply (getRetTy nty')
113126 let corec = case t of
114127 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
115− [TI _ True _ _] -> True
128+ [TI _ True _ _ _] -> True
116129 _ -> False
117130 _ -> False
118− let opts' = if corec then (Coinductive : opts) else opts
131+ -- Productivity checking now via checking for guarded 'Delay'
132+ let opts' = opts -- if corec then (Coinductive : opts) else opts
119133 let usety = if norm then nty' else nty
120134 ds <- checkDef fc [(n, (-1, Nothing, usety))]
121135 addIBC (IBCDef n)
122136 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
123137 addDeferred ds'
124138 setFlags n opts'
125− addDocStr n doc
139+ checkDocs fc argDocs ty
140+ addDocStr n doc argDocs
126141 addIBC (IBCDoc n)
127142 addIBC (IBCFlags n opts')
128− when (Implicit `elem` opts) $ do addCoercion n
129− addIBC (IBCCoercion n)
143+ fputState (opt_inaccessible . ist_optimisation n) inacc
144+ addIBC (IBCOpt n)
145+ when (Implicit `elem` opts') $ do addCoercion n
146+ addIBC (IBCCoercion n)
147+
130148 -- If the function is declared as an error handler and the language
131149 -- extension is enabled, then add it to the list of error handlers.
132150 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
@@ -141,8 +159,6 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
141159 addIBC (IBCErrorHandler n)
142160 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
143161 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
144− when corec $ do setAccessibility n Frozen
145− addIBC (IBCAccess n Frozen)
146162 return usety
147163 where
148164 -- for making an internalapp, we only want the explicit ones, and don't
@@ -167,59 +183,57 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
167183 , ns2 == map txt ["Maybe", "Prelude"]
168184 , ns3 == map txt ["List", "Prelude"]
169185 , ns4 == map txt ["Errors","Reflection","Language"] = True
170− tyIsHandler _ = False
186+ tyIsHandler _ = False
187+
188+-- Get the list of (index, name) of inaccessible arguments from the type.
189+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
190+inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
191+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
192+inaccessibleArgs i (PPi plicity n ty t)
193+ | InaccessibleArg `elem` pargopts plicity
194+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
195+ | otherwise
196+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}
197+inaccessibleArgs _ _ = []
198+
199+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
200+ FC -> FnOpts -> Name -> PTerm -> Idris ()
201+elabPostulate info syn doc fc opts n ty = do
202+ elabType info syn doc [] fc opts n ty
203+ putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
204+ addIBC (IBCPostulate n)
171205
206+ -- remove it from the deferred definitions list
207+ solveDeferred n
172208
173−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
174− FC -> FnOpts -> Name -> PTerm -> Idris ()
175−elabPostulate info syn doc fc opts n ty
176− = do elabType info syn doc fc opts n ty
177− -- make sure it's collapsible, so it is never needed at run time
178− -- start by getting the elaborated type
179− ctxt <- getContext
180− fty <- case lookupTy n ctxt of
181− [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
182− [ty] -> return ty
183− ist <- getIState
184− let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
185− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
186− let postOK = case ap of
187− P _ tn _ -> case lookupCtxt tn
188− (idris_optimisation ist) of
189− [oi] -> collapsible oi
190− _ -> False
191− _ -> False
192− when (not postOK)
193− $ tclift $ tfail (At fc (NonCollapsiblePostulate n))
194− -- remove it from the deferred definitions list
195− solveDeferred n
196−
197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()
198−elabData info syn doc fc opts (PLaterdecl n t_in)
209+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
210+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
199211 = do let codata = Codata `elem` opts
200212 iLOG (show (fc, doc))
201213 checkUndefined fc n
202214 ctxt <- getContext
203215 i <- getIState
204− t_in <- implicit syn n t_in
216+ -- TODO think: something more in info?
217+ t_in <- implicit info syn n t_in
205218 let t = addImpl i t_in
206219 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
207220 (erun fc (build i info False [] n t))
208221 def' <- checkDef fc defer
209222 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
210223 addDeferredTyCon def''
224+ addIBC (IBCDef n)
211225 mapM_ (elabCaseBlock info []) is
212226 (cty, _) <- recheckC fc [] t'
213227 logLvl 2 $ "---> " ++ show cty
214228 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
215229
216−elabData info syn doc fc opts (PDatadecl n t_in dcons)
230+elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
217231 = do let codata = Codata `elem` opts
218232 iLOG (show fc)
219233 undef <- isUndefined fc n
220234 ctxt <- getContext
221235 i <- getIState
222− t_in <- implicit syn n t_in
236+ t_in <- implicit info syn n t_in
223237 let t = addImpl i t_in
224238 ((t', defer, is), log) <-
225239 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -235,33 +249,54 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
235249 logLvl 2 $ "---> " ++ show cty
236250 -- temporary, to check cons
237251 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
238− cons <- mapM (elabCon info syn n codata) dcons
252+ let cnameinfo = cinfo info (map cname dcons)
253+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
239254 ttag <- getName
240255 i <- getIState
241256 let as = map (const Nothing) (getArgTys cty)
242257 let params = findParams (map snd cons)
243258 logLvl 2 $ "Parameters : " ++ show params
244− putIState (i { idris_datatypes =
245− addDef n (TI (map fst cons) codata opts params)
259+ -- TI contains information about mutually declared types - this will
260+ -- be updated when the mutual block is complete
261+ putIState (i { idris_datatypes =
262+ addDef n (TI (map fst cons) codata opts params [n])
246263 (idris_datatypes i) })
247264 addIBC (IBCDef n)
248265 addIBC (IBCData n)
249− addDocStr n doc
266+ checkDocs fc argDocs t_in
267+ addDocStr n doc argDocs
250268 addIBC (IBCDoc n)
251269 let metainf = DataMI params
252270 addIBC (IBCMetaInformation n metainf)
253271 -- TMP HACK! Make this a data option
254− when (n /= sUN "Lazy") $ collapseCons n cons
255272 updateContext (addDatatype (Data n ttag cty cons))
256273 updateContext (setMetaInformation n metainf)
257− mapM_ (checkPositive n) cons
258− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
259− else return ()
274+ mapM_ totcheck (zip (repeat fc) (map fst cons))
275+-- mapM_ (checkPositive n) cons
276+
277+ -- if there's exactly one constructor,
278+ -- mark both the type and the constructor as detaggable
279+ case cons of
280+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n
281+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
282+ _ -> return ()
283+
284+ -- create an eliminator
285+ when (DefaultEliminator `elem` opts) $
286+ evalStateT (elabEliminator params n t dcons info) Map.empty
260287 where
288+ setDetaggable :: Name -> Idris ()
289+ setDetaggable n = do
290+ ist <- getIState
291+ let opt = idris_optimisation ist
292+ case lookupCtxt n opt of
293+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
294+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
295+
261296 checkDefinedAs fc n t ctxt
262297 = case lookupDef n ctxt of
263298 [] -> return ()
264− [TyDecl _ ty] ->
299+ [TyDecl _ ty] ->
265300 case converts ctxt [] t ty of
266301 OK () -> return ()
267302 _ -> tclift $ tfail (At fc (AlreadyDefined n))
@@ -316,38 +351,56 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
316351 | otherwise = count n ts
317352 mParam args (_ : rest) = Nothing : mParam args rest
318353
354+ cname (_, _, n, _, _, _) = n
355+
356+ -- Abuse of ElabInfo.
357+ -- TODO Contemplate whether the ElabInfo type needs modification.
358+ cinfo :: ElabInfo -> [Name] -> ElabInfo
359+ cinfo info ds
360+ = let newps = params info
361+ dsParams = map (\n -> (n, [])) ds
362+ newb = addAlist dsParams (inblock info)
363+ l = liftname info in
364+ info { params = newps,
365+ inblock = newb,
366+ liftname = id -- Is this appropriate?
367+ }
368+
319369type EliminatorState = StateT (Map.Map String Int) Idris
320370
321−-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
322−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->
371+-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
372+elabEliminator :: [Int] -> Name -> PTerm ->
373+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
323374 ElabInfo -> EliminatorState ()
324375elabEliminator paramPos n ty cons info = do
325376 elimLog $ "Elaborating eliminator"
377+ put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
326378 let (cnstrs, _) = splitPi ty
327379 let (splittedTy@(pms, idxs)) = splitPms cnstrs
328380 generalParams <- namePis False pms
329381 motiveIdxs <- namePis False idxs
330382 let motive = mkMotive n paramPos generalParams motiveIdxs
331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
332− name <- freshName $ "elim_" ++ simpleName cnm
333− consTerm <- extractConsTerm c generalParams
334− return (name, expl, consTerm)) cons
383+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do
384+ name <- freshName $ "elim_" ++ simpleName cnm
385+ consTerm <- extractConsTerm c generalParams
386+ return (name, expl, consTerm)) cons
335387 scrutineeIdxs <- namePis False idxs
336388 let motiveConstr = [(motiveName, expl, motive)]
337389 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
338390 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
339− let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
391+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
340392 let clauseConsElimArgs = map getPiName consTerms
341393 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
342394 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
343395 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
396+ elimLog elimSig
344397 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
345398 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
346− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
399+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
347400 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
348401 -- Do not elaborate clauses if there aren't any
349402 case eliminatorClauses of
350− [] -> return ()
403+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
351404 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
352405 where elimLog :: String -> EliminatorState ()
353406 elimLog s = State.lift (logLvl 2 s)
@@ -410,9 +463,9 @@ elabEliminator paramPos n ty cons info = do
410463 freshName key = do
411464 nameMap <- get
412465 let i = fromMaybe 0 (Map.lookup key nameMap)
413− let name = key ++ show i
466+ let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
414467 put $ Map.insert key (i+1) nameMap
415− return (sUN name)
468+ return name
416469
417470 scrutineeName :: Name
418471 scrutineeName = sUN "scrutinee"
@@ -485,7 +538,7 @@ elabEliminator paramPos n ty cons info = do
485538 splitArgPms _ = ([],[])
486539
487540
488− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
541+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
489542 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
490543 i <- State.lift getIState
491544 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -500,12 +553,12 @@ elabEliminator paramPos n ty cons info = do
500553 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
501554 _ -> return implargs
502555
503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
556+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
557+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
505558 let cons' = replaceParams paramPos generalParameters ty
506559 let (args, resTy) = splitPi cons'
507560 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
508− consArgs <- namePis True args
561+ consArgs <- namePis False args
509562 let recArgs = findRecArgs consArgs
510563 let recMotives = map applyRecMotive recArgs
511564 let (_, consIdxs) = splitArgPms resTy
@@ -536,15 +589,15 @@ elabEliminator paramPos n ty cons info = do
536589 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
537590 convertImplPi _ = Nothing
538591
539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
592+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
593+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
541594 let cons' = replaceParams paramPos generalParameters ty
542595 let (args, resTy) = splitPi cons'
543596 i <- State.lift getIState
544597 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
545598 let (_, generalIdxs') = splitArgPms resTy
546599 let generalIdxs = map pexp generalIdxs'
547− consArgs <- namePis True args
600+ consArgs <- namePis False args
548601 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
549602 let recArgs = findRecArgs consArgs
550603 let recElims = map applyRecElim recArgs
@@ -558,10 +611,12 @@ elabEliminator paramPos n ty cons info = do
558611
559612elabPrims :: Idris ()
560613elabPrims = do mapM_ (elabDecl EAll toplevel)
561− (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)
562− (zip
614+ (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
615+ (zip4
563616 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
564− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
617+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
618+ [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
619+ [[], [], [], pairParamDoc, eqParamDoc]))
565620 addNameHint eqTy (sUN "prf")
566621 elabDecl EAll toplevel elimDecl
567622 mapM_ elabPrim primitives
@@ -626,8 +681,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
626681
627682
628683-- | Elaborate a type provider
629−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()
630−elabProvider info syn fc what n ty tm
684+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()
685+elabProvider info syn fc what n
631686 = do i <- getIState
632687 -- Ensure that the experimental extension is enabled
633688 unless (TypeProviders `elem` idris_language_extensions i) $
@@ -637,12 +692,17 @@ elabProvider info syn fc what n ty tm
637692 ctxt <- getContext
638693
639694 -- First elaborate the expected type (and check that it's a type)
640− (ty', typ) <- elabVal toplevel False ty
695+ -- The goal type for a postulate is always Type.
696+ (ty', typ) <- case what of
697+ ProvTerm ty p -> elabVal toplevel False ty
698+ ProvPostulate _ -> elabVal toplevel False PType
641699 unless (isTType typ) $
642700 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
643701
644702 -- Elaborate the provider term to TT and check that the type matches
645− (e, et) <- elabVal toplevel False tm
703+ (e, et) <- case what of
704+ ProvTerm _ tm -> elabVal toplevel False tm
705+ ProvPostulate tm -> elabVal toplevel False tm
646706 unless (isProviderOf (normalise ctxt [] ty') et) $
647707 ifail $ "Expected provider type IO (Provider (" ++
648708 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
@@ -653,25 +713,22 @@ elabProvider info syn fc what n ty tm
653713 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
654714 [Erased, e])
655715 let rhs' = normalise ctxt [] rhs
656− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
716+ logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
657717
658718 -- Extract the provided term or postulate from the type provider
659719 provided <- getProvided fc rhs'
660720
661721 case provided of
662722 Provide tm
663− | what `elem` [ProvTerm, ProvAny] ->
723+ | ProvTerm ty _ <- what ->
664724 do -- Finally add a top-level definition of the provided term
665− elabType info syn "" fc [] n ty
725+ elabType info syn emptyDocstring [] fc [] n ty
666726 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
667− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
668− | otherwise ->
669− ierror . Msg $ "Attempted to provide a term where a postulate was expected."
670− Postulate
671− | what `elem` [ProvPostulate, ProvAny] ->
727+ logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
728+ | ProvPostulate _ <- what ->
672729 do -- Add the postulate
673− elabPostulate info syn "Provided postulate" fc [] n ty
674− logLvl 1 $ "Elaborated provided postulate " ++ show n
730+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
731+ logLvl 3 $ "Elaborated provided postulate " ++ show n
675732 | otherwise ->
676733 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
677734
@@ -687,7 +744,6 @@ elabProvider info syn fc what n ty tm
687744 , prov == txt "Provider" && provs == txt "Providers" = True
688745 isProviderOf _ _ = False
689746
690−-- | Elaborate a type provider
691747elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
692748elabTransform info fc safe lhs_in rhs_in
693749 = do ctxt <- getContext
@@ -721,12 +777,18 @@ elabTransform info fc safe lhs_in rhs_in
721777 addIBC (IBCTrans (clhs_tm, crhs_tm))
722778
723779
724−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
725− PTerm -> String -> Name -> PTerm -> Idris ()
726−elabRecord info syn doc fc tyn ty cdoc cn cty
727− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])
728− cty' <- implicit syn cn cty
780+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
781+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
782+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
783+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
784+ -- TODO think: something more in info?
785+ cty' <- implicit info syn cn cty_in
729786 i <- getIState
787+
788+ -- get bound implicits and propagate to setters (in case they
789+ -- provide useful information for inference)
790+ let extraImpls = getBoundImpls cty'
791+
730792 cty <- case lookupTy cn (tt_ctxt i) of
731793 [t] -> return (delab i t)
732794 _ -> ifail "Something went inexplicably wrong"
@@ -735,14 +797,29 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
735797 let ptys = getProjs [] (renameBs cimp cty)
736798 let ptys_u = getProjs [] cty
737799 let recty = getRecTy cty
738− logLvl 6 $ show (recty, ptys)
800+
801+ -- rename indices when we generate the getter/setter types, so
802+ -- that they don't clash with the names of the projections
803+ -- we're generating
804+ let index_names_in = getRecNameMap "_in" recty
805+ let recty_in = substMatches index_names_in recty
806+
807+ logLvl 1 $ show (recty, ptys)
739808 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
740809 [pexp (PRef fc rec)])) ptys
741− proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
810+
811+ -- Generate projection functions
812+ proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
813+ logLvl 3 $ show proj_decls
742814 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
743815 let implBinds = getImplB id cty'
744− update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
816+
817+ -- Generate update functions
818+ update_decls <- mapM (mkUpdate recty index_names_in extraImpls
819+ (getFieldNames cty')
820+ implBinds (length nonImp)) (zip nonImp [0..])
745821 mapM_ (elabDecl EAll info) (concat proj_decls)
822+ logLvl 3 $ show update_decls
746823 mapM_ (tryElabDecl info) (update_decls)
747824 where
748825-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -757,17 +834,21 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
757834 (\v -> do iputStrLn $ show fc ++
758835 ":Warning - can't generate setter for " ++
759836 show fn ++ " (" ++ show ty ++ ")"
837+-- ++ "\n" ++ pshow i v
760838 putIState i)
761839
762− getImplB k (PPi (Imp l s _ _) n Placeholder sc)
840+ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
841+ getBoundImpls _ = []
842+
843+ getImplB k (PPi (Imp l s _) n Placeholder sc)
763844 = getImplB k sc
764− getImplB k (PPi (Imp l s d p) n ty sc)
765− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc
845+ getImplB k (PPi (Imp l s p) n ty sc)
846+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc
766847 getImplB k (PPi _ n ty sc)
767848 = getImplB k sc
768849 getImplB k _ = k
769850
770− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)
851+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
771852 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
772853 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
773854 renameBs _ t = t
@@ -775,9 +856,19 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
775856 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
776857 getProjs acc r = reverse acc
777858
859+ getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
860+ getFieldNames (PPi _ _ _ s) = getFieldNames s
861+ getFieldNames _ = []
862+
778863 getRecTy (PPi _ n ty s) = getRecTy s
779864 getRecTy t = t
780865
866+ getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args
867+ where
868+ toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))
869+ toMN _ = Nothing
870+ getRecNameMap x _ = []
871+
781872 rec = sMN 0 "rec"
782873
783874 mkp (UN n) = sMN 0 ("p_" ++ str n)
@@ -794,7 +885,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
794885
795886 mkProj recty substs cimp ((pn_in, pty), pos)
796887 = do let pn = expandNS syn pn_in
797− let pfnTy = PTy "" defaultSyntax fc [] pn
888+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
798889 (PPi expl rec recty
799890 (substMatches substs pty))
800891 let pls = repeat Placeholder
@@ -810,13 +901,23 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
810901
811902 implicitise (pa, t) = pa { getTm = t }
812903
813− mkUpdate recty k num ((pn, pty), pos)
904+ -- If the 'pty' we're updating includes anything in 'substs', we're
905+ -- updating the type as well, so use recty', otherwise just use
906+ -- recty
907+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)
814908 = do let setname = expandNS syn $ mkType pn
815909 let valname = sMN 0 "updateval"
816− let pt = k (PPi expl pn pty
817− (PPi expl rec recty recty))
818− let pfnTy = PTy "" defaultSyntax fc [] setname pt
819− let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
910+ let pn_out = sMN 0 (show pn ++ "_out")
911+ let pn_in = sMN 0 (show pn ++ "_in")
912+ let recty_in = substMatches [(pn, PRef fc pn_in)] recty
913+ let recty_out = substMatches [(pn, PRef fc pn_out)] recty
914+ let pt = substMatches inames $
915+ k (implBindUp extras inames (PPi expl pn_out pty
916+ (PPi expl rec recty_in recty_out)))
917+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
918+-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
919+ let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
920+ let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames
820921 let lhsArgs = pls
821922 let rhsArgs = take pos pls ++ (PRef fc valname) :
822923 drop (pos + 1) pls
@@ -830,15 +931,31 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
830931 (map pexp rhsArgs)) []
831932 return (pn, pfnTy, PClauses fc [] setname [pclause])
832933
934+ implBindUp [] is t = t
935+ implBindUp ((n, ty):ns) is t
936+ = let n' = case lookup n is of
937+ Just (PRef _ x) -> x
938+ _ -> n in
939+ if n `elem` allNamesIn t
940+ then PPi impl n' ty (implBindUp ns is t)
941+ else implBindUp ns is t
942+
943+-- FIXME: 'forcenames' is an almighty hack! Need a better way of
944+-- erasing non-forceable things
945+-- ^^^
946+-- TODO: the above is a comment from the past;
947+-- forcenames is probably no longer needed
833948elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
834− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
835−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
949+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
950+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
836951 = do checkUndefined fc n
837952 ctxt <- getContext
838953 i <- getIState
839− t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
954+ t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
840955 let t = addImpl i t_in
841956 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
957+ let inacc = inaccessibleArgs 0 t
958+ logLvl 5 $ "Inaccessible args: " ++ show inacc
842959 ((t', defer, is), log) <-
843960 tclift $ elaborate ctxt n (TType (UVal 0)) []
844961 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -853,12 +970,11 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
853970 tyIs cty'
854971 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
855972 addIBC (IBCDef n)
856− addDocStr n doc
973+ checkDocs fc argDocs t_in
974+ addDocStr n doc argDocs
857975 addIBC (IBCDoc n)
858− let fs = map (getNamePos 0 t) forcenames
859− -- FIXME: 'forcenames' is an almighty hack! Need a better way of
860− -- erasing non-forceable things
861− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
976+ fputState (opt_inaccessible . ist_optimisation n) inacc
977+ addIBC (IBCOpt n)
862978 return (n, cty')
863979 where
864980 tyIs (Bind n b sc) = tyIs sc
@@ -869,12 +985,15 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
869985
870986 mkLazy (PPi pl n ty sc)
871987 = let ty' = if getTyName ty
872− then PApp fc (PRef fc (sUN "Lazy")) [pexp ty]
988+ then PApp fc (PRef fc (sUN "Lazy'"))
989+ [pexp (PRef fc (sUN "LazyCodata")),
990+ pexp ty]
873991 else ty in
874992 PPi pl n ty' (mkLazy sc)
875993 mkLazy t = t
876994
877995 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
996+ getTyName (PRef _ n) = n == nsroot tn
878997 getTyName _ = False
879998
880999
@@ -888,6 +1007,9 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
8881007elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
8891008elabClauses info fc opts n_in cs = let n = liftname info n_in in
8901009 do ctxt <- getContext
1010+ ist <- getIState
1011+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
1012+
8911013 -- Check n actually exists, with no definition yet
8921014 let tys = lookupTy n ctxt
8931015 let reflect = Reflection `elem` opts
@@ -899,33 +1021,18 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
8991021 tclift $ tfail $ At fc (NoTypeDecl n)
9001022 [ty] -> return ty
9011023 let atys = map snd (getArgTys fty)
902− pats_in <- mapM (elabClause info opts)
1024+ cs_elab <- mapM (elabClause info opts)
9031025 (zip [0..] cs)
1026+ let (pats_in, cs_full) = unzip cs_elab
1027+
9041028 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
9051029
906− -- if the return type of 'ty' is collapsible, the optimised version should
907− -- just do nothing
908− ist <- getIState
909− let (ap, _) = unApply (getRetTy fty)
910− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
911− -- FIXME: Really ought to only do this for total functions!
912− let doNothing = case ap of
913− P _ tn _ -> case lookupCtxt tn
914− (idris_optimisation ist) of
915− [oi] -> collapsible oi
916− _ -> False
917− _ -> False
9181030 solveDeferred n
919− ist <- getIState
920− when doNothing $
921− case lookupCtxt n (idris_optimisation ist) of
922− [oi] -> do let opts = addDef n (oi { collapsible = True })
923− (idris_optimisation ist)
924− putIState (ist { idris_optimisation = opts })
925− _ -> do let opts = addDef n (Optimise True False [] [])
926− (idris_optimisation ist)
927− putIState (ist { idris_optimisation = opts })
928− addIBC (IBCOpt n)
1031+
1032+ -- just ensure that the structure exists
1033+ fmodifyState (ist_optimisation n) id
1034+ addIBC (IBCOpt n)
1035+
9291036 ist <- getIState
9301037 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
9311038
@@ -935,11 +1042,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9351042 let tcase = opt_typecase (idris_options ist)
9361043
9371044 -- Summary of what's about to happen: Definitions go:
938−
939− -- pats_in -> pats -> optpats
940− -- pdef comes from pats,
941− -- optpdef comes from optpats
942− -- Then pdef' is optpdef with forcing/collapsing applied everywhere
1045+ --
1046+ -- pats_in -> pats -> pdef -> pdef'
9431047
9441048 -- addCaseDef builds case trees from <pdef> and <pdef'>
9451049
@@ -968,24 +1072,16 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9681072
9691073 numArgs <- tclift $ sameLength pdef
9701074
971− -- patterns after collapsing optimisation applied
972− -- (i.e. check if the function should do nothing at run time)
973− optpats <- if doNothing
974− then return $ [Right (mkApp (P Bound n Erased)
975− (take numArgs (repeat Erased)), Erased)]
976− else stripCollapsed pats
977−
9781075 case specNames opts of
9791076 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
9801077 _ -> return ()
9811078
982− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
9831079 tree@(CaseDef scargs sc _) <- tclift $
984− simpleCase tcase False reflect CompileTime fc atys pdef
1080+ simpleCase tcase False reflect CompileTime fc inacc atys pdef
9851081 cov <- coverage
9861082 pmissing <-
987− if cov
988− then do missing <- genClauses fc n (map getLHS pdef) cs
1083+ if cov && not (hasDefault cs)
1084+ then do missing <- genClauses fc n (map getLHS pdef) cs_full
9891085 -- missing <- genMissing n scargs sc
9901086 missing' <- filterM (checkPossible info fc True n) missing
9911087 let clhs = map getLHS pdef
@@ -1003,7 +1099,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10031099 let pcover = null pmissing
10041100
10051101 -- pdef' is the version that gets compiled for run-time
1006− pdef_in' <- applyOpts optpdef
1102+ pdef_in' <- applyOpts pdef
10071103 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
10081104
10091105 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
@@ -1013,6 +1109,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10131109 let tot = if pcover || AssertTotal `elem` opts
10141110 then Unchecked -- finish checking later
10151111 else Partial NotCovering -- already know it's not total
1112+
10161113 -- case lookupCtxt (namespace info) n (idris_flags ist) of
10171114 -- [fs] -> if TotalFn `elem` fs
10181115 -- then case tot of
@@ -1029,11 +1126,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10291126 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
10301127
10311128 tree' <- tclift $ simpleCase tcase knowncovering reflect
1032− RunTime fc atys pdef'
1033− logLvl 3 (show tree)
1129+ RunTime fc inacc atys pdef'
1130+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
10341131 logLvl 3 $ "Optimised: " ++ show tree'
10351132 ctxt <- getContext
10361133 ist <- getIState
1134+ let opt = idris_optimisation ist
10371135 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
10381136 (idris_patdefs ist) })
10391137 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
@@ -1043,6 +1141,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10431141 reflect
10441142 (AssertTotal `elem` opts)
10451143 atys
1144+ inacc
10461145 pats
10471146 pdef pdef pdef_inl pdef' ty)
10481147 addIBC (IBCDef n)
@@ -1059,7 +1158,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10591158 let used = findUsedArgs sc' scargs'
10601159 -- let scg = buildSCG i sc scargs
10611160 -- add SCG later, when checking totality
1062− let cg = CGInfo scargs' calls [] used []
1161+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore
10631162 logLvl 2 $ "Called names: " ++ show cg
10641163 addToCG n cg
10651164 addToCalledG n (nub (map fst calls)) -- plus names in type!
@@ -1068,7 +1167,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10681167 return ()
10691168 -- addIBC (IBCTotal n tot)
10701169 [] -> return ()
1071− return ()
1170+ -- Check it's covering, if 'covering' option is used. Chase
1171+ -- all called functions, and fail if any of them are also
1172+ -- 'Partial NotCovering'
1173+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
10721174 where
10731175 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
10741176 Right _ -> False
@@ -1088,13 +1190,18 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10881190 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
10891191 depat acc x = (acc, x)
10901192
1193+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1194+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1195+ hasDefault _ = False
1196+
10911197 getLHS (_, l, _) = l
10921198
10931199 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
10941200 force (normalisePats ctxt [] y))
10951201 simple_lhs ctxt t = t
10961202
1097− simple_rt ctxt (p, x, y) = (p, x, force (rt_simplify ctxt [] y))
1203+ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p
1204+ (rt_simplify ctxt [] y)))
10981205
10991206 -- this is so pattern types are in the right form for erasure
11001207 normalisePats ctxt env (Bind n (PVar t) sc)
@@ -1158,10 +1265,10 @@ elabPE info fc caller r =
11581265 (map (\ (lhs, rhs) ->
11591266 (showTmImpls lhs ++ " = " ++
11601267 showTmImpls rhs)) pats)
1161− elabType info defaultSyntax "" fc opts newnm specTy
1268+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
11621269 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11631270 elabClauses info fc opts newnm def
1164− logLvl 1 $ "Specialised " ++ show newnm)
1271+ logLvl 2 $ "Specialised " ++ show newnm)
11651272 -- if it doesn't work, just don't specialise. Could happen for lots
11661273 -- of valid reasons (e.g. local variables in scope which can't be
11671274 -- lifted out).
@@ -1206,8 +1313,8 @@ elabPE info fc caller r =
12061313
12071314-- Elaborate a value, returning any new bindings created (this will only
12081315-- happen if elaborating as a pattern clause)
1209−elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
1210−elabValBind info aspat tm_in
1316+elabValBind :: ElabInfo -> Bool -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
1317+elabValBind info aspat norm tm_in
12111318 = do ctxt <- getContext
12121319 i <- getIState
12131320 let tm = addImpl i tm_in
@@ -1232,14 +1339,17 @@ elabValBind info aspat tm_in
12321339 logLvl 3 ("Value: " ++ show vtm)
12331340-- recheckC (fileFC "(input)") [] tm'
12341341-- logLvl 2 (show vtm)
1235− (vtm, vty) <- recheckC (fileFC "(input)") [] vtm
1342+ (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
1343+
1344+ let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
1345+ else vtm_in
12361346 let bargs = getPBtys vtm
12371347
12381348 return (vtm, vty, bargs)
12391349
12401350elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
12411351elabVal info aspat tm_in
1242− = do (tm, ty, _) <- elabValBind info aspat tm_in
1352+ = do (tm, ty, _) <- elabValBind info aspat False tm_in
12431353 return (tm, ty)
12441354
12451355-- checks if the clause is a possible left hand side. Returns the term if
@@ -1249,7 +1359,7 @@ checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool
12491359checkPossible info fc tcgen fname lhs_in
12501360 = do ctxt <- getContext
12511361 i <- getIState
1252− let lhs = addImpl i lhs_in
1362+ let lhs = addImplPat i lhs_in
12531363 -- if the LHS type checks, it is possible
12541364 case elaborate ctxt (sMN 0 "patLHS") infP []
12551365 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
@@ -1258,24 +1368,53 @@ checkPossible info fc tcgen fname lhs_in
12581368 case recheck ctxt [] (forget lhs_tm) lhs_tm of
12591369 OK _ -> return True
12601370 err -> return False
1261−
1262−-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1263−-- return (not b) -- then return (Just lhs_tm) else return Nothing
1264−-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
1265− Error err -> if tcgen then return False
1266− else return (impossibleError err)
1267− where impossibleError (CantUnify _ topx topy e _ _)
1268− = not (sameFam topx topy || not (impossibleError e))
1269− impossibleError (CantConvert _ _ _) = False
1270− impossibleError (At _ e) = impossibleError e
1271− impossibleError (Elaborating _ _ e) = impossibleError e
1272− impossibleError _ = True
1371+ -- if it's a recoverable error, the case may become possible
1372+ Error err -> if tcgen then return (recoverable ctxt err)
1373+ else return (validCase ctxt err ||
1374+ recoverable ctxt err)
1375+ where validCase ctxt (CantUnify _ topx topy e _ _)
1376+ = let topx' = normalise ctxt [] topx
1377+ topy' = normalise ctxt [] topy in
1378+ not (sameFam topx' topy' || not (validCase ctxt e))
1379+ validCase ctxt (CantConvert _ _ _) = False
1380+ validCase ctxt (At _ e) = validCase ctxt e
1381+ validCase ctxt (Elaborating _ _ e) = validCase ctxt e
1382+ validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
1383+ validCase ctxt _ = True
1384+
1385+ recoverable ctxt (CantUnify r topx topy e _ _)
1386+ = let topx' = normalise ctxt [] topx
1387+ topy' = normalise ctxt [] topy in
1388+ checkRec topx' topy'
1389+ recoverable ctxt (At _ e) = recoverable ctxt e
1390+ recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e
1391+ recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e
1392+ recoverable _ _ = False
12731393
12741394 sameFam topx topy
12751395 = case (unApply topx, unApply topy) of
12761396 ((P _ x _, _), (P _ y _, _)) -> x == y
12771397 _ -> False
12781398
1399+ -- different notion of recoverable than in unification, since we
1400+ -- have no metavars -- just looking to see if a constructor is failing
1401+ -- to unify with a function that may be reduced later
1402+
1403+ checkRec (App f a) p@(P _ _ _) = checkRec f p
1404+ checkRec p@(P _ _ _) (App f a) = checkRec p f
1405+ checkRec fa@(App _ _) fa'@(App _ _)
1406+ | (f, as) <- unApply fa,
1407+ (f', as') <- unApply fa'
1408+ = if (length as /= length as')
1409+ then checkRec f f'
1410+ else checkRec f f' && and (zipWith checkRec as as')
1411+ checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
1412+ checkRec _ _ = False
1413+
1414+ ntRec x y | Ref <- x = True
1415+ | Ref <- y = True
1416+ | otherwise = False -- name is different, unrecoverable
1417+
12791418getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
12801419 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
12811420getFixedInType i env (_ : is) (Bind n (Pi t) sc)
@@ -1338,16 +1477,19 @@ propagateParams ps t (PRef fc n)
13381477 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
13391478propagateParams ps t x = x
13401479
1480+-- Return the elaborated LHS/RHS, and the original LHS with implicits added
13411481elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1342− Idris (Either Term (Term, Term))
1482+ Idris (Either Term (Term, Term), PTerm)
13431483elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
13441484 = do let tcgen = Dictionary `elem` opts
1485+ i <- get
1486+ let lhs = addImpl i lhs_in
13451487 b <- checkPossible info fc tcgen fname lhs_in
13461488 case b of
13471489 True -> tclift $ tfail (At fc
13481490 (Msg $ show lhs_in ++ " is a valid case"))
13491491 False -> do ptm <- mkPatTm lhs_in
1350− return (Left ptm)
1492+ return (Left ptm, lhs)
13511493elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13521494 = do let tcgen = Dictionary `elem` opts
13531495 ctxt <- getContext
@@ -1378,7 +1520,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13781520 inj <- get_inj
13791521 return (res, probs, inj))
13801522
1381− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1523+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
13821524
13831525 let lhs_tm = orderPats (getInferTerm lhs')
13841526 let lhs_ty = getInferType lhs'
@@ -1397,17 +1539,17 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13971539
13981540 rep <- useREPL
13991541 when rep $ do
1400− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)
1401− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1542+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
1543+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
14021544
14031545 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
14041546 -- Elaborate where block
14051547 ist <- getIState
14061548 windex <- getName
1407− let winfo = pinfo (pvars ist lhs_tm) whereblock windex
14081549 let decls = nub (concatMap declared whereblock)
14091550 let defs = nub (decls ++ concatMap defined whereblock)
14101551 let newargs = pvars ist lhs_tm
1552+ let winfo = pinfo info newargs defs windex
14111553 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
14121554
14131555 -- Split the where block into declarations with a type, and those
@@ -1415,8 +1557,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14151557 -- Elaborate those with a type *before* RHS, those without *after*
14161558 let (wbefore, wafter) = sepBlocks wb
14171559
1418− logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1419− mapM_ (elabDecl' EAll info) wbefore
1560+ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1561+ mapM_ (elabDecl' EAll winfo) wbefore
14201562 -- Now build the RHS, using the type of the LHS as the goal.
14211563 i <- getIState -- new implicits from where block
14221564 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
@@ -1431,7 +1573,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14311573 mapM_ setinj (nub (params ++ inj))
14321574 setNextName
14331575 (_, _, is) <- errAt "right hand side of " fname
1434− (erun fc (build i info False opts fname rhs))
1576+ (erun fc (build i winfo False opts fname rhs))
14351577 errAt "right hand side of " fname
14361578 (erun fc $ psolve lhs_tm)
14371579 hs <- get_holes
@@ -1442,14 +1584,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14421584 probs <- get_probs
14431585 return (tm, ds, is, probs))
14441586
1445− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1587+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
14461588
14471589 logLvl 5 "DONE CHECK"
14481590 logLvl 2 $ "---> " ++ show rhs'
1449− when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)
1591+ when (not (null defer)) $ iLOG $ "DEFERRED " ++
1592+ show (map (\ (n, (_,_,t)) -> (n, t)) defer)
14501593 def' <- checkDef fc defer
14511594 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
14521595 addDeferred def''
1596+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
14531597
14541598 when (not (null def')) $ do
14551599 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
@@ -1457,8 +1601,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14571601 -- Now the remaining deferred (i.e. no type declarations) clauses
14581602 -- from the where block
14591603
1460− mapM_ (elabDecl' EAll info) wafter
1461− mapM_ (elabCaseBlock info opts) is
1604+ mapM_ (elabDecl' EAll winfo) wafter
1605+ mapM_ (elabCaseBlock winfo opts) is
14621606
14631607 ctxt <- getContext
14641608 logLvl 5 $ "Rechecking"
@@ -1478,7 +1622,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14781622 rev <- case ret_fam of
14791623 P _ rfamn _ ->
14801624 case lookupCtxt rfamn (idris_datatypes i) of
1481− [TI _ _ dopts _] ->
1625+ [TI _ _ dopts _ _] ->
14821626 return (DataErrRev `elem` dopts)
14831627 _ -> return False
14841628 _ -> return False
@@ -1486,8 +1630,21 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14861630 when (rev || ErrorReverse `elem` opts) $ do
14871631 addIBC (IBCErrRev (crhs, clhs))
14881632 addErrRev (crhs, clhs)
1489− return $ Right (clhs, crhs)
1633+ return $ (Right (clhs, crhs), lhs)
14901634 where
1635+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
1636+ pinfo info ns ds i
1637+ = let newps = params info ++ ns
1638+ dsParams = map (\n -> (n, map fst newps)) ds
1639+ newb = addAlist dsParams (inblock info)
1640+ l = liftname info in
1641+ info { params = newps,
1642+ inblock = newb,
1643+ liftname = id -- (\n -> case lookupCtxt n newb of
1644+ -- Nothing -> n
1645+ -- _ -> MN i (show n)) . l
1646+ }
1647+
14911648 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
14921649 mkLHSapp t = t
14931650
@@ -1500,7 +1657,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15001657-- = NS (UN ('#':show x)) [show cnum, show fname]
15011658
15021659 sepBlocks bs = sepBlocks' [] bs where
1503− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
1660+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)
15041661 = let (bf, af) = sepBlocks' (n : ns) bs in
15051662 (d : bf, af)
15061663 sepBlocks' ns (d@(PClauses _ _ n _) : bs)
@@ -1510,19 +1667,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15101667 (b : bf, af)
15111668 sepBlocks' ns [] = ([], [])
15121669
1513− pinfo ns ps i
1514− = let ds = concatMap declared ps
1515− newps = params info ++ ns
1516− dsParams = map (\n -> (n, map fst newps)) ds
1517− newb = addAlist dsParams (inblock info)
1518− l = liftname info in
1519− info { params = newps,
1520− inblock = newb,
1521− liftname = id -- (\n -> case lookupCtxt n newb of
1522− -- Nothing -> n
1523− -- _ -> MN i (show n)) . l
1524− }
1525−
15261670
15271671 -- if a hole is just an argument/result of a case block, treat it as
15281672 -- the unit type. Hack to help elaborate case in do blocks.
@@ -1559,7 +1703,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15591703 _ -> []
15601704 let params = getParamsInType i [] fn_is fn_ty
15611705 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1562− logLvl 1 ("LHS: " ++ show lhs)
1706+ logLvl 2 ("LHS: " ++ show lhs)
15631707 ((lhs', dlhs, []), _) <-
15641708 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
15651709 (errAt "left hand side of with in " fname
@@ -1589,6 +1733,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15891733 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
15901734 addDeferred def''
15911735 mapM_ (elabCaseBlock info opts) is
1736+ logLvl 5 ("Checked wval " ++ show wval')
15921737 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
15931738 let cwvaltyN = explicitNames cwvalty
15941739 let cwvalN = explicitNames cwval
@@ -1653,7 +1798,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
16531798 mapM_ (elabCaseBlock info opts) is
16541799 logLvl 5 ("Checked RHS " ++ show rhs')
16551800 (crhs, crhsty) <- recheckC fc [] rhs'
1656− return $ Right (clhs, crhs)
1801+ return $ (Right (clhs, crhs), lhs)
16571802 where
16581803 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
16591804 getImps _ = []
@@ -1687,7 +1832,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
16871832 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
16881833 return $ PWith fc wname lhs ws wval withs'
16891834 mkAux wname toplhs ns ns' c
1690− = ifail $ show fc ++ "badly formed with clause"
1835+ = ifail $ show fc ++ ":badly formed with clause"
16911836
16921837 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
16931838 addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]
@@ -1698,8 +1843,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
16981843 return $ substMatches mvars $
16991844 PApp fc (PRef fc' wname)
17001845 (map pexp ns ++ pexp w : (map pexp ns'))
1701− updateLHS n wname mvars ns ns' tm w
1702− = ifail $ "Not implemented match " ++ show tm
1846+ updateLHS n wname mvars ns_in ns_in' tm w
1847+ = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w
17031848
17041849 keepMvar mvs fc v | v `elem` mvs = PRef fc v
17051850 | otherwise = Placeholder
@@ -1717,10 +1862,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17171862
17181863data MArgTy = IA | EA | CA deriving Show
17191864
1720−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1865+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
17211866 FC -> [PTerm] ->
1722− Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1723−elabClass info syn doc fc constraints tn ps ds
1867+ Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()
1868+elabClass info syn doc fc constraints tn ps pDocs ds
17241869 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
17251870 let tty = pibind ps PType
17261871 let constraint = PApp fc (PRef fc tn)
@@ -1744,10 +1889,10 @@ elabClass info syn doc fc constraints tn ps ds
17441889 let cty = impbind ps $ conbind constraints
17451890 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
17461891 constraint
1747− let cons = [("", cn, cty, fc, [])]
1892+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
17481893 let ddecl = PDatadecl tn tty cons
1749− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1750− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
1894+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
1895+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
17511896 -- for each constraint, build a top level function to chase it
17521897 logLvl 5 $ "Building functions"
17531898 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
@@ -1785,9 +1930,9 @@ elabClass info syn doc fc constraints tn ps ds
17851930 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
17861931 conbind [] x = x
17871932
1788− getMName (PTy _ _ _ _ n _) = nsroot n
1789− tdecl allmeths (PTy doc syn _ o n t)
1790− = do t' <- implicit' syn allmeths n t
1933+ getMName (PTy _ _ _ _ _ n _) = nsroot n
1934+ tdecl allmeths (PTy doc _ syn _ o n t)
1935+ = do t' <- implicit' info syn allmeths n t
17911936 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
17921937 return ( (n, (toExp (map fst ps) Exp t')),
17931938 (n, (doc, o, (toExp (map fst ps) Imp t'))),
@@ -1799,7 +1944,7 @@ elabClass info syn doc fc constraints tn ps ds
17991944 case lookup n mtys of
18001945 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
18011946 let ds = map (decorateid defaultdec)
1802− [PTy "" syn fc [] n ty',
1947+ [PTy emptyDocstring [] syn fc [] n ty',
18031948 PClauses fc (o ++ opts) n cs]
18041949 iLOG (show ds)
18051950 return (n, ((defaultdec n, ds!!1), ds))
@@ -1809,7 +1954,7 @@ elabClass info syn doc fc constraints tn ps ds
18091954 defaultdec (UN n) = sUN ("default#" ++ str n)
18101955 defaultdec (NS n ns) = NS (defaultdec n) ns
18111956
1812− tydecl (PTy _ _ _ _ _ _) = True
1957+ tydecl (PTy _ _ _ _ _ _ _) = True
18131958 tydecl _ = False
18141959 instdecl (PInstance _ _ _ _ _ _ _ _) = True
18151960 instdecl _ = False
@@ -1837,7 +1982,7 @@ elabClass info syn doc fc constraints tn ps ds
18371982 addInstance False conn' cfn
18381983 addIBC (IBCInstance False conn' cfn)
18391984-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1840− return [PTy "" syn fc [] cfn ty,
1985+ return [PTy emptyDocstring [] syn fc [] cfn ty,
18411986 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
18421987
18431988 -- Generate a top level function which looks up a method in a given
@@ -1853,35 +1998,35 @@ elabClass info syn doc fc constraints tn ps ds
18531998 iLOG (showTmImpls ty)
18541999 iLOG (show (m, ty', capp, margs))
18552000 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
1856− return [PTy doc syn fc o m ty',
2001+ return [PTy doc [] syn fc o m ty',
18572002 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
18582003
1859− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc
1860− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc
1861− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc
2004+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc
2005+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc
2006+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc
18622007 getMArgs _ = []
18632008
18642009 getMeth (m:ms) (a:as) x | x == a = PRef fc m
18652010 | otherwise = getMeth ms as x
18662011
1867− lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns
2012+ lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns
18682013 lhsArgs (IA : xs) ns = lhsArgs xs ns
18692014 lhsArgs (CA : xs) ns = lhsArgs xs ns
18702015 lhsArgs [] _ = []
18712016
1872− rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns
2017+ rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns
18732018 rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
18742019 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
18752020 rhsArgs [] _ = []
18762021
1877− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
2022+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)
18782023 = PPi p n ty (insertConstraint c sc)
18792024 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
18802025
18812026 -- make arguments explicit and don't bind class parameters
1882− toExp ns e (PPi (Imp l s _ p) n ty sc)
2027+ toExp ns e (PPi (Imp l s p) n ty sc)
18832028 | n `elem` ns = toExp ns e sc
1884− | otherwise = PPi (e l s "" p) n ty (toExp ns e sc)
2029+ | otherwise = PPi (e l s p) n ty (toExp ns e sc)
18852030 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
18862031 toExp ns e sc = sc
18872032
@@ -1897,11 +2042,14 @@ elabInstance info syn what fc cs n ps t expn ds = do
18972042 i <- getIState
18982043 (n, ci) <- case lookupCtxtName n (idris_classes i) of
18992044 [c] -> return c
1900− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
2045+ [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
2046+ cs -> tclift $ tfail $ At fc
2047+ (CantResolveAlts (map fst cs))
19012048 let constraint = PApp fc (PRef fc n) (map pexp ps)
19022049 let iname = mkiname n ps expn
1903− when (what /= EDefns) $ do
1904− nty <- elabType' True info syn "" fc [] iname t
2050+ let emptyclass = null (class_methods ci)
2051+ when (what /= EDefns || (null ds && not emptyclass)) $ do
2052+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
19052053 -- if the instance type matches any of the instances we have already,
19062054 -- and it's not a named instance, then it's overlapping, so report an error
19072055 case expn of
@@ -1909,7 +2057,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19092057 (class_instances ci)
19102058 addInstance intInst n iname
19112059 Just _ -> addInstance intInst n iname
1912− when (what /= ETypes) $ do
2060+ when (what /= ETypes && (not (null ds && not emptyclass))) $ do
19132061 let ips = zip (class_params ci) ps
19142062 let ns = case n of
19152063 NS n ns' -> ns'
@@ -1917,7 +2065,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19172065 -- get the implicit parameters that need passing through to the
19182066 -- where block
19192067 wparams <- mapM (\p -> case p of
1920− PApp _ _ args -> getWParams args
2068+ PApp _ _ args -> getWParams (map getTm args)
19212069 _ -> return []) ps
19222070 let pnames = map pname (concat (nub wparams))
19232071 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
@@ -1940,21 +2088,33 @@ elabInstance info syn what fc cs n ps t expn ds = do
19402088 let wbTys = map mkTyDecl mtys
19412089 let wbVals = map (decorateid (decorate ns iname)) ds'
19422090 let wb = wbTys ++ wbVals
1943− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)
2091+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
19442092 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
19452093 show (concat (nub wparams))
1946− let lhs = PRef fc iname
2094+
2095+ -- Bring variables in instance head into scope
2096+ ist <- getIState
2097+ let headVars = nub $ mapMaybe (\p -> case p of
2098+ PRef _ n ->
2099+ case lookupTy n (tt_ctxt ist) of
2100+ [] -> Just n
2101+ _ -> Nothing
2102+ _ -> Nothing) ps
2103+-- let lhs = PRef fc iname
2104+ let lhs = PApp fc (PRef fc iname)
2105+ (map (\n -> pimp n (PRef fc n) True) headVars)
19472106 let rhs = PApp fc (PRef fc (instanceName ci))
19482107 (map (pexp . mkMethApp) mtys)
2108+
2109+ logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
2110+ logLvl 5 $ "Instance RHS " ++ show rhs
2111+
19492112 let idecls = [PClauses fc [Dictionary] iname
19502113 [PClause fc iname lhs [] rhs wb]]
19512114 iLOG (show idecls)
19522115 mapM_ (elabDecl EAll info) idecls
19532116 addIBC (IBCInstance intInst n iname)
1954−-- -- for each constraint, build a top level function to chase it
1955−-- logLvl 5 $ "Building functions"
1956−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1957−-- mapM_ (elabDecl EAll info) (concat fns)
2117+
19582118 where
19592119 intInst = case ps of
19602120 [PConstant (AType (ATInt ITNative))] -> True
@@ -1979,7 +2139,8 @@ elabInstance info syn what fc cs n ps t expn ds = do
19792139 -- TODO: largely based upon elabType' - should try to abstract
19802140 elabFindOverlapping i ci iname syn t
19812141 = do ty' <- addUsingConstraints syn fc t
1982− ty' <- implicit syn iname ty'
2142+ -- TODO think: something more in info?
2143+ ty' <- implicit info syn iname ty'
19832144 let ty = addImpl i ty'
19842145 ctxt <- getContext
19852146 ((tyT, _, _), _) <-
@@ -2009,17 +2170,17 @@ elabInstance info syn what fc cs n ps t expn ds = do
20092170
20102171 mkMethApp (n, _, _, ty)
20112172 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
2012− lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'
2173+ lamBind i (PPi (Constraint _ _) _ _ sc) sc'
20132174 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
20142175 lamBind i (PPi _ n ty sc) sc'
20152176 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
20162177 lamBind i _ sc = sc
2017− methArgs i (PPi (Imp _ _ _ _) n ty sc)
2018− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
2019− methArgs i (PPi (Exp _ _ _ _) n ty sc)
2020− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
2021− methArgs i (PPi (Constraint _ _ _) n ty sc)
2022− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc
2178+ methArgs i (PPi (Imp _ _ _) n ty sc)
2179+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2180+ methArgs i (PPi (Exp _ _ _) n ty sc)
2181+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2182+ methArgs i (PPi (Constraint _ _) n ty sc)
2183+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
20232184 methArgs i _ = []
20242185
20252186 papp fc f [] = f
@@ -2027,7 +2188,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20272188
20282189 getWParams [] = return []
20292190 getWParams (p : ps)
2030− | PRef _ n <- getTm p
2191+ | PRef _ n <- p
20312192 = do ps' <- getWParams ps
20322193 ctxt <- getContext
20332194 case lookupP n ctxt of
@@ -2035,15 +2196,15 @@ elabInstance info syn what fc cs n ps t expn ds = do
20352196 _ -> return ps'
20362197 getWParams (_ : ps) = getWParams ps
20372198
2038− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2199+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
20392200 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
20402201
2041− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
2202+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
20422203
20432204 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
20442205 conbind [] x = x
20452206
2046− coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
2207+ coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)
20472208 coninsert cs sc = conbind cs sc
20482209
20492210 insertDefaults :: IState -> Name ->
@@ -2101,7 +2262,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
21012262 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
21022263-}
21032264
2104−decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t
2265+decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t
21052266decorateid decorate (PClauses f o n cs)
21062267 = PClauses f o (decorate n) (map dc cs)
21072268 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
@@ -2155,22 +2316,22 @@ elabDecl' _ info (PFix _ _ _)
21552316 = return () -- nothing to elaborate
21562317elabDecl' _ info (PSyntax _ p)
21572318 = return () -- nothing to elaborate
2158−elabDecl' what info (PTy doc s f o n ty)
2319+elabDecl' what info (PTy doc argdocs s f o n ty)
21592320 | what /= EDefns
21602321 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
2161− elabType info s doc f o n ty
2322+ elabType info s doc argdocs f o n ty
21622323 return ()
21632324elabDecl' what info (PPostulate doc s f o n ty)
21642325 | what /= EDefns
21652326 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
21662327 elabPostulate info s doc f o n ty
2167−elabDecl' what info (PData doc s f co d)
2328+elabDecl' what info (PData doc argDocs s f co d)
21682329 | what /= ETypes
21692330 = do iLOG $ "Elaborating " ++ show (d_name d)
2170− elabData info s doc f co d
2331+ elabData info s doc argDocs f co d
21712332 | otherwise
21722333 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
2173− elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))
2334+ elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))
21742335elabDecl' what info d@(PClauses f o n ps)
21752336 | what /= ETypes
21762337 = do iLOG $ "Elaborating clause " ++ show n
@@ -2184,6 +2345,11 @@ elabDecl' what info (PMutual f ps)
21842345 [p] -> elabDecl what info p
21852346 _ -> do mapM_ (elabDecl ETypes info) ps
21862347 mapM_ (elabDecl EDefns info) ps
2348+ -- record mutually defined data definitions
2349+ let datans = concatMap declared (filter isDataDecl ps)
2350+ mapM_ (setMutData datans) datans
2351+ iLOG $ "Rechecking for positivity " ++ show datans
2352+ mapM_ (\x -> do setTotality x Unchecked) datans
21872353 -- Do totality checking after entire mutual block
21882354 i <- get
21892355 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
@@ -2192,6 +2358,16 @@ elabDecl' what info (PMutual f ps)
21922358 mapM_ buildSCG (idris_totcheck i)
21932359 mapM_ checkDeclTotality (idris_totcheck i)
21942360 clear_totcheck
2361+ where isDataDecl (PData _ _ _ _ _ _) = True
2362+ isDataDecl _ = False
2363+
2364+ setMutData ns n
2365+ = do i <- getIState
2366+ case lookupCtxt n (idris_datatypes i) of
2367+ [x] -> do let x' = x { mutual_types = ns }
2368+ putIState $ i { idris_datatypes
2369+ = addDef n x' (idris_datatypes i) }
2370+ _ -> return ()
21952371
21962372elabDecl' what info (PParams f ns ps)
21972373 = do i <- getIState
@@ -2214,30 +2390,30 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
22142390 ninfo = case namespace info of
22152391 Nothing -> info { namespace = Just [n] }
22162392 Just ns -> info { namespace = Just (n:ns) }
2217−elabDecl' what info (PClass doc s f cs n ps ds)
2393+elabDecl' what info (PClass doc s f cs n ps pdocs ds)
22182394 | what /= EDefns
22192395 = do iLOG $ "Elaborating class " ++ show n
2220− elabClass info (s { syn_params = [] }) doc f cs n ps ds
2396+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds
22212397elabDecl' what info (PInstance s f cs n ps t expn ds)
22222398 = do iLOG $ "Elaborating instance " ++ show n
22232399 elabInstance info s what f cs n ps t expn ds
2224−elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
2400+elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)
22252401 | what /= ETypes
22262402 = do iLOG $ "Elaborating record " ++ show tyn
2227− elabRecord info s doc f tyn ty cdoc cn cty
2403+ elabRecord info s doc f tyn ty opts cdoc cn cty
22282404 | otherwise
22292405 = do iLOG $ "Elaborating [type of] " ++ show tyn
2230− elabData info s doc f [] (PLaterdecl tyn ty)
2406+ elabData info s doc [] f [] (PLaterdecl tyn ty)
22312407elabDecl' _ info (PDSL n dsl)
22322408 = do i <- getIState
22332409 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
22342410 addIBC (IBCDSL n)
22352411elabDecl' what info (PDirective i)
22362412 | what /= EDefns = i
2237−elabDecl' what info (PProvider syn fc provWhat n tp tm)
2413+elabDecl' what info (PProvider syn fc provWhat n)
22382414 | what /= EDefns
22392415 = do iLOG $ "Elaborating type provider " ++ show n
2240− elabProvider info syn fc provWhat n tp tm
2416+ elabProvider info syn fc provWhat n
22412417elabDecl' what info (PTransform fc safety old new)
22422418 = elabTransform info fc safety old new
22432419elabDecl' _ _ _ = return () -- skipped this time
@@ -2282,3 +2458,14 @@ inferredDiff fc inf user =
22822458 Right vs -> return False
22832459 Left (x, y) -> return True
22842460
2461+-- | Check a PTerm against documentation and ensure that every documented
2462+-- argument actually exists. This must be run _after_ implicits have been
2463+-- found, or it will give spurious errors.
2464+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
2465+checkDocs fc args tm = cd (Map.fromList args) tm
2466+ where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2467+ cd as _ | Map.null as = return ()
2468+ | otherwise = ierror . At fc . Msg $
2469+ "There is documentation for argument(s) "
2470+ ++ (concat . intersperse ", " . map show . Map.keys) as
2471+ ++ " but they were not found."