@@ -4,6 +4,7 @@
4module Idris.ElabDecls where
4module Idris.ElabDecls where
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7import Idris.DSL
8import Idris.DSL
8import Idris.Error
9import Idris.Error
9import Idris.Delaborate
10import Idris.Delaborate
@@ -16,6 +17,7 @@ import Idris.Primitives
16import Idris.Inliner
17import Idris.Inliner
17import Idris.PartialEval
18import Idris.PartialEval
18import Idris.DeepSeq
19import Idris.DeepSeq
20+import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
21import IRTS.Lang
20import Paths_idris
22import Paths_idris
@@ -26,6 +28,12 @@ import Idris.Core.Execute
26import Idris.Core.Typecheck
28import Idris.Core.Typecheck
27import Idris.Core.CaseTree
29import Idris.Core.CaseTree
31+import Idris.Docstrings
33+import Prelude hiding (id, (.))
34+import Control.Category
36+import Control.Applicative hiding (Const)
29import Control.DeepSeq
37import Control.DeepSeq
30import Control.Monad
38import Control.Monad
31import Control.Monad.State.Strict as State
39import Control.Monad.State.Strict as State
@@ -34,6 +42,7 @@ import Data.Maybe
34import Debug.Trace
42import Debug.Trace
36import qualified Data.Map as Map
44import qualified Data.Map as Map
45+import qualified Data.Set as S
37import qualified Data.Text as T
46import qualified Data.Text as T
38import Data.Char(isLetter, toLower)
47import Data.Char(isLetter, toLower)
39import Data.List.Split (splitOn)
48import Data.List.Split (splitOn)
@@ -56,32 +65,37 @@ checkAddDef add toplvl fc [] = return []
56checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
65checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
57 = do ctxt <- getContext
66 = do ctxt <- getContext
58 (t', _) <- recheckC fc [] t
67 (t', _) <- recheckC fc [] t
59− when add $ addDeferred [(n, (i, top, t, toplvl))]
68+ when add $ do addDeferred [(n, (i, top, t, toplvl))]
60 ns' <- checkAddDef add toplvl fc ns
70 ns' <- checkAddDef add toplvl fc ns
61 return ((n, (i, top, t')) : ns')
71 return ((n, (i, top, t')) : ns')
62-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
72-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
63-- return (n, (i, top, t'))) ns
73-- return (n, (i, top, t'))) ns
65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
75-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
66−elabType :: ElabInfo -> SyntaxInfo -> String ->
76+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
67 FC -> FnOpts -> Name -> PTerm -> Idris Type
77 FC -> FnOpts -> Name -> PTerm -> Idris Type
68elabType = elabType' False
78elabType = elabType' False
70elabType' :: Bool -> -- normalise it
80elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String ->
81+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
72 FC -> FnOpts -> Name -> PTerm -> Idris Type
82 FC -> FnOpts -> Name -> PTerm -> Idris Type
73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
83+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
74− n = liftname info n_in in -}
84+ n = liftname info n_in in -}
75 do checkUndefined fc n
85 do checkUndefined fc n
76 ctxt <- getContext
86 ctxt <- getContext
77 i <- getIState
87 i <- getIState
79− logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'
89+ logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'
80 ty' <- addUsingConstraints syn fc ty'
90 ty' <- addUsingConstraints syn fc ty'
81− ty' <- implicit syn n ty'
91+ ty' <- implicit info syn n ty'
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
83− let ty = addImpl i ty'
84− logLvl 1 $ show n ++ " type " ++ showTmImpls ty
85 ((tyT, defer, is), log) <-
99 ((tyT, defer, is), log) <-
86 tclift $ elaborate ctxt n (TType (UVal 0)) []
100 tclift $ elaborate ctxt n (TType (UVal 0)) []
87 (errAt "type of " n (erun fc (build i info False [] n ty)))
101 (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
89 -- if the type is not complete, note that we'll need to infer
103 -- if the type is not complete, note that we'll need to infer
90 -- things later (for solving metavariables)
104 -- things later (for solving metavariables)
91 when (not (null ds)) $ addTyInferred n
105 when (not (null ds)) $ addTyInferred n
92−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
106+
94 mapM_ (elabCaseBlock info opts) is
107 mapM_ (elabCaseBlock info opts) is
95 ctxt <- getContext
108 ctxt <- getContext
96 logLvl 5 $ "Rechecking"
109 logLvl 5 $ "Rechecking"
@@ -106,27 +119,32 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
106 -- Add normalised type to internals
119 -- Add normalised type to internals
107 rep <- useREPL
120 rep <- useREPL
108 when rep $ do
121 when rep $ do
109− addInternalApp (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?
110− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
123+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))
112 let (t, _) = unApply (getRetTy nty')
125 let (t, _) = unApply (getRetTy nty')
113 let corec = case t of
126 let corec = case t of
114 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
127 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
115− [TI _ True _ _] -> True
128+ [TI _ True _ _ _] -> True
116 _ -> False
129 _ -> False
117 _ -> False
130 _ -> False
131+ -- Productivity checking now via checking for guarded 'Delay'
118− let opts' = if corec then (Coinductive : opts) else opts
132+ let opts' = opts -- if corec then (Coinductive : opts) else opts
119 let usety = if norm then nty' else nty
133 let usety = if norm then nty' else nty
120 ds <- checkDef fc [(n, (-1, Nothing, usety))]
134 ds <- checkDef fc [(n, (-1, Nothing, usety))]
121 addIBC (IBCDef n)
135 addIBC (IBCDef n)
122 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
136 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
123 addDeferred ds'
137 addDeferred ds'
124 setFlags n opts'
138 setFlags n opts'
139+ checkDocs fc argDocs ty
125− addDocStr n doc
140+ addDocStr n doc argDocs
126 addIBC (IBCDoc n)
141 addIBC (IBCDoc n)
127 addIBC (IBCFlags n opts')
142 addIBC (IBCFlags n opts')
143+ fputState (opt_inaccessible . ist_optimisation n) inacc
128− when (Implicit `elem` opts) $ do addCoercion n
145+ when (Implicit `elem` opts') $ do addCoercion n
129− addIBC (IBCCoercion n)
146+ addIBC (IBCCoercion n)
130 -- If the function is declared as an error handler and the language
148 -- If the function is declared as an error handler and the language
131 -- extension is enabled, then add it to the list of error handlers.
149 -- extension is enabled, then add it to the list of error handlers.
132 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
150 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
141 addIBC (IBCErrorHandler n)
159 addIBC (IBCErrorHandler n)
142 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
160 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
143 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
161 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)
146 return usety
162 return usety
148 -- for making an internalapp, we only want the explicit ones, and don't
164 -- 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
167 , ns2 == map txt ["Maybe", "Prelude"]
183 , ns2 == map txt ["Maybe", "Prelude"]
168 , ns3 == map txt ["List", "Prelude"]
184 , ns3 == map txt ["List", "Prelude"]
169 , ns4 == map txt ["Errors","Reflection","Language"] = True
185 , ns4 == map txt ["Errors","Reflection","Language"] = True
170− tyIsHandler _ = False
186+ tyIsHandler _ = False
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}
196+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}
197+inaccessibleArgs _ _ = []
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)
206+ -- remove it from the deferred definitions list
173−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
209+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
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
180− fty <- case lookupTy n ctxt of
181− [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
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
193− $ tclift $ tfail (At fc (NonCollapsiblePostulate n))
194− -- remove it from the deferred definitions list
197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()
198−elabData info syn doc fc opts (PLaterdecl n t_in)
210+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
199 = do let codata = Codata `elem` opts
211 = do let codata = Codata `elem` opts
200 iLOG (show (fc, doc))
212 iLOG (show (fc, doc))
201 checkUndefined fc n
213 checkUndefined fc n
202 ctxt <- getContext
214 ctxt <- getContext
203 i <- getIState
215 i <- getIState
216+ -- TODO think: something more in info?
204− t_in <- implicit syn n t_in
217+ t_in <- implicit info syn n t_in
205 let t = addImpl i t_in
218 let t = addImpl i t_in
206 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
219 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
207 (erun fc (build i info False [] n t))
220 (erun fc (build i info False [] n t))
208 def' <- checkDef fc defer
221 def' <- checkDef fc defer
209 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
222 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
210 addDeferredTyCon def''
223 addDeferredTyCon def''
211 mapM_ (elabCaseBlock info []) is
225 mapM_ (elabCaseBlock info []) is
212 (cty, _) <- recheckC fc [] t'
226 (cty, _) <- recheckC fc [] t'
213 logLvl 2 $ "---> " ++ show cty
227 logLvl 2 $ "---> " ++ show cty
214 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
228 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
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)
217 = do let codata = Codata `elem` opts
231 = do let codata = Codata `elem` opts
218 iLOG (show fc)
232 iLOG (show fc)
219 undef <- isUndefined fc n
233 undef <- isUndefined fc n
220 ctxt <- getContext
234 ctxt <- getContext
221 i <- getIState
235 i <- getIState
222− t_in <- implicit syn n t_in
236+ t_in <- implicit info syn n t_in
223 let t = addImpl i t_in
237 let t = addImpl i t_in
224 ((t', defer, is), log) <-
238 ((t', defer, is), log) <-
225 tclift $ elaborate ctxt n (TType (UVal 0)) []
239 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -235,33 +249,54 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
235 logLvl 2 $ "---> " ++ show cty
249 logLvl 2 $ "---> " ++ show cty
236 -- temporary, to check cons
250 -- temporary, to check cons
237 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
251 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
252+ let cnameinfo = cinfo info (map cname dcons)
238− cons <- mapM (elabCon info syn n codata) dcons
253+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
239 ttag <- getName
254 ttag <- getName
240 i <- getIState
255 i <- getIState
241 let as = map (const Nothing) (getArgTys cty)
256 let as = map (const Nothing) (getArgTys cty)
242 let params = findParams (map snd cons)
257 let params = findParams (map snd cons)
243 logLvl 2 $ "Parameters : " ++ show params
258 logLvl 2 $ "Parameters : " ++ show params
259+ -- TI contains information about mutually declared types - this will
260+ -- be updated when the mutual block is complete
244− putIState (i { idris_datatypes =
261+ putIState (i { idris_datatypes =
245− addDef n (TI (map fst cons) codata opts params)
262+ addDef n (TI (map fst cons) codata opts params [n])
246 (idris_datatypes i) })
263 (idris_datatypes i) })
247 addIBC (IBCDef n)
264 addIBC (IBCDef n)
248 addIBC (IBCData n)
265 addIBC (IBCData n)
266+ checkDocs fc argDocs t_in
249− addDocStr n doc
267+ addDocStr n doc argDocs
250 addIBC (IBCDoc n)
268 addIBC (IBCDoc n)
251 let metainf = DataMI params
269 let metainf = DataMI params
252 addIBC (IBCMetaInformation n metainf)
270 addIBC (IBCMetaInformation n metainf)
253 -- TMP HACK! Make this a data option
271 -- TMP HACK! Make this a data option
254− when (n /= sUN "Lazy") $ collapseCons n cons
255 updateContext (addDatatype (Data n ttag cty cons))
272 updateContext (addDatatype (Data n ttag cty cons))
256 updateContext (setMetaInformation n metainf)
273 updateContext (setMetaInformation n metainf)
274+ mapM_ totcheck (zip (repeat fc) (map fst cons))
257− mapM_ (checkPositive n) cons
275+-- mapM_ (checkPositive n) cons
277+ -- if there's exactly one constructor,
278+ -- mark both the type and the constructor as detaggable
280+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n
281+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
284+ -- create an eliminator
285+ when (DefaultEliminator `elem` opts) $
258− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
286+ evalStateT (elabEliminator params n t dcons info) Map.empty
288+ setDetaggable :: Name -> Idris ()
289+ setDetaggable n = do
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 }
261 checkDefinedAs fc n t ctxt
296 checkDefinedAs fc n t ctxt
262 = case lookupDef n ctxt of
297 = case lookupDef n ctxt of
263 [] -> return ()
298 [] -> return ()
264− [TyDecl _ ty] ->
299+ [TyDecl _ ty] ->
265 case converts ctxt [] t ty of
300 case converts ctxt [] t ty of
266 OK () -> return ()
301 OK () -> return ()
267 _ -> tclift $ tfail (At fc (AlreadyDefined n))
302 _ -> tclift $ tfail (At fc (AlreadyDefined n))
@@ -316,38 +351,56 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
316 | otherwise = count n ts
351 | otherwise = count n ts
317 mParam args (_ : rest) = Nothing : mParam args rest
352 mParam args (_ : rest) = Nothing : mParam args rest
354+ cname (_, _, n, _, _, _) = n
356+ -- Abuse of ElabInfo.
357+ -- TODO Contemplate whether the ElabInfo type needs modification.
358+ cinfo :: ElabInfo -> [Name] -> ElabInfo
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,
366+ liftname = id -- Is this appropriate?
319type EliminatorState = StateT (Map.Map String Int) Idris
369type EliminatorState = StateT (Map.Map String Int) Idris
321−-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
371+-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
322−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->
372+elabEliminator :: [Int] -> Name -> PTerm ->
373+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
323 ElabInfo -> EliminatorState ()
374 ElabInfo -> EliminatorState ()
324elabEliminator paramPos n ty cons info = do
375elabEliminator paramPos n ty cons info = do
325 elimLog $ "Elaborating eliminator"
376 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))
326 let (cnstrs, _) = splitPi ty
378 let (cnstrs, _) = splitPi ty
327 let (splittedTy@(pms, idxs)) = splitPms cnstrs
379 let (splittedTy@(pms, idxs)) = splitPms cnstrs
328 generalParams <- namePis False pms
380 generalParams <- namePis False pms
329 motiveIdxs <- namePis False idxs
381 motiveIdxs <- namePis False idxs
330 let motive = mkMotive n paramPos generalParams motiveIdxs
382 let motive = mkMotive n paramPos generalParams motiveIdxs
331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
383+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do
332− name <- freshName $ "elim_" ++ simpleName cnm
384+ name <- freshName $ "elim_" ++ simpleName cnm
333− consTerm <- extractConsTerm c generalParams
385+ consTerm <- extractConsTerm c generalParams
334− return (name, expl, consTerm)) cons
386+ return (name, expl, consTerm)) cons
335 scrutineeIdxs <- namePis False idxs
387 scrutineeIdxs <- namePis False idxs
336 let motiveConstr = [(motiveName, expl, motive)]
388 let motiveConstr = [(motiveName, expl, motive)]
337 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
389 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
338 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
390 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
340 let clauseConsElimArgs = map getPiName consTerms
392 let clauseConsElimArgs = map getPiName consTerms
341 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
393 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
342 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
394 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
343 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
395 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
344 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
397 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
345 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
398 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
346− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
399+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
347 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
400 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
348 -- Do not elaborate clauses if there aren't any
401 -- Do not elaborate clauses if there aren't any
349 case eliminatorClauses of
402 case eliminatorClauses of
350− [] -> return ()
403+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
351 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
404 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
352 where elimLog :: String -> EliminatorState ()
405 where elimLog :: String -> EliminatorState ()
353 elimLog s = State.lift (logLvl 2 s)
406 elimLog s = State.lift (logLvl 2 s)
@@ -410,9 +463,9 @@ elabEliminator paramPos n ty cons info = do
410 freshName key = do
463 freshName key = do
411 nameMap <- get
464 nameMap <- get
412 let i = fromMaybe 0 (Map.lookup key nameMap)
465 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)
414 put $ Map.insert key (i+1) nameMap
467 put $ Map.insert key (i+1) nameMap
415− return (sUN name)
468+ return name
417 scrutineeName :: Name
470 scrutineeName :: Name
418 scrutineeName = sUN "scrutinee"
471 scrutineeName = sUN "scrutinee"
@@ -485,7 +538,7 @@ elabEliminator paramPos n ty cons info = do
485 splitArgPms _ = ([],[])
538 splitArgPms _ = ([],[])
488− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
541+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
489 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
542 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
490 i <- State.lift getIState
543 i <- State.lift getIState
491 implargs' <- case lookupCtxt cnm (idris_implicits i) of
544 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -500,12 +553,12 @@ elabEliminator paramPos n ty cons info = do
500 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
553 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
501 _ -> return implargs
554 _ -> return implargs
503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
556+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
557+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
505 let cons' = replaceParams paramPos generalParameters ty
558 let cons' = replaceParams paramPos generalParameters ty
506 let (args, resTy) = splitPi cons'
559 let (args, resTy) = splitPi cons'
507 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
560 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
508− consArgs <- namePis True args
561+ consArgs <- namePis False args
509 let recArgs = findRecArgs consArgs
562 let recArgs = findRecArgs consArgs
510 let recMotives = map applyRecMotive recArgs
563 let recMotives = map applyRecMotive recArgs
511 let (_, consIdxs) = splitArgPms resTy
564 let (_, consIdxs) = splitArgPms resTy
@@ -536,15 +589,15 @@ elabEliminator paramPos n ty cons info = do
536 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
589 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
537 convertImplPi _ = Nothing
590 convertImplPi _ = Nothing
539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
592+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
593+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
541 let cons' = replaceParams paramPos generalParameters ty
594 let cons' = replaceParams paramPos generalParameters ty
542 let (args, resTy) = splitPi cons'
595 let (args, resTy) = splitPi cons'
543 i <- State.lift getIState
596 i <- State.lift getIState
544 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
597 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
545 let (_, generalIdxs') = splitArgPms resTy
598 let (_, generalIdxs') = splitArgPms resTy
546 let generalIdxs = map pexp generalIdxs'
599 let generalIdxs = map pexp generalIdxs'
547− consArgs <- namePis True args
600+ consArgs <- namePis False args
548 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
601 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
549 let recArgs = findRecArgs consArgs
602 let recArgs = findRecArgs consArgs
550 let recElims = map applyRecElim recArgs
603 let recElims = map applyRecElim recArgs
@@ -558,10 +611,12 @@ elabEliminator paramPos n ty cons info = do
559elabPrims :: Idris ()
612elabPrims :: Idris ()
560elabPrims = do mapM_ (elabDecl EAll toplevel)
613elabPrims = do mapM_ (elabDecl EAll toplevel)
561− (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)
614+ (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
563 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
616 [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]))
565 addNameHint eqTy (sUN "prf")
620 addNameHint eqTy (sUN "prf")
566 elabDecl EAll toplevel elimDecl
621 elabDecl EAll toplevel elimDecl
567 mapM_ elabPrim primitives
622 mapM_ elabPrim primitives
@@ -626,8 +681,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
628-- | Elaborate a type provider
683-- | Elaborate a type provider
629−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()
684+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()
630−elabProvider info syn fc what n ty tm
685+elabProvider info syn fc what n
631 = do i <- getIState
686 = do i <- getIState
632 -- Ensure that the experimental extension is enabled
687 -- Ensure that the experimental extension is enabled
633 unless (TypeProviders `elem` idris_language_extensions i) $
688 unless (TypeProviders `elem` idris_language_extensions i) $
@@ -637,12 +692,17 @@ elabProvider info syn fc what n ty tm
637 ctxt <- getContext
692 ctxt <- getContext
639 -- First elaborate the expected type (and check that it's a type)
694 -- First elaborate the expected type (and check that it's a type)
695+ -- The goal type for a postulate is always Type.
696+ (ty', typ) <- case what of
640− (ty', typ) <- elabVal toplevel False ty
697+ ProvTerm ty p -> elabVal toplevel False ty
698+ ProvPostulate _ -> elabVal toplevel False PType
641 unless (isTType typ) $
699 unless (isTType typ) $
642 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
700 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
644 -- Elaborate the provider term to TT and check that the type matches
702 -- Elaborate the provider term to TT and check that the type matches
703+ (e, et) <- case what of
704+ ProvTerm _ tm -> elabVal toplevel False tm
645− (e, et) <- elabVal toplevel False tm
705+ ProvPostulate tm -> elabVal toplevel False tm
646 unless (isProviderOf (normalise ctxt [] ty') et) $
706 unless (isProviderOf (normalise ctxt [] ty') et) $
647 ifail $ "Expected provider type IO (Provider (" ++
707 ifail $ "Expected provider type IO (Provider (" ++
648 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
708 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
@@ -653,25 +713,22 @@ elabProvider info syn fc what n ty tm
653 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
713 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
654 [Erased, e])
714 [Erased, e])
655 let rhs' = normalise ctxt [] rhs
715 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
658 -- Extract the provided term or postulate from the type provider
718 -- Extract the provided term or postulate from the type provider
659 provided <- getProvided fc rhs'
719 provided <- getProvided fc rhs'
661 case provided of
721 case provided of
662 Provide tm
722 Provide tm
663− | what `elem` [ProvTerm, ProvAny] ->
723+ | ProvTerm ty _ <- what ->
664 do -- Finally add a top-level definition of the provided term
724 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
666 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
726 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
727+ logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
668− | otherwise ->
728+ | ProvPostulate _ <- what ->
669− ierror . Msg $ "Attempted to provide a term where a postulate was expected."
671− | what `elem` [ProvPostulate, ProvAny] ->
672 do -- Add the postulate
729 do -- Add the postulate
673− elabPostulate info syn "Provided postulate" fc [] n ty
730+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
674− logLvl 1 $ "Elaborated provided postulate " ++ show n
731+ logLvl 3 $ "Elaborated provided postulate " ++ show n
675 | otherwise ->
732 | otherwise ->
676 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
733 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -687,7 +744,6 @@ elabProvider info syn fc what n ty tm
687 , prov == txt "Provider" && provs == txt "Providers" = True
744 , prov == txt "Provider" && provs == txt "Providers" = True
688 isProviderOf _ _ = False
745 isProviderOf _ _ = False
690−-- | Elaborate a type provider
691elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
747elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
692elabTransform info fc safe lhs_in rhs_in
748elabTransform info fc safe lhs_in rhs_in
693 = do ctxt <- getContext
749 = do ctxt <- getContext
@@ -721,12 +777,18 @@ elabTransform info fc safe lhs_in rhs_in
721 addIBC (IBCTrans (clhs_tm, crhs_tm))
777 addIBC (IBCTrans (clhs_tm, crhs_tm))
724−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
780+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
725− PTerm -> String -> Name -> PTerm -> Idris ()
781+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
726−elabRecord info syn doc fc tyn ty cdoc cn cty
782+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
727− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])
783+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
784+ -- TODO think: something more in info?
728− cty' <- implicit syn cn cty
785+ cty' <- implicit info syn cn cty_in
729 i <- getIState
786 i <- getIState
788+ -- get bound implicits and propagate to setters (in case they
789+ -- provide useful information for inference)
790+ let extraImpls = getBoundImpls cty'
730 cty <- case lookupTy cn (tt_ctxt i) of
792 cty <- case lookupTy cn (tt_ctxt i) of
731 [t] -> return (delab i t)
793 [t] -> return (delab i t)
732 _ -> ifail "Something went inexplicably wrong"
794 _ -> ifail "Something went inexplicably wrong"
@@ -735,14 +797,29 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
735 let ptys = getProjs [] (renameBs cimp cty)
797 let ptys = getProjs [] (renameBs cimp cty)
736 let ptys_u = getProjs [] cty
798 let ptys_u = getProjs [] cty
737 let recty = getRecTy cty
799 let recty = getRecTy cty
801+ -- rename indices when we generate the getter/setter types, so
802+ -- that they don't clash with the names of the projections
804+ let index_names_in = getRecNameMap "_in" recty
805+ let recty_in = substMatches index_names_in recty
738− logLvl 6 $ show (recty, ptys)
807+ logLvl 1 $ show (recty, ptys)
739 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
808 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
740 [pexp (PRef fc rec)])) ptys
809 [pexp (PRef fc rec)])) ptys
811+ -- Generate projection functions
741− proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
812+ proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
813+ logLvl 3 $ show proj_decls
742 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
814 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
743 let implBinds = getImplB id cty'
815 let implBinds = getImplB id cty'
817+ -- Generate update functions
818+ update_decls <- mapM (mkUpdate recty index_names_in extraImpls
819+ (getFieldNames cty')
744− update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
820+ implBinds (length nonImp)) (zip nonImp [0..])
745 mapM_ (elabDecl EAll info) (concat proj_decls)
821 mapM_ (elabDecl EAll info) (concat proj_decls)
822+ logLvl 3 $ show update_decls
746 mapM_ (tryElabDecl info) (update_decls)
823 mapM_ (tryElabDecl info) (update_decls)
748-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
825-- 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
757 (\v -> do iputStrLn $ show fc ++
834 (\v -> do iputStrLn $ show fc ++
758 ":Warning - can't generate setter for " ++
835 ":Warning - can't generate setter for " ++
759 show fn ++ " (" ++ show ty ++ ")"
836 show fn ++ " (" ++ show ty ++ ")"
837+-- ++ "\n" ++ pshow i v
760 putIState i)
838 putIState i)
840+ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
841+ getBoundImpls _ = []
762− getImplB k (PPi (Imp l s _ _) n Placeholder sc)
843+ getImplB k (PPi (Imp l s _) n Placeholder sc)
763 = getImplB k sc
844 = getImplB k sc
764− getImplB k (PPi (Imp l s d p) n ty sc)
845+ getImplB k (PPi (Imp l s p) n ty sc)
765− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc
846+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc
766 getImplB k (PPi _ n ty sc)
847 getImplB k (PPi _ n ty sc)
767 = getImplB k sc
848 = getImplB k sc
768 getImplB k _ = k
849 getImplB k _ = k
770− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)
851+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
771 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
852 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
772 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
853 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
773 renameBs _ t = t
854 renameBs _ t = t
@@ -775,9 +856,19 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
775 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
856 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
776 getProjs acc r = reverse acc
857 getProjs acc r = reverse acc
859+ getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
860+ getFieldNames (PPi _ _ _ s) = getFieldNames s
861+ getFieldNames _ = []
778 getRecTy (PPi _ n ty s) = getRecTy s
863 getRecTy (PPi _ n ty s) = getRecTy s
779 getRecTy t = t
864 getRecTy t = t
866+ getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args
868+ toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))
870+ getRecNameMap x _ = []
781 rec = sMN 0 "rec"
872 rec = sMN 0 "rec"
783 mkp (UN n) = sMN 0 ("p_" ++ str n)
874 mkp (UN n) = sMN 0 ("p_" ++ str n)
@@ -794,7 +885,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
795 mkProj recty substs cimp ((pn_in, pty), pos)
886 mkProj recty substs cimp ((pn_in, pty), pos)
796 = do let pn = expandNS syn pn_in
887 = do let pn = expandNS syn pn_in
797− let pfnTy = PTy "" defaultSyntax fc [] pn
888+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
798 (PPi expl rec recty
889 (PPi expl rec recty
799 (substMatches substs pty))
890 (substMatches substs pty))
800 let pls = repeat Placeholder
891 let pls = repeat Placeholder
@@ -810,13 +901,23 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
811 implicitise (pa, t) = pa { getTm = t }
902 implicitise (pa, t) = pa { getTm = t }
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
813− mkUpdate recty k num ((pn, pty), pos)
907+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)
814 = do let setname = expandNS syn $ mkType pn
908 = do let setname = expandNS syn $ mkType pn
815 let valname = sMN 0 "updateval"
909 let valname = sMN 0 "updateval"
816− let pt = k (PPi expl pn pty
910+ let pn_out = sMN 0 (show pn ++ "_out")
817− (PPi expl rec recty recty))
911+ let pn_in = sMN 0 (show pn ++ "_in")
818− let pfnTy = PTy "" defaultSyntax fc [] setname pt
912+ let recty_in = substMatches [(pn, PRef fc pn_in)] recty
819− let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
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
820 let lhsArgs = pls
921 let lhsArgs = pls
821 let rhsArgs = take pos pls ++ (PRef fc valname) :
922 let rhsArgs = take pos pls ++ (PRef fc valname) :
822 drop (pos + 1) pls
923 drop (pos + 1) pls
@@ -830,15 +931,31 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
830 (map pexp rhsArgs)) []
931 (map pexp rhsArgs)) []
831 return (pn, pfnTy, PClauses fc [] setname [pclause])
932 return (pn, pfnTy, PClauses fc [] setname [pclause])
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
939+ if n `elem` allNamesIn t
940+ then PPi impl n' ty (implBindUp ns is t)
941+ else implBindUp ns is t
943+-- FIXME: 'forcenames' is an almighty hack! Need a better way of
944+-- erasing non-forceable things
946+-- TODO: the above is a comment from the past;
947+-- forcenames is probably no longer needed
833elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
948elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
834− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
949+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
835−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
950+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
836 = do checkUndefined fc n
951 = do checkUndefined fc n
837 ctxt <- getContext
952 ctxt <- getContext
838 i <- getIState
953 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)
840 let t = addImpl i t_in
955 let t = addImpl i t_in
841 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
956 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
957+ let inacc = inaccessibleArgs 0 t
958+ logLvl 5 $ "Inaccessible args: " ++ show inacc
842 ((t', defer, is), log) <-
959 ((t', defer, is), log) <-
843 tclift $ elaborate ctxt n (TType (UVal 0)) []
960 tclift $ elaborate ctxt n (TType (UVal 0)) []
844 (errAt "constructor " n (erun fc (build i info False [] n t)))
961 (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)
853 tyIs cty'
970 tyIs cty'
854 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
971 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
855 addIBC (IBCDef n)
972 addIBC (IBCDef n)
856− addDocStr n doc
973+ checkDocs fc argDocs t_in
974+ addDocStr n doc argDocs
857 addIBC (IBCDoc n)
975 addIBC (IBCDoc n)
858− let fs = map (getNamePos 0 t) forcenames
976+ fputState (opt_inaccessible . ist_optimisation n) inacc
859− -- FIXME: 'forcenames' is an almighty hack! Need a better way of
977+ addIBC (IBCOpt n)
860− -- erasing non-forceable things
861− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
862 return (n, cty')
978 return (n, cty')
864 tyIs (Bind n b sc) = tyIs sc
980 tyIs (Bind n b sc) = tyIs sc
@@ -869,12 +985,15 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
870 mkLazy (PPi pl n ty sc)
986 mkLazy (PPi pl n ty sc)
871 = let ty' = if getTyName ty
987 = 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")),
873 else ty in
991 else ty in
874 PPi pl n ty' (mkLazy sc)
992 PPi pl n ty' (mkLazy sc)
875 mkLazy t = t
993 mkLazy t = t
877 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
995 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
996+ getTyName (PRef _ n) = n == nsroot tn
878 getTyName _ = False
997 getTyName _ = False
@@ -888,6 +1007,9 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
888elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
1007elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
889elabClauses info fc opts n_in cs = let n = liftname info n_in in
1008elabClauses info fc opts n_in cs = let n = liftname info n_in in
890 do ctxt <- getContext
1009 do ctxt <- getContext
1011+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
891 -- Check n actually exists, with no definition yet
1013 -- Check n actually exists, with no definition yet
892 let tys = lookupTy n ctxt
1014 let tys = lookupTy n ctxt
893 let reflect = Reflection `elem` opts
1015 let reflect = Reflection `elem` opts
@@ -899,33 +1021,18 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
899 tclift $ tfail $ At fc (NoTypeDecl n)
1021 tclift $ tfail $ At fc (NoTypeDecl n)
900 [ty] -> return ty
1022 [ty] -> return ty
901 let atys = map snd (getArgTys fty)
1023 let atys = map snd (getArgTys fty)
902− pats_in <- mapM (elabClause info opts)
1024+ cs_elab <- mapM (elabClause info opts)
903 (zip [0..] cs)
1025 (zip [0..] cs)
1026+ let (pats_in, cs_full) = unzip cs_elab
904 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
1028 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
906− -- if the return type of 'ty' is collapsible, the optimised version should
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
918 solveDeferred n
1030 solveDeferred n
919− ist <- getIState
1031+
920− when doNothing $
1032+ -- just ensure that the structure exists
921− case lookupCtxt n (idris_optimisation ist) of
1033+ fmodifyState (ist_optimisation n) id
922− [oi] -> do let opts = addDef n (oi { collapsible = True })
1034+ addIBC (IBCOpt n)
923− (idris_optimisation ist)
1035+
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 })
929 ist <- getIState
1036 ist <- getIState
930 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
1037 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
@@ -935,11 +1042,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
935 let tcase = opt_typecase (idris_options ist)
1042 let tcase = opt_typecase (idris_options ist)
937 -- Summary of what's about to happen: Definitions go:
1044 -- Summary of what's about to happen: Definitions go:
939− -- pats_in -> pats -> optpats
1046+ -- pats_in -> pats -> pdef -> pdef'
940− -- pdef comes from pats,
941− -- optpdef comes from optpats
942− -- Then pdef' is optpdef with forcing/collapsing applied everywhere
944 -- addCaseDef builds case trees from <pdef> and <pdef'>
1048 -- addCaseDef builds case trees from <pdef> and <pdef'>
@@ -968,24 +1072,16 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
969 numArgs <- tclift $ sameLength pdef
1073 numArgs <- tclift $ sameLength pdef
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
978 case specNames opts of
1075 case specNames opts of
979 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
1076 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
980 _ -> return ()
1077 _ -> return ()
982− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
983 tree@(CaseDef scargs sc _) <- tclift $
1079 tree@(CaseDef scargs sc _) <- tclift $
984− simpleCase tcase False reflect CompileTime fc atys pdef
1080+ simpleCase tcase False reflect CompileTime fc inacc atys pdef
985 cov <- coverage
1081 cov <- coverage
986 pmissing <-
1082 pmissing <-
987− if cov
1083+ if cov && not (hasDefault cs)
988− then do missing <- genClauses fc n (map getLHS pdef) cs
1084+ then do missing <- genClauses fc n (map getLHS pdef) cs_full
989 -- missing <- genMissing n scargs sc
1085 -- missing <- genMissing n scargs sc
990 missing' <- filterM (checkPossible info fc True n) missing
1086 missing' <- filterM (checkPossible info fc True n) missing
991 let clhs = map getLHS pdef
1087 let clhs = map getLHS pdef
@@ -1003,7 +1099,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1003 let pcover = null pmissing
1099 let pcover = null pmissing
1005 -- pdef' is the version that gets compiled for run-time
1101 -- pdef' is the version that gets compiled for run-time
1006− pdef_in' <- applyOpts optpdef
1102+ pdef_in' <- applyOpts pdef
1007 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1103 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1009 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
1105 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
1013 let tot = if pcover || AssertTotal `elem` opts
1109 let tot = if pcover || AssertTotal `elem` opts
1014 then Unchecked -- finish checking later
1110 then Unchecked -- finish checking later
1015 else Partial NotCovering -- already know it's not total
1111 else Partial NotCovering -- already know it's not total
1016 -- case lookupCtxt (namespace info) n (idris_flags ist) of
1113 -- case lookupCtxt (namespace info) n (idris_flags ist) of
1017 -- [fs] -> if TotalFn `elem` fs
1114 -- [fs] -> if TotalFn `elem` fs
1018 -- then case tot of
1115 -- then case tot of
@@ -1029,11 +1126,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1029 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
1126 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
1031 tree' <- tclift $ simpleCase tcase knowncovering reflect
1128 tree' <- tclift $ simpleCase tcase knowncovering reflect
1032− RunTime fc atys pdef'
1129+ RunTime fc inacc atys pdef'
1033− logLvl 3 (show tree)
1130+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
1034 logLvl 3 $ "Optimised: " ++ show tree'
1131 logLvl 3 $ "Optimised: " ++ show tree'
1035 ctxt <- getContext
1132 ctxt <- getContext
1036 ist <- getIState
1133 ist <- getIState
1134+ let opt = idris_optimisation ist
1037 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
1135 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
1038 (idris_patdefs ist) })
1136 (idris_patdefs ist) })
1039 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
1137 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
1044 (AssertTotal `elem` opts)
1142 (AssertTotal `elem` opts)
1047 pdef pdef pdef_inl pdef' ty)
1146 pdef pdef pdef_inl pdef' ty)
1048 addIBC (IBCDef n)
1147 addIBC (IBCDef n)
@@ -1059,7 +1158,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1059 let used = findUsedArgs sc' scargs'
1158 let used = findUsedArgs sc' scargs'
1060 -- let scg = buildSCG i sc scargs
1159 -- let scg = buildSCG i sc scargs
1061 -- add SCG later, when checking totality
1160 -- 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
1063 logLvl 2 $ "Called names: " ++ show cg
1162 logLvl 2 $ "Called names: " ++ show cg
1064 addToCG n cg
1163 addToCG n cg
1065 addToCalledG n (nub (map fst calls)) -- plus names in type!
1164 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
1068 return ()
1167 return ()
1069 -- addIBC (IBCTotal n tot)
1168 -- addIBC (IBCTotal n tot)
1070 [] -> return ()
1169 [] -> 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
1073 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
1175 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
1074 Right _ -> False
1176 Right _ -> False
@@ -1088,13 +1190,18 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1088 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1190 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1089 depat acc x = (acc, x)
1191 depat acc x = (acc, x)
1193+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1194+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1195+ hasDefault _ = False
1091 getLHS (_, l, _) = l
1197 getLHS (_, l, _) = l
1093 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
1199 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
1094 force (normalisePats ctxt [] y))
1200 force (normalisePats ctxt [] y))
1095 simple_lhs ctxt t = t
1201 simple_lhs ctxt t = t
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)))
1099 -- this is so pattern types are in the right form for erasure
1206 -- this is so pattern types are in the right form for erasure
1100 normalisePats ctxt env (Bind n (PVar t) sc)
1207 normalisePats ctxt env (Bind n (PVar t) sc)
@@ -1158,10 +1265,10 @@ elabPE info fc caller r =
1158 (map (\ (lhs, rhs) ->
1265 (map (\ (lhs, rhs) ->
1159 (showTmImpls lhs ++ " = " ++
1266 (showTmImpls lhs ++ " = " ++
1160 showTmImpls rhs)) pats)
1267 showTmImpls rhs)) pats)
1161− elabType info defaultSyntax "" fc opts newnm specTy
1268+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
1162 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1269 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1163 elabClauses info fc opts newnm def
1270 elabClauses info fc opts newnm def
1164− logLvl 1 $ "Specialised " ++ show newnm)
1271+ logLvl 2 $ "Specialised " ++ show newnm)
1165 -- if it doesn't work, just don't specialise. Could happen for lots
1272 -- if it doesn't work, just don't specialise. Could happen for lots
1166 -- of valid reasons (e.g. local variables in scope which can't be
1273 -- of valid reasons (e.g. local variables in scope which can't be
1167 -- lifted out).
1274 -- lifted out).
@@ -1206,8 +1313,8 @@ elabPE info fc caller r =
1207-- Elaborate a value, returning any new bindings created (this will only
1314-- Elaborate a value, returning any new bindings created (this will only
1208-- happen if elaborating as a pattern clause)
1315-- happen if elaborating as a pattern clause)
1209−elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
1316+elabValBind :: ElabInfo -> Bool -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
1210−elabValBind info aspat tm_in
1317+elabValBind info aspat norm tm_in
1211 = do ctxt <- getContext
1318 = do ctxt <- getContext
1212 i <- getIState
1319 i <- getIState
1213 let tm = addImpl i tm_in
1320 let tm = addImpl i tm_in
@@ -1232,14 +1339,17 @@ elabValBind info aspat tm_in
1232 logLvl 3 ("Value: " ++ show vtm)
1339 logLvl 3 ("Value: " ++ show vtm)
1233-- recheckC (fileFC "(input)") [] tm'
1340-- recheckC (fileFC "(input)") [] tm'
1234-- logLvl 2 (show vtm)
1341-- logLvl 2 (show vtm)
1235− (vtm, vty) <- recheckC (fileFC "(input)") [] vtm
1342+ (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
1344+ let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
1236 let bargs = getPBtys vtm
1346 let bargs = getPBtys vtm
1238 return (vtm, vty, bargs)
1348 return (vtm, vty, bargs)
1240elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
1350elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
1241elabVal info aspat tm_in
1351elabVal info aspat tm_in
1242− = do (tm, ty, _) <- elabValBind info aspat tm_in
1352+ = do (tm, ty, _) <- elabValBind info aspat False tm_in
1243 return (tm, ty)
1353 return (tm, ty)
1245-- checks if the clause is a possible left hand side. Returns the term if
1355-- 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
1249checkPossible info fc tcgen fname lhs_in
1359checkPossible info fc tcgen fname lhs_in
1250 = do ctxt <- getContext
1360 = do ctxt <- getContext
1251 i <- getIState
1361 i <- getIState
1252− let lhs = addImpl i lhs_in
1362+ let lhs = addImplPat i lhs_in
1253 -- if the LHS type checks, it is possible
1363 -- if the LHS type checks, it is possible
1254 case elaborate ctxt (sMN 0 "patLHS") infP []
1364 case elaborate ctxt (sMN 0 "patLHS") infP []
1255 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
1365 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
@@ -1258,24 +1368,53 @@ checkPossible info fc tcgen fname lhs_in
1258 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1368 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1259 OK _ -> return True
1369 OK _ -> return True
1260 err -> return False
1370 err -> return False
1261−
1371+ -- if it's a recoverable error, the case may become possible
1262−-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1372+ Error err -> if tcgen then return (recoverable ctxt err)
1263−-- return (not b) -- then return (Just lhs_tm) else return Nothing
1373+ else return (validCase ctxt err ||
1264−-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
1374+ recoverable ctxt err)
1265− Error err -> if tcgen then return False
1375+ where validCase ctxt (CantUnify _ topx topy e _ _)
1266− else return (impossibleError err)
1376+ = let topx' = normalise ctxt [] topx
1267− where impossibleError (CantUnify _ topx topy e _ _)
1377+ topy' = normalise ctxt [] topy in
1268− = not (sameFam topx topy || not (impossibleError e))
1378+ not (sameFam topx' topy' || not (validCase ctxt e))
1269− impossibleError (CantConvert _ _ _) = False
1379+ validCase ctxt (CantConvert _ _ _) = False
1270− impossibleError (At _ e) = impossibleError e
1380+ validCase ctxt (At _ e) = validCase ctxt e
1271− impossibleError (Elaborating _ _ e) = impossibleError e
1381+ validCase ctxt (Elaborating _ _ e) = validCase ctxt e
1272− impossibleError _ = True
1382+ validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
1383+ validCase ctxt _ = True
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
1274 sameFam topx topy
1394 sameFam topx topy
1275 = case (unApply topx, unApply topy) of
1395 = case (unApply topx, unApply topy) of
1276 ((P _ x _, _), (P _ y _, _)) -> x == y
1396 ((P _ x _, _), (P _ y _, _)) -> x == y
1277 _ -> False
1397 _ -> False
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
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')
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
1414+ ntRec x y | Ref <- x = True
1416+ | otherwise = False -- name is different, unrecoverable
1279getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1418getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1280 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1419 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1281getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1420getFixedInType i env (_ : is) (Bind n (Pi t) sc)
@@ -1338,16 +1477,19 @@ propagateParams ps t (PRef fc n)
1338 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1477 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1339propagateParams ps t x = x
1478propagateParams ps t x = x
1480+-- Return the elaborated LHS/RHS, and the original LHS with implicits added
1341elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1481elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1342− Idris (Either Term (Term, Term))
1482+ Idris (Either Term (Term, Term), PTerm)
1343elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1483elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1344 = do let tcgen = Dictionary `elem` opts
1484 = do let tcgen = Dictionary `elem` opts
1486+ let lhs = addImpl i lhs_in
1345 b <- checkPossible info fc tcgen fname lhs_in
1487 b <- checkPossible info fc tcgen fname lhs_in
1346 case b of
1488 case b of
1347 True -> tclift $ tfail (At fc
1489 True -> tclift $ tfail (At fc
1348 (Msg $ show lhs_in ++ " is a valid case"))
1490 (Msg $ show lhs_in ++ " is a valid case"))
1349 False -> do ptm <- mkPatTm lhs_in
1491 False -> do ptm <- mkPatTm lhs_in
1350− return (Left ptm)
1492+ return (Left ptm, lhs)
1351elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1493elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1352 = do let tcgen = Dictionary `elem` opts
1494 = do let tcgen = Dictionary `elem` opts
1353 ctxt <- getContext
1495 ctxt <- getContext
@@ -1378,7 +1520,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1378 inj <- get_inj
1520 inj <- get_inj
1379 return (res, probs, inj))
1521 return (res, probs, inj))
1381− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1523+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1383 let lhs_tm = orderPats (getInferTerm lhs')
1525 let lhs_tm = orderPats (getInferTerm lhs')
1384 let lhs_ty = getInferType lhs'
1526 let lhs_ty = getInferType lhs'
@@ -1397,17 +1539,17 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1398 rep <- useREPL
1540 rep <- useREPL
1399 when rep $ do
1541 when rep $ do
1400− addInternalApp (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?
1401− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))
1543+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
1403 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1545 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1404 -- Elaborate where block
1546 -- Elaborate where block
1405 ist <- getIState
1547 ist <- getIState
1406 windex <- getName
1548 windex <- getName
1407− let winfo = pinfo (pvars ist lhs_tm) whereblock windex
1408 let decls = nub (concatMap declared whereblock)
1549 let decls = nub (concatMap declared whereblock)
1409 let defs = nub (decls ++ concatMap defined whereblock)
1550 let defs = nub (decls ++ concatMap defined whereblock)
1410 let newargs = pvars ist lhs_tm
1551 let newargs = pvars ist lhs_tm
1552+ let winfo = pinfo info newargs defs windex
1411 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1553 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1413 -- Split the where block into declarations with a type, and those
1555 -- 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)
1415 -- Elaborate those with a type *before* RHS, those without *after*
1557 -- Elaborate those with a type *before* RHS, those without *after*
1416 let (wbefore, wafter) = sepBlocks wb
1558 let (wbefore, wafter) = sepBlocks wb
1418− logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1560+ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1419− mapM_ (elabDecl' EAll info) wbefore
1561+ mapM_ (elabDecl' EAll winfo) wbefore
1420 -- Now build the RHS, using the type of the LHS as the goal.
1562 -- Now build the RHS, using the type of the LHS as the goal.
1421 i <- getIState -- new implicits from where block
1563 i <- getIState -- new implicits from where block
1422 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1564 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)
1431 mapM_ setinj (nub (params ++ inj))
1573 mapM_ setinj (nub (params ++ inj))
1432 setNextName
1574 setNextName
1433 (_, _, is) <- errAt "right hand side of " fname
1575 (_, _, 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))
1435 errAt "right hand side of " fname
1577 errAt "right hand side of " fname
1436 (erun fc $ psolve lhs_tm)
1578 (erun fc $ psolve lhs_tm)
1437 hs <- get_holes
1579 hs <- get_holes
@@ -1442,14 +1584,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1442 probs <- get_probs
1584 probs <- get_probs
1443 return (tm, ds, is, probs))
1585 return (tm, ds, is, probs))
1445− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1587+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1447 logLvl 5 "DONE CHECK"
1589 logLvl 5 "DONE CHECK"
1448 logLvl 2 $ "---> " ++ show rhs'
1590 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)
1450 def' <- checkDef fc defer
1593 def' <- checkDef fc defer
1451 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1594 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1452 addDeferred def''
1595 addDeferred def''
1596+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
1454 when (not (null def')) $ do
1598 when (not (null def')) $ do
1455 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
1599 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)
1457 -- Now the remaining deferred (i.e. no type declarations) clauses
1601 -- Now the remaining deferred (i.e. no type declarations) clauses
1458 -- from the where block
1602 -- from the where block
1460− mapM_ (elabDecl' EAll info) wafter
1604+ mapM_ (elabDecl' EAll winfo) wafter
1461− mapM_ (elabCaseBlock info opts) is
1605+ mapM_ (elabCaseBlock winfo opts) is
1463 ctxt <- getContext
1607 ctxt <- getContext
1464 logLvl 5 $ "Rechecking"
1608 logLvl 5 $ "Rechecking"
@@ -1478,7 +1622,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1478 rev <- case ret_fam of
1622 rev <- case ret_fam of
1479 P _ rfamn _ ->
1623 P _ rfamn _ ->
1480 case lookupCtxt rfamn (idris_datatypes i) of
1624 case lookupCtxt rfamn (idris_datatypes i) of
1481− [TI _ _ dopts _] ->
1625+ [TI _ _ dopts _ _] ->
1482 return (DataErrRev `elem` dopts)
1626 return (DataErrRev `elem` dopts)
1483 _ -> return False
1627 _ -> return False
1484 _ -> return False
1628 _ -> return False
@@ -1486,8 +1630,21 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1486 when (rev || ErrorReverse `elem` opts) $ do
1630 when (rev || ErrorReverse `elem` opts) $ do
1487 addIBC (IBCErrRev (crhs, clhs))
1631 addIBC (IBCErrRev (crhs, clhs))
1488 addErrRev (crhs, clhs)
1632 addErrRev (crhs, clhs)
1489− return $ Right (clhs, crhs)
1633+ return $ (Right (clhs, crhs), lhs)
1635+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
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,
1643+ liftname = id -- (\n -> case lookupCtxt n newb of
1645+ -- _ -> MN i (show n)) . l
1491 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1648 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1492 mkLHSapp t = t
1649 mkLHSapp t = t
@@ -1500,7 +1657,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1500-- = NS (UN ('#':show x)) [show cnum, show fname]
1657-- = NS (UN ('#':show x)) [show cnum, show fname]
1502 sepBlocks bs = sepBlocks' [] bs where
1659 sepBlocks bs = sepBlocks' [] bs where
1503− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)
1660+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)
1504 = let (bf, af) = sepBlocks' (n : ns) bs in
1661 = let (bf, af) = sepBlocks' (n : ns) bs in
1505 (d : bf, af)
1662 (d : bf, af)
1506 sepBlocks' ns (d@(PClauses _ _ n _) : bs)
1663 sepBlocks' ns (d@(PClauses _ _ n _) : bs)
@@ -1510,19 +1667,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1510 (b : bf, af)
1667 (b : bf, af)
1511 sepBlocks' ns [] = ([], [])
1668 sepBlocks' ns [] = ([], [])
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,
1521− liftname = id -- (\n -> case lookupCtxt n newb of
1523− -- _ -> MN i (show n)) . l
1527 -- if a hole is just an argument/result of a case block, treat it as
1671 -- if a hole is just an argument/result of a case block, treat it as
1528 -- the unit type. Hack to help elaborate case in do blocks.
1672 -- 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)
1560 let params = getParamsInType i [] fn_is fn_ty
1704 let params = getParamsInType i [] fn_is fn_ty
1561 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1705 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1562− logLvl 1 ("LHS: " ++ show lhs)
1706+ logLvl 2 ("LHS: " ++ show lhs)
1563 ((lhs', dlhs, []), _) <-
1707 ((lhs', dlhs, []), _) <-
1564 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1708 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1565 (errAt "left hand side of with in " fname
1709 (errAt "left hand side of with in " fname
@@ -1589,6 +1733,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1589 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1733 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1590 addDeferred def''
1734 addDeferred def''
1591 mapM_ (elabCaseBlock info opts) is
1735 mapM_ (elabCaseBlock info opts) is
1736+ logLvl 5 ("Checked wval " ++ show wval')
1592 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1737 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1593 let cwvaltyN = explicitNames cwvalty
1738 let cwvaltyN = explicitNames cwvalty
1594 let cwvalN = explicitNames cwval
1739 let cwvalN = explicitNames cwval
@@ -1653,7 +1798,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1653 mapM_ (elabCaseBlock info opts) is
1798 mapM_ (elabCaseBlock info opts) is
1654 logLvl 5 ("Checked RHS " ++ show rhs')
1799 logLvl 5 ("Checked RHS " ++ show rhs')
1655 (crhs, crhsty) <- recheckC fc [] rhs'
1800 (crhs, crhsty) <- recheckC fc [] rhs'
1656− return $ Right (clhs, crhs)
1801+ return $ (Right (clhs, crhs), lhs)
1658 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
1803 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
1659 getImps _ = []
1804 getImps _ = []
@@ -1687,7 +1832,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1687 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1832 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1688 return $ PWith fc wname lhs ws wval withs'
1833 return $ PWith fc wname lhs ws wval withs'
1689 mkAux wname toplhs ns ns' c
1834 mkAux wname toplhs ns ns' c
1690− = ifail $ show fc ++ "badly formed with clause"
1835+ = ifail $ show fc ++ ":badly formed with clause"
1692 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
1837 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
1693 addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]
1838 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)
1698 return $ substMatches mvars $
1843 return $ substMatches mvars $
1699 PApp fc (PRef fc' wname)
1844 PApp fc (PRef fc' wname)
1700 (map pexp ns ++ pexp w : (map pexp ns'))
1845 (map pexp ns ++ pexp w : (map pexp ns'))
1701− updateLHS n wname mvars ns ns' tm w
1846+ updateLHS n wname mvars ns_in ns_in' tm w
1702− = ifail $ "Not implemented match " ++ show tm
1847+ = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w
1704 keepMvar mvs fc v | v `elem` mvs = PRef fc v
1849 keepMvar mvs fc v | v `elem` mvs = PRef fc v
1705 | otherwise = Placeholder
1850 | otherwise = Placeholder
@@ -1717,10 +1862,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1718data MArgTy = IA | EA | CA deriving Show
1863data MArgTy = IA | EA | CA deriving Show
1720−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1865+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
1721 FC -> [PTerm] ->
1866 FC -> [PTerm] ->
1722− Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1867+ Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()
1723−elabClass info syn doc fc constraints tn ps ds
1868+elabClass info syn doc fc constraints tn ps pDocs ds
1724 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1869 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1725 let tty = pibind ps PType
1870 let tty = pibind ps PType
1726 let constraint = PApp fc (PRef fc tn)
1871 let constraint = PApp fc (PRef fc tn)
@@ -1744,10 +1889,10 @@ elabClass info syn doc fc constraints tn ps ds
1744 let cty = impbind ps $ conbind constraints
1889 let cty = impbind ps $ conbind constraints
1745 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1890 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1746 constraint
1891 constraint
1747− let cons = [("", cn, cty, fc, [])]
1892+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
1748 let ddecl = PDatadecl tn tty cons
1893 let ddecl = PDatadecl tn tty cons
1749− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1894+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
1750− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
1895+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
1751 -- for each constraint, build a top level function to chase it
1896 -- for each constraint, build a top level function to chase it
1752 logLvl 5 $ "Building functions"
1897 logLvl 5 $ "Building functions"
1753 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
1898 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
@@ -1785,9 +1930,9 @@ elabClass info syn doc fc constraints tn ps ds
1785 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
1930 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
1786 conbind [] x = x
1931 conbind [] x = x
1788− getMName (PTy _ _ _ _ n _) = nsroot n
1933+ getMName (PTy _ _ _ _ _ n _) = nsroot n
1789− tdecl allmeths (PTy doc syn _ o n t)
1934+ tdecl allmeths (PTy doc _ syn _ o n t)
1790− = do t' <- implicit' syn allmeths n t
1935+ = do t' <- implicit' info syn allmeths n t
1791 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1936 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1792 return ( (n, (toExp (map fst ps) Exp t')),
1937 return ( (n, (toExp (map fst ps) Exp t')),
1793 (n, (doc, o, (toExp (map fst ps) Imp t'))),
1938 (n, (doc, o, (toExp (map fst ps) Imp t'))),
@@ -1799,7 +1944,7 @@ elabClass info syn doc fc constraints tn ps ds
1799 case lookup n mtys of
1944 case lookup n mtys of
1800 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1945 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1801 let ds = map (decorateid defaultdec)
1946 let ds = map (decorateid defaultdec)
1802− [PTy "" syn fc [] n ty',
1947+ [PTy emptyDocstring [] syn fc [] n ty',
1803 PClauses fc (o ++ opts) n cs]
1948 PClauses fc (o ++ opts) n cs]
1804 iLOG (show ds)
1949 iLOG (show ds)
1805 return (n, ((defaultdec n, ds!!1), ds))
1950 return (n, ((defaultdec n, ds!!1), ds))
@@ -1809,7 +1954,7 @@ elabClass info syn doc fc constraints tn ps ds
1809 defaultdec (UN n) = sUN ("default#" ++ str n)
1954 defaultdec (UN n) = sUN ("default#" ++ str n)
1810 defaultdec (NS n ns) = NS (defaultdec n) ns
1955 defaultdec (NS n ns) = NS (defaultdec n) ns
1812− tydecl (PTy _ _ _ _ _ _) = True
1957+ tydecl (PTy _ _ _ _ _ _ _) = True
1813 tydecl _ = False
1958 tydecl _ = False
1814 instdecl (PInstance _ _ _ _ _ _ _ _) = True
1959 instdecl (PInstance _ _ _ _ _ _ _ _) = True
1815 instdecl _ = False
1960 instdecl _ = False
@@ -1837,7 +1982,7 @@ elabClass info syn doc fc constraints tn ps ds
1837 addInstance False conn' cfn
1982 addInstance False conn' cfn
1838 addIBC (IBCInstance False conn' cfn)
1983 addIBC (IBCInstance False conn' cfn)
1839-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1984-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1840− return [PTy "" syn fc [] cfn ty,
1985+ return [PTy emptyDocstring [] syn fc [] cfn ty,
1841 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1986 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1843 -- Generate a top level function which looks up a method in a given
1988 -- 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
1853 iLOG (showTmImpls ty)
1998 iLOG (showTmImpls ty)
1854 iLOG (show (m, ty', capp, margs))
1999 iLOG (show (m, ty', capp, margs))
1855 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
2000 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
1856− return [PTy doc syn fc o m ty',
2001+ return [PTy doc [] syn fc o m ty',
1857 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
2002 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
1859− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc
2004+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc
1860− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc
2005+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc
1861− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc
2006+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc
1862 getMArgs _ = []
2007 getMArgs _ = []
1864 getMeth (m:ms) (a:as) x | x == a = PRef fc m
2009 getMeth (m:ms) (a:as) x | x == a = PRef fc m
1865 | otherwise = getMeth ms as x
2010 | otherwise = getMeth ms as x
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
1868 lhsArgs (IA : xs) ns = lhsArgs xs ns
2013 lhsArgs (IA : xs) ns = lhsArgs xs ns
1869 lhsArgs (CA : xs) ns = lhsArgs xs ns
2014 lhsArgs (CA : xs) ns = lhsArgs xs ns
1870 lhsArgs [] _ = []
2015 lhsArgs [] _ = []
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
1873 rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
2018 rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
1874 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
2019 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
1875 rhsArgs [] _ = []
2020 rhsArgs [] _ = []
1877− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
2022+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)
1878 = PPi p n ty (insertConstraint c sc)
2023 = PPi p n ty (insertConstraint c sc)
1879 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
2024 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
1881 -- make arguments explicit and don't bind class parameters
2026 -- 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)
1883 | n `elem` ns = toExp ns e sc
2028 | 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)
1885 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
2030 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
1886 toExp ns e sc = sc
2031 toExp ns e sc = sc
@@ -1897,11 +2042,14 @@ elabInstance info syn what fc cs n ps t expn ds = do
1897 i <- getIState
2042 i <- getIState
1898 (n, ci) <- case lookupCtxtName n (idris_classes i) of
2043 (n, ci) <- case lookupCtxtName n (idris_classes i) of
1899 [c] -> return c
2044 [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))
1901 let constraint = PApp fc (PRef fc n) (map pexp ps)
2048 let constraint = PApp fc (PRef fc n) (map pexp ps)
1902 let iname = mkiname n ps expn
2049 let iname = mkiname n ps expn
1903− when (what /= EDefns) $ do
2050+ let emptyclass = null (class_methods ci)
1904− nty <- elabType' True info syn "" fc [] iname t
2051+ when (what /= EDefns || (null ds && not emptyclass)) $ do
2052+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
1905 -- if the instance type matches any of the instances we have already,
2053 -- if the instance type matches any of the instances we have already,
1906 -- and it's not a named instance, then it's overlapping, so report an error
2054 -- and it's not a named instance, then it's overlapping, so report an error
1907 case expn of
2055 case expn of
@@ -1909,7 +2057,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
1909 (class_instances ci)
2057 (class_instances ci)
1910 addInstance intInst n iname
2058 addInstance intInst n iname
1911 Just _ -> addInstance intInst n iname
2059 Just _ -> addInstance intInst n iname
1912− when (what /= ETypes) $ do
2060+ when (what /= ETypes && (not (null ds && not emptyclass))) $ do
1913 let ips = zip (class_params ci) ps
2061 let ips = zip (class_params ci) ps
1914 let ns = case n of
2062 let ns = case n of
1915 NS n ns' -> ns'
2063 NS n ns' -> ns'
@@ -1917,7 +2065,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
1917 -- get the implicit parameters that need passing through to the
2065 -- get the implicit parameters that need passing through to the
1918 -- where block
2066 -- where block
1919 wparams <- mapM (\p -> case p of
2067 wparams <- mapM (\p -> case p of
1920− PApp _ _ args -> getWParams args
2068+ PApp _ _ args -> getWParams (map getTm args)
1921 _ -> return []) ps
2069 _ -> return []) ps
1922 let pnames = map pname (concat (nub wparams))
2070 let pnames = map pname (concat (nub wparams))
1923 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
2071 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
1940 let wbTys = map mkTyDecl mtys
2088 let wbTys = map mkTyDecl mtys
1941 let wbVals = map (decorateid (decorate ns iname)) ds'
2089 let wbVals = map (decorateid (decorate ns iname)) ds'
1942 let wb = wbTys ++ wbVals
2090 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)
1944 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
2092 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
1945 show (concat (nub wparams))
2093 show (concat (nub wparams))
1946− let lhs = PRef fc iname
2094+
2095+ -- Bring variables in instance head into scope
2097+ let headVars = nub $ mapMaybe (\p -> case p of
2099+ case lookupTy n (tt_ctxt ist) of
2103+-- let lhs = PRef fc iname
2104+ let lhs = PApp fc (PRef fc iname)
2105+ (map (\n -> pimp n (PRef fc n) True) headVars)
1947 let rhs = PApp fc (PRef fc (instanceName ci))
2106 let rhs = PApp fc (PRef fc (instanceName ci))
1948 (map (pexp . mkMethApp) mtys)
2107 (map (pexp . mkMethApp) mtys)
2109+ logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
2110+ logLvl 5 $ "Instance RHS " ++ show rhs
1949 let idecls = [PClauses fc [Dictionary] iname
2112 let idecls = [PClauses fc [Dictionary] iname
1950 [PClause fc iname lhs [] rhs wb]]
2113 [PClause fc iname lhs [] rhs wb]]
1951 iLOG (show idecls)
2114 iLOG (show idecls)
1952 mapM_ (elabDecl EAll info) idecls
2115 mapM_ (elabDecl EAll info) idecls
1953 addIBC (IBCInstance intInst n iname)
2116 addIBC (IBCInstance intInst n iname)
1954−-- -- for each constraint, build a top level function to chase it
2117+
1955−-- logLvl 5 $ "Building functions"
1956−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1957−-- mapM_ (elabDecl EAll info) (concat fns)
1959 intInst = case ps of
2119 intInst = case ps of
1960 [PConstant (AType (ATInt ITNative))] -> True
2120 [PConstant (AType (ATInt ITNative))] -> True
@@ -1979,7 +2139,8 @@ elabInstance info syn what fc cs n ps t expn ds = do
1979 -- TODO: largely based upon elabType' - should try to abstract
2139 -- TODO: largely based upon elabType' - should try to abstract
1980 elabFindOverlapping i ci iname syn t
2140 elabFindOverlapping i ci iname syn t
1981 = do ty' <- addUsingConstraints syn fc t
2141 = 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'
1983 let ty = addImpl i ty'
2144 let ty = addImpl i ty'
1984 ctxt <- getContext
2145 ctxt <- getContext
1985 ((tyT, _, _), _) <-
2146 ((tyT, _, _), _) <-
@@ -2009,17 +2170,17 @@ elabInstance info syn what fc cs n ps t expn ds = do
2010 mkMethApp (n, _, _, ty)
2171 mkMethApp (n, _, _, ty)
2011 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
2172 = 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'
2013 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2174 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2014 lamBind i (PPi _ n ty sc) sc'
2175 lamBind i (PPi _ n ty sc) sc'
2015 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2176 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2016 lamBind i _ sc = sc
2177 lamBind i _ sc = sc
2017− methArgs i (PPi (Imp _ _ _ _) n ty sc)
2178+ methArgs i (PPi (Imp _ _ _) n ty sc)
2018− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
2179+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2019− methArgs i (PPi (Exp _ _ _ _) n ty sc)
2180+ methArgs i (PPi (Exp _ _ _) n ty sc)
2020− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc
2181+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2021− methArgs i (PPi (Constraint _ _ _) n ty sc)
2182+ methArgs i (PPi (Constraint _ _) n ty sc)
2022− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc
2183+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
2023 methArgs i _ = []
2184 methArgs i _ = []
2025 papp fc f [] = f
2186 papp fc f [] = f
@@ -2027,7 +2188,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
2028 getWParams [] = return []
2189 getWParams [] = return []
2029 getWParams (p : ps)
2190 getWParams (p : ps)
2030− | PRef _ n <- getTm p
2191+ | PRef _ n <- p
2031 = do ps' <- getWParams ps
2192 = do ps' <- getWParams ps
2032 ctxt <- getContext
2193 ctxt <- getContext
2033 case lookupP n ctxt of
2194 case lookupP n ctxt of
@@ -2035,15 +2196,15 @@ elabInstance info syn what fc cs n ps t expn ds = do
2035 _ -> return ps'
2196 _ -> return ps'
2036 getWParams (_ : ps) = getWParams ps
2197 getWParams (_ : ps) = getWParams ps
2038− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2199+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2039 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2200 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2041− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t
2202+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
2043 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2204 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2044 conbind [] x = x
2205 conbind [] x = x
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)
2047 coninsert cs sc = conbind cs sc
2208 coninsert cs sc = conbind cs sc
2049 insertDefaults :: IState -> Name ->
2210 insertDefaults :: IState -> Name ->
@@ -2101,7 +2262,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
2101 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
2262 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
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
2105decorateid decorate (PClauses f o n cs)
2266decorateid decorate (PClauses f o n cs)
2106 = PClauses f o (decorate n) (map dc cs)
2267 = PClauses f o (decorate n) (map dc cs)
2107 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
2268 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 _ _ _)
2155 = return () -- nothing to elaborate
2316 = return () -- nothing to elaborate
2156elabDecl' _ info (PSyntax _ p)
2317elabDecl' _ info (PSyntax _ p)
2157 = return () -- nothing to elaborate
2318 = 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)
2159 | what /= EDefns
2320 | what /= EDefns
2160 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
2321 = 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
2162 return ()
2323 return ()
2163elabDecl' what info (PPostulate doc s f o n ty)
2324elabDecl' what info (PPostulate doc s f o n ty)
2164 | what /= EDefns
2325 | what /= EDefns
2165 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
2326 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
2166 elabPostulate info s doc f o n ty
2327 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)
2168 | what /= ETypes
2329 | what /= ETypes
2169 = do iLOG $ "Elaborating " ++ show (d_name d)
2330 = do iLOG $ "Elaborating " ++ show (d_name d)
2170− elabData info s doc f co d
2331+ elabData info s doc argDocs f co d
2171 | otherwise
2332 | otherwise
2172 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
2333 = 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))
2174elabDecl' what info d@(PClauses f o n ps)
2335elabDecl' what info d@(PClauses f o n ps)
2175 | what /= ETypes
2336 | what /= ETypes
2176 = do iLOG $ "Elaborating clause " ++ show n
2337 = do iLOG $ "Elaborating clause " ++ show n
@@ -2184,6 +2345,11 @@ elabDecl' what info (PMutual f ps)
2184 [p] -> elabDecl what info p
2345 [p] -> elabDecl what info p
2185 _ -> do mapM_ (elabDecl ETypes info) ps
2346 _ -> do mapM_ (elabDecl ETypes info) ps
2186 mapM_ (elabDecl EDefns info) ps
2347 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
2187 -- Do totality checking after entire mutual block
2353 -- Do totality checking after entire mutual block
2188 i <- get
2354 i <- get
2189 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
2355 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
@@ -2192,6 +2358,16 @@ elabDecl' what info (PMutual f ps)
2192 mapM_ buildSCG (idris_totcheck i)
2358 mapM_ buildSCG (idris_totcheck i)
2193 mapM_ checkDeclTotality (idris_totcheck i)
2359 mapM_ checkDeclTotality (idris_totcheck i)
2194 clear_totcheck
2360 clear_totcheck
2361+ where isDataDecl (PData _ _ _ _ _ _) = True
2362+ isDataDecl _ = False
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) }
2196elabDecl' what info (PParams f ns ps)
2372elabDecl' what info (PParams f ns ps)
2197 = do i <- getIState
2373 = do i <- getIState
@@ -2214,30 +2390,30 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
2214 ninfo = case namespace info of
2390 ninfo = case namespace info of
2215 Nothing -> info { namespace = Just [n] }
2391 Nothing -> info { namespace = Just [n] }
2216 Just ns -> info { namespace = Just (n:ns) }
2392 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)
2218 | what /= EDefns
2394 | what /= EDefns
2219 = do iLOG $ "Elaborating class " ++ show n
2395 = 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
2221elabDecl' what info (PInstance s f cs n ps t expn ds)
2397elabDecl' what info (PInstance s f cs n ps t expn ds)
2222 = do iLOG $ "Elaborating instance " ++ show n
2398 = do iLOG $ "Elaborating instance " ++ show n
2223 elabInstance info s what f cs n ps t expn ds
2399 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)
2225 | what /= ETypes
2401 | what /= ETypes
2226 = do iLOG $ "Elaborating record " ++ show tyn
2402 = 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
2228 | otherwise
2404 | otherwise
2229 = do iLOG $ "Elaborating [type of] " ++ show tyn
2405 = 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)
2231elabDecl' _ info (PDSL n dsl)
2407elabDecl' _ info (PDSL n dsl)
2232 = do i <- getIState
2408 = do i <- getIState
2233 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
2409 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
2234 addIBC (IBCDSL n)
2410 addIBC (IBCDSL n)
2235elabDecl' what info (PDirective i)
2411elabDecl' what info (PDirective i)
2236 | what /= EDefns = i
2412 | what /= EDefns = i
2237−elabDecl' what info (PProvider syn fc provWhat n tp tm)
2413+elabDecl' what info (PProvider syn fc provWhat n)
2238 | what /= EDefns
2414 | what /= EDefns
2239 = do iLOG $ "Elaborating type provider " ++ show n
2415 = do iLOG $ "Elaborating type provider " ++ show n
2240− elabProvider info syn fc provWhat n tp tm
2416+ elabProvider info syn fc provWhat n
2241elabDecl' what info (PTransform fc safety old new)
2417elabDecl' what info (PTransform fc safety old new)
2242 = elabTransform info fc safety old new
2418 = elabTransform info fc safety old new
2243elabDecl' _ _ _ = return () -- skipped this time
2419elabDecl' _ _ _ = return () -- skipped this time
@@ -2282,3 +2458,14 @@ inferredDiff fc inf user =
2282 Right vs -> return False
2458 Right vs -> return False
2283 Left (x, y) -> return True
2459 Left (x, y) -> return True
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."