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)
698 let ctxt' = ctxt { next_tvar = v }
699 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
700 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
703 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
704 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
705 insertAll ((c, fc) : cs) ics
706 = insertAll cs $ S.insert (ConstraintFC c fc) ics
708addDeferred = addDeferred' Ref
709addDeferredTyCon = addDeferred' (TCon 0 0)
711-- | Save information about a name that is not yet defined
712addDeferred' :: NameType
713 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
714 -- ^ The Name is the name being made into a metavar,
715 -- the Int is the number of vars that are part of a
716 -- putative proof context, the Maybe Name is the
717 -- top-level function containing the new metavariable,
718 -- the Type is its type, and the Bool is whether :p is
722 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
723 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
725 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
726 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
729 -- 'tidyNames' is to generate user accessible names in case they are
730 -- needed in tactic scripts
731 tidyNames used (Bind (MN i x) b sc)
732 = let n' = uniqueNameSet (UN x) used in
733 Bind n' b $ tidyNames (S.insert n' used) sc
734 tidyNames used (Bind n b sc)
735 = let n' = uniqueNameSet n used in
736 Bind n' b $ tidyNames (S.insert n' used) sc
739solveDeferred :: FC -> Name -> Idris ()
742 case lookup n (idris_metavars i) of
743 Just (_, _, _, _, False) ->
744 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
745 _ -> putIState $ i { idris_metavars =
746 filter (\(n', _) -> n/=n')
749 filter (notMV n) (ibc_write i)
751 where notMV n (IBCMetavar n') = not (n == n')
754getUndefined :: Idris [Name]
755getUndefined = do i <- getIState
756 return (map fst (idris_metavars i) \\ primDefs)
758isMetavarName :: Name -> IState -> Bool
760 = case lookupNames n (tt_ctxt ist) of
761 (t:_) -> isJust $ lookup t (idris_metavars ist)
764getWidth :: Idris ConsoleWidth
765getWidth = fmap idris_consolewidth getIState
767setWidth :: ConsoleWidth -> Idris ()
768setWidth w = do ist <- getIState
769 put ist { idris_consolewidth = w }
771setDepth :: Maybe Int -> Idris ()
772setDepth d = do ist <- getIState
773 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
775typeDescription :: String
776typeDescription = "The type of types"
779type1Doc :: Doc OutputAnnotation
780type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
783isetPrompt :: String -> Idris ()
784isetPrompt p = do i <- getIState
785 case idris_outputmode i of
786 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
788-- | Tell clients how much was parsed and loaded
789isetLoadedRegion :: Idris ()
790isetLoadedRegion = do i <- getIState
791 let span = idris_parsedSpan i
794 case idris_outputmode i of
796 runIO . hPutStrLn h $
797 convSExp "set-loaded-region" fc n
800setLogLevel :: Int -> Idris ()
801setLogLevel l = do i <- getIState
802 let opts = idris_options i
803 let opt' = opts { opt_logLevel = l }
804 putIState $ i { idris_options = opt' }
806setLogCats :: [LogCat] -> Idris ()
809 let opts = idris_options i
810 let opt' = opts { opt_logcats = cs }
811 putIState $ i { idris_options = opt' }
813setCmdLine :: [Opt] -> Idris ()
814setCmdLine opts = do i <- getIState
815 let iopts = idris_options i
816 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
818getCmdLine :: Idris [Opt]
819getCmdLine = do i <- getIState
820 return (opt_cmdline (idris_options i))
822getDumpHighlighting :: Idris Bool
823getDumpHighlighting = do ist <- getIState
824 return (findC (opt_cmdline (idris_options ist)))
825 where findC = elem DumpHighlights
827getDumpDefun :: Idris (Maybe FilePath)
828getDumpDefun = do i <- getIState
829 return $ findC (opt_cmdline (idris_options i))
830 where findC [] = Nothing
831 findC (DumpDefun x : _) = Just x
832 findC (_ : xs) = findC xs
834getDumpCases :: Idris (Maybe FilePath)
835getDumpCases = do i <- getIState
836 return $ findC (opt_cmdline (idris_options i))
837 where findC [] = Nothing
838 findC (DumpCases x : _) = Just x
839 findC (_ : xs) = findC xs
842logLevel = do i <- getIState
843 return (opt_logLevel (idris_options i))
845setAutoImpls :: Bool -> Idris ()
846setAutoImpls b = do i <- getIState
847 let opts = idris_options i
848 let opt' = opts { opt_autoimpls = b }
849 putIState $ i { idris_options = opt' }
851getAutoImpls :: Idris Bool
852getAutoImpls = do i <- getIState
853 return (opt_autoimpls (idris_options i))
855setErrContext :: Bool -> Idris ()
856setErrContext t = do i <- getIState
857 let opts = idris_options i
858 let opts' = opts { opt_errContext = t }
859 putIState $ i { idris_options = opts' }
861errContext :: Idris Bool
862errContext = do i <- getIState
863 return (opt_errContext (idris_options i))
865getOptimise :: Idris [Optimisation]
866getOptimise = do i <- getIState
867 return (opt_optimise (idris_options i))
869setOptimise :: [Optimisation] -> Idris ()
870setOptimise newopts = do i <- getIState
871 let opts = idris_options i
872 let opts' = opts { opt_optimise = newopts }
873 putIState $ i { idris_options = opts' }
875addOptimise :: Optimisation -> Idris ()
876addOptimise opt = do opts <- getOptimise
877 setOptimise (nub (opt : opts))
879removeOptimise :: Optimisation -> Idris ()
880removeOptimise opt = do opts <- getOptimise
881 setOptimise ((nub opts) \\ [opt])
883-- | Set appropriate optimisation set for the given level. We only
884-- have one optimisation that is configurable at the moment, however!
885setOptLevel :: Int -> Idris ()
886setOptLevel n | n <= 0 = setOptimise []
887setOptLevel 1 = setOptimise []
888setOptLevel 2 = setOptimise [PETransform]
889setOptLevel n | n >= 3 = setOptimise [PETransform]
892useREPL = do i <- getIState
893 return (opt_repl (idris_options i))
895setREPL :: Bool -> Idris ()
896setREPL t = do i <- getIState
897 let opts = idris_options i
898 let opt' = opts { opt_repl = t }
899 putIState $ i { idris_options = opt' }
901showOrigErr :: Idris Bool
902showOrigErr = do i <- getIState
903 return (opt_origerr (idris_options i))
905setShowOrigErr :: Bool -> Idris ()
906setShowOrigErr b = do i <- getIState
907 let opts = idris_options i
908 let opt' = opts { opt_origerr = b }
909 putIState $ i { idris_options = opt' }
911setAutoSolve :: Bool -> Idris ()
912setAutoSolve b = do i <- getIState
913 let opts = idris_options i
914 let opt' = opts { opt_autoSolve = b }
915 putIState $ i { idris_options = opt' }
917setNoBanner :: Bool -> Idris ()
918setNoBanner n = do i <- getIState
919 let opts = idris_options i
920 let opt' = opts { opt_nobanner = n }
921 putIState $ i { idris_options = opt' }
923getNoBanner :: Idris Bool
924getNoBanner = do i <- getIState
925 let opts = idris_options i
926 return (opt_nobanner opts)
928setEvalTypes :: Bool -> Idris ()
929setEvalTypes n = do i <- getIState
930 let opts = idris_options i
931 let opt' = opts { opt_evaltypes = n }
932 putIState $ i { idris_options = opt' }
934getDesugarNats :: Idris Bool
935getDesugarNats = do i <- getIState
936 let opts = idris_options i
937 return (opt_desugarnats opts)
940setDesugarNats :: Bool -> Idris ()
941setDesugarNats n = do i <- getIState
942 let opts = idris_options i
943 let opt' = opts { opt_desugarnats = n }
944 putIState $ i { idris_options = opt' }
946setQuiet :: Bool -> Idris ()
947setQuiet q = do i <- getIState
948 let opts = idris_options i
949 let opt' = opts { opt_quiet = q }
950 putIState $ i { idris_options = opt' }
952getQuiet :: Idris Bool
953getQuiet = do i <- getIState
954 let opts = idris_options i
955 return (opt_quiet opts)
957setCodegen :: Codegen -> Idris ()
958setCodegen t = do i <- getIState
959 let opts = idris_options i
960 let opt' = opts { opt_codegen = t }
961 putIState $ i { idris_options = opt' }
963codegen :: Idris Codegen
964codegen = do i <- getIState
965 return (opt_codegen (idris_options i))
968setOutputTy :: OutputType -> Idris ()
969setOutputTy t = do i <- getIState
970 let opts = idris_options i
971 let opt' = opts { opt_outputTy = t }
972 putIState $ i { idris_options = opt' }
974outputTy :: Idris OutputType
975outputTy = do i <- getIState
976 return $ opt_outputTy $ idris_options i
978setIdeMode :: Bool -> Handle -> Idris ()
979setIdeMode True h = do i <- getIState
980 putIState $ i { idris_outputmode = IdeMode 0 h
981 , idris_colourRepl = False
983setIdeMode False _ = return ()
985setTargetTriple :: String -> Idris ()
986setTargetTriple t = do i <- getIState
987 let opts = idris_options i
988 opt' = opts { opt_triple = t }
989 putIState $ i { idris_options = opt' }
991targetTriple :: Idris String
992targetTriple = do i <- getIState
993 return (opt_triple (idris_options i))
995setTargetCPU :: String -> Idris ()
996setTargetCPU t = do i <- getIState
997 let opts = idris_options i
998 opt' = opts { opt_cpu = t }
999 putIState $ i { idris_options = opt' }
1001targetCPU :: Idris String
1002targetCPU = do i <- getIState
1003 return (opt_cpu (idris_options i))
1005verbose :: Idris Bool
1006verbose = do i <- getIState
1007 -- Quietness overrides verbosity
1008 return (not (opt_quiet (idris_options i)) &&
1009 opt_verbose (idris_options i))
1011setVerbose :: Bool -> Idris ()
1012setVerbose t = do i <- getIState
1013 let opts = idris_options i
1014 let opt' = opts { opt_verbose = t }
1015 putIState $ i { idris_options = opt' }
1017typeInType :: Idris Bool
1018typeInType = do i <- getIState
1019 return (opt_typeintype (idris_options i))
1021setTypeInType :: Bool -> Idris ()
1022setTypeInType t = do i <- getIState
1023 let opts = idris_options i
1024 let opt' = opts { opt_typeintype = t }
1025 putIState $ i { idris_options = opt' }
1027coverage :: Idris Bool
1028coverage = do i <- getIState
1029 return (opt_coverage (idris_options i))
1031setCoverage :: Bool -> Idris ()
1032setCoverage t = do i <- getIState
1033 let opts = idris_options i
1034 let opt' = opts { opt_coverage = t }
1035 putIState $ i { idris_options = opt' }
1037setIBCSubDir :: FilePath -> Idris ()
1038setIBCSubDir fp = do i <- getIState
1039 let opts = idris_options i
1040 let opt' = opts { opt_ibcsubdir = fp }
1041 putIState $ i { idris_options = opt' }
1043valIBCSubDir :: IState -> Idris FilePath
1044valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1046addImportDir :: FilePath -> Idris ()
1047addImportDir fp = do i <- getIState
1048 let opts = idris_options i
1049 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1050 putIState $ i { idris_options = opt' }
1052setImportDirs :: [FilePath] -> Idris ()
1053setImportDirs fps = do i <- getIState
1054 let opts = idris_options i
1055 let opt' = opts { opt_importdirs = fps }
1056 putIState $ i { idris_options = opt' }
1058allImportDirs :: Idris [FilePath]
1059allImportDirs = do i <- getIState
1060 let optdirs = opt_importdirs (idris_options i)
1061 return ("." : reverse optdirs)
1063colourise :: Idris Bool
1064colourise = do i <- getIState
1065 return $ idris_colourRepl i
1067setColourise :: Bool -> Idris ()
1068setColourise b = do i <- getIState
1069 putIState $ i { idris_colourRepl = b }
1071impShow :: Idris Bool
1072impShow = do i <- getIState
1073 return (opt_showimp (idris_options i))
1075setImpShow :: Bool -> Idris ()
1076setImpShow t = do i <- getIState
1077 let opts = idris_options i
1078 let opt' = opts { opt_showimp = t }
1079 putIState $ i { idris_options = opt' }
1081setColour :: ColourType -> IdrisColour -> Idris ()
1082setColour ct c = do i <- getIState
1083 let newTheme = setColour' ct c (idris_colourTheme i)
1084 putIState $ i { idris_colourTheme = newTheme }
1085 where setColour' KeywordColour c t = t { keywordColour = c }
1086 setColour' BoundVarColour c t = t { boundVarColour = c }
1087 setColour' ImplicitColour c t = t { implicitColour = c }
1088 setColour' FunctionColour c t = t { functionColour = c }
1089 setColour' TypeColour c t = t { typeColour = c }
1090 setColour' DataColour c t = t { dataColour = c }
1091 setColour' PromptColour c t = t { promptColour = c }
1092 setColour' PostulateColour c t = t { postulateColour = c }
1095logLvl :: Int -> String -> Idris ()
1096logLvl = logLvlCats []
1098logCoverage :: Int -> String -> Idris ()
1099logCoverage = logLvlCats [ICoverage]
1101logErasure :: Int -> String -> Idris ()
1102logErasure = logLvlCats [IErasure]
1104-- | Log an action of the parser
1105logParser :: Int -> String -> Idris ()
1106logParser = logLvlCats parserCats
1108-- | Log an action of the elaborator.
1109logElab :: Int -> String -> Idris ()
1110logElab = logLvlCats elabCats
1112-- | Log an action of the compiler.
1113logCodeGen :: Int -> String -> Idris ()
1114logCodeGen = logLvlCats codegenCats
1116logIBC :: Int -> String -> Idris ()
1117logIBC = logLvlCats [IIBC]
1119-- | Log aspect of Idris execution
1121-- An empty set of logging levels is used to denote all categories.
1123-- @TODO update IDE protocol
1124logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1125 -> Int -- ^ The Logging level the message should appear.
1126 -> String -- ^ The message to show the developer.
1128logLvlCats cs l str = do
1130 let lvl = opt_logLevel (idris_options i)
1131 let cats = opt_logcats (idris_options i)
1133 when (inCat cs cats || null cats) $
1134 case idris_outputmode i of
1136 runIO $ hPutStrLn h str
1138 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1139 runIO . hPutStrLn h $ convSExp "log" good n
1141 inCat :: [LogCat] -> [LogCat] -> Bool
1142 inCat cs cats = any (`elem` cats) cs
1144cmdOptType :: Opt -> Idris Bool
1145cmdOptType x = do i <- getIState
1146 return $ x `elem` opt_cmdline (idris_options i)
1148noErrors :: Idris Bool
1149noErrors = do i <- getIState
1151 Nothing -> return True
1154setTypeCase :: Bool -> Idris ()
1155setTypeCase t = do i <- getIState
1156 let opts = idris_options i
1157 let opt' = opts { opt_typecase = t }
1158 putIState $ i { idris_options = opt' }
1161-- Dealing with parameters
1163expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1164 [Name] -> -- all names
1165 [Name] -> -- names with no declaration
1167expandParams dec ps ns infs tm = en 0 tm
1169 -- if we shadow a name (say in a lambda binding) that is used in a call to
1170 -- a lifted function, we need access to both names - once in the scope of the
1171 -- binding and once to call the lifted functions. So we'll explicitly shadow
1172 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1173 -- but we didn't...)
1175 mkShadow (UN n) = MN 0 n
1176 mkShadow (MN i n) = MN (i+1) n
1177 mkShadow (NS x s) = NS (mkShadow x) s
1179 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1180 -- that are merely mentioned.
1182 en 0 (PLam fc n nfc t s)
1183 | n `elem` (map fst ps ++ ns)
1184 = let n' = mkShadow n in
1185 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1186 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1187 en 0 (PPi p n nfc t s)
1188 | n `elem` (map fst ps ++ ns)
1189 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1190 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1191 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1192 en 0 (PLet fc n nfc ty v s)
1193 | n `elem` (map fst ps ++ ns)
1194 = let n' = mkShadow n in
1195 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1196 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1197 -- FIXME: Should only do this in a type signature!
1198 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1199 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1200 = let n' = mkShadow n in
1201 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1202 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1203 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1204 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1205 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1206 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1207 en 0 (PHidden t) = PHidden (en 0 t)
1208 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1209 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1210 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1211 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1212 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1213 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1215 en 0 (PQuote (Var n))
1216 | n `nselem` ns = PQuote (Var (dec n))
1217 en 0 (PApp fc (PInferRef fc' hl n) as)
1218 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1219 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1220 en 0 (PApp fc (PRef fc' hl n) as)
1221 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1222 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1223 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1224 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1225 en 0 (PAppBind fc (PRef fc' hl n) as)
1226 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1227 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1228 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1229 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1231 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1232 (map ((pexp . (PRef fc hl)) . fst) ps)
1233 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1234 (map ((pexp . (PRef fc hl)) . fst) ps)
1235 en 0 (PInferRef fc hl n)
1236 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1237 (map ((pexp . (PRef fc hl)) . fst) ps)
1238 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1239 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1240 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1241 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1242 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1243 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1245 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1246 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1248 en ql t = descend (en ql) t
1251 nselem x (y : xs) | nseq x y = True
1252 | otherwise = nselem x xs
1254 nseq x y = nsroot x == nsroot y
1256 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1257 enTacImp ql other = other
1259expandParamsD :: Bool -> -- True = RHS only
1261 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1262expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1263 = if n `elem` ns && (not rhsonly)
1264 then -- trace (show (n, expandParams dec ps ns ty)) $
1265 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1266 else --trace (show (n, expandParams dec ps ns ty)) $
1267 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1268expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1269 = if n `elem` ns && (not rhsonly)
1270 then -- trace (show (n, expandParams dec ps ns ty)) $
1271 PPostulate e doc syn fc nfc o (dec n)
1272 (piBind ps (expandParams dec ps ns [] ty))
1273 else --trace (show (n, expandParams dec ps ns ty)) $
1274 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1275expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1276 = let n' = if n `elem` ns then dec n else n in
1277 PClauses fc opts n' (map expandParamsC cs)
1279 expandParamsC (PClause fc n lhs ws rhs ds)
1280 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1281 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1282 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1283 n' = if n `elem` ns then dec n else n
1284 -- names bound on the lhs should not be expanded on the rhs
1285 ns' = removeBound lhs ns in
1287 (map (expandParams dec ps'' ns' []) ws)
1288 (expandParams dec ps'' ns' [] rhs)
1289 (map (expandParamsD True ist dec ps'' ns') ds)
1290 expandParamsC (PWith fc n lhs ws wval pn ds)
1291 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1292 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1293 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1294 n' = if n `elem` ns then dec n else n
1295 ns' = removeBound lhs ns in
1297 (map (expandParams dec ps'' ns' []) ws)
1298 (expandParams dec ps'' ns' [] wval)
1300 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1301 updateps yn nm [] = []
1302 updateps yn nm (((a, t), i):as)
1303 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1304 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1306 removeBound lhs ns = ns \\ nub (bnames lhs)
1308 bnames (PRef _ _ n) = [n]
1309 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1310 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1311 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1314-- | Expands parameters defined in parameter and where blocks inside of declarations
1315expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1316 = PData doc argDocs syn fc co (expandPData pd)
1318 -- just do the type decl, leave constructors alone (parameters will be
1319 -- added implicitly)
1320 expandPData (PDatadecl n nfc ty cons)
1322 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1324 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1325 econ (doc, argDocs, n, nfc, t, fc, fs)
1326 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1327expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1329expandParamsD rhs ist dec ps ns (PParams f params pds)
1330 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1331 (map (expandParamsD True ist dec ps ns) pds)
1332-- (map (expandParamsD ist dec ps ns) pds)
1333expandParamsD rhs ist dec ps ns (PMutual f pds)
1334 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1335expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1337 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1339 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1342 (map (expandParamsD rhs ist dec ps ns) decls)
1345expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1346 = let cn' = case cn of
1347 Just n -> if n `elem` ns then Just (dec n) else Just n
1348 Nothing -> Nothing in
1349 PInstance doc argDocs info f
1350 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1353 (map (expandParams dec ps ns []) params)
1354 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1355 (expandParams dec ps ns [] ty)
1357 (map (expandParamsD True ist dec ps ns) decls)
1358expandParamsD rhs ist dec ps ns d = d
1360mapsnd f (x, t) = (x, f t)
1362expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1363 = PInstance doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1365expandInstanceScope ist dec ps ns d = d
1367-- | Calculate a priority for a type, for deciding elaboration order
1368-- * if it's just a type variable or concrete type, do it early (0)
1369-- * if there's only type variables and injective constructors, do it next (1)
1370-- * if there's a function type, next (2)
1371-- * finally, everything else (3)
1372getPriority :: IState -> PTerm -> Int
1373getPriority i tm = 1 -- pri tm
1376 case lookupP n (tt_ctxt i) of
1377 ((P (DCon _ _ _) _ _):_) -> 1
1378 ((P (TCon _ _) _ _):_) -> 1
1379 ((P Ref _ _):_) -> 1
1380 [] -> 0 -- must be locally bound, if it's not an error...
1381 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1383 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1384 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1385 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1386 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1387 pri (PTyped l r) = pri l
1388 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1389 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1390 pri (PAlternative _ a as) = maximum (map pri as)
1391 pri (PConstant _ _) = 0
1396addStatics :: Name -> Term -> PTerm -> Idris ()
1397addStatics n tm ptm =
1398 do let (statics, dynamics) = initStatics tm ptm
1401 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1402 Just p -> getNamesFrom 0 (fn_params p) tm ++
1403 concatMap (getParamNames ist . snd) statics
1404 _ -> concatMap (getParamNames ist . snd) statics
1406 let stnames = nub $ concatMap (freeArgNames . snd) statics
1407 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1409 -- also get the arguments which are 'uniquely inferrable' from
1410 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1411 -- or parameters to the type of a static
1412 let statics' = nub $ map fst statics ++
1413 filter (\x -> not (elem x dnames)) stnames
1414 let stpos = staticList statics' tm
1416 unless (null statics) $
1417 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1418 ++ showTmImpls ptm ++ "\n"
1419 ++ show statics ++ "\n" ++ show dynamics
1420 ++ "\n" ++ show paramnames
1421 ++ "\n" ++ show stpos
1422 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1423 addIBC (IBCStatic n)
1425 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1426 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1427 (static, (n, ty) : dynamic)
1428 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1429 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1430 if pstatic p == Static then ((n, ty) : static, dynamic)
1431 else if (not (searchArg p))
1432 then (static, (n, ty) : dynamic)
1433 else (static, dynamic)
1434 initStatics t pt = ([], [])
1436 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1437 = case lookupCtxtExact n (idris_datatypes ist) of
1438 Just ti -> getNamePos 0 (param_pos ti) args
1440 where getNamePos i ps [] = []
1441 getNamePos i ps (P _ n _ : as)
1442 | i `elem` ps = n : getNamePos (i + 1) ps as
1443 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1444 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1445 = n : getParamNames ist sc
1446 getParamNames ist _ = []
1448 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1449 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1450 | otherwise = getNamesFrom (i + 1) ps sc
1451 getNamesFrom i ps sc = []
1453 freeArgNames (Bind n (Pi _ ty _) sc)
1454 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1455 freeArgNames tm = let (_, args) = unApply tm in
1456 concatMap freeNames args
1458 -- if a name appears in a type class or tactic implicit index, it doesn't
1459 -- affect its 'uniquely inferrable' from a static status since these are
1460 -- resolved by searching.
1461 searchArg (Constraint _ _) = True
1462 searchArg (TacImp _ _ _) = True
1465 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1468-- Dealing with implicit arguments
1470-- Add some bound implicits to the using block if they aren't there already
1472addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1473addToUsing us [] = us
1474addToUsing us ((n, t) : ns)
1475 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1476 | otherwise = addToUsing us ns
1477 where impName (UImplicit n _) = Just n
1480-- Add constraint bindings from using block
1482addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1483addUsingConstraints syn fc t
1485 let ns = namesIn [] ist t
1486 let cs = getConstraints t -- check declared constraints
1487 let addconsts = uconsts \\ cs
1488 return (doAdd addconsts ns t)
1489 where uconsts = filter uconst (using syn)
1490 uconst (UConstraint _ _) = True
1494 -- if all of args in ns, then add it
1495 doAdd (UConstraint c args : cs) ns t
1496 | all (\n -> elem n ns) args
1497 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1498 (mkConst c args) (doAdd cs ns t)
1499 | otherwise = doAdd cs ns t
1501 mkConst c args = PApp fc (PRef fc [] c)
1502 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1504 getConstraints (PPi (Constraint _ _) _ _ c sc)
1505 = getcapp c ++ getConstraints sc
1506 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1507 getConstraints _ = []
1509 getcapp (PApp _ (PRef _ _ c) args)
1510 = do ns <- mapM getName args
1511 return (UConstraint c ns)
1514 getName (PExp _ _ _ (PRef _ _ n)) = return n
1517-- | Add implicit bindings from using block, and bind any missing names
1518addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1519addUsingImpls syn n fc t
1520 = do ist <- getIState
1521 autoimpl <- getAutoImpls
1522 let ns_in = implicitNamesIn (map iname uimpls) ist t
1523 let ns = if autoimpl then ns_in
1524 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1526 let badnames = filter (\n -> not (implicitable n) &&
1527 n `notElem` (map iname uimpls)) ns
1528 unless (null badnames) $
1529 throwError (At fc (Elaborating "type of " n Nothing
1530 (NoSuchVariable (head badnames))))
1531 let cs = getArgnames t -- get already bound names
1532 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1533 -- if all names in the arguments of addconsts appear in ns,
1534 -- add the constraint implicitly
1535 return (bindFree ns (doAdd addimpls ns t))
1536 where uimpls = filter uimpl (using syn)
1537 uimpl (UImplicit _ _) = True
1540 iname (UImplicit n _) = n
1541 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1544 -- if all of args in ns, then add it
1545 doAdd (UImplicit n ty : cs) ns t
1547 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1548 | otherwise = doAdd cs ns t
1550 -- bind the free names which weren't in the using block
1553 | elem n (map iname uimpls) = bindFree ns tm
1555 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1557 getArgnames (PPi _ n _ c sc)
1558 = n : getArgnames sc
1561-- Given the original type and the elaborated type, return the implicitness
1562-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1564getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1565getUnboundImplicits i t tm = getImps t (collectImps tm)
1566 where collectImps (PPi p n _ t sc)
1567 = (n, (p, t)) : collectImps sc
1570 scopedimpl (Just i) = not (toplevel_imp i)
1571 scopedimpl _ = False
1573 getImps (Bind n (Pi i _ _) sc) imps
1574 | scopedimpl i = getImps sc imps
1575 getImps (Bind n (Pi _ t _) sc) imps
1576 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1578 argInfo n (Imp opt _ _ _ _) Placeholder
1579 = (True, PImp 0 True opt n Placeholder)
1580 argInfo n (Imp opt _ _ _ _) t'
1581 = (False, PImp (getPriority i t') True opt n t')
1582 argInfo n (Exp opt _ _) t'
1583 = (InaccessibleArg `elem` opt,
1584 PExp (getPriority i t') opt n t')
1585 argInfo n (Constraint opt _) t'
1586 = (InaccessibleArg `elem` opt,
1587 PConstraint 10 opt n t')
1588 argInfo n (TacImp opt _ scr) t'
1589 = (InaccessibleArg `elem` opt,
1590 PTacImplicit 10 opt n scr t')
1591 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1592 where impBind n t = (True, PImp 1 True [] n Placeholder)
1595-- Add implicit Pi bindings for any names in the term which appear in an
1596-- argument position.
1598-- This has become a right mess already. Better redo it some time...
1599-- TODO: This is obsoleted by the new way of elaborating types, (which
1600-- calls addUsingImpls) but there's still a couple of places which use
1601-- it. Clean them up!
1603-- Issue 1739 in the issue tracker
1604-- https://github.com/idris-lang/Idris-dev/issues/1739
1605implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1606implicit info syn n ptm = implicit' info syn [] n ptm
1608implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1609implicit' info syn ignore n ptm
1611 auto <- getAutoImpls
1612 let (tm', impdata) = implicitise auto syn ignore i ptm
1613 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1614-- let (tm'', spos) = findStatics i tm'
1615 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1617 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1619-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1622 -- Detect unknown names in default arguments and throw error if found.
1623 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1624 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1626 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1627 notFoundInDefault kns (PTacImplicit _ _ n script _)
1629 case notFound kns (namesIn [] i script) of
1630 Nothing -> return (n:kns)
1631 Just name -> throwError (NoSuchVariable name)
1632 notFoundInDefault kns p = return ((pname p):kns)
1634 notFound :: [Name] -> [Name] -> Maybe Name
1635 notFound kns [] = Nothing
1636 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1637 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1639-- | Even if auto_implicits is off, we need to call this so we record
1640-- which arguments are implicit
1641implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1642implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1643 let (declimps, ns') = execState (imps True [] tm) ([], [])
1644 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1645 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1646 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1648 then (tm, reverse declimps)
1649 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1651 uvars = map ipair (filter uimplicit (using syn))
1652 pvars = syn_params syn
1654 inUsing n = n `elem` map fst uvars
1656 ipair (UImplicit x y) = (x, y)
1657 uimplicit (UImplicit _ _) = True
1660 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1661 | otherwise = x : dropAll xs ys
1664 -- Find names in argument position in a type, suitable for implicit
1666 -- Not the function position, but do everything else...
1667 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1668 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1670 imps top env ty@(PApp _ f as)
1671 = do (decls, ns) <- get
1672 let isn = nub (implNamesIn uvars ty)
1673 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1674 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1675 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1677 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1678 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1679 imps True (n:env) sc
1680 imps top env (PPi (Exp l _ _) n _ ty sc)
1681 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1682 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1684 (decls, ns) <- get -- ignore decls in HO types
1685 put (PExp (getPriority ist ty) l n Placeholder : decls,
1686 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1687 imps True (n:env) sc
1688 imps top env (PPi (Constraint l _) n _ ty sc)
1689 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1690 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1692 (decls, ns) <- get -- ignore decls in HO types
1693 put (PConstraint 10 l n Placeholder : decls,
1694 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1695 imps True (n:env) sc
1696 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1697 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1698 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1700 (decls, ns) <- get -- ignore decls in HO types
1701 put (PTacImplicit 10 l n scr Placeholder : decls,
1702 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1703 imps True (n:env) sc
1704 imps top env (PRewrite _ _ l r _)
1705 = do (decls, ns) <- get
1706 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1707 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1708 imps top env (PTyped l r)
1710 imps top env (PPair _ _ _ l r)
1711 = do (decls, ns) <- get
1712 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1713 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1714 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1715 = do (decls, ns) <- get
1716 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1717 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1718 imps top env (PDPair _ _ _ l t r)
1719 = do (decls, ns) <- get
1720 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1722 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1723 imps top env (PAlternative ms a as)
1724 = do (decls, ns) <- get
1725 let isn = concatMap (namesIn uvars ist) as
1726 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1727 imps top env (PLam fc n _ ty sc)
1728 = do imps False env ty
1729 imps False (n:env) sc
1730 imps top env (PHidden tm) = imps False env tm
1731 imps top env (PUnifyLog tm) = imps False env tm
1732 imps top env (PNoImplicits tm) = imps False env tm
1733 imps top env (PRunElab fc tm ns) = imps False env tm
1734 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1735 imps top env _ = return ()
1737 pibind using [] sc = sc
1738 pibind using (n:ns) sc
1739 = case lookup n using of
1740 Just ty -> PPi impl_gen
1741 n NoFC ty (pibind using ns sc)
1742 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1743 n NoFC Placeholder (pibind using ns sc)
1745-- | Add implicit arguments in function calls
1746addImplPat :: IState -> PTerm -> PTerm
1747addImplPat = addImpl' True [] [] []
1749addImplBound :: IState -> [Name] -> PTerm -> PTerm
1750addImplBound ist ns = addImpl' False ns [] [] ist
1752addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1753addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1755-- | Add the implicit arguments to applications in the term [Name]
1756-- gives the names to always expend, even when under a binder of that
1757-- name (this is to expand methods with implicit arguments in
1758-- dependent type classes).
1759addImpl :: [Name] -> IState -> PTerm -> PTerm
1760addImpl = addImpl' False [] []
1762-- TODO: in patterns, don't add implicits to function names guarded by constructors
1763-- and *not* inside a PHidden
1765addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1766addImpl' inpat env infns imp_meths ist ptm
1767 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1769 topname = case ptm of
1771 PApp _ (PRef _ _ n) _ -> n
1772 _ -> sUN "" -- doesn't matter then
1774 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1775 ai inpat qq env ds (PRef fc fcs f)
1776 | f `elem` infns = PInferRef fc fcs f
1777 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1778 ai inpat qq env ds (PHidden (PRef fc hl f))
1779 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1780 ai inpat qq env ds (PRewrite fc by l r g)
1781 = let l' = ai inpat qq env ds l
1782 r' = ai inpat qq env ds r
1783 g' = fmap (ai inpat qq env ds) g in
1784 PRewrite fc by l' r' g'
1785 ai inpat qq env ds (PTyped l r)
1786 = let l' = ai inpat qq env ds l
1787 r' = ai inpat qq env ds r in
1789 ai inpat qq env ds (PPair fc hls p l r)
1790 = let l' = ai inpat qq env ds l
1791 r' = ai inpat qq env ds r in
1792 PPair fc hls p l' r'
1793 ai inpat qq env ds (PDPair fc hls p l t r)
1794 = let l' = ai inpat qq env ds l
1795 t' = ai inpat qq env ds t
1796 r' = ai inpat qq env ds r in
1797 PDPair fc hls p l' t' r'
1798 ai inpat qq env ds (PAlternative ms a as)
1799 = let as' = map (ai inpat qq env ds) as in
1800 PAlternative ms a as'
1801 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1802 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1803 = let as' = map (fmap (ai inpat qq env ds)) as in
1804 PApp fc (PInferRef ffc hl f) as'
1805 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1806 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1807 | not (f `elem` map fst env)
1808 = let as' = map (fmap (ai inpat qq env ds)) as in
1809 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1810 | Just (Just ty) <- lookup f env =
1811 let as' = map (fmap (ai inpat qq env ds)) as
1812 arity = getPArity ty in
1813 mkPApp fc arity ftm as'
1814 ai inpat qq env ds (PApp fc f as)
1815 = let f' = ai inpat qq env ds f
1816 as' = map (fmap (ai inpat qq env ds)) as in
1818 ai inpat qq env ds (PWithApp fc f a)
1819 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1820 ai inpat qq env ds (PCase fc c os)
1821 = let c' = ai inpat qq env ds c in
1822 -- leave lhs alone, because they get lifted into a new pattern match
1823 -- definition which is passed through addImpl again
1824 PCase fc c' (map aiCase os)
1827 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1829 -- Anything beginning with a lower case letter, not applied,
1830 -- and no namespace is a pattern variable
1831 patnames (PApp _ (PRef _ _ f) [])
1832 | implicitable f = [(f, Nothing)]
1833 patnames (PRef _ _ f)
1834 | implicitable f = [(f, Nothing)]
1835 patnames (PApp _ (PRef _ _ _) args)
1836 = concatMap patnames (map getTm args)
1837 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1838 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1839 patnames (PAs _ _ t) = patnames t
1840 patnames (PAlternative _ _ ts) = concatMap patnames ts
1844 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1845 (ai inpat qq env ds t)
1846 (ai inpat qq env ds f)
1848 -- If the name in a lambda is an unapplied data constructor name, do this
1849 -- as a 'case' instead because we'll expect to match on it
1850 ai inpat qq env ds (PLam fc n nfc ty sc)
1851 = if canBeDConName n (tt_ctxt ist)
1852 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1853 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1854 [(PRef fc [] n, sc)]))
1855 else let ty' = ai inpat qq env ds ty
1856 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1857 PLam fc n nfc ty' sc'
1858 ai inpat qq env ds (PLet fc n nfc ty val sc)
1859 = if canBeDConName n (tt_ctxt ist)
1860 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1861 else let ty' = ai inpat qq env ds ty
1862 val' = ai inpat qq env ds val
1863 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1864 PLet fc n nfc ty' val' sc'
1865 ai inpat qq env ds (PPi p n nfc ty sc)
1866 = let ty' = ai inpat qq env ds ty
1867 env' = if n `elem` imp_meths then env
1868 else ((n, Just ty) : env)
1869 sc' = ai inpat qq env' ds sc in
1871 ai inpat qq env ds (PGoal fc r n sc)
1872 = let r' = ai inpat qq env ds r
1873 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1875 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1876 -- Don't do PProof or PTactics since implicits get added when scope is
1877 -- properly known in ElabTerm.runTac
1878 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1879 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1880 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1881 (fmap (ai inpat True env ds) g)
1882 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1883 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1884 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1885 ai inpat qq env ds tm = tm
1887 handleErr (Left err) = PElabError err
1888 handleErr (Right x) = x
1890-- if in a pattern, and there are no arguments, and there's no possible
1891-- names with zero explicit arguments, don't add implicits.
1893aiFn :: Name -> Bool -> Bool -> Bool
1896 -> Name -- ^ function being applied
1898 -> [PArg] -- ^ initial arguments (if in a pattern)
1900aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1901 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1903 = case lookupDef f (tt_ctxt ist) of
1904 [] -> Right $ PPatvar ffc f
1905 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1906 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1907 if (not (vname f) || tcname f
1908 || any (conCaf (tt_ctxt ist)) ialts)
1909-- any constructor alts || any allImp ialts))
1910 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1911 else Right $ PPatvar ffc f
1912 where imp (PExp _ _ _ _) = False
1915 allImp xs = all imp xs
1917 unqualified (NS _ _) = False
1918 unqualified _ = True
1920 constructor (TyDecl (DCon _ _ _) _) = True
1921 constructor _ = False
1923 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1925 vname (UN n) = True -- non qualified
1928aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1929 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1930aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1931 -- This is where namespaces get resolved by adding PAlternative
1932 = do let ns = lookupCtxtName f (idris_implicits ist)
1933 let nh = filter (\(n, _) -> notHidden n) ns
1934 let ns' = case trimAlts ds nh of
1938 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1940 [] -> if f `elem` (map fst (idris_metavars ist))
1941 then Right $ PApp fc (PRef ffc [ffc] f) as
1942 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1944 PAlternative [] (ExactlyOne True) $
1945 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1946 (insertImpl ns as)) alts
1948 -- if the name is in imp_meths, we should actually refer to the bound
1949 -- name rather than the global one after expanding implicits
1950 isImpName f f' | f `elem` imp_meths = f
1953 trimAlts [] alts = alts
1955 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1960 notHidden n = case getAccessibility n of
1966 = case lookupDefAccExact n False (tt_ctxt ist) of
1970 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1971 -> [PArg] -- ^ given arguments
1974 = let (as', badimpls) = partition (impIn ps) as in
1975 map addUnknownImp badimpls ++
1976 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1978 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1979 -> [PArg] -- parameters
1980 -> [PArg] -- explicit arguments
1981 -> [PArg] -- implicits given
1983 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1984 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1985 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1986 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1987 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1988 let rtc = PResolveTC fc in
1989 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1990 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1991 case find n imps [] of
1993 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1995 PImp p True l n Placeholder :
1996 insImpAcc (M.insert n Placeholder pnas) ps given imps
1997 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1998 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1999 case find n imps [] of
2001 PTacImplicit p l n sc tm :
2002 insImpAcc (M.insert n tm pnas) ps given imps'
2005 then PTacImplicit p l n sc Placeholder :
2006 insImpAcc (M.insert n Placeholder pnas) ps given imps
2007 else PTacImplicit p l n sc sc :
2008 insImpAcc (M.insert n sc pnas) ps given imps
2009 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2010 insImpAcc _ _ given imps = given ++ imps
2012 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2014 find n [] acc = Nothing
2015 find n (PImp _ _ _ n' t : gs) acc
2016 | n == n' = Just (t, reverse acc ++ gs)
2017 find n (PTacImplicit _ _ n' _ t : gs) acc
2018 | n == n' = Just (t, reverse acc ++ gs)
2019 find n (g : gs) acc = find n gs (g : acc)
2021-- | return True if the second argument is an implicit argument which
2022-- is expected in the implicits, or if it's not an implicit
2023impIn :: [PArg] -> PArg -> Bool
2024impIn ps (PExp _ _ _ _) = True
2025impIn ps (PConstraint _ _ _ _) = True
2026impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2028expArg (PExp _ _ _ _) = True
2029expArg (PConstraint _ _ _ _) = True
2032-- replace non-linear occurrences with _
2034stripLinear :: IState -> PTerm -> PTerm
2035stripLinear i tm = evalState (sl tm) [] where
2036 sl :: PTerm -> State [Name] PTerm
2038 | (_:_) <- lookupTy f (tt_ctxt i)
2039 = return $ PRef fc hl f
2040 | otherwise = do ns <- get
2042 then return $ PHidden (PRef fc hl f) -- Placeholder
2043 else do put (f : ns)
2044 return (PRef fc hl f)
2048 then return $ PHidden (PPatvar fc f) -- Placeholder
2049 else do put (f : ns)
2050 return (PPatvar fc f)
2051 -- Assumption is that variables are all the same in each alternative
2052 sl t@(PAlternative ms b as) = do ns <- get
2054 return (PAlternative ms b as')
2055 where slAlts ns (a : as) = do put ns
2059 slAlts ns [] = return []
2060 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2061 sl (PDPair fc hls p l t r) = do l' <- sl l
2064 return (PDPair fc hls p l' t' r')
2065 sl (PApp fc fn args) = do fn' <- case fn of
2066 -- Just the args, fn isn't matchable as a var
2067 PRef _ _ _ -> return fn
2069 args' <- mapM slA args
2070 return $ PApp fc fn' args'
2071 where slA (PImp p m l n t) = do t' <- sl t
2072 return $ PImp p m l n t'
2073 slA (PExp p l n t) = do t' <- sl t
2074 return $ PExp p l n t'
2075 slA (PConstraint p l n t)
2077 return $ PConstraint p l n t'
2078 slA (PTacImplicit p l n sc t)
2080 return $ PTacImplicit p l n sc t'
2083-- | Remove functions which aren't applied to anything, which must then
2084-- be resolved by unification. Assume names resolved and alternatives
2085-- filled in (so no ambiguity).
2086stripUnmatchable :: IState -> PTerm -> PTerm
2087stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2088 su :: PTerm -> PTerm
2089 su tm@(PRef fc hl f)
2090 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2092 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2093 not (implicitable f)
2095 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2096 not (implicitable f)
2098 su (PApp fc f@(PRef _ _ fn) args)
2099 -- here we use canBeDConName because the impossible pattern
2100 -- check will not necessarily fully resolve constructor names,
2101 -- and these bare names will otherwise get in the way of
2102 -- impossbility checking.
2103 | canBeDConName fn ctxt
2104 = PApp fc f (fmap (fmap su) args)
2106 = PHidden (PApp fc f args)
2107 su (PAlternative ms b alts)
2108 = let alts' = filter (/= Placeholder) (map su alts) in
2109 if null alts' then Placeholder
2110 else PAlternative ms b alts'
2111 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2112 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2113 su t@(PLam fc _ _ _ _) = PHidden t
2114 su t@(PPi _ _ _ _ _) = PHidden t
2115 su t@(PConstant _ c) | isTypeConst c = PHidden t
2120stripUnmatchable i tm = tm
2123mkPApp fc a f as = let rest = drop a as in
2124 if a == 0 then appRest fc f rest
2125 else appRest fc (PApp fc f (take a as)) rest
2128 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2132-- | Find 'static' argument positions
2133-- (the declared ones, plus any names in argument position in the declared
2135-- FIXME: It's possible that this really has to happen after elaboration
2136findStatics :: IState -> PTerm -> (PTerm, [Bool])
2137findStatics ist tm = let (ns, ss) = fs tm
2138 in runState (pos ns ss tm) []
2139 where fs (PPi p n fc t sc)
2140 | Static <- pstatic p
2141 = let (ns, ss) = fs sc in
2142 (namesIn [] ist t : ns, n : ss)
2143 | otherwise = let (ns, ss) = fs sc in
2147 inOne n ns = length (filter id (map (elem n) ns)) == 1
2149 pos ns ss (PPi p n fc t sc)
2150 | elem n ss = do sc' <- pos ns ss sc
2153 return (PPi (p { pstatic = Static }) n fc t sc')
2154 | otherwise = do sc' <- pos ns ss sc
2157 return (PPi p n fc t sc')
2158 pos ns ss t = return t
2160-- for 6.12/7 compatibility
2161data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2163instance Applicative (EitherErr a) where
2167instance Monad (EitherErr a) where
2170 (LeftErr e) >>= k = LeftErr e
2171 RightOK v >>= k = k v
2173toEither (LeftErr e) = Left e
2174toEither (RightOK ho) = Right ho
2176-- | Syntactic match of a against b, returning pair of variables in a
2177-- and what they match. Returns the pair that failed if not a match.
2178matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2179matchClause = matchClause' False
2181matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2182matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2183 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2185 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2188 match' x y = match (fullApp x) (fullApp y)
2189 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2190 | fi == txt "fromInteger" && b == txt "builtins",
2191 PConstant _ (I _) <- getTm x = match (getTm x) x'
2192 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2193 | fi == txt "fromInteger" && b == txt "builtins",
2194 PConstant _ (I _) <- getTm x = match (getTm x) x'
2195 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2196 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2197 match (PApp _ f args) (PApp _ f' args')
2198 | length args == length args'
2199 = do mf <- match' f f'
2200 ms <- zipWithM matchArg args args'
2201 return (mf ++ concat ms)
2202 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2203 match (PPatvar f n) xr = match (PRef f [f] n) xr
2204 match xr (PPatvar f n) = match xr (PRef f [f] n)
2205 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2206 match (PRef _ _ n) tm@(PRef _ _ n')
2207 | n == n' && not names &&
2208 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2209 || tm == Placeholder)
2211 -- if one namespace is missing, drop the other
2212 | n == n' || n == dropNS n' || dropNS n == n' = return []
2213 where dropNS (NS n _) = n
2215 match (PRef _ _ n) tm
2216 | not names && (not (isConName n (tt_ctxt i) ||
2217 isFnName n (tt_ctxt i)) || tm == Placeholder)
2219 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2220 = do ml <- match' l l'
2223 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2226 match (PTyped l r) x = match l x
2227 match x (PTyped l r) = match x l
2228 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2231 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2234 return (ml ++ mt ++ mr)
2235 match (PAlternative _ a as) (PAlternative _ a' as')
2236 = do ms <- zipWithM match' as as'
2238 match a@(PAlternative _ _ as) b
2239 = do let ms = zipWith match' as (repeat b)
2240 case (rights (map toEither ms)) of
2243 match (PCase _ _ _) _ = return [] -- lifted out
2244 match (PMetavar _ _) _ = return [] -- modified
2245 match (PInferRef _ _ _) _ = return [] -- modified
2246 match (PQuote _) _ = return []
2247 match (PProof _) _ = return []
2248 match (PTactics _) _ = return []
2249 match (PResolveTC _) (PResolveTC _) = return []
2250 match (PTrue _ _) (PTrue _ _) = return []
2251 match (PReturn _) (PReturn _) = return []
2252 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2255 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2258 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2259 mty <- match' ty ty'
2261 return (mt ++ mty ++ ms)
2262 match (PHidden x) (PHidden y)
2263 | RightOK xs <- match x y = return xs -- to collect variables
2264 | otherwise = return [] -- Otherwise hidden things are unmatchable
2266 | RightOK xs <- match x y = return xs
2267 | otherwise = return []
2269 | RightOK xs <- match x y = return xs
2270 | otherwise = return []
2271 match (PUnifyLog x) y = match' x y
2272 match x (PUnifyLog y) = match' x y
2273 match (PNoImplicits x) y = match' x y
2274 match x (PNoImplicits y) = match' x y
2275 match Placeholder _ = return []
2276 match _ Placeholder = return []
2277 match (PResolveTC _) _ = return []
2278 match a b | a == b = return []
2279 | otherwise = LeftErr (a, b)
2281 checkRpts (RightOK ms) = check ms where
2283 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2286 check (_:xs) = check xs
2288 checkRpts (LeftErr x) = Left x
2290substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2291substMatches ms = substMatchesShadow ms []
2293-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2294-- substMatchesShadow [] shs t = t
2295-- substMatchesShadow ((n,tm):ns) shs t
2296-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2298substMatch :: Name -> PTerm -> PTerm -> PTerm
2299substMatch n = substMatchShadow n []
2301substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2302substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2304substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2305substMatchesShadow nmap shs t = sm shs t where
2306 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2307 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2308 sm xs (PPi p x fc t sc)
2310 = let x' = nextName x in
2311 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2312 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2313 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2314 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2315 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2316 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2317 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2319 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2320 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2321 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2322 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2323 sm xs (PHidden x) = PHidden (sm xs x)
2324 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2325 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2326 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2327 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2330 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2333shadow :: Name -> Name -> PTerm -> PTerm
2334shadow n n' t = sm 0 t where
2335 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2336 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2337 | otherwise = PLam fc x xfc (sm 0 t) sc
2338 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2339 | otherwise = PPi p x fc (sm 0 t) sc
2340 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2341 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2342 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2343 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2344 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2345 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2346 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2347 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2348 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2349 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2350 sm 0 (PAlternative ms a as)
2351 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2352 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2353 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2354 sm 0 (PHidden x) = PHidden (sm 0 x)
2355 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2356 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2357 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2358 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2359 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2360 sm ql x = descend (sm ql) x
2362 shadowAlt p@(x, oldn) = (update x, update oldn)
2363 update oldn | n == oldn = n'
2366-- | Rename any binders which are repeated (so that we don't have to
2367-- mess about with shadowing anywhere else).
2368mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2369mkUniqueNames env shadows tm
2370 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2372 initMap = M.fromList shadows
2374 inScope :: S.Set Name
2375 inScope = S.fromList $ boundNamesIn tm
2377 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2378 return (arg { getTm = t' })
2380 -- Initialise the unique name with the environment length (so we're not
2381 -- looking for too long...)
2382 initN (UN n) l = UN $ txt (str n ++ show l)
2383 initN (MN i s) l = MN (i+l) s
2386 -- FIXME: Probably ought to do this for completeness! It's fine as
2387 -- long as there are no bindings inside tactics though.
2388 mkUniqT _ nmap tac = return tac
2390 mkUniq :: Int -- ^ The number of quotations that we're under
2391 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2392 mkUniq 0 nmap (PLam fc n nfc ty sc)
2396 then do let n' = uniqueNameSet (initN n (S.size env))
2397 (S.union env inScope)
2398 return (n', sc) -- shadow n n' sc)
2400 put (S.insert n' env)
2401 let nmap' = M.insert n n' nmap
2402 ty' <- mkUniq 0 nmap ty
2403 sc'' <- mkUniq 0 nmap' sc'
2404 return $! PLam fc n' nfc ty' sc''
2405 mkUniq 0 nmap (PPi p n fc ty sc)
2409 then do let n' = uniqueNameSet (initN n (S.size env))
2410 (S.union env inScope)
2411 return (n', sc) -- shadow n n' sc)
2413 put (S.insert n' env)
2414 let nmap' = M.insert n n' nmap
2415 ty' <- mkUniq 0 nmap ty
2416 sc'' <- mkUniq 0 nmap' sc'
2417 return $! PPi p n' fc ty' sc''
2418 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2422 then do let n' = uniqueNameSet (initN n (S.size env))
2423 (S.union env inScope)
2424 return (n', sc) -- shadow n n' sc)
2426 put (S.insert n' env)
2427 let nmap' = M.insert n n' nmap
2428 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2429 sc'' <- mkUniq 0 nmap' sc'
2430 return $! PLet fc n' nfc ty' val' sc''
2431 mkUniq 0 nmap (PApp fc t args)
2432 = do t' <- mkUniq 0 nmap t
2433 args' <- mapM (mkUniqA 0 nmap) args
2434 return $! PApp fc t' args'
2435 mkUniq 0 nmap (PAppBind fc t args)
2436 = do t' <- mkUniq 0 nmap t
2437 args' <- mapM (mkUniqA 0 nmap) args
2438 return $! PAppBind fc t' args'
2439 mkUniq 0 nmap (PCase fc t alts)
2440 = do t' <- mkUniq 0 nmap t
2441 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2442 return (x', y')) alts
2443 return $! PCase fc t' alts'
2444 mkUniq 0 nmap (PIfThenElse fc c t f)
2445 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2446 mkUniq 0 nmap (PPair fc hls p l r)
2447 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2448 return $! PPair fc hls p l' r'
2449 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2452 (n', sc') <- if n `S.member` env
2453 then do let n' = uniqueNameSet n (S.union env inScope)
2454 return (n', sc) -- shadow n n' sc)
2456 put (S.insert n' env)
2457 let nmap' = M.insert n n' nmap
2458 t' <- mkUniq 0 nmap t
2459 sc'' <- mkUniq 0 nmap' sc'
2460 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2461 mkUniq 0 nmap (PDPair fc hls p l t r)
2462 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2463 return $! PDPair fc hls p l' t' r'
2464 mkUniq 0 nmap (PAlternative ns b as)
2465 -- store the nmap and defer the rest until we've pruned the set
2466 -- during elaboration
2467 = return $ PAlternative (ns ++ M.toList nmap) b as
2468 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2469 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2470 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2471 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2472 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2473 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2474 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2475 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2476 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2477 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2480 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2482 mkUniq ql nmap (PQuasiquote tm ty) =
2483 do tm' <- mkUniq (ql + 1) nmap tm
2485 Nothing -> return Nothing
2486 Just t -> fmap Just $ mkUniq ql nmap t
2487 return $! PQuasiquote tm' ty'
2488 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2490 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