@@ -20,6 +20,16 @@ import Idris.DeepSeq
2020import Idris.Output (iputStrLn, pshow, iWarn)
2121import IRTS.Lang
2222
23+import Idris.Elab.Utils
24+import Idris.Elab.Type
25+import Idris.Elab.Clause
26+import Idris.Elab.Data
27+import Idris.Elab.Record
28+import Idris.Elab.Class
29+import Idris.Elab.Instance
30+import Idris.Elab.Provider
31+import Idris.Elab.Value
32+
2333import Idris.Core.TT
2434import Idris.Core.Elaborate hiding (Tactic(..))
2535import Idris.Core.Evaluate
@@ -48,638 +58,14 @@ import Data.List.Split (splitOn)
4858
4959import Util.Pretty(pretty, text)
5060
51−recheckC fc env t
52− = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
53− ctxt <- getContext
54− (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
55− Error e -> tfail (At fc e)
56− OK x -> return x
57− addConstraints fc cs
58− return (tm, ty)
59−
60−
61−checkDef fc ns = checkAddDef False True fc ns
62−
63−checkAddDef add toplvl fc [] = return []
64−checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
65− = do ctxt <- getContext
66− (t', _) <- recheckC fc [] t
67− when add $ do addDeferred [(n, (i, top, t, toplvl))]
68− addIBC (IBCDef n)
69− ns' <- checkAddDef add toplvl fc ns
70− return ((n, (i, top, t')) : ns')
71−-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
72−-- return (n, (i, top, t'))) ns
73−
74−buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->
75− Idris (Type, PTerm, [(Int, Name)])
76−buildType info syn fc opts n ty' = do
77− ctxt <- getContext
78− i <- getIState
79−
80− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
81− ty' <- addUsingConstraints syn fc ty'
82− ty' <- addUsingImpls syn n fc ty'
83− let ty = addImpl i ty'
84−
85− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
86− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
87−
88− ((tyT', defer, is), log) <-
89− tclift $ elaborate ctxt n (TType (UVal 0)) []
90− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))
91−
92− let tyT = patToImp tyT'
93−
94− logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'
95−
96− ds <- checkAddDef True False fc defer
97− -- if the type is not complete, note that we'll need to infer
98− -- things later (for solving metavariables)
99− when (not (null ds)) $ addTyInferred n
100−
101− mapM_ (elabCaseBlock info opts) is
102− ctxt <- getContext
103− logLvl 5 $ "Rechecking"
104− logLvl 6 $ show tyT
105− logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
106− (cty, _) <- recheckC fc [] tyT
107−
108− -- record the implicit and inaccessible arguments
109− i <- getIState
110− let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty
111− let inacc = inaccessibleImps 0 cty inaccData
112− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc
113−
114− putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }
115− logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)
116− addIBC (IBCImp n)
117−
118− return (cty, ty, inacc)
119− where
120− patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)
121− patToImp (Bind n b sc) = Bind n b (patToImp sc)
122− patToImp t = t
123−
124−
125−-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
126−elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
127− FC -> FnOpts -> Name -> PTerm -> Idris Type
128−elabType = elabType' False
129−
130−elabType' :: Bool -> -- normalise it
131− ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
132− FC -> FnOpts -> Name -> PTerm -> Idris Type
133−elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
134− n = liftname info n_in in -}
135− do checkUndefined fc n
136− (cty, ty, inacc) <- buildType info syn fc opts n ty'
137−
138− addStatics n cty ty
139− let nty = cty -- normalise ctxt [] cty
140− -- if the return type is something coinductive, freeze the definition
141− ctxt <- getContext
142− let nty' = normalise ctxt [] nty
143− logLvl 2 $ "Rechecked to " ++ show nty'
144−
145− -- Add normalised type to internals
146− i <- getIState
147− rep <- useREPL
148− when rep $ do
149− addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
150− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
151−
152− let (t, _) = unApply (getRetTy nty')
153− let corec = case t of
154− P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
155− [TI _ True _ _ _] -> True
156− _ -> False
157− _ -> False
158− -- Productivity checking now via checking for guarded 'Delay'
159− let opts' = opts -- if corec then (Coinductive : opts) else opts
160− let usety = if norm then nty' else nty
161− ds <- checkDef fc [(n, (-1, Nothing, usety))]
162− addIBC (IBCDef n)
163− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
164− addDeferred ds'
165− setFlags n opts'
166− checkDocs fc argDocs ty
167− addDocStr n doc argDocs
168− addIBC (IBCDoc n)
169− addIBC (IBCFlags n opts')
170− fputState (opt_inaccessible . ist_optimisation n) inacc
171− addIBC (IBCOpt n)
172− when (Implicit `elem` opts') $ do addCoercion n
173− addIBC (IBCCoercion n)
174−
175− -- If the function is declared as an error handler and the language
176− -- extension is enabled, then add it to the list of error handlers.
177− errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
178− when (ErrorHandler `elem` opts) $ do
179− if errorReflection
180− then
181− -- TODO: Check that the declared type is the correct type for an error handler:
182− -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
183− if tyIsHandler nty'
184− then do i <- getIState
185− putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
186− addIBC (IBCErrorHandler n)
187− else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
188− else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
189− return usety
190− where
191− -- for making an internalapp, we only want the explicit ones, and don't
192− -- want the parameters, so just take the arguments which correspond to the
193− -- user declared explicit ones
194− mergeTy (PPi e n ty sc) (PPi e' n' _ sc')
195− | e == e' = PPi e n ty (mergeTy sc sc')
196− | otherwise = mergeTy sc sc'
197− mergeTy _ sc = sc
198−
199− err = txt "Err"
200− maybe = txt "Maybe"
201− lst = txt "List"
202− errrep = txt "ErrorReportPart"
203−
204− tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
205− (App (P _ (NS (UN m) ns2) _)
206− (App (P _ (NS (UN l) ns3) _)
207− (P _ (NS (UN r) ns4) _))))
208− | e == err && m == maybe && l == lst && r == errrep
209− , ns1 == map txt ["Errors","Reflection","Language"]
210− , ns2 == map txt ["Maybe", "Prelude"]
211− , ns3 == map txt ["List", "Prelude"]
212− , ns4 == map txt ["Reflection","Language"] = True
213− tyIsHandler _ = False
214−
215−-- Get the list of (index, name) of inaccessible arguments from an elaborated
216−-- type
217−inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]
218−inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)
219− | inacc = (i, n) : inaccessibleImps (i + 1) sc ins
220− | otherwise = inaccessibleImps (i + 1) sc ins
221−inaccessibleImps _ _ _ = []
222−
223−-- Get the list of (index, name) of inaccessible arguments from the type.
224−inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
225−inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
226− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
227−inaccessibleArgs i (PPi plicity n ty t)
228− | InaccessibleArg `elem` pargopts plicity
229− = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
230− | otherwise
231− = inaccessibleArgs (i+1) t -- a {regular : Implicit}
232−inaccessibleArgs _ _ = []
233−
234−elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
235− FC -> FnOpts -> Name -> PTerm -> Idris ()
236−elabPostulate info syn doc fc opts n ty = do
237− elabType info syn doc [] fc opts n ty
238− putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
239− addIBC (IBCPostulate n)
240−
241− -- remove it from the deferred definitions list
242− solveDeferred n
243−
244−elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
245−elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
246− = do let codata = Codata `elem` opts
247− iLOG (show (fc, doc))
248− checkUndefined fc n
249− (cty, t, inacc) <- buildType info syn fc [] n t_in
250−
251− addIBC (IBCDef n)
252− updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
253−
254−elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
255− = do let codata = Codata `elem` opts
256− iLOG (show fc)
257− undef <- isUndefined fc n
258− (cty, t, inacc) <- buildType info syn fc [] n t_in
259− -- if n is defined already, make sure it is just a type declaration
260− -- with the same type we've just elaborated
261− i <- getIState
262− checkDefinedAs fc n cty (tt_ctxt i)
263− -- temporary, to check cons
264− when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
265− let cnameinfo = cinfo info (map cname dcons)
266− cons <- mapM (elabCon cnameinfo syn n codata) dcons
267− ttag <- getName
268− i <- getIState
269− let as = map (const Nothing) (getArgTys cty)
270− let params = findParams (map snd cons)
271− logLvl 2 $ "Parameters : " ++ show params
272− -- TI contains information about mutually declared types - this will
273− -- be updated when the mutual block is complete
274− putIState (i { idris_datatypes =
275− addDef n (TI (map fst cons) codata opts params [n])
276− (idris_datatypes i) })
277− addIBC (IBCDef n)
278− addIBC (IBCData n)
279− checkDocs fc argDocs t
280− addDocStr n doc argDocs
281− addIBC (IBCDoc n)
282− let metainf = DataMI params
283− addIBC (IBCMetaInformation n metainf)
284− -- TMP HACK! Make this a data option
285− updateContext (addDatatype (Data n ttag cty cons))
286− updateContext (setMetaInformation n metainf)
287− mapM_ totcheck (zip (repeat fc) (map fst cons))
288−-- mapM_ (checkPositive n) cons
289−
290− -- if there's exactly one constructor,
291− -- mark both the type and the constructor as detaggable
292− case cons of
293− [(cn,ct)] -> setDetaggable cn >> setDetaggable n
294− >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
295− _ -> return ()
296−
297− -- create an eliminator
298− when (DefaultEliminator `elem` opts) $
299− evalStateT (elabCaseFun True params n t dcons info) Map.empty
300− -- create a case function
301− when (DefaultCaseFun `elem` opts) $
302− evalStateT (elabCaseFun False params n t dcons info) Map.empty
303− where
304− setDetaggable :: Name -> Idris ()
305− setDetaggable n = do
306− ist <- getIState
307− let opt = idris_optimisation ist
308− case lookupCtxt n opt of
309− [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
310− _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
311−
312− checkDefinedAs fc n t ctxt
313− = case lookupDef n ctxt of
314− [] -> return ()
315− [TyDecl _ ty] ->
316− case converts ctxt [] t ty of
317− OK () -> return ()
318− _ -> tclift $ tfail (At fc (AlreadyDefined n))
319− _ -> tclift $ tfail (At fc (AlreadyDefined n))
320− -- parameters are names which are unchanged across the structure,
321− -- which appear exactly once in the return type of a constructor
322−
323− -- First, find all applications of the constructor, then check over
324− -- them for repeated arguments
325−
326− findParams :: [Type] -> [Int]
327− findParams ts = let allapps = concatMap getDataApp ts in
328− paramPos allapps
329−
330− paramPos [] = []
331− paramPos (args : rest)
332− = dropNothing $ keepSame (zip [0..] args) rest
333−
334− dropNothing [] = []
335− dropNothing ((x, Nothing) : ts) = dropNothing ts
336− dropNothing ((x, _) : ts) = x : dropNothing ts
337−
338− keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
339− [(Int, Maybe Name)]
340− keepSame as [] = as
341− keepSame as (args : rest) = keepSame (update as args) rest
342− where
343− update [] _ = []
344− update _ [] = []
345− update ((n, Just x) : as) (Just x' : args)
346− | x == x' = (n, Just x) : update as args
347− update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
348−
349− getDataApp :: Type -> [[Maybe Name]]
350− getDataApp f@(App _ _)
351− | (P _ d _, args) <- unApply f
352− = if (d == n) then [mParam args args] else []
353− getDataApp (Bind n (Pi t) sc)
354− = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
355− getDataApp _ = []
356−
357− -- keep the arguments which are single names, which don't appear
358− -- elsewhere
359−
360− mParam args [] = []
361− mParam args (P Bound n _ : rest)
362− | count n args == 1
363− = Just n : mParam args rest
364− where count n [] = 0
365− count n (t : ts)
366− | n `elem` freeNames t = 1 + count n ts
367− | otherwise = count n ts
368− mParam args (_ : rest) = Nothing : mParam args rest
369−
370− cname (_, _, n, _, _, _) = n
371−
372− -- Abuse of ElabInfo.
373− -- TODO Contemplate whether the ElabInfo type needs modification.
374− cinfo :: ElabInfo -> [Name] -> ElabInfo
375− cinfo info ds
376− = let newps = params info
377− dsParams = map (\n -> (n, [])) ds
378− newb = addAlist dsParams (inblock info)
379− l = liftname info in
380− info { params = newps,
381− inblock = newb,
382− liftname = id -- Is this appropriate?
383− }
384−
385−-- FIXME: 'forcenames' is an almighty hack! Need a better way of
386−-- erasing non-forceable things
387−-- ^^^
388−-- TODO: the above is a comment from the past;
389−-- forcenames is probably no longer needed
390−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
391− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
392−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
393− = do checkUndefined fc n
394− (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)
395− ctxt <- getContext
396− let cty' = normalise ctxt [] cty
397−
398− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
399− logLvl 5 $ "Inaccessible args: " ++ show inacc
400− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
401−
402− addIBC (IBCDef n)
403− checkDocs fc argDocs t
404− addDocStr n doc argDocs
405− addIBC (IBCDoc n)
406− fputState (opt_inaccessible . ist_optimisation n) inacc
407− addIBC (IBCOpt n)
408− return (n, cty')
409− where
410− tyIs (Bind n b sc) = tyIs sc
411− tyIs t | (P _ n' _, _) <- unApply t
412− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
413− else return ()
414− tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))
415−
416− mkLazy (PPi pl n ty sc)
417− = let ty' = if getTyName ty
418− then PApp fc (PRef fc (sUN "Lazy'"))
419− [pexp (PRef fc (sUN "LazyCodata")),
420− pexp ty]
421− else ty in
422− PPi pl n ty' (mkLazy sc)
423− mkLazy t = t
424−
425− getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
426− getTyName (PRef _ n) = n == nsroot tn
427− getTyName _ = False
428−
429−
430− getNamePos :: Int -> PTerm -> Name -> Maybe Int
431− getNamePos i (PPi _ n _ sc) x | n == x = Just i
432− | otherwise = getNamePos (i + 1) sc x
433− getNamePos _ _ _ = Nothing
434−
435−type EliminatorState = StateT (Map.Map String Int) Idris
436−
437−-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
438−-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
439−-- rename to caseFun to match updated intend
440−elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
441− [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
442− ElabInfo -> EliminatorState ()
443−elabCaseFun ind paramPos n ty cons info = do
444− elimLog $ "Elaborating case function"
445− put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
446− let (cnstrs, _) = splitPi ty
447− let (splittedTy@(pms, idxs)) = splitPms cnstrs
448− generalParams <- namePis False pms
449− motiveIdxs <- namePis False idxs
450− let motive = mkMotive n paramPos generalParams motiveIdxs
451− consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do
452− let casefunt = if ind then "elim_" else "case_"
453− name <- freshName $ casefunt ++ simpleName cnm
454− consTerm <- extractConsTerm c generalParams
455− return (name, expl, consTerm)) cons
456− scrutineeIdxs <- namePis False idxs
457− let motiveConstr = [(motiveName, expl, motive)]
458− let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
459− let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
460− let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
461− let clauseConsElimArgs = map getPiName consTerms
462− let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
463− let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
464− let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy
465− elimLog elimSig
466− eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
467− let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
468− elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
469− State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
470− -- Do not elaborate clauses if there aren't any
471− case eliminatorClauses of
472− [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
473− _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
474− where elimLog :: String -> EliminatorState ()
475− elimLog s = State.lift (logLvl 2 s)
476−
477− elimFC :: FC
478− elimFC = fileFC "(casefun)"
479−
480− elimDeclName :: Name
481− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n
482−
483− applyNS :: Name -> [String] -> Name
484− applyNS n [] = n
485− applyNS n ns = sNS n ns
486−
487− splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
488− splitPi = splitPi' []
489− where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
490− splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
491− splitPi' acc t = (reverse acc, t)
492−
493− splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
494− splitPms cnstrs = (map fst pms, map fst idxs)
495− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
496−
497− isMachineGenerated :: Name -> Bool
498− isMachineGenerated (MN _ _) = True
499− isMachineGenerated _ = False
500−
501− namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
502− namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
503− let oldNames = map fst names
504− let params = map snd names
505− return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
506−
507− mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
508− mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
509− mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
510− return (oldName, (name, pl, piarg))
511− where keyOf :: PTerm -> String
512− keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
513− keyOf (PApp _ tyf _) = keyOf tyf
514− keyOf PType = "ty__"
515− keyOf _ = "carg__"
516− nameStart :: Name -> Char
517− nameStart n = nameStart' (simpleName n)
518− where nameStart' :: String -> Char
519− nameStart' "" = ' '
520− nameStart' ns = head ns
521−
522− simpleName :: Name -> String
523− simpleName (NS n _) = simpleName n
524− simpleName (MN i n) = str n ++ show i
525− simpleName n = show n
526−
527− nameSpaces :: Name -> [String]
528− nameSpaces (NS _ ns) = map str ns
529− nameSpaces _ = []
530−
531− freshName :: String -> EliminatorState Name
532− freshName key = do
533− nameMap <- get
534− let i = fromMaybe 0 (Map.lookup key nameMap)
535− let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
536− put $ Map.insert key (i+1) nameMap
537− return name
538−
539− scrutineeName :: Name
540− scrutineeName = sUN "scrutinee"
54161
542− scrutineeArgName :: Name
543− scrutineeArgName = sUN "scrutineeArg"
544−
545− motiveName :: Name
546− motiveName = sUN "prop"
547−
548− mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
549− mkMotive n paramPos params indicies =
550− let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
551− in piConstr (indicies ++ [scrutineeTy]) PType
552−
553− piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
554− piConstr [] ty = ty
555− piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)
556−
557− interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
558− interlievePos idxs [] l2 i = l2
559− interlievePos idxs l1 [] i = l1
560− interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
561− interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
562−
563− replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
564− replaceParams paramPos params cns =
565− let (_, cnsResTy) = splitPi cns
566− in case cnsResTy of
567− PApp _ _ args ->
568− let oldParams = paramNamesOf 0 paramPos args
569− in removeParamPis oldParams params cns
570− _ -> cns
571−
572− removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
573− removeParamPis oldParams params (PPi pl n tyb tyr) =
574− case findIndex (== n) oldParams of
575− Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
576− Just i -> (removeParamPis oldParams params tyr)
577− removeParamPis oldParams params (PRef _ n) =
578− case findIndex (== n) oldParams of
579− Nothing -> (PRef elimFC n)
580− Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
581− removeParamPis oldParams params (PApp _ cns args) =
582− PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
583− where replaceParamArgs :: [PArg] -> [PArg]
584− replaceParamArgs [] = []
585− replaceParamArgs (arg:args) =
586− case extractName (getTm arg) of
587− [] -> arg:replaceParamArgs args
588− [n] ->
589− case findIndex (== n) oldParams of
590− Nothing -> arg:replaceParamArgs args
591− Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args
592− removeParamPis oldParams params t = t
593−
594− paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
595− paramNamesOf i paramPos [] = []
596− paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
597−
598− extractName :: PTerm -> [Name]
599− extractName (PRef _ n) = [n]
600− extractName _ = []
601−
602− splitArgPms :: PTerm -> ([PTerm], [PTerm])
603− splitArgPms (PApp _ f args) = splitArgPms' args
604− where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
605− splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
606− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
607− splitArgPms _ = ([],[])
608−
609−
610− implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
611− implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
612− i <- State.lift getIState
613− implargs' <- case lookupCtxt cnm (idris_implicits i) of
614− [] -> do fail $ "Error while showing implicits for " ++ show cnm
615− [args] -> do return args
616− _ -> do fail $ "Ambigous name for " ++ show cnm
617− let implargs = mapMaybe convertImplPi implargs'
618− let (_, cnsResTy) = splitPi ty
619− case cnsResTy of
620− PApp _ _ args ->
621− let oldParams = paramNamesOf 0 paramPos args
622− in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
623− _ -> return implargs
624−
625− extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
626− extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
627− let cons' = replaceParams paramPos generalParameters ty
628− let (args, resTy) = splitPi cons'
629− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
630− consArgs <- namePis False args
631− let recArgs = findRecArgs consArgs
632− let recMotives = if ind then map applyRecMotive recArgs else []
633− let (_, consIdxs) = splitArgPms resTy
634− return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
635− where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
636− applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
637− where (_, idxs) = splitArgPms ty
638−
639− findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
640− findRecArgs [] = []
641− findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
642− findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
643− findRecArgs (ty:rs) = findRecArgs rs
644−
645− applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
646− applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)
647−
648− convertArg :: (Name, Plicity, PTerm) -> PArg
649− convertArg (n, _, _) = pexp (PRef elimFC n)
650−
651− applyMotive :: [PTerm] -> PTerm -> PTerm
652− applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])
653−
654− getPiName :: (Name, Plicity, PTerm) -> Name
655− getPiName (name,_,_) = name
656−
657− convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
658− convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
659− convertImplPi _ = Nothing
660−
661− generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
662− generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
663− let cons' = replaceParams paramPos generalParameters ty
664− let (args, resTy) = splitPi cons'
665− i <- State.lift getIState
666− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
667− let (_, generalIdxs') = splitArgPms resTy
668− let generalIdxs = map pexp generalIdxs'
669− consArgs <- namePis False args
670− let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
671− let recArgs = findRecArgs consArgs
672− let recElims = if ind then map applyRecElim recArgs else []
673− let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
674− return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
675− where applyRecElim :: (Name, Plicity, PTerm) -> PArg
676− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
677− where (_, idxs) = splitArgPms recTy
62+-- Top level elaborator info, supporting recursive elaboration
63+recinfo :: ElabInfo
64+recinfo = EInfo [] emptyContext id Nothing elabDecl'
67865
67966-- | Elaborate primitives
680−
68167elabPrims :: Idris ()
682−elabPrims = do mapM_ (elabDecl EAll toplevel)
68+elabPrims = do mapM_ (elabDecl' EAll recinfo)
68369 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
68470 (zip4
68571 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
@@ -687,7 +73,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
68773 [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
68874 [[], [], [], pairParamDoc, eqParamDoc]))
68975 addNameHint eqTy (sUN "prf")
690− elabDecl EAll toplevel elimDecl
76+ elabDecl' EAll recinfo elimDecl
69177 mapM_ elabPrim primitives
69278 -- Special case prim__believe_me because it doesn't work on just constants
69379 elabBelieveMe
@@ -748,71 +134,6 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
748134 idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i
749135 }
750136
751−
752−-- | Elaborate a type provider
753−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()
754−elabProvider info syn fc what n
755− = do i <- getIState
756− -- Ensure that the experimental extension is enabled
757− unless (TypeProviders `elem` idris_language_extensions i) $
758− ifail $ "Failed to define type provider \"" ++ show n ++
759− "\".\nYou must turn on the TypeProviders extension."
760−
761− ctxt <- getContext
762−
763− -- First elaborate the expected type (and check that it's a type)
764− -- The goal type for a postulate is always Type.
765− (ty', typ) <- case what of
766− ProvTerm ty p -> elabVal toplevel ERHS ty
767− ProvPostulate _ -> elabVal toplevel ERHS PType
768− unless (isTType typ) $
769− ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
770−
771− -- Elaborate the provider term to TT and check that the type matches
772− (e, et) <- case what of
773− ProvTerm _ tm -> elabVal toplevel ERHS tm
774− ProvPostulate tm -> elabVal toplevel ERHS tm
775− unless (isProviderOf (normalise ctxt [] ty') et) $
776− ifail $ "Expected provider type IO (Provider (" ++
777− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
778−
779− -- Execute the type provider and normalise the result
780− -- use 'run__provider' to convert to a primitive IO action
781−
782− rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
783− [Erased, e])
784− let rhs' = normalise ctxt [] rhs
785− logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
786−
787− -- Extract the provided term or postulate from the type provider
788− provided <- getProvided fc rhs'
789−
790− case provided of
791− Provide tm
792− | ProvTerm ty _ <- what ->
793− do -- Finally add a top-level definition of the provided term
794− elabType info syn emptyDocstring [] fc [] n ty
795− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
796− logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
797− | ProvPostulate _ <- what ->
798− do -- Add the postulate
799− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
800− logLvl 3 $ "Elaborated provided postulate " ++ show n
801− | otherwise ->
802− ierror . Msg $ "Attempted to provide a postulate where a term was expected."
803−
804− where isTType :: TT Name -> Bool
805− isTType (TType _) = True
806− isTType _ = False
807−
808− isProviderOf :: TT Name -> TT Name -> Bool
809− isProviderOf tp prov
810− | (P _ (UN io) _, [prov']) <- unApply prov
811− , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'
812− , tp == tp', io == txt "IO"
813− , prov == txt "Provider" && provs == txt "Providers" = True
814− isProviderOf _ _ = False
815−
816137elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
817138elabTransform info fc safe lhs_in rhs_in
818139 = do ctxt <- getContext
@@ -845,1518 +166,13 @@ elabTransform info fc safe lhs_in rhs_in
845166 addTrans (clhs_tm, crhs_tm)
846167 addIBC (IBCTrans (clhs_tm, crhs_tm))
847168
848−
849−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
850− PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
851−elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
852− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
853− -- TODO think: something more in info?
854− cty' <- implicit info syn cn cty_in
855− i <- getIState
856−
857− -- get bound implicits and propagate to setters (in case they
858− -- provide useful information for inference)
859− let extraImpls = getBoundImpls cty'
860−
861− cty <- case lookupTy cn (tt_ctxt i) of
862− [t] -> return (delab i t)
863− _ -> ifail "Something went inexplicably wrong"
864− cimp <- case lookupCtxt cn (idris_implicits i) of
865− [imps] -> return imps
866− ppos <- case lookupCtxt tyn (idris_datatypes i) of
867− [ti] -> return $ param_pos ti
868− let cty_imp = renameBs cimp cty
869− let ptys = getProjs [] cty_imp
870− let ptys_u = getProjs [] cty
871− let recty = getRecTy cty_imp
872− let recty_u = getRecTy cty
873−
874− let paramNames = getPNames recty ppos
875−
876− -- rename indices when we generate the getter/setter types, so
877− -- that they don't clash with the names of the projections
878− -- we're generating
879− let index_names_in = getRecNameMap "_in" ppos recty
880− let recty_in = substMatches index_names_in recty
881−
882− logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)
883− -- Substitute indices with projection functions, and parameters with
884− -- the updated parameter name
885− let substs = map (\ (n, _) ->
886− if n `elem` paramNames
887− then (n, PRef fc (mkp n))
888− else (n, PApp fc (PRef fc n)
889− [pexp (PRef fc rec)]))
890− ptys
891−
892− -- Generate projection functions
893− proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
894− logLvl 3 $ show proj_decls
895− let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
896− let implBinds = getImplB id cty'
897−
898− -- Generate update functions
899− update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls
900− (getFieldNames cty')
901− implBinds (length nonImp)) (zip nonImp [0..])
902− mapM_ (elabDecl EAll info) (concat proj_decls)
903− logLvl 3 $ show update_decls
904− mapM_ (tryElabDecl info) (update_decls)
905− where
906−-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
907−
908− isNonImp (PExp _ _ _ _, a) = Just a
909− isNonImp _ = Nothing
910−
911− getPNames (PApp _ _ as) ppos = getpn as ppos
912− where
913− getpn as [] = []
914− getpn as (i:is) | length as > i,
915− PRef _ n <- getTm (as!!i) = n : getpn as is
916− | otherwise = getpn as is
917− getPNames _ _ = []
918−
919− tryElabDecl info (fn, ty, val)
920− = do i <- getIState
921− idrisCatch (do elabDecl' EAll info ty
922− elabDecl' EAll info val)
923− (\v -> do iputStrLn $ show fc ++
924− ":Warning - can't generate setter for " ++
925− show fn ++ " (" ++ show ty ++ ")"
926−-- ++ "\n" ++ pshow i v
927− putIState i)
928−
929− getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
930− getBoundImpls _ = []
931−
932− getImplB k (PPi (Imp l s _) n Placeholder sc)
933− = getImplB k sc
934− getImplB k (PPi (Imp l s p) n ty sc)
935− = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc
936− getImplB k (PPi _ n ty sc)
937− = getImplB k sc
938− getImplB k _ = k
939−
940− renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
941− = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
942− renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
943− renameBs _ t = t
944−
945− getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
946− getProjs acc r = reverse acc
947−
948− getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
949− getFieldNames (PPi _ _ _ s) = getFieldNames s
950− getFieldNames _ = []
951−
952− getRecTy (PPi _ n ty s) = getRecTy s
953− getRecTy t = t
954−
955− -- make sure we pick a consistent name for parameters; any name will do
956− -- otherwise
957− getRecNameMap x ppos (PApp fc t args)
958− = mapMaybe toMN (zip [0..] (map getTm args))
959− where
960− toMN (i, PRef fc n)
961− | i `elem` ppos = Just (n, PRef fc (mkp n))
962− | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))
963− toMN _ = Nothing
964− getRecNameMap x _ _ = []
965−
966− rec = sMN 0 "rec"
967−
968− -- only UNs propagate properly as parameters (bit of a hack then...)
969− mkp (UN n) = sUN ("_p_" ++ str n)
970− mkp (MN i n) = sMN i ("p_" ++ str n)
971− mkp (NS n s) = NS (mkp n) s
972−
973− mkImp (UN n) = sUN ("implicit_" ++ str n)
974− mkImp (MN i n) = sMN i ("implicit_" ++ str n)
975− mkImp (NS n s) = NS (mkImp n) s
976−
977− mkType (UN n) = sUN ("set_" ++ str n)
978− mkType (MN i n) = sMN i ("set_" ++ str n)
979− mkType (NS n s) = NS (mkType n) s
980−
981− mkProj recty substs cimp ((pn_in, pty), pos)
982− = do let pn = expandNS syn pn_in -- projection name
983− -- use pn_in in the indices, consistently, to avoid clash
984− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
985− (PPi expl rec recty
986− (substMatches substs pty))
987− let pls = repeat Placeholder
988− let before = pos
989− let after = length substs - (pos + 1)
990− let args = take before pls ++ PRef fc (mkp pn_in) : take after pls
991− let iargs = map implicitise (zip cimp args)
992− let lhs = PApp fc (PRef fc pn)
993− [pexp (PApp fc (PRef fc cn) iargs)]
994− let rhs = PRef fc (mkp pn_in)
995− let pclause = PClause fc pn lhs [] rhs []
996− return [pfnTy, PClauses fc [] pn [pclause]]
997−
998− implicitise (pa, t) = pa { getTm = t }
999−
1000− -- If the 'pty' we're updating includes anything in 'substs', we're
1001− -- updating the type as well, so use recty', otherwise just use
1002− -- recty
1003− mkUpdate recty inames extras fnames k num ((pn, pty), pos)
1004− = do let setname = expandNS syn $ mkType pn
1005− let valname = sMN 0 "updateval"
1006− let pn_out = sMN 0 (show pn ++ "_out")
1007− let pn_in = sMN 0 (show pn ++ "_in")
1008− let recty_in = substMatches [(pn, PRef fc pn_in)] recty
1009− let recty_out = substMatches [(pn, PRef fc pn_out)] recty
1010− let pt = substMatches inames $
1011− k (implBindUp extras inames (PPi expl pn_out pty
1012− (PPi expl rec recty_in recty_out)))
1013− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
1014−-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
1015− let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
1016− let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames
1017− let lhsArgs = pls
1018− let rhsArgs = take pos pls ++ (PRef fc valname) :
1019− drop (pos + 1) pls
1020− let before = pos
1021− let pclause = PClause fc setname (PApp fc (PRef fc setname)
1022− [pexp (PRef fc valname),
1023− pexp (PApp fc (PRef fc cn)
1024− (map pexp lhsArgs))])
1025− []
1026− (PApp fc (PRef fc cn)
1027− (map pexp rhsArgs)) []
1028− return (pn, pfnTy, PClauses fc [] setname [pclause])
1029−
1030− implBindUp [] is t = t
1031− implBindUp ((n, ty):ns) is t
1032− = let n' = case lookup n is of
1033− Just (PRef _ x) -> x
1034− _ -> n in
1035− if n `elem` allNamesIn t
1036− then PPi impl n' ty (implBindUp ns is t)
1037− else implBindUp ns is t
1038−
1039−-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
1040−-- top-level definition.
1041−elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
1042−elabClauses info fc opts n_in cs = let n = liftname info n_in in
1043− do ctxt <- getContext
1044− ist <- getIState
1045− inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
1046−
1047− -- Check n actually exists, with no definition yet
1048− let tys = lookupTy n ctxt
1049− let reflect = Reflection `elem` opts
1050− checkUndefined n ctxt
1051− unless (length tys > 1) $ do
1052− fty <- case tys of
1053− [] -> -- TODO: turn into a CAF if there's no arguments
1054− -- question: CAFs in where blocks?
1055− tclift $ tfail $ At fc (NoTypeDecl n)
1056− [ty] -> return ty
1057− let atys = map snd (getArgTys fty)
1058− cs_elab <- mapM (elabClause info opts)
1059− (zip [0..] cs)
1060− let (pats_in, cs_full) = unzip cs_elab
1061−
1062− logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
1063−
1064− solveDeferred n
1065−
1066− -- just ensure that the structure exists
1067− fmodifyState (ist_optimisation n) id
1068− addIBC (IBCOpt n)
1069−
1070− ist <- getIState
1071− let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
1072−
1073− -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
1074− -- show l ++ " = " ++
1075− -- show r) pats))
1076− let tcase = opt_typecase (idris_options ist)
1077−
1078− -- Summary of what's about to happen: Definitions go:
1079− --
1080− -- pats_in -> pats -> pdef -> pdef'
1081−
1082− -- addCaseDef builds case trees from <pdef> and <pdef'>
1083−
1084− -- pdef is the compile-time pattern definition.
1085− -- This will get further optimised for run-time, and, separately,
1086− -- further inlined to help with totality checking.
1087− let pdef = map debind pats
1088−
1089− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats
1090− logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef
1091−
1092− -- Look for 'static' names and generate new specialised
1093− -- definitions for them
1094−
1095− mapM_ (\ e -> case e of
1096− Left _ -> return ()
1097− Right (l, r) -> elabPE info fc n r) pats
1098−
1099− -- NOTE: Need to store original definition so that proofs which
1100− -- rely on its structure aren't affected by any changes to the
1101− -- inliner. Just use the inlined version to generate pdef' and to
1102− -- help with later inlinings.
1103−
1104− ist <- getIState
1105− let pdef_inl = inlineDef ist pdef
1106−
1107− numArgs <- tclift $ sameLength pdef
1108−
1109− case specNames opts of
1110− Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
1111− _ -> return ()
1112−
1113− erInfo <- getErasureInfo <$> getIState
1114− tree@(CaseDef scargs sc _) <- tclift $
1115− simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo
1116− cov <- coverage
1117− pmissing <-
1118− if cov && not (hasDefault cs)
1119− then do missing <- genClauses fc n (map getLHS pdef) cs_full
1120− -- missing <- genMissing n scargs sc
1121− missing' <- filterM (checkPossible info fc True n) missing
1122− let clhs = map getLHS pdef
1123− logLvl 2 $ "Must be unreachable:\n" ++
1124− showSep "\n" (map showTmImpls missing') ++
1125− "\nAgainst: " ++
1126− showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
1127− -- filter out anything in missing' which is
1128− -- matched by any of clhs. This might happen since
1129− -- unification may force a variable to take a
1130− -- particular form, rather than force a case
1131− -- to be impossible.
1132− return (filter (noMatch ist clhs) missing')
1133− else return []
1134− let pcover = null pmissing
1135−
1136− -- pdef' is the version that gets compiled for run-time
1137− pdef_in' <- applyOpts pdef
1138− let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1139−
1140− logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
1141−
1142− ist <- getIState
1143− -- let wf = wellFounded ist n sc
1144− let tot = if pcover || AssertTotal `elem` opts
1145− then Unchecked -- finish checking later
1146− else Partial NotCovering -- already know it's not total
1147−
1148− -- case lookupCtxt (namespace info) n (idris_flags ist) of
1149− -- [fs] -> if TotalFn `elem` fs
1150− -- then case tot of
1151− -- Total _ -> return ()
1152− -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
1153− -- else return ()
1154− -- _ -> return ()
1155− case tree of
1156− CaseDef _ _ [] -> return ()
1157− CaseDef _ _ xs -> mapM_ (\x ->
1158− iputStrLn $ show fc ++
1159− ":warning - Unreachable case: " ++
1160− show (delab ist x)) xs
1161− let knowncovering = (pcover && cov) || AssertTotal `elem` opts
1162−
1163− tree' <- tclift $ simpleCase tcase knowncovering reflect
1164− RunTime fc inacc atys pdef' erInfo
1165− logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
1166− logLvl 3 $ "Optimised: " ++ show tree'
1167− ctxt <- getContext
1168− ist <- getIState
1169− let opt = idris_optimisation ist
1170− putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
1171− (idris_patdefs ist) })
1172− let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
1173− case lookupTy n ctxt of
1174− [ty] -> do updateContext (addCasedef n erInfo caseInfo
1175− tcase knowncovering
1176− reflect
1177− (AssertTotal `elem` opts)
1178− atys
1179− inacc
1180− pats
1181− pdef pdef pdef_inl pdef' ty)
1182− addIBC (IBCDef n)
1183− setTotality n tot
1184− when (not reflect) $ do totcheck (fc, n)
1185− defer_totcheck (fc, n)
1186− when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
1187− i <- getIState
1188− case lookupDef n (tt_ctxt i) of
1189− (CaseOp _ _ _ _ _ cd : _) ->
1190− let (scargs, sc) = cases_compiletime cd
1191− (scargs', sc') = cases_runtime cd in
1192− do let calls = findCalls sc' scargs'
1193− let used = findUsedArgs sc' scargs'
1194− -- let scg = buildSCG i sc scargs
1195− -- add SCG later, when checking totality
1196− let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore
1197− logLvl 2 $ "Called names: " ++ show cg
1198− addToCG n cg
1199− addToCalledG n (nub (map fst calls)) -- plus names in type!
1200− addIBC (IBCCG n)
1201− _ -> return ()
1202− return ()
1203− -- addIBC (IBCTotal n tot)
1204− [] -> return ()
1205− -- Check it's covering, if 'covering' option is used. Chase
1206− -- all called functions, and fail if any of them are also
1207− -- 'Partial NotCovering'
1208− when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
1209− where
1210− noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
1211− Right _ -> False
1212− Left miss -> True) cs
1213−
1214− checkUndefined n ctxt = case lookupDef n ctxt of
1215− [] -> return ()
1216− [TyDecl _ _] -> return ()
1217− _ -> tclift $ tfail (At fc (AlreadyDefined n))
1218−
1219− debind (Right (x, y)) = let (vs, x') = depat [] x
1220− (_, y') = depat [] y in
1221− (vs, x', y')
1222− debind (Left x) = let (vs, x') = depat [] x in
1223− (vs, x', Impossible)
1224−
1225− depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1226− depat acc x = (acc, x)
1227−
1228− hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1229− , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1230− hasDefault _ = False
1231−
1232− getLHS (_, l, _) = l
1233−
1234− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
1235− force (normalisePats ctxt [] y))
1236− simple_lhs ctxt t = t
1237−
1238− simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p
1239− (rt_simplify ctxt [] y)))
1240−
1241− -- this is so pattern types are in the right form for erasure
1242− normalisePats ctxt env (Bind n (PVar t) sc)
1243− = let t' = normalise ctxt env t in
1244− Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)
1245− normalisePats ctxt env (Bind n (PVTy t) sc)
1246− = let t' = normalise ctxt env t in
1247− Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)
1248− normalisePats ctxt env t = t
1249−
1250− specNames [] = Nothing
1251− specNames (Specialise ns : _) = Just ns
1252− specNames (_ : xs) = specNames xs
1253−
1254− sameLength ((_, x, _) : xs)
1255− = do l <- sameLength xs
1256− let (f, as) = unApply x
1257− if (null xs || l == length as) then return (length as)
1258− else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
1259− sameLength [] = return 0
1260−
1261− -- apply all transformations (just specialisation for now, add
1262− -- user defined transformation rules later)
1263− doTransforms ist pats =
1264− case specNames opts of
1265− Nothing -> pats
1266− Just ns -> partial_eval (tt_ctxt ist) ns pats
1267−
1268−-- | Find 'static' applications in a term and partially evaluate them
1269−elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()
1270−elabPE info fc caller r =
1271− do ist <- getIState
1272− let sa = getSpecApps ist [] r
1273− mapM_ (mkSpecialised ist) sa
1274− where
1275− -- TODO: Add a PTerm level transformation rule, which is basically the
1276− -- new definition in reverse (before specialising it).
1277− -- RHS => LHS where implicit arguments are left blank in the
1278− -- transformation.
1279−
1280− -- Apply that transformation after every PClauses elaboration
1281−
1282− mkSpecialised ist specapp_in = do
1283− let (specTy, specapp) = getSpecTy ist specapp_in
1284− let (n, newnm, pats) = getSpecClause ist specapp
1285− let undef = case lookupDef newnm (tt_ctxt ist) of
1286− [] -> True
1287− _ -> False
1288− logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))
1289− idrisCatch
1290− (when (undef && all (concreteArg ist) (snd specapp)) $ do
1291− cgns <- getAllNames n
1292− let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++
1293− mapMaybe specName (snd specapp))]
1294− logLvl 3 $ "Specialising application: " ++ show specapp
1295− logLvl 2 $ "New name: " ++ show newnm
1296− iLOG $ "PE definition type : " ++ (show specTy)
1297− ++ "\n" ++ show opts
1298− logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1299− showSep "\n"
1300− (map (\ (lhs, rhs) ->
1301− (showTmImpls lhs ++ " = " ++
1302− showTmImpls rhs)) pats)
1303− elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
1304− let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1305− elabClauses info fc opts newnm def
1306− logLvl 2 $ "Specialised " ++ show newnm)
1307− -- if it doesn't work, just don't specialise. Could happen for lots
1308− -- of valid reasons (e.g. local variables in scope which can't be
1309− -- lifted out).
1310− (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))
1311−
1312− specName (ImplicitS, tm)
1313− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)
1314− specName (ExplicitS, tm)
1315− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)
1316− specName _ = Nothing
1317−
1318− concreteArg ist (ImplicitS, tm) = concreteTm ist tm
1319− concreteArg ist (ExplicitS, tm) = concreteTm ist tm
1320− concreteArg ist _ = True
1321−
1322− concreteTm ist tm | (P _ n _, _) <- unApply tm =
1323− case lookupTy n (tt_ctxt ist) of
1324− [] -> False
1325− _ -> True
1326− concreteTm ist (Constant _) = True
1327− concreteTm ist _ = False
1328−
1329− -- get the type of a specialised application
1330− getSpecTy ist (n, args)
1331− = case lookupTy n (tt_ctxt ist) of
1332− [ty] -> let (specty_in, args') = specType args (explicitNames ty)
1333− specty = normalise (tt_ctxt ist) [] (finalise specty_in)
1334− t = mkPE_TyDecl ist args' (explicitNames specty) in
1335− (t, (n, args'))
1336−-- (normalise (tt_ctxt ist) [] (specType args ty))
1337− _ -> error "Can't happen (getSpecTy)"
1338−
1339− -- get the clause of a specialised application
1340− getSpecClause ist (n, args)
1341− = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++
1342− showSep "_" (map showArg args)) in
1343− -- UN (show n ++ show (map snd args)) in
1344− (n, newnm, mkPE_TermDecl ist newnm n args)
1345− where showArg (ExplicitS, n) = show n
1346− showArg (ImplicitS, n) = show n
1347− showArg _ = ""
1348−
1349−
1350−-- Elaborate a value, returning any new bindings created (this will only
1351−-- happen if elaborating as a pattern clause)
1352−elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
1353−elabValBind info aspat norm tm_in
1354− = do ctxt <- getContext
1355− i <- getIState
1356− let tm = addImpl i tm_in
1357− logLvl 10 (showTmImpls tm)
1358− -- try:
1359− -- * ordinary elaboration
1360− -- * elaboration as a Type
1361− -- * elaboration as a function a -> b
1362−
1363− ((tm', defer, is), _) <-
1364−-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
1365−-- (build i info aspat (MN 0 "val") tm))
1366− tclift (elaborate ctxt (sMN 0 "val") infP []
1367− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
1368− let vtm = orderPats (getInferTerm tm')
1369−
1370− def' <- checkDef (fileFC "(input)") defer
1371− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
1372− addDeferred def''
1373− mapM_ (elabCaseBlock info []) is
1374−
1375− logLvl 3 ("Value: " ++ show vtm)
1376−-- recheckC (fileFC "(input)") [] tm'
1377−-- logLvl 2 (show vtm)
1378− (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
1379−
1380− let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
1381− else vtm_in
1382− let bargs = getPBtys vtm
1383−
1384− return (vtm, vty, bargs)
1385−
1386−elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
1387−elabVal info aspat tm_in
1388− = do (tm, ty, _) <- elabValBind info aspat False tm_in
1389− return (tm, ty)
1390−
1391−-- checks if the clause is a possible left hand side. Returns the term if
1392−-- possible, otherwise Nothing.
1393−
1394−checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool
1395−checkPossible info fc tcgen fname lhs_in
1396− = do ctxt <- getContext
1397− i <- getIState
1398− let lhs = addImplPat i lhs_in
1399− -- if the LHS type checks, it is possible
1400− case elaborate ctxt (sMN 0 "patLHS") infP []
1401− (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of
1402− OK ((lhs', _, _), _) ->
1403− do let lhs_tm = orderPats (getInferTerm lhs')
1404− case recheck ctxt [] (forget lhs_tm) lhs_tm of
1405− OK _ -> return True
1406− err -> return False
1407− -- if it's a recoverable error, the case may become possible
1408− Error err -> if tcgen then return (recoverable ctxt err)
1409− else return (validCase ctxt err ||
1410− recoverable ctxt err)
1411− where validCase ctxt (CantUnify _ topx topy e _ _)
1412− = let topx' = normalise ctxt [] topx
1413− topy' = normalise ctxt [] topy in
1414− not (sameFam topx' topy' || not (validCase ctxt e))
1415− validCase ctxt (CantConvert _ _ _) = False
1416− validCase ctxt (At _ e) = validCase ctxt e
1417− validCase ctxt (Elaborating _ _ e) = validCase ctxt e
1418− validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
1419− validCase ctxt _ = True
1420−
1421− recoverable ctxt (CantUnify r topx topy e _ _)
1422− = let topx' = normalise ctxt [] topx
1423− topy' = normalise ctxt [] topy in
1424− checkRec topx' topy'
1425− recoverable ctxt (At _ e) = recoverable ctxt e
1426− recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e
1427− recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e
1428− recoverable _ _ = False
1429−
1430− sameFam topx topy
1431− = case (unApply topx, unApply topy) of
1432− ((P _ x _, _), (P _ y _, _)) -> x == y
1433− _ -> False
1434−
1435− -- different notion of recoverable than in unification, since we
1436− -- have no metavars -- just looking to see if a constructor is failing
1437− -- to unify with a function that may be reduced later
1438−
1439− checkRec (App f a) p@(P _ _ _) = checkRec f p
1440− checkRec p@(P _ _ _) (App f a) = checkRec p f
1441− checkRec fa@(App _ _) fa'@(App _ _)
1442− | (f, as) <- unApply fa,
1443− (f', as') <- unApply fa'
1444− = if (length as /= length as')
1445− then checkRec f f'
1446− else checkRec f f' && and (zipWith checkRec as as')
1447− checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
1448− checkRec _ _ = False
1449−
1450− ntRec x y | Ref <- x = True
1451− | Ref <- y = True
1452− | otherwise = False -- name is different, unrecoverable
1453−
1454−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1455− = nub $ getFixedInType i env [] t ++
1456− getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1457−getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1458− = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1459−getFixedInType i env is tm@(App f a)
1460− | (P _ tn _, args) <- unApply tm
1461− = case lookupCtxt tn (idris_datatypes i) of
1462− [t] -> nub $ paramNames args env (param_pos t) ++
1463− getFixedInType i env is f ++
1464− getFixedInType i env is a
1465− [] -> nub $ getFixedInType i env is f ++
1466− getFixedInType i env is a
1467− | otherwise = nub $ getFixedInType i env is f ++
1468− getFixedInType i env is a
1469−getFixedInType i _ _ _ = []
1470−
1471−getFlexInType i env ps (Bind n (Pi t) sc)
1472− = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
1473− getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
1474−getFlexInType i env ps tm@(App f a)
1475− | (P _ tn _, args) <- unApply tm
1476− = case lookupCtxt tn (idris_datatypes i) of
1477− [t] -> nub $ paramNames args env [x | x <- [0..length args],
1478− not (x `elem` param_pos t)]
1479− ++ getFlexInType i env ps f ++
1480− getFlexInType i env ps a
1481− [] -> nub $ getFlexInType i env ps f ++
1482− getFlexInType i env ps a
1483− | otherwise = nub $ getFlexInType i env ps f ++
1484− getFlexInType i env ps a
1485−getFlexInType i _ _ _ = []
1486−
1487−-- Treat a name as a parameter if it appears in parameter positions in
1488−-- types, and never in a non-parameter position in a (non-param) argument type.
1489−
1490−getParamsInType i env ps t = let fix = getFixedInType i env ps t
1491− flex = getFlexInType i env fix t in
1492− [x | x <- fix, not (x `elem` flex)]
1493−
1494−paramNames args env [] = []
1495−paramNames args env (p : ps)
1496− | length args > p = case args!!p of
1497− P _ n _ -> if n `elem` env
1498− then n : paramNames args env ps
1499− else paramNames args env ps
1500− _ -> paramNames args env ps
1501− | otherwise = paramNames args env ps
1502−
1503−propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm
1504−propagateParams i ps t tm@(PApp _ (PRef fc n) args)
1505− = PApp fc (PRef fc n) (addP t args)
1506− where addP (Bind n _ sc) (t : ts)
1507− | Placeholder <- getTm t,
1508− n `elem` ps,
1509− not (n `elem` allNamesIn tm)
1510− = t { getTm = PRef fc n } : addP sc ts
1511− addP (Bind n _ sc) (t : ts) = t : addP sc ts
1512− addP _ ts = ts
1513−propagateParams i ps t (PRef fc n)
1514− = case lookupCtxt n (idris_implicits i) of
1515− [is] -> let ps' = filter (isImplicit is) ps in
1516− PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')
1517− _ -> PRef fc n
1518− where isImplicit [] n = False
1519− isImplicit (PImp _ _ _ x _ : is) n | x == n = True
1520− isImplicit (_ : is) n = isImplicit is n
1521−propagateParams i ps t x = x
1522−
1523−-- Return the elaborated LHS/RHS, and the original LHS with implicits added
1524−elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1525− Idris (Either Term (Term, Term), PTerm)
1526−elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1527− = do let tcgen = Dictionary `elem` opts
1528− i <- get
1529− let lhs = addImpl i lhs_in
1530− b <- checkPossible info fc tcgen fname lhs_in
1531− case b of
1532− True -> tclift $ tfail (At fc
1533− (Msg $ show lhs_in ++ " is a valid case"))
1534− False -> do ptm <- mkPatTm lhs_in
1535− return (Left ptm, lhs)
1536−elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1537− = do let tcgen = Dictionary `elem` opts
1538− ctxt <- getContext
1539−
1540− -- Build the LHS as an "Infer", and pull out its type and
1541− -- pattern bindings
1542− i <- getIState
1543− inf <- isTyInferred fname
1544− -- get the parameters first, to pass through to any where block
1545− let fn_ty = case lookupTy fname (tt_ctxt i) of
1546− [t] -> t
1547− _ -> error "Can't happen (elabClause function type)"
1548− let fn_is = case lookupCtxt fname (idris_implicits i) of
1549− [t] -> t
1550− _ -> []
1551− let params = getParamsInType i [] fn_is fn_ty
1552− let lhs = mkLHSapp $ stripUnmatchable i $
1553− propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))
1554− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
1555− logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
1556− "\n" ++ show (fn_ty, fn_is))
1557−
1558− (((lhs', dlhs, []), probs, inj), _) <-
1559− tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1560− (do res <- errAt "left hand side of " fname
1561− (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))
1562− probs <- get_probs
1563− inj <- get_inj
1564− return (res, probs, inj))
1565−
1566− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1567−
1568− let lhs_tm = orderPats (getInferTerm lhs')
1569− let lhs_ty = getInferType lhs'
1570− logLvl 3 ("Elaborated: " ++ show lhs_tm)
1571− logLvl 3 ("Elaborated type: " ++ show lhs_ty)
1572− logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)
1573−
1574− -- If we're inferring metavariables in the type, don't recheck,
1575− -- because we're only doing this to try to work out those metavariables
1576− (clhs_c, clhsty) <- if not inf
1577− then recheckC fc [] lhs_tm
1578− else return (lhs_tm, lhs_ty)
1579− let clhs = normalise ctxt [] clhs_c
1580−
1581− logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
1582−
1583− rep <- useREPL
1584− when rep $ do
1585− addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
1586− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
1587−
1588− logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
1589− -- Elaborate where block
1590− ist <- getIState
1591− windex <- getName
1592− let decls = nub (concatMap declared whereblock)
1593− let defs = nub (decls ++ concatMap defined whereblock)
1594− let newargs = pvars ist lhs_tm
1595− let winfo = pinfo info newargs defs windex
1596− let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1597−
1598− -- Split the where block into declarations with a type, and those
1599− -- without
1600− -- Elaborate those with a type *before* RHS, those without *after*
1601− let (wbefore, wafter) = sepBlocks wb
1602−
1603− logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1604− mapM_ (elabDecl' EAll winfo) wbefore
1605− -- Now build the RHS, using the type of the LHS as the goal.
1606− i <- getIState -- new implicits from where block
1607− logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1608− let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
1609− (expandParams decorate newargs defs (defs \\ decls) rhs_in)
1610− logLvl 2 $ "RHS: " ++ showTmImpls rhs
1611− ctxt <- getContext -- new context with where block added
1612− logLvl 5 "STARTING CHECK"
1613− ((rhs', defer, is, probs), _) <-
1614− tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
1615− (do pbinds ist lhs_tm
1616− mapM_ setinj (nub (params ++ inj))
1617− setNextName
1618− (_, _, is) <- errAt "right hand side of " fname
1619− (erun fc (build i winfo ERHS opts fname rhs))
1620− errAt "right hand side of " fname
1621− (erun fc $ psolve lhs_tm)
1622− hs <- get_holes
1623− aux <- getAux
1624− mapM_ (elabCaseHole aux) hs
1625− tt <- get_term
1626− let (tm, ds) = runState (collectDeferred (Just fname) tt) []
1627− probs <- get_probs
1628− return (tm, ds, is, probs))
1629−
1630− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1631−
1632− logLvl 5 "DONE CHECK"
1633− logLvl 2 $ "---> " ++ show rhs'
1634− when (not (null defer)) $ iLOG $ "DEFERRED " ++
1635− show (map (\ (n, (_,_,t)) -> (n, t)) defer)
1636− def' <- checkDef fc defer
1637− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1638− addDeferred def''
1639− mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
1640−
1641− when (not (null def')) $ do
1642− mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
1643−
1644− -- Now the remaining deferred (i.e. no type declarations) clauses
1645− -- from the where block
1646−
1647− mapM_ (elabDecl' EAll winfo) wafter
1648− mapM_ (elabCaseBlock winfo opts) is
1649−
1650− ctxt <- getContext
1651− logLvl 5 $ "Rechecking"
1652− logLvl 6 $ " ==> " ++ show (forget rhs')
1653− (crhs, crhsty) <- if not inf
1654− then recheckC fc [] rhs'
1655− else return (rhs', clhsty)
1656− logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
1657− case converts ctxt [] clhsty crhsty of
1658− OK _ -> return ()
1659− Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
1660− i <- getIState
1661− checkInferred fc (delab' i crhs True True) rhs
1662− -- if the function is declared '%error_reverse', or its type,
1663− -- then we'll try running it in reverse to improve error messages
1664− let (ret_fam, _) = unApply (getRetTy crhsty)
1665− rev <- case ret_fam of
1666− P _ rfamn _ ->
1667− case lookupCtxt rfamn (idris_datatypes i) of
1668− [TI _ _ dopts _ _] ->
1669− return (DataErrRev `elem` dopts)
1670− _ -> return False
1671− _ -> return False
1672−
1673− when (rev || ErrorReverse `elem` opts) $ do
1674− addIBC (IBCErrRev (crhs, clhs))
1675− addErrRev (crhs, clhs)
1676− return $ (Right (clhs, crhs), lhs)
1677− where
1678− pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
1679− pinfo info ns ds i
1680− = let newps = params info ++ ns
1681− dsParams = map (\n -> (n, map fst newps)) ds
1682− newb = addAlist dsParams (inblock info)
1683− l = liftname info in
1684− info { params = newps,
1685− inblock = newb,
1686− liftname = id -- (\n -> case lookupCtxt n newb of
1687− -- Nothing -> n
1688− -- _ -> MN i (show n)) . l
1689− }
1690−
1691− mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1692− mkLHSapp t = t
1693−
1694− decorate (NS x ns)
1695− = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
1696−-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
1697− decorate x
1698− = SN (WhereN cnum fname x)
1699−-- = NS (SN (WhereN cnum fname x)) [show cnum]
1700−-- = NS (UN ('#':show x)) [show cnum, show fname]
1701−
1702− sepBlocks bs = sepBlocks' [] bs where
1703− sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)
1704− = let (bf, af) = sepBlocks' (n : ns) bs in
1705− (d : bf, af)
1706− sepBlocks' ns (d@(PClauses _ _ n _) : bs)
1707− | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
1708− (bf, d : af)
1709− sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
1710− (b : bf, af)
1711− sepBlocks' ns [] = ([], [])
1712−
1713−
1714− -- if a hole is just an argument/result of a case block, treat it as
1715− -- the unit type. Hack to help elaborate case in do blocks.
1716− elabCaseHole aux h = do
1717− focus h
1718− g <- goal
1719− case g of
1720− TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve
1721− _ -> return ()
1722−
1723− -- Is the name a pattern argument in the declaration
1724− isArg :: Name -> PDecl -> Bool
1725− isArg n (PClauses _ _ _ cs) = any isArg' cs
1726− where
1727− isArg' (PClause _ _ (PApp _ _ args) _ _ _)
1728− = any (\x -> case x of
1729− PRef _ n' -> n == n'
1730− _ -> False) (map getTm args)
1731− isArg' _ = False
1732− isArg _ _ = False
1733−
1734−elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1735− = do let tcgen = Dictionary `elem` opts
1736− ctxt <- getContext
1737− -- Build the LHS as an "Infer", and pull out its type and
1738− -- pattern bindings
1739− i <- getIState
1740− -- get the parameters first, to pass through to any where block
1741− let fn_ty = case lookupTy fname (tt_ctxt i) of
1742− [t] -> t
1743− _ -> error "Can't happen (elabClause function type)"
1744− let fn_is = case lookupCtxt fname (idris_implicits i) of
1745− [t] -> t
1746− _ -> []
1747− let params = getParamsInType i [] fn_is fn_ty
1748− let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))
1749− logLvl 2 ("LHS: " ++ show lhs)
1750− ((lhs', dlhs, []), _) <-
1751− tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
1752− (errAt "left hand side of with in " fname
1753− (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )
1754− let lhs_tm = orderPats (getInferTerm lhs')
1755− let lhs_ty = getInferType lhs'
1756− let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
1757− logLvl 3 (show lhs_tm)
1758− (clhs, clhsty) <- recheckC fc [] lhs_tm
1759− logLvl 5 ("Checked " ++ show clhs)
1760− let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
1761− let wval = addImplBound i (map fst bargs) wval_in
1762− logLvl 5 ("Checking " ++ showTmImpls wval)
1763− -- Elaborate wval in this context
1764− ((wval', defer, is), _) <-
1765− tclift $ elaborate ctxt (sMN 0 "withRHS")
1766− (bindTyArgs PVTy bargs infP) []
1767− (do pbinds i lhs_tm
1768− setNextName
1769− -- TODO: may want where here - see winfo abpve
1770− (_', d, is) <- errAt "with value in " fname
1771− (erun fc (build i info ERHS opts fname (infTerm wval)))
1772− erun fc $ psolve lhs_tm
1773− tt <- get_term
1774− return (tt, d, is))
1775− def' <- checkDef fc defer
1776− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1777− addDeferred def''
1778− mapM_ (elabCaseBlock info opts) is
1779− logLvl 5 ("Checked wval " ++ show wval')
1780− (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
1781− let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1782− let cwvalN = explicitNames (normalise ctxt [] cwval)
1783− logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
1784− let pvars = map fst (getPBtys cwvalty)
1785− -- we need the unelaborated term to get the names it depends on
1786− -- rather than a de Bruijn index.
1787− let pdeps = usedNamesIn pvars i (delab i cwvalty)
1788− let (bargs_pre, bargs_post) = split pdeps bargs []
1789− logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
1790− " depends on " ++ show pdeps ++ " from " ++ show pvars)
1791− logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
1792− windex <- getName
1793− -- build a type declaration for the new function:
1794− -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
1795− let wargval = getRetTy cwvalN
1796− let wargtype = getRetTy cwvaltyN
1797− logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)
1798− let wtype = bindTyArgs Pi (bargs_pre ++
1799− (sMN 0 "warg", wargtype) :
1800− map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)
1801− (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)
1802− logLvl 5 ("New function type " ++ show wtype)
1803− let wname = sMN windex (show fname)
1804−
1805− let imps = getImps wtype -- add to implicits context
1806− putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
1807− addIBC (IBCDef wname)
1808− def' <- checkDef fc [(wname, (-1, Nothing, wtype))]
1809− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1810− addDeferred def''
1811−
1812− -- in the subdecls, lhs becomes:
1813− -- fname pats | wpat [rest]
1814− -- ==> fname' ps wpat [rest], match pats against toplevel for ps
1815− wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))
1816− withblock
1817− logLvl 3 ("with block " ++ show wb)
1818− -- propagate totality assertion to the new definitions
1819− when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]
1820− mapM_ (elabDecl EAll info) wb
1821−
1822− -- rhs becomes: fname' ps wval
1823− let rhs = PApp fc (PRef fc wname)
1824− (map (pexp . (PRef fc) . fst) bargs_pre ++
1825− pexp wval :
1826− (map (pexp . (PRef fc) . fst) bargs_post))
1827− logLvl 5 ("New RHS " ++ showTmImpls rhs)
1828− ctxt <- getContext -- New context with block added
1829− i <- getIState
1830− ((rhs', defer, is), _) <-
1831− tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []
1832− (do pbinds i lhs_tm
1833− setNextName
1834− (_, d, is) <- erun fc (build i info ERHS opts fname rhs)
1835− psolve lhs_tm
1836− tt <- get_term
1837− return (tt, d, is))
1838− def' <- checkDef fc defer
1839− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1840− addDeferred def''
1841− mapM_ (elabCaseBlock info opts) is
1842− logLvl 5 ("Checked RHS " ++ show rhs')
1843− (crhs, crhsty) <- recheckC fc [] rhs'
1844− return $ (Right (clhs, crhs), lhs)
1845− where
1846− getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
1847− getImps _ = []
1848−
1849− mkAuxC wname lhs ns ns' (PClauses fc o n cs)
1850− | True = do cs' <- mapM (mkAux wname lhs ns ns') cs
1851− return $ PClauses fc o wname cs'
1852− | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n
1853− mkAuxC wname lhs ns ns' d = return $ d
1854−
1855− mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
1856− = do i <- getIState
1857− let tm = addImplPat i tm_in
1858− logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1859− showTmImpls toplhs)
1860− case matchClause i toplhs tm of
1861− Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"
1862− Right mvars ->
1863− do logLvl 3 ("Match vars : " ++ show mvars)
1864− lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1865− return $ PClause fc wname lhs ws rhs wheres
1866− mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
1867− = do i <- getIState
1868− let tm = addImplPat i tm_in
1869− logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1870− showTmImpls toplhs)
1871− withs' <- mapM (mkAuxC wname toplhs ns ns') withs
1872− case matchClause i toplhs tm of
1873− Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
1874− Right mvars ->
1875− do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
1876− return $ PWith fc wname lhs ws wval withs'
1877− mkAux wname toplhs ns ns' c
1878− = ifail $ show fc ++ ":badly formed with clause"
1879−
1880− addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
1881− addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]
1882−
1883− updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w
1884− = let ns = map (keepMvar (map fst mvars) fc') ns_in
1885− ns' = map (keepMvar (map fst mvars) fc') ns_in' in
1886− return $ substMatches mvars $
1887− PApp fc (PRef fc' wname)
1888− (map pexp ns ++ pexp w : (map pexp ns'))
1889− updateLHS n wname mvars ns_in ns_in' tm w
1890− = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w
1891−
1892− keepMvar mvs fc v | v `elem` mvs = PRef fc v
1893− | otherwise = Placeholder
1894−
1895− fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1896− fullApp x = x
1897−
1898− split [] rest pre = (reverse pre, rest)
1899− split deps ((n, ty) : rest) pre
1900− | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
1901− | otherwise = split deps rest ((n, ty) : pre)
1902− split deps [] pre = (reverse pre, [])
1903−
1904− abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
1905−
1906−data MArgTy = IA | EA | CA deriving Show
1907−
1908−elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
1909− FC -> [PTerm] ->
1910− Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()
1911−elabClass info syn_in doc fc constraints tn ps pDocs ds
1912− = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
1913− let tty = pibind ps PType
1914− let constraint = PApp fc (PRef fc tn)
1915− (map (pexp . PRef fc) (map fst ps))
1916−
1917− let syn = syn_in { using = addToUsing (using syn_in) ps }
1918−
1919− -- build data declaration
1920− let mdecls = filter tydecl ds -- method declarations
1921− let idecls = filter instdecl ds -- default superclass instance declarations
1922− mapM_ checkDefaultSuperclassInstance idecls
1923− let mnames = map getMName mdecls
1924− logLvl 2 $ "Building methods " ++ show mnames
1925− ims <- mapM (tdecl mnames) mdecls
1926− defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
1927− (filter clause ds)
1928− let (methods, imethods)
1929− = unzip (map (\ ( x,y,z) -> (x, y)) ims)
1930− let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1931− addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])
1932− -- build instance constructor type
1933− -- decorate names of functions to ensure they can't be referred
1934− -- to elsewhere in the class declaration
1935− let cty = impbind ps $ conbind constraints
1936− $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1937− constraint
1938− let cons = [(emptyDocstring, [], cn, cty, fc, [])]
1939− let ddecl = PDatadecl tn tty cons
1940− logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
1941− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
1942− -- for each constraint, build a top level function to chase it
1943− logLvl 5 $ "Building functions"
1944−-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
1945−-- ++ using syn }
1946− fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
1947− mapM_ (elabDecl EAll info) (concat fns)
1948− -- for each method, build a top level function
1949− fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
1950− mapM_ (elabDecl EAll info) (concat fns)
1951− -- add the default definitions
1952− mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
1953− addIBC (IBCClass tn)
1954− where
1955− nodoc (n, (_, o, t)) = (n, (o, t))
1956− pibind [] x = x
1957− pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
1958−
1959− mdec (UN n) = SN (MethodN (UN n))
1960− mdec (NS x n) = NS (mdec x) n
1961− mdec x = x
1962−
1963− -- TODO: probably should normalise
1964− checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)
1965− = do when (not $ null cs) . tclift
1966− $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))
1967− i <- getIState
1968− let t = PApp fc (PRef fc n) (map pexp ps)
1969− let isConstrained = any (== t) constraints
1970− when (not isConstrained) . tclift
1971− $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
1972− return ()
1973−
1974− impbind [] x = x
1975− impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1976− conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
1977− conbind [] x = x
1978−
1979− getMName (PTy _ _ _ _ _ n _) = nsroot n
1980− tdecl allmeths (PTy doc _ syn _ o n t)
1981− = do t' <- implicit' info syn allmeths n t
1982− logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1983− return ( (n, (toExp (map fst ps) Exp t')),
1984− (n, (doc, o, (toExp (map fst ps) Imp t'))),
1985− (n, (syn, o, t) ) )
1986− tdecl _ _ = ifail "Not allowed in a class declaration"
1987−
1988− -- Create default definitions
1989− defdecl mtys c d@(PClauses fc opts n cs) =
1990− case lookup n mtys of
1991− Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1992− let ds = map (decorateid defaultdec)
1993− [PTy emptyDocstring [] syn fc [] n ty',
1994− PClauses fc (o ++ opts) n cs]
1995− iLOG (show ds)
1996− return (n, ((defaultdec n, ds!!1), ds))
1997− _ -> ifail $ show n ++ " is not a method"
1998− defdecl _ _ _ = ifail "Can't happen (defdecl)"
1999−
2000− defaultdec (UN n) = sUN ("default#" ++ str n)
2001− defaultdec (NS n ns) = NS (defaultdec n) ns
2002−
2003− tydecl (PTy _ _ _ _ _ _ _) = True
2004− tydecl _ = False
2005− instdecl (PInstance _ _ _ _ _ _ _ _) = True
2006− instdecl _ = False
2007− clause (PClauses _ _ _ _) = True
2008− clause _ = False
2009−
2010− -- Generate a function for chasing a dictionary constraint
2011− cfun cn c syn all con
2012− = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)
2013− -- SN (ParentN cn (show con))
2014− let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
2015− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
2016− let lhs = PApp fc (PRef fc cfn) [pconst capp]
2017− let rhs = PResolveTC (fileFC "HACK")
2018− let ty = PPi constraint (sMN 0 "pc") c con
2019− iLOG (showTmImpls ty)
2020− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
2021− i <- getIState
2022− let conn = case con of
2023− PRef _ n -> n
2024− PApp _ (PRef _ n) _ -> n
2025− let conn' = case lookupCtxtName conn (idris_classes i) of
2026− [(n, _)] -> n
2027− _ -> conn
2028− addInstance False conn' cfn
2029− addIBC (IBCInstance False conn' cfn)
2030−-- iputStrLn ("Added " ++ show (conn, cfn, ty))
2031− return [PTy emptyDocstring [] syn fc [] cfn ty,
2032− PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
2033−
2034− -- Generate a top level function which looks up a method in a given
2035− -- dictionary (this is inlinable, always)
2036− tfun cn c syn all (m, (doc, o, ty))
2037− = do let ty' = insertConstraint c ty
2038− let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
2039− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
2040− let margs = getMArgs ty
2041− let anames = map (\x -> sMN x "arg") [0..]
2042− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
2043− let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
2044− iLOG (showTmImpls ty)
2045− iLOG (show (m, ty', capp, margs))
2046− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
2047− return [PTy doc [] syn fc o m ty',
2048− PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
2049−
2050− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc
2051− getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc
2052− getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc
2053− getMArgs _ = []
2054−
2055− getMeth (m:ms) (a:as) x | x == a = PRef fc m
2056− | otherwise = getMeth ms as x
2057−
2058− lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns
2059− lhsArgs (IA : xs) ns = lhsArgs xs ns
2060− lhsArgs (CA : xs) ns = lhsArgs xs ns
2061− lhsArgs [] _ = []
2062−
2063− rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns
2064− rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns
2065− rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
2066− rhsArgs [] _ = []
2067−
2068− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)
2069− = PPi p n ty (insertConstraint c sc)
2070− insertConstraint c sc = PPi constraint (sMN 0 "class") c sc
2071−
2072− -- make arguments explicit and don't bind class parameters
2073− toExp ns e (PPi (Imp l s p) n ty sc)
2074− | n `elem` ns = toExp ns e sc
2075− | otherwise = PPi (e l s p) n ty (toExp ns e sc)
2076− toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
2077− toExp ns e sc = sc
2078−
2079−elabInstance :: ElabInfo -> SyntaxInfo ->
2080− ElabWhat -> -- phase
2081− FC -> [PTerm] -> -- constraints
2082− Name -> -- the class
2083− [PTerm] -> -- class parameters (i.e. instance)
2084− PTerm -> -- full instance type
2085− Maybe Name -> -- explicit name
2086− [PDecl] -> Idris ()
2087−elabInstance info syn what fc cs n ps t expn ds = do
2088− i <- getIState
2089− (n, ci) <- case lookupCtxtName n (idris_classes i) of
2090− [c] -> return c
2091− [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
2092− cs -> tclift $ tfail $ At fc
2093− (CantResolveAlts (map fst cs))
2094− let constraint = PApp fc (PRef fc n) (map pexp ps)
2095− let iname = mkiname n ps expn
2096− let emptyclass = null (class_methods ci)
2097− when (what /= EDefns || (null ds && not emptyclass)) $ do
2098− nty <- elabType' True info syn emptyDocstring [] fc [] iname t
2099− -- if the instance type matches any of the instances we have already,
2100− -- and it's not a named instance, then it's overlapping, so report an error
2101− case expn of
2102− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
2103− (class_instances ci)
2104− addInstance intInst n iname
2105− Just _ -> addInstance intInst n iname
2106− when (what /= ETypes && (not (null ds && not emptyclass))) $ do
2107− let ips = zip (class_params ci) ps
2108− let ns = case n of
2109− NS n ns' -> ns'
2110− _ -> []
2111− -- get the implicit parameters that need passing through to the
2112− -- where block
2113− wparams <- mapM (\p -> case p of
2114− PApp _ _ args -> getWParams (map getTm args)
2115− _ -> return []) ps
2116− let pnames = map pname (concat (nub wparams))
2117− let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
2118− undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
2119− mapM_ (elabDecl EAll info) undefinedSuperclassInstances
2120− let all_meths = map (nsroot . fst) (class_methods ci)
2121− let mtys = map (\ (n, (op, t)) ->
2122− let t_in = substMatchesShadow ips pnames t
2123− mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))
2124− all_meths
2125− t' = substMatchesShadow mnamemap pnames t_in in
2126− (decorate ns iname n,
2127− op, coninsert cs t', t'))
2128− (class_methods ci)
2129− logLvl 3 (show (mtys, ips))
2130− let ds' = insertDefaults i iname (class_defaults ci) ns ds
2131− iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)
2132− mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
2133− mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
2134− let wbTys = map mkTyDecl mtys
2135− let wbVals = map (decorateid (decorate ns iname)) ds'
2136− let wb = wbTys ++ wbVals
2137− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
2138− logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
2139− show (concat (nub wparams))
2140−
2141− -- Bring variables in instance head into scope
2142− ist <- getIState
2143− let headVars = nub $ mapMaybe (\p -> case p of
2144− PRef _ n ->
2145− case lookupTy n (tt_ctxt ist) of
2146− [] -> Just n
2147− _ -> Nothing
2148− _ -> Nothing) ps
2149−-- let lhs = PRef fc iname
2150− let lhs = PApp fc (PRef fc iname)
2151− (map (\n -> pimp n (PRef fc n) True) headVars)
2152− let rhs = PApp fc (PRef fc (instanceName ci))
2153− (map (pexp . mkMethApp) mtys)
2154−
2155− logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
2156− logLvl 5 $ "Instance RHS " ++ show rhs
2157−
2158− let idecls = [PClauses fc [Dictionary] iname
2159− [PClause fc iname lhs [] rhs wb]]
2160− iLOG (show idecls)
2161− mapM_ (elabDecl EAll info) idecls
2162− addIBC (IBCInstance intInst n iname)
2163−
2164− where
2165− intInst = case ps of
2166− [PConstant (AType (ATInt ITNative))] -> True
2167− _ -> False
2168−
2169− mkiname n' ps' expn' =
2170− case expn' of
2171− Nothing -> SN (sInstanceN n' (map show ps'))
2172− Just nm -> nm
2173−
2174− substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
2175− = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
2176−
2177− isOverlapping i (PInstance syn _ _ n ps t expn _)
2178− = case lookupCtxtName n (idris_classes i) of
2179− [(n, ci)] -> let iname = (mkiname n ps expn) in
2180− case lookupTy iname (tt_ctxt i) of
2181− [] -> elabFindOverlapping i ci iname syn t
2182− (_:_) -> return True
2183− _ -> return False -- couldn't find class, just let elabInstance fail later
2184−
2185− -- TODO: largely based upon elabType' - should try to abstract
2186− elabFindOverlapping i ci iname syn t
2187− = do ty' <- addUsingConstraints syn fc t
2188− -- TODO think: something more in info?
2189− ty' <- implicit info syn iname ty'
2190− let ty = addImpl i ty'
2191− ctxt <- getContext
2192− ((tyT, _, _), _) <-
2193− tclift $ elaborate ctxt iname (TType (UVal 0)) []
2194− (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))
2195− ctxt <- getContext
2196− (cty, _) <- recheckC fc [] tyT
2197− let nty = normalise ctxt [] cty
2198− return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
2199−
2200− findOverlapping i t n
2201− | take 2 (show n) == "@@" = Nothing
2202− | otherwise
2203− = case lookupTy n (tt_ctxt i) of
2204− [t'] -> let tret = getRetType t
2205− tret' = getRetType (delab i t') in
2206− case matchClause i tret' tret of
2207− Right ms -> Just tret'
2208− Left _ -> case matchClause i tret tret' of
2209− Right ms -> Just tret'
2210− Left _ -> Nothing
2211− _ -> Nothing
2212− overlapping t' = tclift $ tfail (At fc (Msg $
2213− "Overlapping instance: " ++ show t' ++ " already defined"))
2214− getRetType (PPi _ _ _ sc) = getRetType sc
2215− getRetType t = t
2216−
2217− mkMethApp (n, _, _, ty)
2218− = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
2219− lamBind i (PPi (Constraint _ _) _ _ sc) sc'
2220− = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2221− lamBind i (PPi _ n ty sc) sc'
2222− = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
2223− lamBind i _ sc = sc
2224− methArgs i (PPi (Imp _ _ _) n ty sc)
2225− = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2226− methArgs i (PPi (Exp _ _ _) n ty sc)
2227− = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2228− methArgs i (PPi (Constraint _ _) n ty sc)
2229− = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
2230− methArgs i _ = []
2231−
2232− papp fc f [] = f
2233− papp fc f as = PApp fc f as
2234−
2235− getWParams [] = return []
2236− getWParams (p : ps)
2237− | PRef _ n <- p
2238− = do ps' <- getWParams ps
2239− ctxt <- getContext
2240− case lookupP n ctxt of
2241− [] -> return (pimp n (PRef fc n) True : ps')
2242− _ -> return ps'
2243− getWParams (_ : ps) = getWParams ps
2244−
2245− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2246− decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2247−
2248− mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
2249−
2250− conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2251− conbind [] x = x
2252−
2253− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)
2254− coninsert cs sc = conbind cs sc
2255−
2256− insertDefaults :: IState -> Name ->
2257− [(Name, (Name, PDecl))] -> [T.Text] ->
2258− [PDecl] -> [PDecl]
2259− insertDefaults i iname [] ns ds = ds
2260− insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
2261− = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
2262−
2263− insertDef i meth def clauses ns iname decls
2264− | null $ filter (clauseFor meth iname ns) decls
2265− = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
2266− -- trace (show newd) $
2267− decls ++ [newd]
2268− | otherwise = decls
2269−
2270− warnMissing decls ns iname meth
2271− | null $ filter (clauseFor meth iname ns) decls
2272− = iWarn fc . text $ "method " ++ show meth ++ " not defined"
2273− | otherwise = return ()
2274−
2275− checkInClass ns meth
2276− | not (null (filter (eqRoot meth) ns)) = return ()
2277− | otherwise = tclift $ tfail (At fc (Msg $
2278− show meth ++ " not a method of class " ++ show n))
2279−
2280− eqRoot x y = nsroot x == nsroot y
2281−
2282− clauseFor m iname ns (PClauses _ _ m' _)
2283− = decorate ns iname m == decorate ns iname m'
2284− clauseFor m iname ns _ = False
2285−
2286−{- This won't work yet. Can it ever, in this form?
2287−
2288− cfun cn c syn all con
2289− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
2290− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
2291− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
2292− let lhs = PApp fc (PRef fc cfn) [pconst capp]
2293− let rhs = PResolveTC (FC "HACK" 0)
2294− let ty = PPi constraint (MN 0 "pc") c con
2295− iLOG (showImp True ty)
2296− iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
2297− i <- getIState
2298− let conn = case con of
2299− PRef _ n -> n
2300− PApp _ (PRef _ n) _ -> n
2301− let conn' = case lookupCtxtName Nothing conn (idris_classes i) of
2302− [(n, _)] -> n
2303− _ -> conn
2304− addInstance False conn' cfn
2305− addIBC (IBCInstance False conn' cfn)
2306− iputStrLn ("Added " ++ show (conn, cfn, ty) ++ "\n" ++ show (lhs, rhs))
2307− return [PTy "" syn fc [] cfn ty,
2308− PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
2309−-}
2310−
2311−decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t
2312−decorateid decorate (PClauses f o n cs)
2313− = PClauses f o (decorate n) (map dc cs)
2314− where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
2315− dc (PWith fc n t as w ds)
2316− = PWith fc (decorate n) (dappname t) as w
2317− (map (decorateid decorate) ds)
2318− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
2319− dappname t = t
2320−
2321−
2322−-- if 't' is a type class application, assume its arguments are injective
2323−pbinds :: IState -> Term -> ElabD ()
2324−pbinds i (Bind n (PVar t) sc)
2325− = do attack; patbind n
2326− case unApply t of
2327− (P _ c _, args) -> case lookupCtxt c (idris_classes i) of
2328− [] -> return ()
2329− _ -> -- type class, set as injective
2330− mapM_ setinjArg args
2331− _ -> return ()
2332− pbinds i sc
2333− where setinjArg (P _ n _) = setinj n
2334− setinjArg _ = return ()
2335−pbinds i tm = return ()
2336−
2337−pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)
2338−pbty _ tm = tm
2339−
2340−getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc
2341−getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc
2342−getPBtys _ = []
2343−
2344−psolve (Bind n (PVar t) sc) = do solve; psolve sc
2345−psolve tm = return ()
2346−
2347−pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc
2348−pvars ist _ = []
2349−
2350−data ElabWhat = ETypes | EDefns | EAll
2351− deriving (Show, Eq)
2352−
2353169elabDecls :: ElabInfo -> [PDecl] -> Idris ()
2354170elabDecls info ds = do mapM_ (elabDecl EAll info) ds
2355−-- mapM_ (elabDecl EDefns info) ds
2356171
2357172elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
2358173elabDecl what info d
2359− = idrisCatch (withErrorReflection $ elabDecl' what info d) (setAndReport)
174+ = let info' = info { rec_elabDecl = elabDecl' } in
175+ idrisCatch (withErrorReflection $ elabDecl' what info' d) (setAndReport)
2360176
2361177elabDecl' _ info (PFix _ _ _)
2362178 = return () -- nothing to elaborate
@@ -2464,54 +280,3 @@ elabDecl' what info (PTransform fc safety old new)
2464280 = elabTransform info fc safety old new
2465281elabDecl' _ _ _ = return () -- skipped this time
2466282
2467−elabCaseBlock info opts d@(PClauses f o n ps)
2468− = do addIBC (IBCDef n)
2469− logLvl 5 $ "CASE BLOCK: " ++ show (n, d)
2470− let opts' = nub (o ++ opts)
2471− -- propagate totality assertion to the new definitions
2472− when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]
2473− elabDecl' EAll info (PClauses f opts' n ps )
2474−
2475−-- elabDecl' info (PImport i) = loadModule i
2476−
2477−-- Check that the result of type checking matches what the programmer wrote
2478−-- (i.e. - if we inferred any arguments that the user provided, make sure
2479−-- they are the same!)
2480−
2481−checkInferred :: FC -> PTerm -> PTerm -> Idris ()
2482−checkInferred fc inf user =
2483− do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++
2484− showTmImpls user
2485− logLvl 10 $ "Checking match"
2486− i <- getIState
2487− tclift $ case matchClause' True i user inf of
2488− _ -> return ()
2489−-- Left (x, y) -> tfail $ At fc
2490−-- (Msg $ "The type-checked term and given term do not match: "
2491−-- ++ show x ++ " and " ++ show y)
2492− logLvl 10 $ "Checked match"
2493−-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)
2494−
2495−-- Return whether inferred term is different from given term
2496−-- (as above, but return a Bool)
2497−
2498−inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
2499−inferredDiff fc inf user =
2500− do i <- getIState
2501− logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++
2502− showTmImpls user
2503− tclift $ case matchClause' True i user inf of
2504− Right vs -> return False
2505− Left (x, y) -> return True
2506−
2507−-- | Check a PTerm against documentation and ensure that every documented
2508−-- argument actually exists. This must be run _after_ implicits have been
2509−-- found, or it will give spurious errors.
2510−checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
2511−checkDocs fc args tm = cd (Map.fromList args) tm
2512− where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2513− cd as _ | Map.null as = return ()
2514− | otherwise = ierror . At fc . Msg $
2515− "There is documentation for argument(s) "
2516− ++ (concat . intersperse ", " . map show . Map.keys) as
2517− ++ " but they were not found."