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