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