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 [] -> if f `elem` (map fst (idris_metavars ist))
1943 then Right $ PApp fc (PRef ffc [ffc] f) as
1944 else 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 trimAlts [] alts = alts
1957 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1962 notHidden n = case getAccessibility n of
1968 = case lookupDefAccExact n False (tt_ctxt ist) of
1972 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1973 -> [PArg] -- ^ given arguments
1976 = let (as', badimpls) = partition (impIn ps) as in
1977 map addUnknownImp badimpls ++
1978 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1980 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1981 -> [PArg] -- parameters
1982 -> [PArg] -- explicit arguments
1983 -> [PArg] -- implicits given
1985 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1986 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1987 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1988 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1989 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1990 let rtc = PResolveTC fc in
1991 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1992 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1993 case find n imps [] of
1995 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1997 PImp p True l n Placeholder :
1998 insImpAcc (M.insert n Placeholder pnas) ps given imps
1999 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2000 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2001 case find n imps [] of
2003 PTacImplicit p l n sc tm :
2004 insImpAcc (M.insert n tm pnas) ps given imps'
2007 then PTacImplicit p l n sc Placeholder :
2008 insImpAcc (M.insert n Placeholder pnas) ps given imps
2009 else PTacImplicit p l n sc sc :
2010 insImpAcc (M.insert n sc pnas) ps given imps
2011 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2012 insImpAcc _ _ given imps = given ++ imps
2014 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2016 find n [] acc = Nothing
2017 find n (PImp _ _ _ n' t : gs) acc
2018 | n == n' = Just (t, reverse acc ++ gs)
2019 find n (PTacImplicit _ _ n' _ t : gs) acc
2020 | n == n' = Just (t, reverse acc ++ gs)
2021 find n (g : gs) acc = find n gs (g : acc)
2023-- | return True if the second argument is an implicit argument which
2024-- is expected in the implicits, or if it's not an implicit
2025impIn :: [PArg] -> PArg -> Bool
2026impIn ps (PExp _ _ _ _) = True
2027impIn ps (PConstraint _ _ _ _) = True
2028impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2030expArg (PExp _ _ _ _) = True
2031expArg (PConstraint _ _ _ _) = True
2034-- replace non-linear occurrences with _
2036stripLinear :: IState -> PTerm -> PTerm
2037stripLinear i tm = evalState (sl tm) [] where
2038 sl :: PTerm -> State [Name] PTerm
2040 | (_:_) <- lookupTy f (tt_ctxt i)
2041 = return $ PRef fc hl f
2042 | otherwise = do ns <- get
2044 then return $ PHidden (PRef fc hl f) -- Placeholder
2045 else do put (f : ns)
2046 return (PRef fc hl f)
2050 then return $ PHidden (PPatvar fc f) -- Placeholder
2051 else do put (f : ns)
2052 return (PPatvar fc f)
2053 -- Assumption is that variables are all the same in each alternative
2054 sl t@(PAlternative ms b as) = do ns <- get
2056 return (PAlternative ms b as')
2057 where slAlts ns (a : as) = do put ns
2061 slAlts ns [] = return []
2062 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2063 sl (PDPair fc hls p l t r) = do l' <- sl l
2066 return (PDPair fc hls p l' t' r')
2067 sl (PApp fc fn args) = do fn' <- case fn of
2068 -- Just the args, fn isn't matchable as a var
2069 PRef _ _ _ -> return fn
2071 args' <- mapM slA args
2072 return $ PApp fc fn' args'
2073 where slA (PImp p m l n t) = do t' <- sl t
2074 return $ PImp p m l n t'
2075 slA (PExp p l n t) = do t' <- sl t
2076 return $ PExp p l n t'
2077 slA (PConstraint p l n t)
2079 return $ PConstraint p l n t'
2080 slA (PTacImplicit p l n sc t)
2082 return $ PTacImplicit p l n sc t'
2085-- | Remove functions which aren't applied to anything, which must then
2086-- be resolved by unification. Assume names resolved and alternatives
2087-- filled in (so no ambiguity).
2088stripUnmatchable :: IState -> PTerm -> PTerm
2089stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2090 su :: PTerm -> PTerm
2091 su tm@(PRef fc hl f)
2092 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2094 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2095 not (implicitable f)
2097 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2098 not (implicitable f)
2100 su (PApp fc f@(PRef _ _ fn) args)
2101 -- here we use canBeDConName because the impossible pattern
2102 -- check will not necessarily fully resolve constructor names,
2103 -- and these bare names will otherwise get in the way of
2104 -- impossbility checking.
2105 | canBeDConName fn ctxt
2106 = PApp fc f (fmap (fmap su) args)
2108 = PHidden (PApp fc f args)
2109 su (PAlternative ms b alts)
2110 = let alts' = filter (/= Placeholder) (map su alts) in
2111 if null alts' then Placeholder
2112 else PAlternative ms b alts'
2113 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2114 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2115 su t@(PLam fc _ _ _ _) = PHidden t
2116 su t@(PPi _ _ _ _ _) = PHidden t
2117 su t@(PConstant _ c) | isTypeConst c = PHidden t
2122stripUnmatchable i tm = tm
2125mkPApp fc a f as = let rest = drop a as in
2126 if a == 0 then appRest fc f rest
2127 else appRest fc (PApp fc f (take a as)) rest
2130 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2134-- | Find 'static' argument positions
2135-- (the declared ones, plus any names in argument position in the declared
2137-- FIXME: It's possible that this really has to happen after elaboration
2138findStatics :: IState -> PTerm -> (PTerm, [Bool])
2139findStatics ist tm = let (ns, ss) = fs tm
2140 in runState (pos ns ss tm) []
2141 where fs (PPi p n fc t sc)
2142 | Static <- pstatic p
2143 = let (ns, ss) = fs sc in
2144 (namesIn [] ist t : ns, n : ss)
2145 | otherwise = let (ns, ss) = fs sc in
2149 inOne n ns = length (filter id (map (elem n) ns)) == 1
2151 pos ns ss (PPi p n fc t sc)
2152 | elem n ss = do sc' <- pos ns ss sc
2155 return (PPi (p { pstatic = Static }) n fc t sc')
2156 | otherwise = do sc' <- pos ns ss sc
2159 return (PPi p n fc t sc')
2160 pos ns ss t = return t
2162-- for 6.12/7 compatibility
2163data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2165instance Applicative (EitherErr a) where
2169instance Monad (EitherErr a) where
2172 (LeftErr e) >>= k = LeftErr e
2173 RightOK v >>= k = k v
2175toEither (LeftErr e) = Left e
2176toEither (RightOK ho) = Right ho
2178-- | Syntactic match of a against b, returning pair of variables in a
2179-- and what they match. Returns the pair that failed if not a match.
2180matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2181matchClause = matchClause' False
2183matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2184matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2185 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2187 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2190 match' x y = match (fullApp x) (fullApp y)
2191 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2192 | fi == txt "fromInteger" && b == txt "builtins",
2193 PConstant _ (I _) <- getTm x = match (getTm x) x'
2194 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2195 | fi == txt "fromInteger" && b == txt "builtins",
2196 PConstant _ (I _) <- getTm x = match (getTm x) x'
2197 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2198 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2199 match (PApp _ f args) (PApp _ f' args')
2200 | length args == length args'
2201 = do mf <- match' f f'
2202 ms <- zipWithM matchArg args args'
2203 return (mf ++ concat ms)
2204 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2205 match (PPatvar f n) xr = match (PRef f [f] n) xr
2206 match xr (PPatvar f n) = match xr (PRef f [f] n)
2207 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2208 match (PRef _ _ n) tm@(PRef _ _ n')
2209 | n == n' && not names &&
2210 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2211 || tm == Placeholder)
2213 -- if one namespace is missing, drop the other
2214 | n == n' || n == dropNS n' || dropNS n == n' = return []
2215 where dropNS (NS n _) = n
2217 match (PRef _ _ n) tm
2218 | not names && (not (isConName n (tt_ctxt i) ||
2219 isFnName n (tt_ctxt i)) || tm == Placeholder)
2221 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2222 = do ml <- match' l l'
2225 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2228 match (PTyped l r) x = match l x
2229 match x (PTyped l r) = match x l
2230 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2233 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2236 return (ml ++ mt ++ mr)
2237 match (PAlternative _ a as) (PAlternative _ a' as')
2238 = do ms <- zipWithM match' as as'
2240 match a@(PAlternative _ _ as) b
2241 = do let ms = zipWith match' as (repeat b)
2242 case (rights (map toEither ms)) of
2245 match (PCase _ _ _) _ = return [] -- lifted out
2246 match (PMetavar _ _) _ = return [] -- modified
2247 match (PInferRef _ _ _) _ = return [] -- modified
2248 match (PQuote _) _ = return []
2249 match (PProof _) _ = return []
2250 match (PTactics _) _ = return []
2251 match (PResolveTC _) (PResolveTC _) = return []
2252 match (PTrue _ _) (PTrue _ _) = return []
2253 match (PReturn _) (PReturn _) = return []
2254 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2257 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2260 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2261 mty <- match' ty ty'
2263 return (mt ++ mty ++ ms)
2264 match (PHidden x) (PHidden y)
2265 | RightOK xs <- match x y = return xs -- to collect variables
2266 | otherwise = return [] -- Otherwise hidden things are unmatchable
2268 | RightOK xs <- match x y = return xs
2269 | otherwise = return []
2271 | RightOK xs <- match x y = return xs
2272 | otherwise = return []
2273 match (PUnifyLog x) y = match' x y
2274 match x (PUnifyLog y) = match' x y
2275 match (PNoImplicits x) y = match' x y
2276 match x (PNoImplicits y) = match' x y
2277 match Placeholder _ = return []
2278 match _ Placeholder = return []
2279 match (PResolveTC _) _ = return []
2280 match a b | a == b = return []
2281 | otherwise = LeftErr (a, b)
2283 checkRpts (RightOK ms) = check ms where
2285 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2288 check (_:xs) = check xs
2290 checkRpts (LeftErr x) = Left x
2292substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2293substMatches ms = substMatchesShadow ms []
2295-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2296-- substMatchesShadow [] shs t = t
2297-- substMatchesShadow ((n,tm):ns) shs t
2298-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2300substMatch :: Name -> PTerm -> PTerm -> PTerm
2301substMatch n = substMatchShadow n []
2303substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2304substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2306substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2307substMatchesShadow nmap shs t = sm shs t where
2308 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2309 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2310 sm xs (PPi p x fc t sc)
2312 = let x' = nextName x in
2313 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2314 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2315 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2316 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2317 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2318 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2319 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2321 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2322 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2323 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2324 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2325 sm xs (PHidden x) = PHidden (sm xs x)
2326 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2327 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2328 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2329 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2332 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2335shadow :: Name -> Name -> PTerm -> PTerm
2336shadow n n' t = sm 0 t where
2337 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2338 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2339 | otherwise = PLam fc x xfc (sm 0 t) sc
2340 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2341 | otherwise = PPi p x fc (sm 0 t) sc
2342 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2343 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2344 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2345 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2346 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2347 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2348 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2349 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2350 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2351 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2352 sm 0 (PAlternative ms a as)
2353 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2354 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2355 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2356 sm 0 (PHidden x) = PHidden (sm 0 x)
2357 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2358 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2359 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2360 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2361 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2362 sm ql x = descend (sm ql) x
2364 shadowAlt p@(x, oldn) = (update x, update oldn)
2365 update oldn | n == oldn = n'
2368-- | Rename any binders which are repeated (so that we don't have to
2369-- mess about with shadowing anywhere else).
2370mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2371mkUniqueNames env shadows tm
2372 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2374 initMap = M.fromList shadows
2376 inScope :: S.Set Name
2377 inScope = S.fromList $ boundNamesIn tm
2379 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2380 return (arg { getTm = t' })
2382 -- Initialise the unique name with the environment length (so we're not
2383 -- looking for too long...)
2384 initN (UN n) l = UN $ txt (str n ++ show l)
2385 initN (MN i s) l = MN (i+l) s
2388 -- FIXME: Probably ought to do this for completeness! It's fine as
2389 -- long as there are no bindings inside tactics though.
2390 mkUniqT _ nmap tac = return tac
2392 mkUniq :: Int -- ^ The number of quotations that we're under
2393 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2394 mkUniq 0 nmap (PLam fc n nfc ty sc)
2398 then do let n' = uniqueNameSet (initN n (S.size env))
2399 (S.union env inScope)
2400 return (n', sc) -- shadow n n' sc)
2402 put (S.insert n' env)
2403 let nmap' = M.insert n n' nmap
2404 ty' <- mkUniq 0 nmap ty
2405 sc'' <- mkUniq 0 nmap' sc'
2406 return $! PLam fc n' nfc ty' sc''
2407 mkUniq 0 nmap (PPi p n fc ty sc)
2411 then do let n' = uniqueNameSet (initN n (S.size env))
2412 (S.union env inScope)
2413 return (n', sc) -- shadow n n' sc)
2415 put (S.insert n' env)
2416 let nmap' = M.insert n n' nmap
2417 ty' <- mkUniq 0 nmap ty
2418 sc'' <- mkUniq 0 nmap' sc'
2419 return $! PPi p n' fc ty' sc''
2420 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2424 then do let n' = uniqueNameSet (initN n (S.size env))
2425 (S.union env inScope)
2426 return (n', sc) -- shadow n n' sc)
2428 put (S.insert n' env)
2429 let nmap' = M.insert n n' nmap
2430 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2431 sc'' <- mkUniq 0 nmap' sc'
2432 return $! PLet fc n' nfc ty' val' sc''
2433 mkUniq 0 nmap (PApp fc t args)
2434 = do t' <- mkUniq 0 nmap t
2435 args' <- mapM (mkUniqA 0 nmap) args
2436 return $! PApp fc t' args'
2437 mkUniq 0 nmap (PAppBind fc t args)
2438 = do t' <- mkUniq 0 nmap t
2439 args' <- mapM (mkUniqA 0 nmap) args
2440 return $! PAppBind fc t' args'
2441 mkUniq 0 nmap (PCase fc t alts)
2442 = do t' <- mkUniq 0 nmap t
2443 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2444 return (x', y')) alts
2445 return $! PCase fc t' alts'
2446 mkUniq 0 nmap (PIfThenElse fc c t f)
2447 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2448 mkUniq 0 nmap (PPair fc hls p l r)
2449 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2450 return $! PPair fc hls p l' r'
2451 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2454 (n', sc') <- if n `S.member` env
2455 then do let n' = uniqueNameSet n (S.union env inScope)
2456 return (n', sc) -- shadow n n' sc)
2458 put (S.insert n' env)
2459 let nmap' = M.insert n n' nmap
2460 t' <- mkUniq 0 nmap t
2461 sc'' <- mkUniq 0 nmap' sc'
2462 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2463 mkUniq 0 nmap (PDPair fc hls p l t r)
2464 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2465 return $! PDPair fc hls p l' t' r'
2466 mkUniq 0 nmap (PAlternative ns b as)
2467 -- store the nmap and defer the rest until we've pruned the set
2468 -- during elaboration
2469 = return $ PAlternative (ns ++ M.toList nmap) b as
2470 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2471 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2472 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2473 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2474 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2475 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2476 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2477 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2478 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2479 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2482 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2484 mkUniq ql nmap (PQuasiquote tm ty) =
2485 do tm' <- mkUniq (ql + 1) nmap tm
2487 Nothing -> return Nothing
2488 Just t -> fmap Just $ mkUniq ql nmap t
2489 return $! PQuasiquote tm' ty'
2490 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2492 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