git.iko.soy/Idris-dev
on 2b0224a help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2170 lines 92 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.Docstrings
13import Idris.IdeMode hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import System.Console.Haskeline
18import System.IO
20import Control.Applicative
21import Control.Monad (liftM3)
22import Control.Monad.State
24import Data.List hiding (insert,union)
25import Data.Char
26import qualified Data.Text as T
27import Data.Either
28import qualified Data.Map as M
29import Data.Maybe
30import qualified Data.Set as S
31import Data.Word (Word)
33import Debug.Trace
35import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
37import Util.Pretty
38import Util.ScreenSize
39import Util.System
41getContext :: Idris Context
42getContext = do i <- getIState; return (tt_ctxt i)
44forCodegen :: Codegen -> [(Codegen, a)] -> [a]
45forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
47getObjectFiles :: Codegen -> Idris [FilePath]
48getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
50addObjectFile :: Codegen -> FilePath -> Idris ()
51addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
53getLibs :: Codegen -> Idris [String]
54getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
56addLib :: Codegen -> String -> Idris ()
57addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
59getFlags :: Codegen -> Idris [String]
60getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
62addFlag :: Codegen -> String -> Idris ()
63addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
65addDyLib :: [String] -> Idris (Either DynamicLib String)
66addDyLib libs = do i <- getIState
67 let ls = idris_dynamic_libs i
68 let importdirs = opt_importdirs (idris_options i)
69 case mapMaybe (findDyLib ls) libs of
70 x:_ -> return (Left x)
71 [] -> do
72 handle <- lift . lift .
73 mapM (\l -> catchIO (tryLoadLib importdirs l)
74 (\_ -> return Nothing)) $ libs
75 case msum handle of
76 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
77 concat (intersperse "," libs) ++ "\"")
78 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
79 return (Left x)
80 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
81 findDyLib [] l = Nothing
82 findDyLib (lib:libs) l | l == lib_name lib = Just lib
83 | otherwise = findDyLib libs l
85getAutoImports :: Idris [FilePath]
86getAutoImports = do i <- getIState
87 return (opt_autoImport (idris_options i))
89addAutoImport :: FilePath -> Idris ()
90addAutoImport fp = do i <- getIState
91 let opts = idris_options i
92 let autoimps = opt_autoImport opts
93 put (i { idris_options = opts { opt_autoImport =
94 fp : opt_autoImport opts } } )
96addHdr :: Codegen -> String -> Idris ()
97addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
99addImported :: Bool -> FilePath -> Idris ()
100addImported pub f
101 = do i <- getIState
102 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
104addLangExt :: LanguageExt -> Idris ()
105addLangExt TypeProviders = do i <- getIState
106 putIState $ i {
107 idris_language_extensions = TypeProviders : idris_language_extensions i
108 }
109addLangExt ErrorReflection = do i <- getIState
110 putIState $ i {
111 idris_language_extensions = ErrorReflection : idris_language_extensions i
112 }
114-- Transforms are organised by the function being applied on the lhs of the
115-- transform, to make looking up appropriate transforms quicker
116addTrans :: Name -> (Term, Term) -> Idris ()
117addTrans basefn t
118 = do i <- getIState
119 let t' = case lookupCtxtExact basefn (idris_transforms i) of
120 Just def -> (t : def)
121 Nothing -> [t]
122 putIState $ i { idris_transforms = addDef basefn t'
123 (idris_transforms i) }
125addErrRev :: (Term, Term) -> Idris ()
126addErrRev t = do i <- getIState
127 putIState $ i { idris_errRev = t : idris_errRev i }
129addErasureUsage :: Name -> Int -> Idris ()
130addErasureUsage n i = do ist <- getIState
131 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
133addExport :: Name -> Idris ()
134addExport n = do ist <- getIState
135 putIState $ ist { idris_exports = n : idris_exports ist }
137addUsedName :: FC -> Name -> Name -> Idris ()
138addUsedName fc n arg
139 = do ist <- getIState
140 case lookupTyName n (tt_ctxt ist) of
141 [(n', ty)] -> addUsage n' 0 ty
142 [] -> throwError (At fc (NoSuchVariable n))
143 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
144 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
145 addErasureUsage n i
146 | otherwise = addUsage n (i + 1) sc
147 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
149getErasureUsage :: Idris [(Name, Int)]
150getErasureUsage = do ist <- getIState;
151 return (idris_erasureUsed ist)
153getExports :: Idris [Name]
154getExports = do ist <- getIState
155 return (idris_exports ist)
157totcheck :: (FC, Name) -> Idris ()
158totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
160defer_totcheck :: (FC, Name) -> Idris ()
161defer_totcheck n
162 = do i <- getIState;
163 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
165clear_totcheck :: Idris ()
166clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
168setFlags :: Name -> [FnOpt] -> Idris ()
169setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
171setFnInfo :: Name -> FnInfo -> Idris ()
172setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
174setAccessibility :: Name -> Accessibility -> Idris ()
175setAccessibility n a
176 = do i <- getIState
177 let ctxt = setAccess n a (tt_ctxt i)
178 putIState $ i { tt_ctxt = ctxt }
180setTotality :: Name -> Totality -> Idris ()
181setTotality n a
182 = do i <- getIState
183 let ctxt = setTotal n a (tt_ctxt i)
184 putIState $ i { tt_ctxt = ctxt }
186getTotality :: Name -> Idris Totality
187getTotality n
188 = do i <- getIState
189 case lookupTotal n (tt_ctxt i) of
190 [t] -> return t
191 _ -> return (Total [])
193-- Get coercions which might return the required type
194getCoercionsTo :: IState -> Type -> [Name]
195getCoercionsTo i ty =
196 let cs = idris_coercions i
197 (fn,_) = unApply (getRetTy ty) in
198 findCoercions fn cs
199 where findCoercions t [] = []
200 findCoercions t (n : ns) =
201 let ps = case lookupTy n (tt_ctxt i) of
202 [ty'] -> case unApply (getRetTy ty') of
203 (t', _) ->
204 if t == t' then [n] else []
205 _ -> [] in
206 ps ++ findCoercions t ns
208addToCG :: Name -> CGInfo -> Idris ()
209addToCG n cg
210 = do i <- getIState
211 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
213addTyInferred :: Name -> Idris ()
214addTyInferred n
215 = do i <- getIState
216 putIState $ i { idris_tyinfodata =
217 addDef n TIPartial (idris_tyinfodata i) }
219addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
220addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
221 mapM_ addConstraint ts
222 return ()
223 where addConstraint (x, y) = findMVApps x y
225 findMVApps x y
226 = do let (fx, argsx) = unApply x
227 let (fy, argsy) = unApply y
228 if (not (fx == fy))
229 then do
230 tryAddMV fx y
231 tryAddMV fy x
232 else mapM_ addConstraint (zip argsx argsy)
234 tryAddMV (P _ mv _) y =
235 do ist <- get
236 case lookup mv (idris_metavars ist) of
237 Just _ -> addConstraintRule mv y
238 _ -> return ()
239 tryAddMV _ _ = return ()
241 addConstraintRule :: Name -> Term -> Idris ()
242 addConstraintRule n t
243 = do ist <- get
244 logLvl 1 $ "TI constraint: " ++ show (n, t)
245 case lookupCtxt n (idris_tyinfodata ist) of
246 [TISolution ts] ->
247 do mapM_ (checkConsistent t) ts
248 let ti' = addDef n (TISolution (t : ts))
249 (idris_tyinfodata ist)
250 put $ ist { idris_tyinfodata = ti' }
251 _ ->
252 do let ti' = addDef n (TISolution [t])
253 (idris_tyinfodata ist)
254 put $ ist { idris_tyinfodata = ti' }
256 -- Check a solution is consistent with previous solutions
257 -- Meaning: If heads are both data types, they had better be the
258 -- same.
259 checkConsistent :: Term -> Term -> Idris ()
260 checkConsistent x y =
261 do let (fx, _) = unApply x
262 let (fy, _) = unApply y
263 case (fx, fy) of
264 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
265 (P (TCon _ _) n _, Constant _) -> errWhen True
266 (Constant _, P (TCon _ _) n' _) -> errWhen True
267 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
268 _ -> return ()
270 where errWhen True
271 = throwError (At fc
272 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
273 errWhen False = return ()
275isTyInferred :: Name -> Idris Bool
276isTyInferred n
277 = do i <- getIState
278 case lookupCtxt n (idris_tyinfodata i) of
279 [TIPartial] -> return True
280 _ -> return False
282-- | Adds error handlers for a particular function and argument. If names are
283-- ambiguous, all matching handlers are updated.
284addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
285addFunctionErrorHandlers f arg hs =
286 do i <- getIState
287 let oldHandlers = idris_function_errorhandlers i
288 let newHandlers = flip (addDef f) oldHandlers $
289 case lookupCtxtExact f oldHandlers of
290 Nothing -> M.singleton arg (S.fromList hs)
291 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
292 -- will always be one of those two, thus no extra case
293 putIState $ i { idris_function_errorhandlers = newHandlers }
295getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
296getFunctionErrorHandlers f arg = do i <- getIState
297 return . maybe [] S.toList $
298 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
301-- Trace all the names in a call graph starting at the given name
302getAllNames :: Name -> Idris [Name]
303getAllNames n = allNames [] n
305allNames :: [Name] -> Name -> Idris [Name]
306allNames ns n | n `elem` ns = return []
307allNames ns n = do i <- getIState
308 case lookupCtxtExact n (idris_callgraph i) of
309 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
310 return (nub (n : concat more))
311 _ -> return [n]
313addCoercion :: Name -> Idris ()
314addCoercion n = do i <- getIState
315 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
317addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
318addDocStr n doc args
319 = do i <- getIState
320 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
322addNameHint :: Name -> Name -> Idris ()
323addNameHint ty n
324 = do i <- getIState
325 ty' <- case lookupCtxtName ty (idris_implicits i) of
326 [(tyn, _)] -> return tyn
327 [] -> throwError (NoSuchVariable ty)
328 tyns -> throwError (CantResolveAlts (map fst tyns))
329 let ns' = case lookupCtxt ty' (idris_namehints i) of
330 [ns] -> ns ++ [n]
331 _ -> [n]
332 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
334getNameHints :: IState -> Name -> [Name]
335getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
336getNameHints i n =
337 case lookupCtxt n (idris_namehints i) of
338 [ns] -> ns
339 _ -> []
341-- Issue #1737 in the Issue Tracker.
342-- https://github.com/idris-lang/Idris-dev/issues/1737
343addToCalledG :: Name -> [Name] -> Idris ()
344addToCalledG n ns = return () -- TODO
346push_estack :: Name -> Bool -> Idris ()
347push_estack n inst
348 = do i <- getIState
349 putIState (i { elab_stack = (n, inst) : elab_stack i })
351pop_estack :: Idris ()
352pop_estack = do i <- getIState
353 putIState (i { elab_stack = ptail (elab_stack i) })
354 where ptail [] = []
355 ptail (x : xs) = xs
357-- | Add a class instance function.
358--
359-- Precondition: the instance should have the correct type.
360--
361-- Dodgy hack 1: Put integer instances first in the list so they are
362-- resolved by default.
363--
364-- Dodgy hack 2: put constraint chasers (@@) last
365addInstance :: Bool -- ^ whether the name is an Integer instance
366 -> Bool -- ^ whether to include the instance in instance search
367 -> Name -- ^ the name of the class
368 -> Name -- ^ the name of the instance
369 -> Idris ()
370addInstance int res n i
371 = do ist <- getIState
372 case lookupCtxt n (idris_classes ist) of
373 [CI a b c d e ins fds] ->
374 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
375 putIState $ ist { idris_classes = cs }
376 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)
377 putIState $ ist { idris_classes = cs }
378 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
379 addI i ins | int = (i, res) : ins
380 | chaser n = ins ++ [(i, res)]
381 | otherwise = insI i ins
382 insI i [] = [(i, res)]
383 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
384 | otherwise = n : insI i ns
386 chaser (UN nm)
387 | ('@':'@':_) <- str nm = True
388 chaser (NS n _) = chaser n
389 chaser _ = False
391addClass :: Name -> ClassInfo -> Idris ()
392addClass n i
393 = do ist <- getIState
394 let i' = case lookupCtxt n (idris_classes ist) of
395 [c] -> c { class_instances = class_instances i }
396 _ -> i
397 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
399addAutoHint :: Name -> Name -> Idris ()
400addAutoHint n hint =
401 do ist <- getIState
402 case lookupCtxtExact n (idris_autohints ist) of
403 Nothing ->
404 do let hs = addDef n [hint] (idris_autohints ist)
405 putIState $ ist { idris_autohints = hs }
406 Just nhints ->
407 do let hs = addDef n (hint : nhints) (idris_autohints ist)
408 putIState $ ist { idris_autohints = hs }
410getAutoHints :: Name -> Idris [Name]
411getAutoHints n = do ist <- getIState
412 case lookupCtxtExact n (idris_autohints ist) of
413 Nothing -> return []
414 Just ns -> return ns
416addIBC :: IBCWrite -> Idris ()
417addIBC ibc@(IBCDef n)
418 = do i <- getIState
419 when (notDef (ibc_write i)) $
420 putIState $ i { ibc_write = ibc : ibc_write i }
421 where notDef [] = True
422 notDef (IBCDef n': is) | n == n' = False
423 notDef (_ : is) = notDef is
424addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
426clearIBC :: Idris ()
427clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
429resetNameIdx :: Idris ()
430resetNameIdx = do i <- getIState
431 put (i { idris_nameIdx = (0, emptyContext) })
433-- Used to preserve sharing of names
434addNameIdx :: Name -> Idris (Int, Name)
435addNameIdx n = do i <- getIState
436 let (i', x) = addNameIdx' i n
437 putIState i'
438 return x
440addNameIdx' :: IState -> Name -> (IState, (Int, Name))
441addNameIdx' i n
442 = let idxs = snd (idris_nameIdx i) in
443 case lookupCtxt n idxs of
444 [x] -> (i, x)
445 _ -> let i' = fst (idris_nameIdx i) + 1 in
446 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
448getSymbol :: Name -> Idris Name
449getSymbol n = do i <- getIState
450 case M.lookup n (idris_symbols i) of
451 Just n' -> return n'
452 Nothing -> do let sym' = M.insert n n (idris_symbols i)
453 put (i { idris_symbols = sym' })
454 return n
456getHdrs :: Codegen -> Idris [String]
457getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
459getImported :: Idris [(FilePath, Bool)]
460getImported = do i <- getIState; return (idris_imported i)
462setErrSpan :: FC -> Idris ()
463setErrSpan x = do i <- getIState;
464 case (errSpan i) of
465 Nothing -> putIState $ i { errSpan = Just x }
466 Just _ -> return ()
468clearErr :: Idris ()
469clearErr = do i <- getIState
470 putIState $ i { errSpan = Nothing }
472getSO :: Idris (Maybe String)
473getSO = do i <- getIState
474 return (compiled_so i)
476setSO :: Maybe String -> Idris ()
477setSO s = do i <- getIState
478 putIState $ (i { compiled_so = s })
480getIState :: Idris IState
481getIState = get
483putIState :: IState -> Idris ()
484putIState = put
486updateIState :: (IState -> IState) -> Idris ()
487updateIState f = do i <- getIState
488 putIState $ f i
490withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
491withContext ctx name dflt action = do
492 ist <- getIState
493 case lookupCtxt name (ctx ist) of
494 [x] -> action x
495 _ -> return dflt
497withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
498withContext_ ctx name action = withContext ctx name () action
500-- | A version of liftIO that puts errors into the exception type of the Idris monad
501runIO :: IO a -> Idris a
502runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
503-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
504--
505-- Issue #1738 on the issue tracker.
506-- https://github.com/idris-lang/Idris-dev/issues/1738
508getName :: Idris Int
509getName = do i <- getIState;
510 let idx = idris_name i;
511 putIState $ (i { idris_name = idx + 1 })
512 return idx
514-- InternalApp keeps track of the real function application for making case splits from, not the application the
515-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
516addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
517addInternalApp fp l t
518 = do i <- getIState
519 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
521getInternalApp :: FilePath -> Int -> Idris PTerm
522getInternalApp fp l = do i <- getIState
523 case lookup (fp, l) (idris_lineapps i) of
524 Just n' -> return n'
525 Nothing -> return Placeholder
526 -- TODO: What if it's not there?
528-- Pattern definitions are only used for coverage checking, so erase them
529-- when we're done
530clearOrigPats :: Idris ()
531clearOrigPats = do i <- get
532 let ps = idris_patdefs i
533 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
534 put (i { idris_patdefs = ps' })
536-- Erase types from Ps in the context (basically ending up with what's in
537-- the .ibc, which is all we need after all the analysis is done)
538clearPTypes :: Idris ()
539clearPTypes = do i <- get
540 let ctxt = tt_ctxt i
541 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
542 where pErase (CaseOp c t tys orig tot cds)
543 = CaseOp c t tys orig [] (pErase' cds)
544 pErase x = x
545 pErase' (CaseDefs _ (cs, c) _ rs)
546 = let c' = (cs, fmap pEraseType c) in
547 CaseDefs c' c' c' rs
549checkUndefined :: FC -> Name -> Idris ()
550checkUndefined fc n
551 = do i <- getContext
552 case lookupTy n i of
553 (_:_) -> throwError . Msg $ show fc ++ ":" ++
554 show n ++ " already defined"
555 _ -> return ()
557isUndefined :: FC -> Name -> Idris Bool
558isUndefined fc n
559 = do i <- getContext
560 case lookupTyExact n i of
561 Just _ -> return False
562 _ -> return True
564setContext :: Context -> Idris ()
565setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
567updateContext :: (Context -> Context) -> Idris ()
568updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
570addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
571addConstraints fc (v, cs)
572 = do i <- getIState
573 let ctxt = tt_ctxt i
574 let ctxt' = ctxt { next_tvar = v }
575 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
576 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
577 where
578 insertAll [] c = c
579 insertAll ((c, fc) : cs) ics
580 = insertAll cs $ S.insert (ConstraintFC c fc) ics
582addDeferred = addDeferred' Ref
583addDeferredTyCon = addDeferred' (TCon 0 0)
585-- | Save information about a name that is not yet defined
586addDeferred' :: NameType
587 -> [(Name, (Int, Maybe Name, Type, Bool))]
588 -- ^ The Name is the name being made into a metavar,
589 -- the Int is the number of vars that are part of a
590 -- putative proof context, the Maybe Name is the
591 -- top-level function containing the new metavariable,
592 -- the Type is its type, and the Bool is whether :p is
593 -- allowed
594 -> Idris ()
595addDeferred' nt ns
596 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
597 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
598 i <- getIState
599 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
600 idris_metavars i }
601 where
602 -- 'tidyNames' is to generate user accessible names in case they are
603 -- needed in tactic scripts
604 tidyNames used (Bind (MN i x) b sc)
605 = let n' = uniqueNameSet (UN x) used in
606 Bind n' b $ tidyNames (S.insert n' used) sc
607 tidyNames used (Bind n b sc)
608 = let n' = uniqueNameSet n used in
609 Bind n' b $ tidyNames (S.insert n' used) sc
610 tidyNames used b = b
612solveDeferred :: Name -> Idris ()
613solveDeferred n = do i <- getIState
614 putIState $ i { idris_metavars =
615 filter (\(n', _) -> n/=n')
616 (idris_metavars i),
617 ibc_write =
618 filter (notMV n) (ibc_write i)
619 }
620 where notMV n (IBCMetavar n') = not (n == n')
621 notMV n _ = True
623getUndefined :: Idris [Name]
624getUndefined = do i <- getIState
625 return (map fst (idris_metavars i) \\ primDefs)
627isMetavarName :: Name -> IState -> Bool
628isMetavarName n ist
629 = case lookupNames n (tt_ctxt ist) of
630 (t:_) -> isJust $ lookup t (idris_metavars ist)
631 _ -> False
633getWidth :: Idris ConsoleWidth
634getWidth = fmap idris_consolewidth getIState
636setWidth :: ConsoleWidth -> Idris ()
637setWidth w = do ist <- getIState
638 put ist { idris_consolewidth = w }
643type1Doc :: Doc OutputAnnotation
644type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
647isetPrompt :: String -> Idris ()
648isetPrompt p = do i <- getIState
649 case idris_outputmode i of
650 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
652-- | Tell clients how much was parsed and loaded
653isetLoadedRegion :: Idris ()
654isetLoadedRegion = do i <- getIState
655 let span = idris_parsedSpan i
656 case span of
657 Just fc ->
658 case idris_outputmode i of
659 IdeMode n h ->
660 runIO . hPutStrLn h $
661 convSExp "set-loaded-region" fc n
662 Nothing -> return ()
664setLogLevel :: Int -> Idris ()
665setLogLevel l = do i <- getIState
666 let opts = idris_options i
667 let opt' = opts { opt_logLevel = l }
668 putIState $ i { idris_options = opt' }
670setCmdLine :: [Opt] -> Idris ()
671setCmdLine opts = do i <- getIState
672 let iopts = idris_options i
673 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
675getCmdLine :: Idris [Opt]
676getCmdLine = do i <- getIState
677 return (opt_cmdline (idris_options i))
679getDumpDefun :: Idris (Maybe FilePath)
680getDumpDefun = do i <- getIState
681 return $ findC (opt_cmdline (idris_options i))
682 where findC [] = Nothing
683 findC (DumpDefun x : _) = Just x
684 findC (_ : xs) = findC xs
686getDumpCases :: Idris (Maybe FilePath)
687getDumpCases = do i <- getIState
688 return $ findC (opt_cmdline (idris_options i))
689 where findC [] = Nothing
690 findC (DumpCases x : _) = Just x
691 findC (_ : xs) = findC xs
693logLevel :: Idris Int
694logLevel = do i <- getIState
695 return (opt_logLevel (idris_options i))
697setErrContext :: Bool -> Idris ()
698setErrContext t = do i <- getIState
699 let opts = idris_options i
700 let opts' = opts { opt_errContext = t }
701 putIState $ i { idris_options = opts' }
703errContext :: Idris Bool
704errContext = do i <- getIState
705 return (opt_errContext (idris_options i))
707getOptimise :: Idris [Optimisation]
708getOptimise = do i <- getIState
709 return (opt_optimise (idris_options i))
711setOptimise :: [Optimisation] -> Idris ()
712setOptimise newopts = do i <- getIState
713 let opts = idris_options i
714 let opts' = opts { opt_optimise = newopts }
715 putIState $ i { idris_options = opts' }
717addOptimise :: Optimisation -> Idris ()
718addOptimise opt = do opts <- getOptimise
719 setOptimise (nub (opt : opts))
721removeOptimise :: Optimisation -> Idris ()
722removeOptimise opt = do opts <- getOptimise
723 setOptimise ((nub opts) \\ [opt])
725-- Set appropriate optimisation set for the given level. We only have
726-- one optimisation that is configurable at the moment, however!
727setOptLevel :: Int -> Idris ()
728setOptLevel n | n <= 0 = setOptimise []
729setOptLevel 1 = setOptimise []
730setOptLevel 2 = setOptimise [PETransform]
731setOptLevel n | n >= 3 = setOptimise [PETransform]
733useREPL :: Idris Bool
734useREPL = do i <- getIState
735 return (opt_repl (idris_options i))
737setREPL :: Bool -> Idris ()
738setREPL t = do i <- getIState
739 let opts = idris_options i
740 let opt' = opts { opt_repl = t }
741 putIState $ i { idris_options = opt' }
743showOrigErr :: Idris Bool
744showOrigErr = do i <- getIState
745 return (opt_origerr (idris_options i))
747setShowOrigErr :: Bool -> Idris ()
748setShowOrigErr b = do i <- getIState
749 let opts = idris_options i
750 let opt' = opts { opt_origerr = b }
751 putIState $ i { idris_options = opt' }
753setAutoSolve :: Bool -> Idris ()
754setAutoSolve b = do i <- getIState
755 let opts = idris_options i
756 let opt' = opts { opt_autoSolve = b }
757 putIState $ i { idris_options = opt' }
759setNoBanner :: Bool -> Idris ()
760setNoBanner n = do i <- getIState
761 let opts = idris_options i
762 let opt' = opts { opt_nobanner = n }
763 putIState $ i { idris_options = opt' }
765getNoBanner :: Idris Bool
766getNoBanner = do i <- getIState
767 let opts = idris_options i
768 return (opt_nobanner opts)
770setQuiet :: Bool -> Idris ()
771setQuiet q = do i <- getIState
772 let opts = idris_options i
773 let opt' = opts { opt_quiet = q }
774 putIState $ i { idris_options = opt' }
776getQuiet :: Idris Bool
777getQuiet = do i <- getIState
778 let opts = idris_options i
779 return (opt_quiet opts)
781setCodegen :: Codegen -> Idris ()
782setCodegen t = do i <- getIState
783 let opts = idris_options i
784 let opt' = opts { opt_codegen = t }
785 putIState $ i { idris_options = opt' }
787codegen :: Idris Codegen
788codegen = do i <- getIState
789 return (opt_codegen (idris_options i))
791setOutputTy :: OutputType -> Idris ()
792setOutputTy t = do i <- getIState
793 let opts = idris_options i
794 let opt' = opts { opt_outputTy = t }
795 putIState $ i { idris_options = opt' }
797outputTy :: Idris OutputType
798outputTy = do i <- getIState
799 return $ opt_outputTy $ idris_options i
801setIdeMode :: Bool -> Handle -> Idris ()
802setIdeMode True h = do i <- getIState
803 putIState $ i { idris_outputmode = IdeMode 0 h
804 , idris_colourRepl = False
805 }
806setIdeMode False _ = return ()
808setTargetTriple :: String -> Idris ()
809setTargetTriple t = do i <- getIState
810 let opts = idris_options i
811 opt' = opts { opt_triple = t }
812 putIState $ i { idris_options = opt' }
814targetTriple :: Idris String
815targetTriple = do i <- getIState
816 return (opt_triple (idris_options i))
818setTargetCPU :: String -> Idris ()
819setTargetCPU t = do i <- getIState
820 let opts = idris_options i
821 opt' = opts { opt_cpu = t }
822 putIState $ i { idris_options = opt' }
824targetCPU :: Idris String
825targetCPU = do i <- getIState
826 return (opt_cpu (idris_options i))
828verbose :: Idris Bool
829verbose = do i <- getIState
830 -- Quietness overrides verbosity
831 return (not (opt_quiet (idris_options i)) &&
832 opt_verbose (idris_options i))
834setVerbose :: Bool -> Idris ()
835setVerbose t = do i <- getIState
836 let opts = idris_options i
837 let opt' = opts { opt_verbose = t }
838 putIState $ i { idris_options = opt' }
840typeInType :: Idris Bool
841typeInType = do i <- getIState
842 return (opt_typeintype (idris_options i))
844setTypeInType :: Bool -> Idris ()
845setTypeInType t = do i <- getIState
846 let opts = idris_options i
847 let opt' = opts { opt_typeintype = t }
848 putIState $ i { idris_options = opt' }
850coverage :: Idris Bool
851coverage = do i <- getIState
852 return (opt_coverage (idris_options i))
854setCoverage :: Bool -> Idris ()
855setCoverage t = do i <- getIState
856 let opts = idris_options i
857 let opt' = opts { opt_coverage = t }
858 putIState $ i { idris_options = opt' }
860setIBCSubDir :: FilePath -> Idris ()
861setIBCSubDir fp = do i <- getIState
862 let opts = idris_options i
863 let opt' = opts { opt_ibcsubdir = fp }
864 putIState $ i { idris_options = opt' }
866valIBCSubDir :: IState -> Idris FilePath
867valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
869addImportDir :: FilePath -> Idris ()
870addImportDir fp = do i <- getIState
871 let opts = idris_options i
872 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
873 putIState $ i { idris_options = opt' }
875setImportDirs :: [FilePath] -> Idris ()
876setImportDirs fps = do i <- getIState
877 let opts = idris_options i
878 let opt' = opts { opt_importdirs = fps }
879 putIState $ i { idris_options = opt' }
881allImportDirs :: Idris [FilePath]
882allImportDirs = do i <- getIState
883 let optdirs = opt_importdirs (idris_options i)
884 return ("." : reverse optdirs)
886colourise :: Idris Bool
887colourise = do i <- getIState
888 return $ idris_colourRepl i
890setColourise :: Bool -> Idris ()
891setColourise b = do i <- getIState
892 putIState $ i { idris_colourRepl = b }
894impShow :: Idris Bool
895impShow = do i <- getIState
896 return (opt_showimp (idris_options i))
898setImpShow :: Bool -> Idris ()
899setImpShow t = do i <- getIState
900 let opts = idris_options i
901 let opt' = opts { opt_showimp = t }
902 putIState $ i { idris_options = opt' }
904setColour :: ColourType -> IdrisColour -> Idris ()
905setColour ct c = do i <- getIState
906 let newTheme = setColour' ct c (idris_colourTheme i)
907 putIState $ i { idris_colourTheme = newTheme }
908 where setColour' KeywordColour c t = t { keywordColour = c }
909 setColour' BoundVarColour c t = t { boundVarColour = c }
910 setColour' ImplicitColour c t = t { implicitColour = c }
911 setColour' FunctionColour c t = t { functionColour = c }
912 setColour' TypeColour c t = t { typeColour = c }
913 setColour' DataColour c t = t { dataColour = c }
914 setColour' PromptColour c t = t { promptColour = c }
915 setColour' PostulateColour c t = t { postulateColour = c }
917logLvl :: Int -> String -> Idris ()
918logLvl l str = do i <- getIState
919 let lvl = opt_logLevel (idris_options i)
920 when (lvl >= l) $
921 case idris_outputmode i of
922 RawOutput h -> do runIO $ hPutStrLn h str
923 IdeMode n h ->
924 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
925 runIO . hPutStrLn h $ convSExp "log" good n
927cmdOptType :: Opt -> Idris Bool
928cmdOptType x = do i <- getIState
929 return $ x `elem` opt_cmdline (idris_options i)
931iLOG :: String -> Idris ()
932iLOG = logLvl 1
934noErrors :: Idris Bool
935noErrors = do i <- getIState
936 case errSpan i of
937 Nothing -> return True
938 _ -> return False
940setTypeCase :: Bool -> Idris ()
941setTypeCase t = do i <- getIState
942 let opts = idris_options i
943 let opt' = opts { opt_typecase = t }
944 putIState $ i { idris_options = opt' }
947-- Dealing with parameters
949expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
950 [Name] -> -- all names
951 [Name] -> -- names with no declaration
952 PTerm -> PTerm
953expandParams dec ps ns infs tm = en tm
954 where
955 -- if we shadow a name (say in a lambda binding) that is used in a call to
956 -- a lifted function, we need access to both names - once in the scope of the
957 -- binding and once to call the lifted functions. So we'll explicitly shadow
958 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
959 -- but we didn't...)
961 mkShadow (UN n) = MN 0 n
962 mkShadow (MN i n) = MN (i+1) n
963 mkShadow (NS x s) = NS (mkShadow x) s
965 en (PLam fc n nfc t s)
966 | n `elem` (map fst ps ++ ns)
967 = let n' = mkShadow n in
968 PLam fc n' nfc (en t) (en (shadow n n' s))
969 | otherwise = PLam fc n nfc (en t) (en s)
970 en (PPi p n nfc t s)
971 | n `elem` (map fst ps ++ ns)
972 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
973 PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))
974 | otherwise = PPi (enTacImp p) n nfc (en t) (en s)
975 en (PLet fc n nfc ty v s)
976 | n `elem` (map fst ps ++ ns)
977 = let n' = mkShadow n in
978 PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))
979 | otherwise = PLet fc n nfc (en ty) (en v) (en s)
980 -- FIXME: Should only do this in a type signature!
981 en (PDPair f p (PRef f' n) t r)
982 | n `elem` (map fst ps ++ ns) && t /= Placeholder
983 = let n' = mkShadow n in
984 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
985 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
986 en (PTyped l r) = PTyped (en l) (en r)
987 en (PPair f p l r) = PPair f p (en l) (en r)
988 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
989 en (PAlternative a as) = PAlternative a (map en as)
990 en (PHidden t) = PHidden (en t)
991 en (PUnifyLog t) = PUnifyLog (en t)
992 en (PDisamb ds t) = PDisamb ds (en t)
993 en (PNoImplicits t) = PNoImplicits (en t)
994 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
995 en (PProof ts) = PProof (map (fmap en) ts)
996 en (PTactics ts) = PTactics (map (fmap en) ts)
998 en (PQuote (Var n))
999 | n `nselem` ns = PQuote (Var (dec n))
1000 en (PApp fc (PInferRef fc' n) as)
1001 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
1002 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1003 en (PApp fc (PRef fc' n) as)
1004 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
1005 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1006 | n `nselem` ns = PApp fc (PRef fc' (dec n))
1007 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1008 en (PAppBind fc (PRef fc' n) as)
1009 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
1010 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1011 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
1012 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1013 en (PRef fc n)
1014 | n `elem` infs = PApp fc (PInferRef fc (dec n))
1015 (map (pexp . (PRef fc)) (map fst ps))
1016 | n `nselem` ns = PApp fc (PRef fc (dec n))
1017 (map (pexp . (PRef fc)) (map fst ps))
1018 en (PInferRef fc n)
1019 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
1020 (map (pexp . (PRef fc)) (map fst ps))
1021 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1022 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1023 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1024 en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)
1025 en (PRunElab fc tm) = PRunElab fc (en tm)
1026 en t = t
1028 nselem x [] = False
1029 nselem x (y : xs) | nseq x y = True
1030 | otherwise = nselem x xs
1032 nseq x y = nsroot x == nsroot y
1034 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1035 enTacImp other = other
1037expandParamsD :: Bool -> -- True = RHS only
1038 IState ->
1039 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1040expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1041 = if n `elem` ns && (not rhsonly)
1042 then -- trace (show (n, expandParams dec ps ns ty)) $
1043 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1044 else --trace (show (n, expandParams dec ps ns ty)) $
1045 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1046expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc o n ty)
1047 = if n `elem` ns && (not rhsonly)
1048 then -- trace (show (n, expandParams dec ps ns ty)) $
1049 PPostulate e doc syn fc o (dec n) (piBind ps
1050 (expandParams dec ps ns [] ty))
1051 else --trace (show (n, expandParams dec ps ns ty)) $
1052 PPostulate e doc syn fc o n (expandParams dec ps ns [] ty)
1053expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1054 = let n' = if n `elem` ns then dec n else n in
1055 PClauses fc opts n' (map expandParamsC cs)
1056 where
1057 expandParamsC (PClause fc n lhs ws rhs ds)
1058 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1059 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1060 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1061 n' = if n `elem` ns then dec n else n
1062 -- names bound on the lhs should not be expanded on the rhs
1063 ns' = removeBound lhs ns in
1064 PClause fc n' lhs'
1065 (map (expandParams dec ps'' ns' []) ws)
1066 (expandParams dec ps'' ns' [] rhs)
1067 (map (expandParamsD True ist dec ps'' ns') ds)
1068 expandParamsC (PWith fc n lhs ws wval pn ds)
1069 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1070 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1071 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1072 n' = if n `elem` ns then dec n else n
1073 ns' = removeBound lhs ns in
1074 PWith fc n' lhs'
1075 (map (expandParams dec ps'' ns' []) ws)
1076 (expandParams dec ps'' ns' [] wval)
1077 pn
1078 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1079 updateps yn nm [] = []
1080 updateps yn nm (((a, t), i):as)
1081 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1082 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1084 removeBound lhs ns = ns \\ nub (bnames lhs)
1086 bnames (PRef _ n) = [n]
1087 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1088 bnames (PPair _ _ l r) = bnames l ++ bnames r
1089 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1090 bnames _ = []
1092-- | Expands parameters defined in parameter and where blocks inside of declarations
1093expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1094 = PData doc argDocs syn fc co (expandPData pd)
1095 where
1096 -- just do the type decl, leave constructors alone (parameters will be
1097 -- added implicitly)
1098 expandPData (PDatadecl n nfc ty cons)
1099 = if n `elem` ns
1100 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1101 (map econ cons)
1102 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1103 econ (doc, argDocs, n, nfc, t, fc, fs)
1104 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1105expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1106 = d
1107expandParamsD rhs ist dec ps ns (PParams f params pds)
1108 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1109 (map (expandParamsD True ist dec ps ns) pds)
1110-- (map (expandParamsD ist dec ps ns) pds)
1111expandParamsD rhs ist dec ps ns (PMutual f pds)
1112 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1113expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1114 = PClass doc info f
1115 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1116 n nfc
1117 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1118 pDocs
1119 fds
1120 (map (expandParamsD rhs ist dec ps ns) decls)
1121 cn
1122 cd
1123expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)
1124 = PInstance doc argDocs info f
1125 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1127 nfc
1128 (map (expandParams dec ps ns []) params)
1129 (expandParams dec ps ns [] ty)
1130 cn
1131 (map (expandParamsD rhs ist dec ps ns) decls)
1132expandParamsD rhs ist dec ps ns d = d
1134mapsnd f (x, t) = (x, f t)
1136-- Calculate a priority for a type, for deciding elaboration order
1137-- * if it's just a type variable or concrete type, do it early (0)
1138-- * if there's only type variables and injective constructors, do it next (1)
1139-- * if there's a function type, next (2)
1140-- * finally, everything else (3)
1142getPriority :: IState -> PTerm -> Int
1143getPriority i tm = 1 -- pri tm
1144 where
1145 pri (PRef _ n) =
1146 case lookupP n (tt_ctxt i) of
1147 ((P (DCon _ _ _) _ _):_) -> 1
1148 ((P (TCon _ _) _ _):_) -> 1
1149 ((P Ref _ _):_) -> 1
1150 [] -> 0 -- must be locally bound, if it's not an error...
1151 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1152 pri (PTrue _ _) = 0
1153 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1154 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1155 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1156 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1157 pri (PTyped l r) = pri l
1158 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1159 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1160 pri (PAlternative a as) = maximum (map pri as)
1161 pri (PConstant _ _) = 0
1162 pri Placeholder = 1
1163 pri _ = 3
1166addStatics :: Name -> Term -> PTerm -> Idris ()
1167addStatics n tm ptm =
1168 do let (statics, dynamics) = initStatics tm ptm
1169 ist <- getIState
1170 let paramnames
1171 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1172 Just p -> getNamesFrom 0 (fn_params p) tm ++
1173 concatMap (getParamNames ist) (map snd statics)
1174 _ -> concatMap (getParamNames ist) (map snd statics)
1176 let stnames = nub $ concatMap freeArgNames (map snd statics)
1177 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1178 \\ paramnames
1179 -- also get the arguments which are 'uniquely inferrable' from
1180 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1181 -- or parameters to the type of a static
1182 let statics' = nub $ map fst statics ++
1183 filter (\x -> not (elem x dnames)) stnames
1184 let stpos = staticList statics' tm
1185 i <- getIState
1186 when (not (null statics)) $
1187 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1188 ++ showTmImpls ptm ++ "\n"
1189 ++ show statics ++ "\n" ++ show dynamics
1190 ++ "\n" ++ show paramnames
1191 ++ "\n" ++ show stpos
1192 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1193 addIBC (IBCStatic n)
1194 where
1195 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1196 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1197 (static, (n, ty) : dynamic)
1198 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1199 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1200 if pstatic p == Static then ((n, ty) : static, dynamic)
1201 else if (not (searchArg p))
1202 then (static, (n, ty) : dynamic)
1203 else (static, dynamic)
1204 initStatics t pt = ([], [])
1206 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1207 = case lookupCtxtExact n (idris_datatypes ist) of
1208 Just ti -> getNamePos 0 (param_pos ti) args
1209 Nothing -> []
1210 where getNamePos i ps [] = []
1211 getNamePos i ps (P _ n _ : as)
1212 | i `elem` ps = n : getNamePos (i + 1) ps as
1213 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1214 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1215 = n : getParamNames ist sc
1216 getParamNames ist _ = []
1218 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1219 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1220 | otherwise = getNamesFrom (i + 1) ps sc
1221 getNamesFrom i ps sc = []
1223 freeArgNames (Bind n (Pi _ ty _) sc)
1224 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1225 freeArgNames tm = let (_, args) = unApply tm in
1226 concatMap freeNames args
1228 -- if a name appears in a type class or tactic implicit index, it doesn't
1229 -- affect its 'uniquely inferrable' from a static status since these are
1230 -- resolved by searching.
1231 searchArg (Constraint _ _) = True
1232 searchArg (TacImp _ _ _) = True
1233 searchArg _ = False
1235 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1236 staticList _ _ = []
1238-- Dealing with implicit arguments
1240-- Add some bound implicits to the using block if they aren't there already
1242addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1243addToUsing us [] = us
1244addToUsing us ((n, t) : ns)
1245 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1246 | otherwise = addToUsing us ns
1247 where impName (UImplicit n _) = Just n
1248 impName _ = Nothing
1250-- Add constraint bindings from using block
1252addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1253addUsingConstraints syn fc t
1254 = do ist <- get
1255 let ns = namesIn [] ist t
1256 let cs = getConstraints t -- check declared constraints
1257 let addconsts = uconsts \\ cs
1258 return (doAdd addconsts ns t)
1259 where uconsts = filter uconst (using syn)
1260 uconst (UConstraint _ _) = True
1261 uconst _ = False
1263 doAdd [] _ t = t
1264 -- if all of args in ns, then add it
1265 doAdd (UConstraint c args : cs) ns t
1266 | all (\n -> elem n ns) args
1267 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1268 (mkConst c args) (doAdd cs ns t)
1269 | otherwise = doAdd cs ns t
1271 mkConst c args = PApp fc (PRef fc c)
1272 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1274 getConstraints (PPi (Constraint _ _) _ _ c sc)
1275 = getcapp c ++ getConstraints sc
1276 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1277 getConstraints _ = []
1279 getcapp (PApp _ (PRef _ c) args)
1280 = do ns <- mapM getName args
1281 return (UConstraint c ns)
1282 getcapp _ = []
1284 getName (PExp _ _ _ (PRef _ n)) = return n
1285 getName _ = []
1287-- Add implicit bindings from using block, and bind any missing names
1288addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1289addUsingImpls syn n fc t
1290 = do ist <- getIState
1291 let ns = implicitNamesIn (map iname uimpls) ist t
1292 let badnames = filter (\n -> not (implicitable n) &&
1293 n `notElem` (map iname uimpls)) ns
1294 when (not (null badnames)) $
1295 throwError (At fc (Elaborating "type of " n
1296 (NoSuchVariable (head badnames))))
1297 let cs = getArgnames t -- get already bound names
1298 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1299 -- if all names in the arguments of addconsts appear in ns,
1300 -- add the constraint implicitly
1301 return (bindFree ns (doAdd addimpls ns t))
1302 where uimpls = filter uimpl (using syn)
1303 uimpl (UImplicit _ _) = True
1304 uimpl _ = False
1306 iname (UImplicit n _) = n
1307 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1309 doAdd [] _ t = t
1310 -- if all of args in ns, then add it
1311 doAdd (UImplicit n ty : cs) ns t
1312 | elem n ns
1313 = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)
1314 | otherwise = doAdd cs ns t
1316 -- bind the free names which weren't in the using block
1317 bindFree [] tm = tm
1318 bindFree (n:ns) tm
1319 | elem n (map iname uimpls) = bindFree ns tm
1320 | otherwise
1321 = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1323 getArgnames (PPi _ n _ c sc)
1324 = n : getArgnames sc
1325 getArgnames _ = []
1327-- Given the original type and the elaborated type, return the implicitness
1328-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1330getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1331getUnboundImplicits i t tm = getImps t (collectImps tm)
1332 where collectImps (PPi p n _ t sc)
1333 = (n, (p, t)) : collectImps sc
1334 collectImps _ = []
1336 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1337 getImps (Bind n (Pi _ t _) sc) imps
1338 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1339 where
1340 argInfo n (Imp opt _ _ _) Placeholder
1341 = (True, PImp 0 True opt n Placeholder)
1342 argInfo n (Imp opt _ _ _) t'
1343 = (False, PImp (getPriority i t') True opt n t')
1344 argInfo n (Exp opt _ _) t'
1345 = (InaccessibleArg `elem` opt,
1346 PExp (getPriority i t') opt n t')
1347 argInfo n (Constraint opt _) t'
1348 = (InaccessibleArg `elem` opt,
1349 PConstraint 10 opt n t')
1350 argInfo n (TacImp opt _ scr) t'
1351 = (InaccessibleArg `elem` opt,
1352 PTacImplicit 10 opt n scr t')
1353 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1354 where impBind n t = (True, PImp 1 True [] n Placeholder)
1355 getImps sc tm = []
1357-- Add implicit Pi bindings for any names in the term which appear in an
1358-- argument position.
1360-- This has become a right mess already. Better redo it some time...
1361-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1362-- a couple of places which use it. Clean them up!
1364-- Issue 1739 in the issue tracker
1365-- https://github.com/idris-lang/Idris-dev/issues/1739
1366implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1367implicit info syn n ptm = implicit' info syn [] n ptm
1369implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1370implicit' info syn ignore n ptm
1371 = do i <- getIState
1372 let (tm', impdata) = implicitise syn ignore i ptm
1373 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1374-- let (tm'', spos) = findStatics i tm'
1375 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1376 addIBC (IBCImp n)
1377 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1378-- i <- get
1379-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1380 return tm'
1381 where
1382 -- Detect unknown names in default arguments and throw error if found.
1383 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1384 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1386 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1387 notFoundInDefault kns (PTacImplicit _ _ n script _)
1388 = do i <- getIState
1389 case notFound kns (namesIn [] i script) of
1390 Nothing -> return (n:kns)
1391 Just name -> throwError (NoSuchVariable name)
1392 notFoundInDefault kns p = return ((pname p):kns)
1394 notFound :: [Name] -> [Name] -> Maybe Name
1395 notFound kns [] = Nothing
1396 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1397 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1399implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1400implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1401 let (declimps, ns') = execState (imps True [] tm) ([], [])
1402 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1403 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1404 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1405 if null ns
1406 then (tm, reverse declimps)
1407 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1408 where
1409 uvars = map ipair (filter uimplicit (using syn))
1410 pvars = syn_params syn
1412 inUsing n = n `elem` map fst uvars
1414 ipair (UImplicit x y) = (x, y)
1415 uimplicit (UImplicit _ _) = True
1416 uimplicit _ = False
1418 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1419 | otherwise = x : dropAll xs ys
1420 dropAll [] ys = []
1422 -- Find names in argument position in a type, suitable for implicit
1423 -- binding
1424 -- Not the function position, but do everything else...
1425 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1426 implNamesIn uv t = namesIn uv ist t
1428 imps top env (PApp _ f as)
1429 = do (decls, ns) <- get
1430 let isn = concatMap (namesIn uvars ist) (map getTm as)
1431 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1432 imps top env (PPi (Imp l _ _ _) n _ ty sc)
1433 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1434 (decls , ns) <- get
1435 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1436 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1437 imps True (n:env) sc
1438 imps top env (PPi (Exp l _ _) n _ ty sc)
1439 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1440 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1441 _ -> [])
1442 (decls, ns) <- get -- ignore decls in HO types
1443 put (PExp (getPriority ist ty) l n Placeholder : decls,
1444 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1445 imps True (n:env) sc
1446 imps top env (PPi (Constraint l _) n _ ty sc)
1447 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1448 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1449 _ -> [])
1450 (decls, ns) <- get -- ignore decls in HO types
1451 put (PConstraint 10 l n Placeholder : decls,
1452 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1453 imps True (n:env) sc
1454 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1455 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1456 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1457 _ -> [])
1458 (decls, ns) <- get -- ignore decls in HO types
1459 put (PTacImplicit 10 l n scr Placeholder : decls,
1460 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1461 imps True (n:env) sc
1462 imps top env (PRewrite _ l r _)
1463 = do (decls, ns) <- get
1464 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1465 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1466 imps top env (PTyped l r)
1467 = imps top env l
1468 imps top env (PPair _ _ l r)
1469 = do (decls, ns) <- get
1470 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1471 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1472 imps top env (PDPair _ _ (PRef _ n) t r)
1473 = do (decls, ns) <- get
1474 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1475 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1476 imps top env (PDPair _ _ l t r)
1477 = do (decls, ns) <- get
1478 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1479 namesIn uvars ist r
1480 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1481 imps top env (PAlternative a as)
1482 = do (decls, ns) <- get
1483 let isn = concatMap (namesIn uvars ist) as
1484 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1485 imps top env (PLam fc n _ ty sc)
1486 = do imps False env ty
1487 imps False (n:env) sc
1488 imps top env (PHidden tm) = imps False env tm
1489 imps top env (PUnifyLog tm) = imps False env tm
1490 imps top env (PNoImplicits tm) = imps False env tm
1491 imps top env (PRunElab fc tm) = imps False env tm
1492 imps top env _ = return ()
1494 pibind using [] sc = sc
1495 pibind using (n:ns) sc
1496 = case lookup n using of
1497 Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)
1498 Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder
1499 (pibind using ns sc)
1501-- Add implicit arguments in function calls
1502addImplPat :: IState -> PTerm -> PTerm
1503addImplPat = addImpl' True [] [] []
1505addImplBound :: IState -> [Name] -> PTerm -> PTerm
1506addImplBound ist ns = addImpl' False ns [] [] ist
1508addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1509addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1511-- | Add the implicit arguments to applications in the term
1512-- [Name] gives the names to always expend, even when under a binder of
1513-- that name (this is to expand methods with implicit arguments in dependent
1514-- type classes).
1515addImpl :: [Name] -> IState -> PTerm -> PTerm
1516addImpl = addImpl' False [] []
1518-- TODO: in patterns, don't add implicits to function names guarded by constructors
1519-- and *not* inside a PHidden
1521addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1522addImpl' inpat env infns imp_meths ist ptm
1523 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1524 where
1525 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1526 ai qq env ds (PRef fc f)
1527 | f `elem` infns = PInferRef fc f
1528 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds []
1529 ai qq env ds (PHidden (PRef fc f))
1530 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds [])
1531 ai qq env ds (PRewrite fc l r g)
1532 = let l' = ai qq env ds l
1533 r' = ai qq env ds r
1534 g' = fmap (ai qq env ds) g in
1535 PRewrite fc l' r' g'
1536 ai qq env ds (PTyped l r)
1537 = let l' = ai qq env ds l
1538 r' = ai qq env ds r in
1539 PTyped l' r'
1540 ai qq env ds (PPair fc p l r)
1541 = let l' = ai qq env ds l
1542 r' = ai qq env ds r in
1543 PPair fc p l' r'
1544 ai qq env ds (PDPair fc p l t r)
1545 = let l' = ai qq env ds l
1546 t' = ai qq env ds t
1547 r' = ai qq env ds r in
1548 PDPair fc p l' t' r'
1549 ai qq env ds (PAlternative a as)
1550 = let as' = map (ai qq env ds) as in
1551 PAlternative a as'
1552 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1553 ai qq env ds (PApp fc (PInferRef ffc f) as)
1554 = let as' = map (fmap (ai qq env ds)) as in
1555 PApp fc (PInferRef ffc f) as'
1556 ai qq env ds (PApp fc ftm@(PRef ffc f) as)
1557 | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc f) as)
1558 | not (f `elem` map fst env)
1559 = let as' = map (fmap (ai qq env ds)) as in
1560 handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'
1561 | Just (Just ty) <- lookup f env =
1562 let as' = map (fmap (ai qq env ds)) as
1563 arity = getPArity ty in
1564 mkPApp fc arity ftm as'
1565 ai qq env ds (PApp fc f as)
1566 = let f' = ai qq env ds f
1567 as' = map (fmap (ai qq env ds)) as in
1568 mkPApp fc 1 f' as'
1569 ai qq env ds (PCase fc c os)
1570 = let c' = ai qq env ds c in
1571 -- leave os alone, because they get lifted into a new pattern match
1572 -- definition which is passed through addImpl again with more scope
1573 -- information
1574 PCase fc c' os
1576 ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)
1577 (ai qq env ds t)
1578 (ai qq env ds f)
1580 -- If the name in a lambda is a constructor name, do this as a 'case'
1581 -- instead (it is harmless to do so, especially since the lambda will
1582 -- be lifted anyway!)
1583 ai qq env ds (PLam fc n nfc ty sc)
1584 = case lookupDef n (tt_ctxt ist) of
1585 [] -> let ty' = ai qq env ds ty
1586 sc' = ai qq ((n, Just ty):env) ds sc in
1587 PLam fc n nfc ty' sc'
1588 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1589 (PCase fc (PRef fc (sMN 0 "lamp") )
1590 [(PRef fc n, sc)]))
1591 ai qq env ds (PLet fc n nfc ty val sc)
1592 = case lookupDef n (tt_ctxt ist) of
1593 [] -> let ty' = ai qq env ds ty
1594 val' = ai qq env ds val
1595 sc' = ai qq ((n, Just ty):env) ds sc in
1596 PLet fc n nfc ty' val' sc'
1597 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1598 ai qq env ds (PPi p n nfc ty sc)
1599 = let ty' = ai qq env ds ty
1600 env' = if n `elem` imp_meths then env
1601 else ((n, Just ty) : env)
1602 sc' = ai qq env' ds sc in
1603 PPi p n nfc ty' sc'
1604 ai qq env ds (PGoal fc r n sc)
1605 = let r' = ai qq env ds r
1606 sc' = ai qq ((n, Nothing):env) ds sc in
1607 PGoal fc r' n sc'
1608 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1609 -- Don't do PProof or PTactics since implicits get added when scope is
1610 -- properly known in ElabTerm.runTac
1611 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1612 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1613 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1614 (fmap (ai True env ds) g)
1615 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1616 ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)
1617 ai qq env ds tm = tm
1619 handleErr (Left err) = PElabError err
1620 handleErr (Right x) = x
1622-- if in a pattern, and there are no arguments, and there's no possible
1623-- names with zero explicit arguments, don't add implicits.
1625aiFn :: Bool -> Bool -> Bool
1626 -> [Name]
1627 -> IState -> FC
1628 -> Name -- ^ function being applied
1629 -> FC -> [[T.Text]]
1630 -> [PArg] -- ^ initial arguments
1631 -> Either Err PTerm
1632aiFn inpat True qq imp_meths ist fc f ffc ds []
1633 = case lookupDef f (tt_ctxt ist) of
1634 [] -> Right $ PPatvar ffc f
1635 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1636 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1637 if (not (vname f) || tcname f
1638 || any (conCaf (tt_ctxt ist)) ialts)
1639-- any constructor alts || any allImp ialts))
1640 then aiFn inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1641 else Right $ PPatvar ffc f
1642 where imp (PExp _ _ _ _) = False
1643 imp _ = True
1644-- allImp [] = False
1645 allImp xs = all imp xs
1646 constructor (TyDecl (DCon _ _ _) _) = True
1647 constructor _ = False
1649 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1651 vname (UN n) = True -- non qualified
1652 vname _ = False
1654aiFn inpat expat qq imp_meths ist fc f ffc ds as
1655 | f `elem` primNames = Right $ PApp fc (PRef ffc f) as
1656aiFn inpat expat qq imp_meths ist fc f ffc ds as
1657 -- This is where namespaces get resolved by adding PAlternative
1658 = do let ns = lookupCtxtName f (idris_implicits ist)
1659 let nh = filter (\(n, _) -> notHidden n) ns
1660 let ns' = case trimAlts ds nh of
1661 [] -> nh
1662 x -> x
1663 case ns' of
1664 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc (isImpName f f')) (insertImpl ns as)
1665 [] -> if f `elem` (map fst (idris_metavars ist))
1666 then Right $ PApp fc (PRef ffc f) as
1667 else Right $ mkPApp fc (length as) (PRef ffc f) as
1668 alts -> Right $
1669 PAlternative (ExactlyOne True) $
1670 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc (isImpName f f'))
1671 (insertImpl ns as)) alts
1672 where
1673 -- if the name is in imp_meths, we should actually refer to the bound
1674 -- name rather than the global one after expanding implicits
1675 isImpName f f' | f `elem` imp_meths = f
1676 | otherwise = f'
1678 trimAlts [] alts = alts
1679 trimAlts ns alts
1680 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1682 nspace (NS _ s) = s
1683 nspace _ = []
1685 notHidden n = case getAccessibility n of
1686 Hidden -> False
1687 _ -> True
1689 getAccessibility n
1690 = case lookupDefAccExact n False (tt_ctxt ist) of
1691 Just (n,t) -> t
1692 _ -> Public
1694 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1695 -> [PArg] -- ^ given arguments
1696 -> [PArg]
1697 insertImpl ps as
1698 = let (as', badimpls) = partition (impIn ps) as in
1699 map addUnknownImp badimpls ++
1700 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1702 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1703 -> [PArg] -- parameters
1704 -> [PArg] -- explicit arguments
1705 -> [PArg] -- implicits given
1706 -> [PArg]
1707 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1708 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1709 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1710 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1711 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1712 let rtc = PResolveTC fc in
1713 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1714 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1715 case find n imps [] of
1716 Just (tm, imps') ->
1717 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1718 Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
1719 PImp p True l n ph :
1720 insImpAcc (M.insert n ph pnas) ps given imps
1721 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1722 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1723 case find n imps [] of
1724 Just (tm, imps') ->
1725 PTacImplicit p l n sc tm :
1726 insImpAcc (M.insert n tm pnas) ps given imps'
1727 Nothing ->
1728 if inpat
1729 then PTacImplicit p l n sc Placeholder :
1730 insImpAcc (M.insert n Placeholder pnas) ps given imps
1731 else PTacImplicit p l n sc sc :
1732 insImpAcc (M.insert n sc pnas) ps given imps
1733 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1734 insImpAcc _ _ given imps = given ++ imps
1736 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1738 find n [] acc = Nothing
1739 find n (PImp _ _ _ n' t : gs) acc
1740 | n == n' = Just (t, reverse acc ++ gs)
1741 find n (PTacImplicit _ _ n' _ t : gs) acc
1742 | n == n' = Just (t, reverse acc ++ gs)
1743 find n (g : gs) acc = find n gs (g : acc)
1745-- return True if the second argument is an implicit argument which is
1746-- expected in the implicits, or if it's not an implicit
1747impIn :: [PArg] -> PArg -> Bool
1748impIn ps (PExp _ _ _ _) = True
1749impIn ps (PConstraint _ _ _ _) = True
1750impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1752expArg (PExp _ _ _ _) = True
1753expArg (PConstraint _ _ _ _) = True
1754expArg _ = False
1756-- replace non-linear occurrences with _
1758stripLinear :: IState -> PTerm -> PTerm
1759stripLinear i tm = evalState (sl tm) [] where
1760 sl :: PTerm -> State [Name] PTerm
1761 sl (PRef fc f)
1762 | (_:_) <- lookupTy f (tt_ctxt i)
1763 = return $ PRef fc f
1764 | otherwise = do ns <- get
1765 if (f `elem` ns)
1766 then return $ PHidden (PRef fc f) -- Placeholder
1767 else do put (f : ns)
1768 return (PRef fc f)
1769 sl (PPatvar fc f)
1770 = do ns <- get
1771 if (f `elem` ns)
1772 then return $ PHidden (PPatvar fc f) -- Placeholder
1773 else do put (f : ns)
1774 return (PPatvar fc f)
1775 -- Assumption is that variables are all the same in each alternative
1776 sl t@(PAlternative b as) = do ns <- get
1777 as' <- slAlts ns as
1778 return (PAlternative b as')
1779 where slAlts ns (a : as) = do put ns
1780 a' <- sl a
1781 as' <- slAlts ns as
1782 return (a' : as')
1783 slAlts ns [] = return []
1784 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1785 sl (PDPair fc p l t r) = do l' <- sl l
1786 t' <- sl t
1787 r' <- sl r
1788 return (PDPair fc p l' t' r')
1789 sl (PApp fc fn args) = do fn' <- case fn of
1790 -- Just the args, fn isn't matchable as a var
1791 PRef _ _ -> return fn
1792 t -> sl t
1793 args' <- mapM slA args
1794 return $ PApp fc fn' args'
1795 where slA (PImp p m l n t) = do t' <- sl t
1796 return $ PImp p m l n t'
1797 slA (PExp p l n t) = do t' <- sl t
1798 return $ PExp p l n t'
1799 slA (PConstraint p l n t)
1800 = do t' <- sl t
1801 return $ PConstraint p l n t'
1802 slA (PTacImplicit p l n sc t)
1803 = do t' <- sl t
1804 return $ PTacImplicit p l n sc t'
1805 sl x = return x
1807-- | Remove functions which aren't applied to anything, which must then
1808-- be resolved by unification. Assume names resolved and alternatives
1809-- filled in (so no ambiguity).
1810stripUnmatchable :: IState -> PTerm -> PTerm
1811stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1812 su :: PTerm -> PTerm
1813 su (PRef fc f)
1814 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1815 = Placeholder
1816 su (PApp fc f@(PRef _ fn) args)
1817 -- here we use canBeDConName because the impossible pattern
1818 -- check will not necessarily fully resolve constructor names,
1819 -- and these bare names will otherwise get in the way of
1820 -- impossbility checking.
1821 | canBeDConName fn ctxt
1822 = PApp fc f (fmap (fmap su) args)
1823 su (PApp fc f args)
1824 = PHidden (PApp fc f args)
1825 su (PAlternative b alts)
1826 = let alts' = filter (/= Placeholder) (map su alts) in
1827 if null alts' then Placeholder
1828 else PAlternative b alts'
1829 su (PPair fc p l r) = PPair fc p (su l) (su r)
1830 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1831 su t@(PLam fc _ _ _ _) = PHidden t
1832 su t@(PPi _ _ _ _ _) = PHidden t
1833 su t = t
1835 ctxt = tt_ctxt i
1837stripUnmatchable i tm = tm
1839mkPApp fc a f [] = f
1840mkPApp fc a f as = let rest = drop a as in
1841 if a == 0 then appRest fc f rest
1842 else appRest fc (PApp fc f (take a as)) rest
1843 where
1844 appRest fc f [] = f
1845 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1847-- Find 'static' argument positions
1848-- (the declared ones, plus any names in argument position in the declared
1849-- statics)
1850-- FIXME: It's possible that this really has to happen after elaboration
1852findStatics :: IState -> PTerm -> (PTerm, [Bool])
1853findStatics ist tm = trace (show tm) $
1854 let (ns, ss) = fs tm in
1855 runState (pos ns ss tm) []
1856 where fs (PPi p n fc t sc)
1857 | Static <- pstatic p
1858 = let (ns, ss) = fs sc in
1859 (namesIn [] ist t : ns, n : ss)
1860 | otherwise = let (ns, ss) = fs sc in
1861 (ns, ss)
1862 fs _ = ([], [])
1864 inOne n ns = length (filter id (map (elem n) ns)) == 1
1866 pos ns ss (PPi p n fc t sc)
1867 | elem n ss = do sc' <- pos ns ss sc
1868 spos <- get
1869 put (True : spos)
1870 return (PPi (p { pstatic = Static }) n fc t sc')
1871 | otherwise = do sc' <- pos ns ss sc
1872 spos <- get
1873 put (False : spos)
1874 return (PPi p n fc t sc')
1875 pos ns ss t = return t
1877-- for 6.12/7 compatibility
1878data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1880instance Applicative (EitherErr a) where
1881 pure = return
1882 (<*>) = ap
1884instance Monad (EitherErr a) where
1885 return = RightOK
1887 (LeftErr e) >>= k = LeftErr e
1888 RightOK v >>= k = k v
1890toEither (LeftErr e) = Left e
1891toEither (RightOK ho) = Right ho
1893-- | Syntactic match of a against b, returning pair of variables in a
1894-- and what they match. Returns the pair that failed if not a match.
1895matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1896matchClause = matchClause' False
1898matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1899matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1900 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1902 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1903 fullApp x = x
1905 match' x y = match (fullApp x) (fullApp y)
1906 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1907 | fi == txt "fromInteger" && b == txt "builtins",
1908 PConstant _ (I _) <- getTm x = match (getTm x) x'
1909 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1910 | fi == txt "fromInteger" && b == txt "builtins",
1911 PConstant _ (I _) <- getTm x = match (getTm x) x'
1912 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1913 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1914 match (PApp _ f args) (PApp _ f' args')
1915 | length args == length args'
1916 = do mf <- match' f f'
1917 ms <- zipWithM matchArg args args'
1918 return (mf ++ concat ms)
1919 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1920 match (PPatvar f n) xr = match (PRef f n) xr
1921 match xr (PPatvar f n) = match xr (PRef f n)
1922 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1923 match (PRef _ n) tm@(PRef _ n')
1924 | n == n' && not names &&
1925 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1926 || tm == Placeholder)
1927 = return [(n, tm)]
1928 -- if one namespace is missing, drop the other
1929 | n == n' || n == dropNS n' || dropNS n == n' = return []
1930 where dropNS (NS n _) = n
1931 dropNS n = n
1932 match (PRef _ n) tm
1933 | not names && (not (isConName n (tt_ctxt i) ||
1934 isFnName n (tt_ctxt i)) || tm == Placeholder)
1935 = return [(n, tm)]
1936 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1937 = do ml <- match' l l'
1938 mr <- match' r r'
1939 return (ml ++ mr)
1940 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1941 mr <- match r r'
1942 return (ml ++ mr)
1943 match (PTyped l r) x = match l x
1944 match x (PTyped l r) = match x l
1945 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1946 mr <- match' r r'
1947 return (ml ++ mr)
1948 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1949 mt <- match' t t'
1950 mr <- match' r r'
1951 return (ml ++ mt ++ mr)
1952 match (PAlternative a as) (PAlternative a' as')
1953 = do ms <- zipWithM match' as as'
1954 return (concat ms)
1955 match a@(PAlternative _ as) b
1956 = do let ms = zipWith match' as (repeat b)
1957 case (rights (map toEither ms)) of
1958 (x: _) -> return x
1959 _ -> LeftErr (a, b)
1960 match (PCase _ _ _) _ = return [] -- lifted out
1961 match (PMetavar _ _) _ = return [] -- modified
1962 match (PInferRef _ _) _ = return [] -- modified
1963 match (PQuote _) _ = return []
1964 match (PProof _) _ = return []
1965 match (PTactics _) _ = return []
1966 match (PResolveTC _) (PResolveTC _) = return []
1967 match (PTrue _ _) (PTrue _ _) = return []
1968 match (PReturn _) (PReturn _) = return []
1969 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
1970 ms <- match' s s'
1971 return (mt ++ ms)
1972 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
1973 ms <- match' s s'
1974 return (mt ++ ms)
1975 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
1976 mty <- match' ty ty'
1977 ms <- match' s s'
1978 return (mt ++ mty ++ ms)
1979 match (PHidden x) (PHidden y)
1980 | RightOK xs <- match x y = return xs -- to collect variables
1981 | otherwise = return [] -- Otherwise hidden things are unmatchable
1982 match (PHidden x) y
1983 | RightOK xs <- match x y = return xs
1984 | otherwise = return []
1985 match x (PHidden y)
1986 | RightOK xs <- match x y = return xs
1987 | otherwise = return []
1988 match (PUnifyLog x) y = match' x y
1989 match x (PUnifyLog y) = match' x y
1990 match (PNoImplicits x) y = match' x y
1991 match x (PNoImplicits y) = match' x y
1992 match Placeholder _ = return []
1993 match _ Placeholder = return []
1994 match (PResolveTC _) _ = return []
1995 match a b | a == b = return []
1996 | otherwise = LeftErr (a, b)
1998 checkRpts (RightOK ms) = check ms where
1999 check ((n,t):xs)
2000 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2001 then Left (t, t')
2002 else check xs
2003 check (_:xs) = check xs
2004 check [] = Right ms
2005 checkRpts (LeftErr x) = Left x
2007substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2008substMatches ms = substMatchesShadow ms []
2010substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2011substMatchesShadow [] shs t = t
2012substMatchesShadow ((n,tm):ns) shs t
2013 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2015substMatch :: Name -> PTerm -> PTerm -> PTerm
2016substMatch n = substMatchShadow n []
2018substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2019substMatchShadow n shs tm t = sm shs t where
2020 sm xs (PRef _ n') | n == n' = tm
2021 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2022 sm xs (PPi p x fc t sc)
2023 | x `elem` xs
2024 = let x' = nextName x in
2025 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC x') t))
2026 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
2027 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2028 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2029 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2030 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2031 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2032 (fmap (sm xs) tm)
2033 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2034 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
2035 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
2036 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
2037 sm xs (PHidden x) = PHidden (sm xs x)
2038 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2039 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2040 sm xs (PRunElab fc script) = PRunElab fc (sm xs script)
2041 sm xs x = x
2043 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2044 fullApp x = x
2046shadow :: Name -> Name -> PTerm -> PTerm
2047shadow n n' t = sm t where
2048 sm (PRef fc x) | n == x = PRef fc n'
2049 sm (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm t) (sm sc)
2050 | otherwise = PLam fc x xfc (sm t) sc
2051 sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)
2052 | otherwise = PPi p x fc (sm t) sc
2053 sm (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm t) (sm v) (sm sc)
2054 | otherwise = PLet fc x xfc (sm t) (sm v) sc
2055 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
2056 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
2057 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
2058 sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)
2059 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
2060 sm (PTyped x y) = PTyped (sm x) (sm y)
2061 sm (PPair f p x y) = PPair f p (sm x) (sm y)
2062 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
2063 sm (PAlternative a as) = PAlternative a (map sm as)
2064 sm (PTactics ts) = PTactics (map (fmap sm) ts)
2065 sm (PProof ts) = PProof (map (fmap sm) ts)
2066 sm (PHidden x) = PHidden (sm x)
2067 sm (PUnifyLog x) = PUnifyLog (sm x)
2068 sm (PNoImplicits x) = PNoImplicits (sm x)
2069 sm x = x
2071-- Rename any binders which are repeated (so that we don't have to mess
2072-- about with shadowing anywhere else).
2074mkUniqueNames :: [Name] -> PTerm -> PTerm
2075mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2076 inScope :: S.Set Name
2077 inScope = S.fromList $ boundNamesIn tm
2079 mkUniqA arg = do t' <- mkUniq (getTm arg)
2080 return (arg { getTm = t' })
2082 -- Initialise the unique name with the environment length (so we're not
2083 -- looking for too long...)
2084 initN (UN n) l = UN $ txt (str n ++ show l)
2085 initN (MN i s) l = MN (i+l) s
2086 initN n l = n
2088 -- FIXME: Probably ought to do this for completeness! It's fine as
2089 -- long as there are no bindings inside tactics though.
2090 mkUniqT tac = return tac
2092 mkUniq :: PTerm -> State (S.Set Name) PTerm
2093 mkUniq (PLam fc n nfc ty sc)
2094 = do env <- get
2095 (n', sc') <-
2096 if n `S.member` env
2097 then do let n' = uniqueNameSet (initN n (S.size env))
2098 (S.union env inScope)
2099 return (n', shadow n n' sc)
2100 else return (n, sc)
2101 put (S.insert n' env)
2102 ty' <- mkUniq ty
2103 sc'' <- mkUniq sc'
2104 return $! PLam fc n' nfc ty' sc''
2105 mkUniq (PPi p n fc ty sc)
2106 = do env <- get
2107 (n', sc') <-
2108 if n `S.member` env
2109 then do let n' = uniqueNameSet (initN n (S.size env))
2110 (S.union env inScope)
2111 return (n', shadow n n' sc)
2112 else return (n, sc)
2113 put (S.insert n' env)
2114 ty' <- mkUniq ty
2115 sc'' <- mkUniq sc'
2116 return $! PPi p n' fc ty' sc''
2117 mkUniq (PLet fc n nfc ty val sc)
2118 = do env <- get
2119 (n', sc') <-
2120 if n `S.member` env
2121 then do let n' = uniqueNameSet (initN n (S.size env))
2122 (S.union env inScope)
2123 return (n', shadow n n' sc)
2124 else return (n, sc)
2125 put (S.insert n' env)
2126 ty' <- mkUniq ty; val' <- mkUniq val
2127 sc'' <- mkUniq sc'
2128 return $! PLet fc n' nfc ty' val' sc''
2129 mkUniq (PApp fc t args)
2130 = do t' <- mkUniq t
2131 args' <- mapM mkUniqA args
2132 return $! PApp fc t' args'
2133 mkUniq (PAppBind fc t args)
2134 = do t' <- mkUniq t
2135 args' <- mapM mkUniqA args
2136 return $! PAppBind fc t' args'
2137 mkUniq (PCase fc t alts)
2138 = do t' <- mkUniq t
2139 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2140 return (x', y')) alts
2141 return $! PCase fc t' alts'
2142 mkUniq (PIfThenElse fc c t f)
2143 = liftM3 (PIfThenElse fc) (mkUniq c) (mkUniq t) (mkUniq f)
2144 mkUniq (PPair fc p l r)
2145 = do l' <- mkUniq l; r' <- mkUniq r
2146 return $! PPair fc p l' r'
2147 mkUniq (PDPair fc p (PRef fc' n) t sc)
2148 | t /= Placeholder
2149 = do env <- get
2150 (n', sc') <- if n `S.member` env
2151 then do let n' = uniqueNameSet n (S.union env inScope)
2152 return (n', shadow n n' sc)
2153 else return (n, sc)
2154 put (S.insert n' env)
2155 t' <- mkUniq t
2156 sc'' <- mkUniq sc'
2157 return $! PDPair fc p (PRef fc' n') t' sc''
2158 mkUniq (PDPair fc p l t r)
2159 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2160 return $! PDPair fc p l' t' r'
2161 mkUniq (PAlternative b as)
2162 = liftM (PAlternative b) (mapM mkUniq as)
2163 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2164 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2165 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2166 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2167 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2168 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2169 mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)
2170 mkUniq t = return t