2Module : Idris.AbsSyntax
3Description : Provides Idris' core data definitions and utility code.
6Maintainer : The Idris Community.
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
9 TypeSynonymInstances, PatternGuards #-}
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
13 , module Idris.AbsSyntaxTree
17import Idris.Core.Evaluate
18import Idris.Core.Elaborate hiding (Tactic(..))
19import Idris.Core.Typecheck
20import Idris.AbsSyntaxTree
22import Idris.Docstrings
23import Idris.IdeMode hiding (Opt(..))
24import IRTS.CodegenCommon
25import Util.DynamicLinker
27import System.Console.Haskeline
29import System.Directory (canonicalizePath, doesFileExist)
31import Control.Applicative
32import Control.Monad (liftM3)
33import Control.Monad.State
35import Data.List hiding (insert,union)
37import qualified Data.Text as T
39import qualified Data.Map as M
41import qualified Data.Set as S
42import Data.Word (Word)
44import Data.Generics.Uniplate.Data (descend, descendM)
48import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
54getContext :: Idris Context
55getContext = do i <- getIState; return (tt_ctxt i)
57forCodegen :: Codegen -> [(Codegen, a)] -> [a]
58forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
60 eqLang (Via _ x) (Via _ y) = x == y
61 eqLang Bytecode Bytecode = True
64getObjectFiles :: Codegen -> Idris [FilePath]
65getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
67addObjectFile :: Codegen -> FilePath -> Idris ()
68addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
70getLibs :: Codegen -> Idris [String]
71getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
73addLib :: Codegen -> String -> Idris ()
74addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
76getFlags :: Codegen -> Idris [String]
77getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
79addFlag :: Codegen -> String -> Idris ()
80addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
82addDyLib :: [String] -> Idris (Either DynamicLib String)
83addDyLib libs = do i <- getIState
84 let ls = idris_dynamic_libs i
85 let importdirs = opt_importdirs (idris_options i)
86 case mapMaybe (findDyLib ls) libs of
87 x:_ -> return (Left x)
89 handle <- lift . lift .
90 mapM (\l -> catchIO (tryLoadLib importdirs l)
91 (\_ -> return Nothing)) $ libs
93 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
94 intercalate "," libs ++ "\"")
95 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
97 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
98 findDyLib [] l = Nothing
99 findDyLib (lib:libs) l | l == lib_name lib = Just lib
100 | otherwise = findDyLib libs l
102getAutoImports :: Idris [FilePath]
103getAutoImports = do i <- getIState
104 return (opt_autoImport (idris_options i))
106addAutoImport :: FilePath -> Idris ()
107addAutoImport fp = do i <- getIState
108 let opts = idris_options i
109 let autoimps = opt_autoImport opts
110 put (i { idris_options = opts { opt_autoImport =
111 fp : opt_autoImport opts } } )
113addDefinedName :: Name -> Idris ()
114addDefinedName n = do ist <- getIState
115 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
117getDefinedNames :: Idris [Name]
118getDefinedNames = do ist <- getIState
119 return (S.toList (idris_inmodule ist))
121addTT :: Term -> Idris (Maybe Term)
122addTT t = do ist <- getIState
123 case M.lookup t (idris_ttstats ist) of
124 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
125 putIState $ ist { idris_ttstats = tt' }
127 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
128 putIState $ ist { idris_ttstats = tt' }
132dumpTT = do ist <- get
133 let sts = sortBy count (M.toList (idris_ttstats ist))
137 count (_,x) (_,y) = compare y x
138 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
140addHdr :: Codegen -> String -> Idris ()
141addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
143addImported :: Bool -> FilePath -> Idris ()
146 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
148addLangExt :: LanguageExt -> Idris ()
149addLangExt TypeProviders = do i <- getIState
151 idris_language_extensions = TypeProviders : idris_language_extensions i
153addLangExt ErrorReflection = do i <- getIState
155 idris_language_extensions = ErrorReflection : idris_language_extensions i
158-- | Transforms are organised by the function being applied on the lhs
159-- of the transform, to make looking up appropriate transforms quicker
160addTrans :: Name -> (Term, Term) -> Idris ()
163 let t' = case lookupCtxtExact basefn (idris_transforms i) of
164 Just def -> (t : def)
166 putIState $ i { idris_transforms = addDef basefn t'
167 (idris_transforms i) }
169addErrRev :: (Term, Term) -> Idris ()
170addErrRev t = do i <- getIState
171 putIState $ i { idris_errRev = t : idris_errRev i }
173addErasureUsage :: Name -> Int -> Idris ()
174addErasureUsage n i = do ist <- getIState
175 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
177addExport :: Name -> Idris ()
178addExport n = do ist <- getIState
179 putIState $ ist { idris_exports = n : idris_exports ist }
181addUsedName :: FC -> Name -> Name -> Idris ()
183 = do ist <- getIState
184 case lookupTyName n (tt_ctxt ist) of
185 [(n', ty)] -> addUsage n' 0 ty
186 [] -> throwError (At fc (NoSuchVariable n))
187 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
188 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
190 | otherwise = addUsage n (i + 1) sc
191 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
193getErasureUsage :: Idris [(Name, Int)]
194getErasureUsage = do ist <- getIState;
195 return (idris_erasureUsed ist)
197getExports :: Idris [Name]
198getExports = do ist <- getIState
199 return (idris_exports ist)
201totcheck :: (FC, Name) -> Idris ()
202totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
204defer_totcheck :: (FC, Name) -> Idris ()
207 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
209clear_totcheck :: Idris ()
210clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
212setFlags :: Name -> [FnOpt] -> Idris ()
213setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
215setFnInfo :: Name -> FnInfo -> Idris ()
216setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
218setAccessibility :: Name -> Accessibility -> Idris ()
221 let ctxt = setAccess n a (tt_ctxt i)
222 putIState $ i { tt_ctxt = ctxt }
224-- | get the accessibility of a name outside this module
225getFromHideList :: Name -> Idris (Maybe Accessibility)
226getFromHideList n = do i <- getIState
227 return $ lookupCtxtExact n (hide_list i)
229setTotality :: Name -> Totality -> Idris ()
232 let ctxt = setTotal n a (tt_ctxt i)
233 putIState $ i { tt_ctxt = ctxt }
235setInjectivity :: Name -> Injectivity -> Idris ()
238 let ctxt = setInjective n a (tt_ctxt i)
239 putIState $ i { tt_ctxt = ctxt }
241getTotality :: Name -> Idris Totality
244 case lookupTotal n (tt_ctxt i) of
246 _ -> return (Total [])
248-- Get coercions which might return the required type
249getCoercionsTo :: IState -> Type -> [Name]
251 let cs = idris_coercions i
252 (fn,_) = unApply (getRetTy ty) in
254 where findCoercions t [] = []
255 findCoercions t (n : ns) =
256 let ps = case lookupTy n (tt_ctxt i) of
257 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
258 (t', _) -> [n | t == t']
260 ps ++ findCoercions t ns
262addToCG :: Name -> CGInfo -> Idris ()
265 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
267addCalls :: Name -> [Name] -> Idris ()
270 case lookupCtxtExact n (idris_callgraph i) of
271 Nothing -> addToCG n (CGInfo calls [] [])
272 Just (CGInfo cs scg used) ->
273 addToCG n (CGInfo (nub (calls ++ cs)) scg used)
275addTyInferred :: Name -> Idris ()
278 putIState $ i { idris_tyinfodata =
279 addDef n TIPartial (idris_tyinfodata i) }
281addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
282addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
283 mapM_ addConstraint ts
285 where addConstraint (x, y) = findMVApps x y
288 = do let (fx, argsx) = unApply x
289 let (fy, argsy) = unApply y
294 else mapM_ addConstraint (zip argsx argsy)
296 tryAddMV (P _ mv _) y =
298 case lookup mv (idris_metavars ist) of
299 Just _ -> addConstraintRule mv y
301 tryAddMV _ _ = return ()
303 addConstraintRule :: Name -> Term -> Idris ()
304 addConstraintRule n t
306 logLvl 1 $ "TI constraint: " ++ show (n, t)
307 case lookupCtxt n (idris_tyinfodata ist) of
309 do mapM_ (checkConsistent t) ts
310 let ti' = addDef n (TISolution (t : ts))
311 (idris_tyinfodata ist)
312 put $ ist { idris_tyinfodata = ti' }
314 do let ti' = addDef n (TISolution [t])
315 (idris_tyinfodata ist)
316 put $ ist { idris_tyinfodata = ti' }
318 -- Check a solution is consistent with previous solutions
319 -- Meaning: If heads are both data types, they had better be the
321 checkConsistent :: Term -> Term -> Idris ()
322 checkConsistent x y =
323 do let (fx, _) = unApply x
324 let (fy, _) = unApply y
326 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
327 (P (TCon _ _) n _, Constant _) -> errWhen True
328 (Constant _, P (TCon _ _) n' _) -> errWhen True
329 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
334 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
335 errWhen False = return ()
337isTyInferred :: Name -> Idris Bool
340 case lookupCtxt n (idris_tyinfodata i) of
341 [TIPartial] -> return True
344-- | Adds error handlers for a particular function and argument. If
345-- names are ambiguous, all matching handlers are updated.
346addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
347addFunctionErrorHandlers f arg hs =
349 let oldHandlers = idris_function_errorhandlers i
350 let newHandlers = flip (addDef f) oldHandlers $
351 case lookupCtxtExact f oldHandlers of
352 Nothing -> M.singleton arg (S.fromList hs)
353 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
354 -- will always be one of those two, thus no extra case
355 putIState $ i { idris_function_errorhandlers = newHandlers }
357getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
358getFunctionErrorHandlers f arg = do i <- getIState
359 return . maybe [] S.toList $
360 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
363-- | Trace all the names in a call graph starting at the given name
364getAllNames :: Name -> Idris [Name]
365getAllNames n = allNames [] n
367allNames :: [Name] -> Name -> Idris [Name]
368allNames ns n | n `elem` ns = return []
369allNames ns n = do i <- getIState
370 case lookupCtxtExact n (idris_callgraph i) of
371 Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')
372 return (nub (n : concat more))
375addCoercion :: Name -> Idris ()
376addCoercion n = do i <- getIState
377 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
379addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
382 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
384addNameHint :: Name -> Name -> Idris ()
387 ty' <- case lookupCtxtName ty (idris_implicits i) of
388 [(tyn, _)] -> return tyn
389 [] -> throwError (NoSuchVariable ty)
390 tyns -> throwError (CantResolveAlts (map fst tyns))
391 let ns' = case lookupCtxt ty' (idris_namehints i) of
394 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
396getNameHints :: IState -> Name -> [Name]
397getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
399 case lookupCtxt n (idris_namehints i) of
403addDeprecated :: Name -> String -> Idris ()
404addDeprecated n reason = do
406 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
408getDeprecated :: Name -> Idris (Maybe String)
411 return $ lookupCtxtExact n (idris_deprecated i)
414addFragile :: Name -> String -> Idris ()
415addFragile n reason = do
417 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
419getFragile :: Name -> Idris (Maybe String)
422 return $ lookupCtxtExact n (idris_fragile i)
424push_estack :: Name -> Bool -> Idris ()
427 putIState (i { elab_stack = (n, inst) : elab_stack i })
429pop_estack :: Idris ()
430pop_estack = do i <- getIState
431 putIState (i { elab_stack = ptail (elab_stack i) })
435-- | Add a class instance function.
437-- Precondition: the instance should have the correct type.
439-- Dodgy hack 1: Put integer instances first in the list so they are
440-- resolved by default.
442-- Dodgy hack 2: put constraint chasers (ParentN) last
443addInstance :: Bool -- ^ whether the name is an Integer instance
444 -> Bool -- ^ whether to include the instance in instance search
445 -> Name -- ^ the name of the class
446 -> Name -- ^ the name of the instance
448addInstance int res n i
449 = do ist <- getIState
450 case lookupCtxt n (idris_classes ist) of
451 [CI a b c d e ins fds] ->
452 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
453 putIState $ ist { idris_classes = cs }
454 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)
455 putIState $ ist { idris_classes = cs }
456 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
457 addI i ins | int = (i, res) : ins
458 | chaser n = ins ++ [(i, res)]
459 | otherwise = insI i ins
460 insI i [] = [(i, res)]
461 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
462 | otherwise = n : insI i ns
464 chaser (SN (ParentN _ _)) = True
465 chaser (NS n _) = chaser n
468-- | Add a privileged implementation - one which instance search will
469-- happily resolve immediately if it is type correct This is used for
470-- naming parent implementations when defining an implementation with
471-- constraints. Returns the old list, so we can revert easily at the
473addOpenImpl :: [Name] -> Idris [Name]
474addOpenImpl ns = do ist <- getIState
475 ns' <- mapM (checkValid ist) ns
476 let open = idris_openimpls ist
477 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
481 = case lookupCtxtName n (idris_implicits ist) of
482 [(n', _)] -> return n'
483 [] -> throwError (NoSuchVariable n)
484 more -> throwError (CantResolveAlts (map fst more))
486setOpenImpl :: [Name] -> Idris ()
487setOpenImpl ns = do ist <- getIState
488 putIState $ ist { idris_openimpls = ns }
490getOpenImpl :: Idris [Name]
491getOpenImpl = do ist <- getIState
492 return (idris_openimpls ist)
494addClass :: Name -> ClassInfo -> Idris ()
496 = do ist <- getIState
497 let i' = case lookupCtxt n (idris_classes ist) of
498 [c] -> c { class_instances = class_instances i }
500 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
502addRecord :: Name -> RecordInfo -> Idris ()
503addRecord n ri = do ist <- getIState
504 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
506addAutoHint :: Name -> Name -> Idris ()
509 case lookupCtxtExact n (idris_autohints ist) of
511 do let hs = addDef n [hint] (idris_autohints ist)
512 putIState $ ist { idris_autohints = hs }
514 do let hs = addDef n (hint : nhints) (idris_autohints ist)
515 putIState $ ist { idris_autohints = hs }
517getAutoHints :: Name -> Idris [Name]
518getAutoHints n = do ist <- getIState
519 case lookupCtxtExact n (idris_autohints ist) of
523addIBC :: IBCWrite -> Idris ()
526 when (notDef (ibc_write i)) $
527 putIState $ i { ibc_write = ibc : ibc_write i }
528 where notDef [] = True
529 notDef (IBCDef n': is) | n == n' = False
530 notDef (_ : is) = notDef is
531addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
534clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
535 idris_inmodule = S.empty }
537resetNameIdx :: Idris ()
538resetNameIdx = do i <- getIState
539 put (i { idris_nameIdx = (0, emptyContext) })
541-- | Used to preserve sharing of names
542addNameIdx :: Name -> Idris (Int, Name)
543addNameIdx n = do i <- getIState
544 let (i', x) = addNameIdx' i n
548addNameIdx' :: IState -> Name -> (IState, (Int, Name))
550 = let idxs = snd (idris_nameIdx i) in
551 case lookupCtxt n idxs of
553 _ -> let i' = fst (idris_nameIdx i) + 1 in
554 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
556getSymbol :: Name -> Idris Name
557getSymbol n = do i <- getIState
558 case M.lookup n (idris_symbols i) of
560 Nothing -> do let sym' = M.insert n n (idris_symbols i)
561 put (i { idris_symbols = sym' })
564getHdrs :: Codegen -> Idris [String]
565getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
567getImported :: Idris [(FilePath, Bool)]
568getImported = do i <- getIState; return (idris_imported i)
570setErrSpan :: FC -> Idris ()
571setErrSpan x = do i <- getIState;
573 Nothing -> putIState $ i { errSpan = Just x }
577clearErr = do i <- getIState
578 putIState $ i { errSpan = Nothing }
580getSO :: Idris (Maybe String)
581getSO = do i <- getIState
582 return (compiled_so i)
584setSO :: Maybe String -> Idris ()
585setSO s = do i <- getIState
586 putIState (i { compiled_so = s })
588getIState :: Idris IState
591putIState :: IState -> Idris ()
594updateIState :: (IState -> IState) -> Idris ()
595updateIState f = do i <- getIState
598withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
599withContext ctx name dflt action = do
601 case lookupCtxt name (ctx ist) of
605withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
606withContext_ ctx name action = withContext ctx name () action
608-- | A version of liftIO that puts errors into the exception type of
610runIO :: IO a -> Idris a
611runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
612-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
614-- Issue #1738 on the issue tracker.
615-- https://github.com/idris-lang/Idris-dev/issues/1738
618getName = do i <- getIState;
619 let idx = idris_name i;
620 putIState (i { idris_name = idx + 1 })
623-- | InternalApp keeps track of the real function application for
624-- making case splits from, not the application the programmer wrote,
625-- which doesn't have the whole context in any case other than top
627addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
630 -- We canonicalise the path to make "./Test/Module.idr" equal
631 -- to "Test/Module.idr"
632 exists <- runIO $ doesFileExist fp
634 do fp' <- runIO $ canonicalizePath fp
635 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
637getInternalApp :: FilePath -> Int -> Idris PTerm
638getInternalApp fp l = do i <- getIState
639 -- We canonicalise the path to make
640 -- "./Test/Module.idr" equal to
642 exists <- runIO $ doesFileExist fp
644 then do fp' <- runIO $ canonicalizePath fp
645 case lookup (fp', l) (idris_lineapps i) of
647 Nothing -> return Placeholder
648 -- TODO: What if it's not there?
649 else return Placeholder
651-- | Pattern definitions are only used for coverage checking, so erase
652-- them when we're done
653clearOrigPats :: Idris ()
654clearOrigPats = do i <- get
655 let ps = idris_patdefs i
656 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
657 put (i { idris_patdefs = ps' })
659-- | Erase types from Ps in the context (basically ending up with
660-- what's in the .ibc, which is all we need after all the analysis is
662clearPTypes :: Idris ()
663clearPTypes = do i <- get
665 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
666 where pErase (CaseOp c t tys orig tot cds)
667 = CaseOp c t tys orig [] (pErase' cds)
669 pErase' (CaseDefs _ (cs, c) _ rs)
670 = let c' = (cs, fmap pEraseType c) in
673checkUndefined :: FC -> Name -> Idris ()
677 (_:_) -> throwError . Msg $ show fc ++ ":" ++
678 show n ++ " already defined"
681isUndefined :: FC -> Name -> Idris Bool
684 case lookupTyExact n i of
685 Just _ -> return False
688setContext :: Context -> Idris ()
689setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
691updateContext :: (Context -> Context) -> Idris ()
692updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
694addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
695addConstraints fc (v, cs)
696 = do tit <- typeInType
700 let ctxt' = ctxt { next_tvar = v }
701 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
702 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
705 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
706 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
707 insertAll ((c, fc) : cs) ics
708 = insertAll cs $ S.insert (ConstraintFC c fc) ics
710addDeferred = addDeferred' Ref
711addDeferredTyCon = addDeferred' (TCon 0 0)
713-- | Save information about a name that is not yet defined
714addDeferred' :: NameType
715 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
716 -- ^ The Name is the name being made into a metavar,
717 -- the Int is the number of vars that are part of a
718 -- putative proof context, the Maybe Name is the
719 -- top-level function containing the new metavariable,
720 -- the Type is its type, and the Bool is whether :p is
724 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
725 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
727 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
728 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
731 -- 'tidyNames' is to generate user accessible names in case they are
732 -- needed in tactic scripts
733 tidyNames used (Bind (MN i x) b sc)
734 = let n' = uniqueNameSet (UN x) used in
735 Bind n' b $ tidyNames (S.insert n' used) sc
736 tidyNames used (Bind n b sc)
737 = let n' = uniqueNameSet n used in
738 Bind n' b $ tidyNames (S.insert n' used) sc
741solveDeferred :: FC -> Name -> Idris ()
744 case lookup n (idris_metavars i) of
745 Just (_, _, _, _, False) ->
746 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
747 _ -> putIState $ i { idris_metavars =
748 filter (\(n', _) -> n/=n')
751 filter (notMV n) (ibc_write i)
753 where notMV n (IBCMetavar n') = not (n == n')
756getUndefined :: Idris [Name]
757getUndefined = do i <- getIState
758 return (map fst (idris_metavars i) \\ primDefs)
760isMetavarName :: Name -> IState -> Bool
762 = case lookupNames n (tt_ctxt ist) of
763 (t:_) -> isJust $ lookup t (idris_metavars ist)
766getWidth :: Idris ConsoleWidth
767getWidth = fmap idris_consolewidth getIState
769setWidth :: ConsoleWidth -> Idris ()
770setWidth w = do ist <- getIState
771 put ist { idris_consolewidth = w }
773setDepth :: Maybe Int -> Idris ()
774setDepth d = do ist <- getIState
775 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
777typeDescription :: String
778typeDescription = "The type of types"
781type1Doc :: Doc OutputAnnotation
782type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
785isetPrompt :: String -> Idris ()
786isetPrompt p = do i <- getIState
787 case idris_outputmode i of
788 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
790-- | Tell clients how much was parsed and loaded
791isetLoadedRegion :: Idris ()
792isetLoadedRegion = do i <- getIState
793 let span = idris_parsedSpan i
796 case idris_outputmode i of
798 runIO . hPutStrLn h $
799 convSExp "set-loaded-region" fc n
802setLogLevel :: Int -> Idris ()
803setLogLevel l = do i <- getIState
804 let opts = idris_options i
805 let opt' = opts { opt_logLevel = l }
806 putIState $ i { idris_options = opt' }
808setLogCats :: [LogCat] -> Idris ()
811 let opts = idris_options i
812 let opt' = opts { opt_logcats = cs }
813 putIState $ i { idris_options = opt' }
815setCmdLine :: [Opt] -> Idris ()
816setCmdLine opts = do i <- getIState
817 let iopts = idris_options i
818 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
820getCmdLine :: Idris [Opt]
821getCmdLine = do i <- getIState
822 return (opt_cmdline (idris_options i))
824getDumpHighlighting :: Idris Bool
825getDumpHighlighting = do ist <- getIState
826 return (findC (opt_cmdline (idris_options ist)))
827 where findC = elem DumpHighlights
829getDumpDefun :: Idris (Maybe FilePath)
830getDumpDefun = do i <- getIState
831 return $ findC (opt_cmdline (idris_options i))
832 where findC [] = Nothing
833 findC (DumpDefun x : _) = Just x
834 findC (_ : xs) = findC xs
836getDumpCases :: Idris (Maybe FilePath)
837getDumpCases = do i <- getIState
838 return $ findC (opt_cmdline (idris_options i))
839 where findC [] = Nothing
840 findC (DumpCases x : _) = Just x
841 findC (_ : xs) = findC xs
844logLevel = do i <- getIState
845 return (opt_logLevel (idris_options i))
847setAutoImpls :: Bool -> Idris ()
848setAutoImpls b = do i <- getIState
849 let opts = idris_options i
850 let opt' = opts { opt_autoimpls = b }
851 putIState $ i { idris_options = opt' }
853getAutoImpls :: Idris Bool
854getAutoImpls = do i <- getIState
855 return (opt_autoimpls (idris_options i))
857setErrContext :: Bool -> Idris ()
858setErrContext t = do i <- getIState
859 let opts = idris_options i
860 let opts' = opts { opt_errContext = t }
861 putIState $ i { idris_options = opts' }
863errContext :: Idris Bool
864errContext = do i <- getIState
865 return (opt_errContext (idris_options i))
867getOptimise :: Idris [Optimisation]
868getOptimise = do i <- getIState
869 return (opt_optimise (idris_options i))
871setOptimise :: [Optimisation] -> Idris ()
872setOptimise newopts = do i <- getIState
873 let opts = idris_options i
874 let opts' = opts { opt_optimise = newopts }
875 putIState $ i { idris_options = opts' }
877addOptimise :: Optimisation -> Idris ()
878addOptimise opt = do opts <- getOptimise
879 setOptimise (nub (opt : opts))
881removeOptimise :: Optimisation -> Idris ()
882removeOptimise opt = do opts <- getOptimise
883 setOptimise ((nub opts) \\ [opt])
885-- | Set appropriate optimisation set for the given level. We only
886-- have one optimisation that is configurable at the moment, however!
887setOptLevel :: Int -> Idris ()
888setOptLevel n | n <= 0 = setOptimise []
889setOptLevel 1 = setOptimise []
890setOptLevel 2 = setOptimise [PETransform]
891setOptLevel n | n >= 3 = setOptimise [PETransform]
894useREPL = do i <- getIState
895 return (opt_repl (idris_options i))
897setREPL :: Bool -> Idris ()
898setREPL t = do i <- getIState
899 let opts = idris_options i
900 let opt' = opts { opt_repl = t }
901 putIState $ i { idris_options = opt' }
903showOrigErr :: Idris Bool
904showOrigErr = do i <- getIState
905 return (opt_origerr (idris_options i))
907setShowOrigErr :: Bool -> Idris ()
908setShowOrigErr b = do i <- getIState
909 let opts = idris_options i
910 let opt' = opts { opt_origerr = b }
911 putIState $ i { idris_options = opt' }
913setAutoSolve :: Bool -> Idris ()
914setAutoSolve b = do i <- getIState
915 let opts = idris_options i
916 let opt' = opts { opt_autoSolve = b }
917 putIState $ i { idris_options = opt' }
919setNoBanner :: Bool -> Idris ()
920setNoBanner n = do i <- getIState
921 let opts = idris_options i
922 let opt' = opts { opt_nobanner = n }
923 putIState $ i { idris_options = opt' }
925getNoBanner :: Idris Bool
926getNoBanner = do i <- getIState
927 let opts = idris_options i
928 return (opt_nobanner opts)
930setEvalTypes :: Bool -> Idris ()
931setEvalTypes n = do i <- getIState
932 let opts = idris_options i
933 let opt' = opts { opt_evaltypes = n }
934 putIState $ i { idris_options = opt' }
936getDesugarNats :: Idris Bool
937getDesugarNats = do i <- getIState
938 let opts = idris_options i
939 return (opt_desugarnats opts)
942setDesugarNats :: Bool -> Idris ()
943setDesugarNats n = do i <- getIState
944 let opts = idris_options i
945 let opt' = opts { opt_desugarnats = n }
946 putIState $ i { idris_options = opt' }
948setQuiet :: Bool -> Idris ()
949setQuiet q = do i <- getIState
950 let opts = idris_options i
951 let opt' = opts { opt_quiet = q }
952 putIState $ i { idris_options = opt' }
954getQuiet :: Idris Bool
955getQuiet = do i <- getIState
956 let opts = idris_options i
957 return (opt_quiet opts)
959setCodegen :: Codegen -> Idris ()
960setCodegen t = do i <- getIState
961 let opts = idris_options i
962 let opt' = opts { opt_codegen = t }
963 putIState $ i { idris_options = opt' }
965codegen :: Idris Codegen
966codegen = do i <- getIState
967 return (opt_codegen (idris_options i))
970setOutputTy :: OutputType -> Idris ()
971setOutputTy t = do i <- getIState
972 let opts = idris_options i
973 let opt' = opts { opt_outputTy = t }
974 putIState $ i { idris_options = opt' }
976outputTy :: Idris OutputType
977outputTy = do i <- getIState
978 return $ opt_outputTy $ idris_options i
980setIdeMode :: Bool -> Handle -> Idris ()
981setIdeMode True h = do i <- getIState
982 putIState $ i { idris_outputmode = IdeMode 0 h
983 , idris_colourRepl = False
985setIdeMode False _ = return ()
987setTargetTriple :: String -> Idris ()
988setTargetTriple t = do i <- getIState
989 let opts = idris_options i
990 opt' = opts { opt_triple = t }
991 putIState $ i { idris_options = opt' }
993targetTriple :: Idris String
994targetTriple = do i <- getIState
995 return (opt_triple (idris_options i))
997setTargetCPU :: String -> Idris ()
998setTargetCPU t = do i <- getIState
999 let opts = idris_options i
1000 opt' = opts { opt_cpu = t }
1001 putIState $ i { idris_options = opt' }
1003targetCPU :: Idris String
1004targetCPU = do i <- getIState
1005 return (opt_cpu (idris_options i))
1007verbose :: Idris Bool
1008verbose = do i <- getIState
1009 -- Quietness overrides verbosity
1010 return (not (opt_quiet (idris_options i)) &&
1011 opt_verbose (idris_options i))
1013setVerbose :: Bool -> Idris ()
1014setVerbose t = do i <- getIState
1015 let opts = idris_options i
1016 let opt' = opts { opt_verbose = t }
1017 putIState $ i { idris_options = opt' }
1019typeInType :: Idris Bool
1020typeInType = do i <- getIState
1021 return (opt_typeintype (idris_options i))
1023setTypeInType :: Bool -> Idris ()
1024setTypeInType t = do i <- getIState
1025 let opts = idris_options i
1026 let opt' = opts { opt_typeintype = t }
1027 putIState $ i { idris_options = opt' }
1029coverage :: Idris Bool
1030coverage = do i <- getIState
1031 return (opt_coverage (idris_options i))
1033setCoverage :: Bool -> Idris ()
1034setCoverage t = do i <- getIState
1035 let opts = idris_options i
1036 let opt' = opts { opt_coverage = t }
1037 putIState $ i { idris_options = opt' }
1039setIBCSubDir :: FilePath -> Idris ()
1040setIBCSubDir fp = do i <- getIState
1041 let opts = idris_options i
1042 let opt' = opts { opt_ibcsubdir = fp }
1043 putIState $ i { idris_options = opt' }
1045valIBCSubDir :: IState -> Idris FilePath
1046valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1048addImportDir :: FilePath -> Idris ()
1049addImportDir fp = do i <- getIState
1050 let opts = idris_options i
1051 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1052 putIState $ i { idris_options = opt' }
1054setImportDirs :: [FilePath] -> Idris ()
1055setImportDirs fps = do i <- getIState
1056 let opts = idris_options i
1057 let opt' = opts { opt_importdirs = fps }
1058 putIState $ i { idris_options = opt' }
1060allImportDirs :: Idris [FilePath]
1061allImportDirs = do i <- getIState
1062 let optdirs = opt_importdirs (idris_options i)
1063 return ("." : reverse optdirs)
1065colourise :: Idris Bool
1066colourise = do i <- getIState
1067 return $ idris_colourRepl i
1069setColourise :: Bool -> Idris ()
1070setColourise b = do i <- getIState
1071 putIState $ i { idris_colourRepl = b }
1073impShow :: Idris Bool
1074impShow = do i <- getIState
1075 return (opt_showimp (idris_options i))
1077setImpShow :: Bool -> Idris ()
1078setImpShow t = do i <- getIState
1079 let opts = idris_options i
1080 let opt' = opts { opt_showimp = t }
1081 putIState $ i { idris_options = opt' }
1083setColour :: ColourType -> IdrisColour -> Idris ()
1084setColour ct c = do i <- getIState
1085 let newTheme = setColour' ct c (idris_colourTheme i)
1086 putIState $ i { idris_colourTheme = newTheme }
1087 where setColour' KeywordColour c t = t { keywordColour = c }
1088 setColour' BoundVarColour c t = t { boundVarColour = c }
1089 setColour' ImplicitColour c t = t { implicitColour = c }
1090 setColour' FunctionColour c t = t { functionColour = c }
1091 setColour' TypeColour c t = t { typeColour = c }
1092 setColour' DataColour c t = t { dataColour = c }
1093 setColour' PromptColour c t = t { promptColour = c }
1094 setColour' PostulateColour c t = t { postulateColour = c }
1097logLvl :: Int -> String -> Idris ()
1098logLvl = logLvlCats []
1100logCoverage :: Int -> String -> Idris ()
1101logCoverage = logLvlCats [ICoverage]
1103logErasure :: Int -> String -> Idris ()
1104logErasure = logLvlCats [IErasure]
1106-- | Log an action of the parser
1107logParser :: Int -> String -> Idris ()
1108logParser = logLvlCats parserCats
1110-- | Log an action of the elaborator.
1111logElab :: Int -> String -> Idris ()
1112logElab = logLvlCats elabCats
1114-- | Log an action of the compiler.
1115logCodeGen :: Int -> String -> Idris ()
1116logCodeGen = logLvlCats codegenCats
1118logIBC :: Int -> String -> Idris ()
1119logIBC = logLvlCats [IIBC]
1121-- | Log aspect of Idris execution
1123-- An empty set of logging levels is used to denote all categories.
1125-- @TODO update IDE protocol
1126logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1127 -> Int -- ^ The Logging level the message should appear.
1128 -> String -- ^ The message to show the developer.
1130logLvlCats cs l str = do
1132 let lvl = opt_logLevel (idris_options i)
1133 let cats = opt_logcats (idris_options i)
1135 when (inCat cs cats || null cats) $
1136 case idris_outputmode i of
1138 runIO $ hPutStrLn h str
1140 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1141 runIO . hPutStrLn h $ convSExp "log" good n
1143 inCat :: [LogCat] -> [LogCat] -> Bool
1144 inCat cs cats = any (`elem` cats) cs
1146cmdOptType :: Opt -> Idris Bool
1147cmdOptType x = do i <- getIState
1148 return $ x `elem` opt_cmdline (idris_options i)
1150noErrors :: Idris Bool
1151noErrors = do i <- getIState
1153 Nothing -> return True
1156setTypeCase :: Bool -> Idris ()
1157setTypeCase t = do i <- getIState
1158 let opts = idris_options i
1159 let opt' = opts { opt_typecase = t }
1160 putIState $ i { idris_options = opt' }
1163-- Dealing with parameters
1165expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1166 [Name] -> -- all names
1167 [Name] -> -- names with no declaration
1169expandParams dec ps ns infs tm = en 0 tm
1171 -- if we shadow a name (say in a lambda binding) that is used in a call to
1172 -- a lifted function, we need access to both names - once in the scope of the
1173 -- binding and once to call the lifted functions. So we'll explicitly shadow
1174 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1175 -- but we didn't...)
1177 mkShadow (UN n) = MN 0 n
1178 mkShadow (MN i n) = MN (i+1) n
1179 mkShadow (NS x s) = NS (mkShadow x) s
1181 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1182 -- that are merely mentioned.
1184 en 0 (PLam fc n nfc t s)
1185 | n `elem` (map fst ps ++ ns)
1186 = let n' = mkShadow n in
1187 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1188 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1189 en 0 (PPi p n nfc t s)
1190 | n `elem` (map fst ps ++ ns)
1191 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1192 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1193 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1194 en 0 (PLet fc n nfc ty v s)
1195 | n `elem` (map fst ps ++ ns)
1196 = let n' = mkShadow n in
1197 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1198 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1199 -- FIXME: Should only do this in a type signature!
1200 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1201 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1202 = let n' = mkShadow n in
1203 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1204 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1205 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1206 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1207 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1208 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1209 en 0 (PHidden t) = PHidden (en 0 t)
1210 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1211 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1212 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1213 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1214 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1215 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1217 en 0 (PQuote (Var n))
1218 | n `nselem` ns = PQuote (Var (dec n))
1219 en 0 (PApp fc (PInferRef fc' hl n) as)
1220 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1221 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1222 en 0 (PApp fc (PRef fc' hl n) as)
1223 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1224 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1225 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1226 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1227 en 0 (PAppBind fc (PRef fc' hl n) as)
1228 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1229 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1230 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1231 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1233 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1234 (map ((pexp . (PRef fc hl)) . fst) ps)
1235 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1236 (map ((pexp . (PRef fc hl)) . fst) ps)
1237 en 0 (PInferRef fc hl n)
1238 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1239 (map ((pexp . (PRef fc hl)) . fst) ps)
1240 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1241 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1242 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1243 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1244 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1245 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1247 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1248 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1250 en ql t = descend (en ql) t
1253 nselem x (y : xs) | nseq x y = True
1254 | otherwise = nselem x xs
1256 nseq x y = nsroot x == nsroot y
1258 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1259 enTacImp ql other = other
1261expandParamsD :: Bool -> -- True = RHS only
1263 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1264expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1265 = if n `elem` ns && (not rhsonly)
1266 then -- trace (show (n, expandParams dec ps ns ty)) $
1267 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1268 else --trace (show (n, expandParams dec ps ns ty)) $
1269 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1270expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1271 = if n `elem` ns && (not rhsonly)
1272 then -- trace (show (n, expandParams dec ps ns ty)) $
1273 PPostulate e doc syn fc nfc o (dec n)
1274 (piBind ps (expandParams dec ps ns [] ty))
1275 else --trace (show (n, expandParams dec ps ns ty)) $
1276 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1277expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1278 = let n' = if n `elem` ns then dec n else n in
1279 PClauses fc opts n' (map expandParamsC cs)
1281 expandParamsC (PClause fc n lhs ws rhs ds)
1282 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1283 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1284 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1285 n' = if n `elem` ns then dec n else n
1286 -- names bound on the lhs should not be expanded on the rhs
1287 ns' = removeBound lhs ns in
1289 (map (expandParams dec ps'' ns' []) ws)
1290 (expandParams dec ps'' ns' [] rhs)
1291 (map (expandParamsD True ist dec ps'' ns') ds)
1292 expandParamsC (PWith fc n lhs ws wval pn ds)
1293 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1294 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1295 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1296 n' = if n `elem` ns then dec n else n
1297 ns' = removeBound lhs ns in
1299 (map (expandParams dec ps'' ns' []) ws)
1300 (expandParams dec ps'' ns' [] wval)
1302 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1303 updateps yn nm [] = []
1304 updateps yn nm (((a, t), i):as)
1305 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1306 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1308 removeBound lhs ns = ns \\ nub (bnames lhs)
1310 bnames (PRef _ _ n) = [n]
1311 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1312 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1313 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1316-- | Expands parameters defined in parameter and where blocks inside of declarations
1317expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1318 = PData doc argDocs syn fc co (expandPData pd)
1320 -- just do the type decl, leave constructors alone (parameters will be
1321 -- added implicitly)
1322 expandPData (PDatadecl n nfc ty cons)
1324 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1326 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1327 econ (doc, argDocs, n, nfc, t, fc, fs)
1328 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1329expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1331expandParamsD rhs ist dec ps ns (PParams f params pds)
1332 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1333 (map (expandParamsD True ist dec ps ns) pds)
1334-- (map (expandParamsD ist dec ps ns) pds)
1335expandParamsD rhs ist dec ps ns (PMutual f pds)
1336 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1337expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1339 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1341 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1344 (map (expandParamsD rhs ist dec ps ns) decls)
1347expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1348 = let cn' = case cn of
1349 Just n -> if n `elem` ns then Just (dec n) else Just n
1350 Nothing -> Nothing in
1351 PInstance doc argDocs info f
1352 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1355 (map (expandParams dec ps ns []) params)
1356 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1357 (expandParams dec ps ns [] ty)
1359 (map (expandParamsD True ist dec ps ns) decls)
1360expandParamsD rhs ist dec ps ns d = d
1362mapsnd f (x, t) = (x, f t)
1364expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1365 = PInstance doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1367expandInstanceScope ist dec ps ns d = d
1369-- | Calculate a priority for a type, for deciding elaboration order
1370-- * if it's just a type variable or concrete type, do it early (0)
1371-- * if there's only type variables and injective constructors, do it next (1)
1372-- * if there's a function type, next (2)
1373-- * finally, everything else (3)
1374getPriority :: IState -> PTerm -> Int
1375getPriority i tm = 1 -- pri tm
1378 case lookupP n (tt_ctxt i) of
1379 ((P (DCon _ _ _) _ _):_) -> 1
1380 ((P (TCon _ _) _ _):_) -> 1
1381 ((P Ref _ _):_) -> 1
1382 [] -> 0 -- must be locally bound, if it's not an error...
1383 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1385 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1386 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1387 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1388 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1389 pri (PTyped l r) = pri l
1390 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1391 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1392 pri (PAlternative _ a as) = maximum (map pri as)
1393 pri (PConstant _ _) = 0
1398addStatics :: Name -> Term -> PTerm -> Idris ()
1399addStatics n tm ptm =
1400 do let (statics, dynamics) = initStatics tm ptm
1403 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1404 Just p -> getNamesFrom 0 (fn_params p) tm ++
1405 concatMap (getParamNames ist . snd) statics
1406 _ -> concatMap (getParamNames ist . snd) statics
1408 let stnames = nub $ concatMap (freeArgNames . snd) statics
1409 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1411 -- also get the arguments which are 'uniquely inferrable' from
1412 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1413 -- or parameters to the type of a static
1414 let statics' = nub $ map fst statics ++
1415 filter (\x -> not (elem x dnames)) stnames
1416 let stpos = staticList statics' tm
1418 unless (null statics) $
1419 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1420 ++ showTmImpls ptm ++ "\n"
1421 ++ show statics ++ "\n" ++ show dynamics
1422 ++ "\n" ++ show paramnames
1423 ++ "\n" ++ show stpos
1424 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1425 addIBC (IBCStatic n)
1427 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1428 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1429 (static, (n, ty) : dynamic)
1430 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1431 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1432 if pstatic p == Static then ((n, ty) : static, dynamic)
1433 else if (not (searchArg p))
1434 then (static, (n, ty) : dynamic)
1435 else (static, dynamic)
1436 initStatics t pt = ([], [])
1438 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1439 = case lookupCtxtExact n (idris_datatypes ist) of
1440 Just ti -> getNamePos 0 (param_pos ti) args
1442 where getNamePos i ps [] = []
1443 getNamePos i ps (P _ n _ : as)
1444 | i `elem` ps = n : getNamePos (i + 1) ps as
1445 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1446 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1447 = n : getParamNames ist sc
1448 getParamNames ist _ = []
1450 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1451 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1452 | otherwise = getNamesFrom (i + 1) ps sc
1453 getNamesFrom i ps sc = []
1455 freeArgNames (Bind n (Pi _ ty _) sc)
1456 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1457 freeArgNames tm = let (_, args) = unApply tm in
1458 concatMap freeNames args
1460 -- if a name appears in a type class or tactic implicit index, it doesn't
1461 -- affect its 'uniquely inferrable' from a static status since these are
1462 -- resolved by searching.
1463 searchArg (Constraint _ _) = True
1464 searchArg (TacImp _ _ _) = True
1467 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1470-- Dealing with implicit arguments
1472-- Add some bound implicits to the using block if they aren't there already
1474addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1475addToUsing us [] = us
1476addToUsing us ((n, t) : ns)
1477 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1478 | otherwise = addToUsing us ns
1479 where impName (UImplicit n _) = Just n
1482-- Add constraint bindings from using block
1484addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1485addUsingConstraints syn fc t
1487 let ns = namesIn [] ist t
1488 let cs = getConstraints t -- check declared constraints
1489 let addconsts = uconsts \\ cs
1490 return (doAdd addconsts ns t)
1491 where uconsts = filter uconst (using syn)
1492 uconst (UConstraint _ _) = True
1496 -- if all of args in ns, then add it
1497 doAdd (UConstraint c args : cs) ns t
1498 | all (\n -> elem n ns) args
1499 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1500 (mkConst c args) (doAdd cs ns t)
1501 | otherwise = doAdd cs ns t
1503 mkConst c args = PApp fc (PRef fc [] c)
1504 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1506 getConstraints (PPi (Constraint _ _) _ _ c sc)
1507 = getcapp c ++ getConstraints sc
1508 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1509 getConstraints _ = []
1511 getcapp (PApp _ (PRef _ _ c) args)
1512 = do ns <- mapM getName args
1513 return (UConstraint c ns)
1516 getName (PExp _ _ _ (PRef _ _ n)) = return n
1519-- | Add implicit bindings from using block, and bind any missing names
1520addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1521addUsingImpls syn n fc t
1522 = do ist <- getIState
1523 autoimpl <- getAutoImpls
1524 let ns_in = implicitNamesIn (map iname uimpls) ist t
1525 let ns = if autoimpl then ns_in
1526 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1528 let badnames = filter (\n -> not (implicitable n) &&
1529 n `notElem` (map iname uimpls)) ns
1530 unless (null badnames) $
1531 throwError (At fc (Elaborating "type of " n Nothing
1532 (NoSuchVariable (head badnames))))
1533 let cs = getArgnames t -- get already bound names
1534 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1535 -- if all names in the arguments of addconsts appear in ns,
1536 -- add the constraint implicitly
1537 return (bindFree ns (doAdd addimpls ns t))
1538 where uimpls = filter uimpl (using syn)
1539 uimpl (UImplicit _ _) = True
1542 iname (UImplicit n _) = n
1543 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1546 -- if all of args in ns, then add it
1547 doAdd (UImplicit n ty : cs) ns t
1549 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1550 | otherwise = doAdd cs ns t
1552 -- bind the free names which weren't in the using block
1555 | elem n (map iname uimpls) = bindFree ns tm
1557 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1559 getArgnames (PPi _ n _ c sc)
1560 = n : getArgnames sc
1563-- Given the original type and the elaborated type, return the implicitness
1564-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1566getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1567getUnboundImplicits i t tm = getImps t (collectImps tm)
1568 where collectImps (PPi p n _ t sc)
1569 = (n, (p, t)) : collectImps sc
1572 scopedimpl (Just i) = not (toplevel_imp i)
1573 scopedimpl _ = False
1575 getImps (Bind n (Pi i _ _) sc) imps
1576 | scopedimpl i = getImps sc imps
1577 getImps (Bind n (Pi _ t _) sc) imps
1578 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1580 argInfo n (Imp opt _ _ _ _) Placeholder
1581 = (True, PImp 0 True opt n Placeholder)
1582 argInfo n (Imp opt _ _ _ _) t'
1583 = (False, PImp (getPriority i t') True opt n t')
1584 argInfo n (Exp opt _ _) t'
1585 = (InaccessibleArg `elem` opt,
1586 PExp (getPriority i t') opt n t')
1587 argInfo n (Constraint opt _) t'
1588 = (InaccessibleArg `elem` opt,
1589 PConstraint 10 opt n t')
1590 argInfo n (TacImp opt _ scr) t'
1591 = (InaccessibleArg `elem` opt,
1592 PTacImplicit 10 opt n scr t')
1593 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1594 where impBind n t = (True, PImp 1 True [] n Placeholder)
1597-- Add implicit Pi bindings for any names in the term which appear in an
1598-- argument position.
1600-- This has become a right mess already. Better redo it some time...
1601-- TODO: This is obsoleted by the new way of elaborating types, (which
1602-- calls addUsingImpls) but there's still a couple of places which use
1603-- it. Clean them up!
1605-- Issue 1739 in the issue tracker
1606-- https://github.com/idris-lang/Idris-dev/issues/1739
1607implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1608implicit info syn n ptm = implicit' info syn [] n ptm
1610implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1611implicit' info syn ignore n ptm
1613 auto <- getAutoImpls
1614 let (tm', impdata) = implicitise auto syn ignore i ptm
1615 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1616-- let (tm'', spos) = findStatics i tm'
1617 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1619 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1621-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1624 -- Detect unknown names in default arguments and throw error if found.
1625 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1626 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1628 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1629 notFoundInDefault kns (PTacImplicit _ _ n script _)
1631 case notFound kns (namesIn [] i script) of
1632 Nothing -> return (n:kns)
1633 Just name -> throwError (NoSuchVariable name)
1634 notFoundInDefault kns p = return ((pname p):kns)
1636 notFound :: [Name] -> [Name] -> Maybe Name
1637 notFound kns [] = Nothing
1638 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1639 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1641-- | Even if auto_implicits is off, we need to call this so we record
1642-- which arguments are implicit
1643implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1644implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1645 let (declimps, ns') = execState (imps True [] tm) ([], [])
1646 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1647 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1648 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1650 then (tm, reverse declimps)
1651 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1653 uvars = map ipair (filter uimplicit (using syn))
1654 pvars = syn_params syn
1656 inUsing n = n `elem` map fst uvars
1658 ipair (UImplicit x y) = (x, y)
1659 uimplicit (UImplicit _ _) = True
1662 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1663 | otherwise = x : dropAll xs ys
1666 -- Find names in argument position in a type, suitable for implicit
1668 -- Not the function position, but do everything else...
1669 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1670 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1672 imps top env ty@(PApp _ f as)
1673 = do (decls, ns) <- get
1674 let isn = nub (implNamesIn uvars ty)
1675 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1676 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1677 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1679 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1680 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1681 imps True (n:env) sc
1682 imps top env (PPi (Exp l _ _) n _ ty sc)
1683 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1684 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1686 (decls, ns) <- get -- ignore decls in HO types
1687 put (PExp (getPriority ist ty) l n Placeholder : decls,
1688 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1689 imps True (n:env) sc
1690 imps top env (PPi (Constraint l _) n _ ty sc)
1691 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1692 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1694 (decls, ns) <- get -- ignore decls in HO types
1695 put (PConstraint 10 l n Placeholder : decls,
1696 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1697 imps True (n:env) sc
1698 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1699 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1700 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1702 (decls, ns) <- get -- ignore decls in HO types
1703 put (PTacImplicit 10 l n scr Placeholder : decls,
1704 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1705 imps True (n:env) sc
1706 imps top env (PRewrite _ _ l r _)
1707 = do (decls, ns) <- get
1708 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1709 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1710 imps top env (PTyped l r)
1712 imps top env (PPair _ _ _ l r)
1713 = do (decls, ns) <- get
1714 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1715 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1716 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1717 = do (decls, ns) <- get
1718 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1719 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1720 imps top env (PDPair _ _ _ l t r)
1721 = do (decls, ns) <- get
1722 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1724 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1725 imps top env (PAlternative ms a as)
1726 = do (decls, ns) <- get
1727 let isn = concatMap (namesIn uvars ist) as
1728 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1729 imps top env (PLam fc n _ ty sc)
1730 = do imps False env ty
1731 imps False (n:env) sc
1732 imps top env (PHidden tm) = imps False env tm
1733 imps top env (PUnifyLog tm) = imps False env tm
1734 imps top env (PNoImplicits tm) = imps False env tm
1735 imps top env (PRunElab fc tm ns) = imps False env tm
1736 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1737 imps top env _ = return ()
1739 pibind using [] sc = sc
1740 pibind using (n:ns) sc
1741 = case lookup n using of
1742 Just ty -> PPi impl_gen
1743 n NoFC ty (pibind using ns sc)
1744 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1745 n NoFC Placeholder (pibind using ns sc)
1747-- | Add implicit arguments in function calls
1748addImplPat :: IState -> PTerm -> PTerm
1749addImplPat = addImpl' True [] [] []
1751addImplBound :: IState -> [Name] -> PTerm -> PTerm
1752addImplBound ist ns = addImpl' False ns [] [] ist
1754addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1755addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1757-- | Add the implicit arguments to applications in the term [Name]
1758-- gives the names to always expend, even when under a binder of that
1759-- name (this is to expand methods with implicit arguments in
1760-- dependent type classes).
1761addImpl :: [Name] -> IState -> PTerm -> PTerm
1762addImpl = addImpl' False [] []
1764-- TODO: in patterns, don't add implicits to function names guarded by constructors
1765-- and *not* inside a PHidden
1767addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1768addImpl' inpat env infns imp_meths ist ptm
1769 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1771 topname = case ptm of
1773 PApp _ (PRef _ _ n) _ -> n
1774 _ -> sUN "" -- doesn't matter then
1776 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1777 ai inpat qq env ds (PRef fc fcs f)
1778 | f `elem` infns = PInferRef fc fcs f
1779 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1780 ai inpat qq env ds (PHidden (PRef fc hl f))
1781 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1782 ai inpat qq env ds (PRewrite fc by l r g)
1783 = let l' = ai inpat qq env ds l
1784 r' = ai inpat qq env ds r
1785 g' = fmap (ai inpat qq env ds) g in
1786 PRewrite fc by l' r' g'
1787 ai inpat qq env ds (PTyped l r)
1788 = let l' = ai inpat qq env ds l
1789 r' = ai inpat qq env ds r in
1791 ai inpat qq env ds (PPair fc hls p l r)
1792 = let l' = ai inpat qq env ds l
1793 r' = ai inpat qq env ds r in
1794 PPair fc hls p l' r'
1795 ai inpat qq env ds (PDPair fc hls p l t r)
1796 = let l' = ai inpat qq env ds l
1797 t' = ai inpat qq env ds t
1798 r' = ai inpat qq env ds r in
1799 PDPair fc hls p l' t' r'
1800 ai inpat qq env ds (PAlternative ms a as)
1801 = let as' = map (ai inpat qq env ds) as in
1802 PAlternative ms a as'
1803 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1804 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1805 = let as' = map (fmap (ai inpat qq env ds)) as in
1806 PApp fc (PInferRef ffc hl f) as'
1807 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1808 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1809 | not (f `elem` map fst env)
1810 = let as' = map (fmap (ai inpat qq env ds)) as in
1811 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1812 | Just (Just ty) <- lookup f env =
1813 let as' = map (fmap (ai inpat qq env ds)) as
1814 arity = getPArity ty in
1815 mkPApp fc arity ftm as'
1816 ai inpat qq env ds (PApp fc f as)
1817 = let f' = ai inpat qq env ds f
1818 as' = map (fmap (ai inpat qq env ds)) as in
1820 ai inpat qq env ds (PWithApp fc f a)
1821 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1822 ai inpat qq env ds (PCase fc c os)
1823 = let c' = ai inpat qq env ds c in
1824 -- leave lhs alone, because they get lifted into a new pattern match
1825 -- definition which is passed through addImpl again
1826 PCase fc c' (map aiCase os)
1829 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1831 -- Anything beginning with a lower case letter, not applied,
1832 -- and no namespace is a pattern variable
1833 patnames (PApp _ (PRef _ _ f) [])
1834 | implicitable f = [(f, Nothing)]
1835 patnames (PRef _ _ f)
1836 | implicitable f = [(f, Nothing)]
1837 patnames (PApp _ (PRef _ _ _) args)
1838 = concatMap patnames (map getTm args)
1839 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1840 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1841 patnames (PAs _ _ t) = patnames t
1842 patnames (PAlternative _ _ ts) = concatMap patnames ts
1846 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1847 (ai inpat qq env ds t)
1848 (ai inpat qq env ds f)
1850 -- If the name in a lambda is an unapplied data constructor name, do this
1851 -- as a 'case' instead because we'll expect to match on it
1852 ai inpat qq env ds (PLam fc n nfc ty sc)
1853 = if canBeDConName n (tt_ctxt ist)
1854 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1855 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1856 [(PRef fc [] n, sc)]))
1857 else let ty' = ai inpat qq env ds ty
1858 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1859 PLam fc n nfc ty' sc'
1860 ai inpat qq env ds (PLet fc n nfc ty val sc)
1861 = if canBeDConName n (tt_ctxt ist)
1862 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1863 else let ty' = ai inpat qq env ds ty
1864 val' = ai inpat qq env ds val
1865 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1866 PLet fc n nfc ty' val' sc'
1867 ai inpat qq env ds (PPi p n nfc ty sc)
1868 = let ty' = ai inpat qq env ds ty
1869 env' = if n `elem` imp_meths then env
1870 else ((n, Just ty) : env)
1871 sc' = ai inpat qq env' ds sc in
1873 ai inpat qq env ds (PGoal fc r n sc)
1874 = let r' = ai inpat qq env ds r
1875 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1877 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1878 -- Don't do PProof or PTactics since implicits get added when scope is
1879 -- properly known in ElabTerm.runTac
1880 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1881 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1882 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1883 (fmap (ai inpat True env ds) g)
1884 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1885 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1886 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1887 ai inpat qq env ds tm = tm
1889 handleErr (Left err) = PElabError err
1890 handleErr (Right x) = x
1892-- if in a pattern, and there are no arguments, and there's no possible
1893-- names with zero explicit arguments, don't add implicits.
1895aiFn :: Name -> Bool -> Bool -> Bool
1898 -> Name -- ^ function being applied
1900 -> [PArg] -- ^ initial arguments (if in a pattern)
1902aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1903 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1905 = case lookupDef f (tt_ctxt ist) of
1906 [] -> Right $ PPatvar ffc f
1907 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1908 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1909 if (not (vname f) || tcname f
1910 || any (conCaf (tt_ctxt ist)) ialts)
1911-- any constructor alts || any allImp ialts))
1912 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1913 else Right $ PPatvar ffc f
1914 where imp (PExp _ _ _ _) = False
1917 allImp xs = all imp xs
1919 unqualified (NS _ _) = False
1920 unqualified _ = True
1922 constructor (TyDecl (DCon _ _ _) _) = True
1923 constructor _ = False
1925 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1927 vname (UN n) = True -- non qualified
1930aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1931 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1932aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1933 -- This is where namespaces get resolved by adding PAlternative
1934 = do let ns = lookupCtxtName f (idris_implicits ist)
1935 let nh = filter (\(n, _) -> notHidden n) ns
1936 let ns' = case trimAlts ds nh of
1940 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1942 [] -> case metaVar f (map fst (idris_metavars ist)) of
1943 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1944 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1946 PAlternative [] (ExactlyOne True) $
1947 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1948 (insertImpl ns as)) alts
1950 -- if the name is in imp_meths, we should actually refer to the bound
1951 -- name rather than the global one after expanding implicits
1952 isImpName f f' | f `elem` imp_meths = f
1955 -- If it's a metavariable name, try to qualify it from the list of
1956 -- unsolved metavariables
1957 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1958 metaVar f (_ : ns) = metaVar f ns
1959 metaVar f [] = Nothing
1961 trimAlts [] alts = alts
1963 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1968 notHidden n = case getAccessibility n of
1974 = case lookupDefAccExact n False (tt_ctxt ist) of
1978 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1979 -> [PArg] -- ^ given arguments
1982 = let (as', badimpls) = partition (impIn ps) as in
1983 map addUnknownImp badimpls ++
1984 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1986 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1987 -> [PArg] -- parameters
1988 -> [PArg] -- explicit arguments
1989 -> [PArg] -- implicits given
1991 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1992 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1993 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1994 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1995 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1996 let rtc = PResolveTC fc in
1997 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1998 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1999 case find n imps [] of
2001 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2003 PImp p True l n Placeholder :
2004 insImpAcc (M.insert n Placeholder pnas) ps given imps
2005 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2006 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2007 case find n imps [] of
2009 PTacImplicit p l n sc tm :
2010 insImpAcc (M.insert n tm pnas) ps given imps'
2013 then PTacImplicit p l n sc Placeholder :
2014 insImpAcc (M.insert n Placeholder pnas) ps given imps
2015 else PTacImplicit p l n sc sc :
2016 insImpAcc (M.insert n sc pnas) ps given imps
2017 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2018 insImpAcc _ _ given imps = given ++ imps
2020 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2022 find n [] acc = Nothing
2023 find n (PImp _ _ _ n' t : gs) acc
2024 | n == n' = Just (t, reverse acc ++ gs)
2025 find n (PTacImplicit _ _ n' _ t : gs) acc
2026 | n == n' = Just (t, reverse acc ++ gs)
2027 find n (g : gs) acc = find n gs (g : acc)
2029-- | return True if the second argument is an implicit argument which
2030-- is expected in the implicits, or if it's not an implicit
2031impIn :: [PArg] -> PArg -> Bool
2032impIn ps (PExp _ _ _ _) = True
2033impIn ps (PConstraint _ _ _ _) = True
2034impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2036expArg (PExp _ _ _ _) = True
2037expArg (PConstraint _ _ _ _) = True
2040-- replace non-linear occurrences with _
2042stripLinear :: IState -> PTerm -> PTerm
2043stripLinear i tm = evalState (sl tm) [] where
2044 sl :: PTerm -> State [Name] PTerm
2046 | (_:_) <- lookupTy f (tt_ctxt i)
2047 = return $ PRef fc hl f
2048 | otherwise = do ns <- get
2050 then return $ PHidden (PRef fc hl f) -- Placeholder
2051 else do put (f : ns)
2052 return (PRef fc hl f)
2056 then return $ PHidden (PPatvar fc f) -- Placeholder
2057 else do put (f : ns)
2058 return (PPatvar fc f)
2059 -- Assumption is that variables are all the same in each alternative
2060 sl t@(PAlternative ms b as) = do ns <- get
2062 return (PAlternative ms b as')
2063 where slAlts ns (a : as) = do put ns
2067 slAlts ns [] = return []
2068 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2069 sl (PDPair fc hls p l t r) = do l' <- sl l
2072 return (PDPair fc hls p l' t' r')
2073 sl (PApp fc fn args) = do fn' <- case fn of
2074 -- Just the args, fn isn't matchable as a var
2075 PRef _ _ _ -> return fn
2077 args' <- mapM slA args
2078 return $ PApp fc fn' args'
2079 where slA (PImp p m l n t) = do t' <- sl t
2080 return $ PImp p m l n t'
2081 slA (PExp p l n t) = do t' <- sl t
2082 return $ PExp p l n t'
2083 slA (PConstraint p l n t)
2085 return $ PConstraint p l n t'
2086 slA (PTacImplicit p l n sc t)
2088 return $ PTacImplicit p l n sc t'
2091-- | Remove functions which aren't applied to anything, which must then
2092-- be resolved by unification. Assume names resolved and alternatives
2093-- filled in (so no ambiguity).
2094stripUnmatchable :: IState -> PTerm -> PTerm
2095stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2096 su :: PTerm -> PTerm
2097 su tm@(PRef fc hl f)
2098 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2100 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2101 not (implicitable f)
2103 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2104 not (implicitable f)
2106 su (PApp fc f@(PRef _ _ fn) args)
2107 -- here we use canBeDConName because the impossible pattern
2108 -- check will not necessarily fully resolve constructor names,
2109 -- and these bare names will otherwise get in the way of
2110 -- impossbility checking.
2111 | canBeDConName fn ctxt
2112 = PApp fc f (fmap (fmap su) args)
2114 = PHidden (PApp fc f args)
2115 su (PAlternative ms b alts)
2116 = let alts' = filter (/= Placeholder) (map su alts) in
2117 if null alts' then Placeholder
2118 else PAlternative ms b alts'
2119 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2120 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2121 su t@(PLam fc _ _ _ _) = PHidden t
2122 su t@(PPi _ _ _ _ _) = PHidden t
2123 su t@(PConstant _ c) | isTypeConst c = PHidden t
2128stripUnmatchable i tm = tm
2131mkPApp fc a f as = let rest = drop a as in
2132 if a == 0 then appRest fc f rest
2133 else appRest fc (PApp fc f (take a as)) rest
2136 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2140-- | Find 'static' argument positions
2141-- (the declared ones, plus any names in argument position in the declared
2143-- FIXME: It's possible that this really has to happen after elaboration
2144findStatics :: IState -> PTerm -> (PTerm, [Bool])
2145findStatics ist tm = let (ns, ss) = fs tm
2146 in runState (pos ns ss tm) []
2147 where fs (PPi p n fc t sc)
2148 | Static <- pstatic p
2149 = let (ns, ss) = fs sc in
2150 (namesIn [] ist t : ns, n : ss)
2151 | otherwise = let (ns, ss) = fs sc in
2155 inOne n ns = length (filter id (map (elem n) ns)) == 1
2157 pos ns ss (PPi p n fc t sc)
2158 | elem n ss = do sc' <- pos ns ss sc
2161 return (PPi (p { pstatic = Static }) n fc t sc')
2162 | otherwise = do sc' <- pos ns ss sc
2165 return (PPi p n fc t sc')
2166 pos ns ss t = return t
2168-- for 6.12/7 compatibility
2169data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2171instance Applicative (EitherErr a) where
2175instance Monad (EitherErr a) where
2178 (LeftErr e) >>= k = LeftErr e
2179 RightOK v >>= k = k v
2181toEither (LeftErr e) = Left e
2182toEither (RightOK ho) = Right ho
2184-- | Syntactic match of a against b, returning pair of variables in a
2185-- and what they match. Returns the pair that failed if not a match.
2186matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2187matchClause = matchClause' False
2189matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2190matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2191 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2193 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2196 match' x y = match (fullApp x) (fullApp y)
2197 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2198 | fi == txt "fromInteger" && b == txt "builtins",
2199 PConstant _ (I _) <- getTm x = match (getTm x) x'
2200 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2201 | fi == txt "fromInteger" && b == txt "builtins",
2202 PConstant _ (I _) <- getTm x = match (getTm x) x'
2203 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2204 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2205 match (PApp _ f args) (PApp _ f' args')
2206 | length args == length args'
2207 = do mf <- match' f f'
2208 ms <- zipWithM matchArg args args'
2209 return (mf ++ concat ms)
2210 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2211 match (PPatvar f n) xr = match (PRef f [f] n) xr
2212 match xr (PPatvar f n) = match xr (PRef f [f] n)
2213 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2214 match (PRef _ _ n) tm@(PRef _ _ n')
2215 | n == n' && not names &&
2216 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2217 || tm == Placeholder)
2219 -- if one namespace is missing, drop the other
2220 | n == n' || n == dropNS n' || dropNS n == n' = return []
2221 where dropNS (NS n _) = n
2223 match (PRef _ _ n) tm
2224 | not names && (not (isConName n (tt_ctxt i) ||
2225 isFnName n (tt_ctxt i)) || tm == Placeholder)
2227 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2228 = do ml <- match' l l'
2231 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2234 match (PTyped l r) x = match l x
2235 match x (PTyped l r) = match x l
2236 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2239 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2242 return (ml ++ mt ++ mr)
2243 match (PAlternative _ a as) (PAlternative _ a' as')
2244 = do ms <- zipWithM match' as as'
2246 match a@(PAlternative _ _ as) b
2247 = do let ms = zipWith match' as (repeat b)
2248 case (rights (map toEither ms)) of
2251 match (PCase _ _ _) _ = return [] -- lifted out
2252 match (PMetavar _ _) _ = return [] -- modified
2253 match (PInferRef _ _ _) _ = return [] -- modified
2254 match (PQuote _) _ = return []
2255 match (PProof _) _ = return []
2256 match (PTactics _) _ = return []
2257 match (PResolveTC _) (PResolveTC _) = return []
2258 match (PTrue _ _) (PTrue _ _) = return []
2259 match (PReturn _) (PReturn _) = return []
2260 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2263 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2266 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2267 mty <- match' ty ty'
2269 return (mt ++ mty ++ ms)
2270 match (PHidden x) (PHidden y)
2271 | RightOK xs <- match x y = return xs -- to collect variables
2272 | otherwise = return [] -- Otherwise hidden things are unmatchable
2274 | RightOK xs <- match x y = return xs
2275 | otherwise = return []
2277 | RightOK xs <- match x y = return xs
2278 | otherwise = return []
2279 match (PUnifyLog x) y = match' x y
2280 match x (PUnifyLog y) = match' x y
2281 match (PNoImplicits x) y = match' x y
2282 match x (PNoImplicits y) = match' x y
2283 match Placeholder _ = return []
2284 match _ Placeholder = return []
2285 match (PResolveTC _) _ = return []
2286 match a b | a == b = return []
2287 | otherwise = LeftErr (a, b)
2289 checkRpts (RightOK ms) = check ms where
2291 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2294 check (_:xs) = check xs
2296 checkRpts (LeftErr x) = Left x
2298substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2299substMatches ms = substMatchesShadow ms []
2301-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2302-- substMatchesShadow [] shs t = t
2303-- substMatchesShadow ((n,tm):ns) shs t
2304-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2306substMatch :: Name -> PTerm -> PTerm -> PTerm
2307substMatch n = substMatchShadow n []
2309substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2310substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2312substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2313substMatchesShadow nmap shs t = sm shs t where
2314 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2315 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2316 sm xs (PPi p x fc t sc)
2318 = let x' = nextName x in
2319 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2320 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2321 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2322 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2323 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2324 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2325 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2327 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2328 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2329 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2330 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2331 sm xs (PHidden x) = PHidden (sm xs x)
2332 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2333 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2334 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2335 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2338 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2341shadow :: Name -> Name -> PTerm -> PTerm
2342shadow n n' t = sm 0 t where
2343 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2344 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2345 | otherwise = PLam fc x xfc (sm 0 t) sc
2346 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2347 | otherwise = PPi p x fc (sm 0 t) sc
2348 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2349 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2350 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2351 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2352 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2353 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2354 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2355 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2356 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2357 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2358 sm 0 (PAlternative ms a as)
2359 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2360 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2361 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2362 sm 0 (PHidden x) = PHidden (sm 0 x)
2363 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2364 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2365 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2366 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2367 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2368 sm ql x = descend (sm ql) x
2370 shadowAlt p@(x, oldn) = (update x, update oldn)
2371 update oldn | n == oldn = n'
2374-- | Rename any binders which are repeated (so that we don't have to
2375-- mess about with shadowing anywhere else).
2376mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2377mkUniqueNames env shadows tm
2378 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2380 initMap = M.fromList shadows
2382 inScope :: S.Set Name
2383 inScope = S.fromList $ boundNamesIn tm
2385 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2386 return (arg { getTm = t' })
2388 -- Initialise the unique name with the environment length (so we're not
2389 -- looking for too long...)
2390 initN (UN n) l = UN $ txt (str n ++ show l)
2391 initN (MN i s) l = MN (i+l) s
2394 -- FIXME: Probably ought to do this for completeness! It's fine as
2395 -- long as there are no bindings inside tactics though.
2396 mkUniqT _ nmap tac = return tac
2398 mkUniq :: Int -- ^ The number of quotations that we're under
2399 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2400 mkUniq 0 nmap (PLam fc n nfc ty sc)
2404 then do let n' = uniqueNameSet (initN n (S.size env))
2405 (S.union env inScope)
2406 return (n', sc) -- shadow n n' sc)
2408 put (S.insert n' env)
2409 let nmap' = M.insert n n' nmap
2410 ty' <- mkUniq 0 nmap ty
2411 sc'' <- mkUniq 0 nmap' sc'
2412 return $! PLam fc n' nfc ty' sc''
2413 mkUniq 0 nmap (PPi p n fc ty sc)
2417 then do let n' = uniqueNameSet (initN n (S.size env))
2418 (S.union env inScope)
2419 return (n', sc) -- shadow n n' sc)
2421 put (S.insert n' env)
2422 let nmap' = M.insert n n' nmap
2423 ty' <- mkUniq 0 nmap ty
2424 sc'' <- mkUniq 0 nmap' sc'
2425 return $! PPi p n' fc ty' sc''
2426 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2430 then do let n' = uniqueNameSet (initN n (S.size env))
2431 (S.union env inScope)
2432 return (n', sc) -- shadow n n' sc)
2434 put (S.insert n' env)
2435 let nmap' = M.insert n n' nmap
2436 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2437 sc'' <- mkUniq 0 nmap' sc'
2438 return $! PLet fc n' nfc ty' val' sc''
2439 mkUniq 0 nmap (PApp fc t args)
2440 = do t' <- mkUniq 0 nmap t
2441 args' <- mapM (mkUniqA 0 nmap) args
2442 return $! PApp fc t' args'
2443 mkUniq 0 nmap (PAppBind fc t args)
2444 = do t' <- mkUniq 0 nmap t
2445 args' <- mapM (mkUniqA 0 nmap) args
2446 return $! PAppBind fc t' args'
2447 mkUniq 0 nmap (PCase fc t alts)
2448 = do t' <- mkUniq 0 nmap t
2449 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2450 return (x', y')) alts
2451 return $! PCase fc t' alts'
2452 mkUniq 0 nmap (PIfThenElse fc c t f)
2453 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2454 mkUniq 0 nmap (PPair fc hls p l r)
2455 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2456 return $! PPair fc hls p l' r'
2457 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2460 (n', sc') <- if n `S.member` env
2461 then do let n' = uniqueNameSet n (S.union env inScope)
2462 return (n', sc) -- shadow n n' sc)
2464 put (S.insert n' env)
2465 let nmap' = M.insert n n' nmap
2466 t' <- mkUniq 0 nmap t
2467 sc'' <- mkUniq 0 nmap' sc'
2468 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2469 mkUniq 0 nmap (PDPair fc hls p l t r)
2470 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2471 return $! PDPair fc hls p l' t' r'
2472 mkUniq 0 nmap (PAlternative ns b as)
2473 -- store the nmap and defer the rest until we've pruned the set
2474 -- during elaboration
2475 = return $ PAlternative (ns ++ M.toList nmap) b as
2476 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2477 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2478 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2479 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2480 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2481 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2482 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2483 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2484 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2485 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2488 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2490 mkUniq ql nmap (PQuasiquote tm ty) =
2491 do tm' <- mkUniq (ql + 1) nmap tm
2493 Nothing -> return Nothing
2494 Just t -> fmap Just $ mkUniq ql nmap t
2495 return $! PQuasiquote tm' ty'
2496 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2498 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list