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