1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
12import Idris.Docstrings
13import Idris.IdeMode hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import System.Console.Haskeline
19import System.Directory (canonicalizePath, doesFileExist)
21import Control.Applicative
22import Control.Monad (liftM3)
23import Control.Monad.State
25import Data.List hiding (insert,union)
27import qualified Data.Text as T
29import qualified Data.Map as M
31import qualified Data.Set as S
32import Data.Word (Word)
34import Data.Generics.Uniplate.Data (descend, descendM)
38import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
44getContext :: Idris Context
45getContext = do i <- getIState; return (tt_ctxt i)
47forCodegen :: Codegen -> [(Codegen, a)] -> [a]
48forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
50getObjectFiles :: Codegen -> Idris [FilePath]
51getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
53addObjectFile :: Codegen -> FilePath -> Idris ()
54addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
56getLibs :: Codegen -> Idris [String]
57getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
59addLib :: Codegen -> String -> Idris ()
60addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
62getFlags :: Codegen -> Idris [String]
63getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
65addFlag :: Codegen -> String -> Idris ()
66addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
68addDyLib :: [String] -> Idris (Either DynamicLib String)
69addDyLib libs = do i <- getIState
70 let ls = idris_dynamic_libs i
71 let importdirs = opt_importdirs (idris_options i)
72 case mapMaybe (findDyLib ls) libs of
73 x:_ -> return (Left x)
75 handle <- lift . lift .
76 mapM (\l -> catchIO (tryLoadLib importdirs l)
77 (\_ -> return Nothing)) $ libs
79 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
80 intercalate "," libs ++ "\"")
81 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
83 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
84 findDyLib [] l = Nothing
85 findDyLib (lib:libs) l | l == lib_name lib = Just lib
86 | otherwise = findDyLib libs l
88getAutoImports :: Idris [FilePath]
89getAutoImports = do i <- getIState
90 return (opt_autoImport (idris_options i))
92addAutoImport :: FilePath -> Idris ()
93addAutoImport fp = do i <- getIState
94 let opts = idris_options i
95 let autoimps = opt_autoImport opts
96 put (i { idris_options = opts { opt_autoImport =
97 fp : opt_autoImport opts } } )
99addDefinedName :: Name -> Idris ()
100addDefinedName n = do ist <- getIState
101 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
103getDefinedNames :: Idris [Name]
104getDefinedNames = do ist <- getIState
105 return (S.toList (idris_inmodule ist))
107addTT :: Term -> Idris (Maybe Term)
108addTT t = do ist <- getIState
109 case M.lookup t (idris_ttstats ist) of
110 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
111 putIState $ ist { idris_ttstats = tt' }
113 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
114 putIState $ ist { idris_ttstats = tt' }
118dumpTT = do ist <- get
119 let sts = sortBy count (M.toList (idris_ttstats ist))
123 count (_,x) (_,y) = compare y x
124 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
126addHdr :: Codegen -> String -> Idris ()
127addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
129addImported :: Bool -> FilePath -> Idris ()
132 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
134addLangExt :: LanguageExt -> Idris ()
135addLangExt TypeProviders = do i <- getIState
137 idris_language_extensions = TypeProviders : idris_language_extensions i
139addLangExt ErrorReflection = do i <- getIState
141 idris_language_extensions = ErrorReflection : idris_language_extensions i
144-- Transforms are organised by the function being applied on the lhs of the
145-- transform, to make looking up appropriate transforms quicker
146addTrans :: Name -> (Term, Term) -> Idris ()
149 let t' = case lookupCtxtExact basefn (idris_transforms i) of
150 Just def -> (t : def)
152 putIState $ i { idris_transforms = addDef basefn t'
153 (idris_transforms i) }
155addErrRev :: (Term, Term) -> Idris ()
156addErrRev t = do i <- getIState
157 putIState $ i { idris_errRev = t : idris_errRev i }
159addErasureUsage :: Name -> Int -> Idris ()
160addErasureUsage n i = do ist <- getIState
161 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
163addExport :: Name -> Idris ()
164addExport n = do ist <- getIState
165 putIState $ ist { idris_exports = n : idris_exports ist }
167addUsedName :: FC -> Name -> Name -> Idris ()
169 = do ist <- getIState
170 case lookupTyName n (tt_ctxt ist) of
171 [(n', ty)] -> addUsage n' 0 ty
172 [] -> throwError (At fc (NoSuchVariable n))
173 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
174 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
176 | otherwise = addUsage n (i + 1) sc
177 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
179getErasureUsage :: Idris [(Name, Int)]
180getErasureUsage = do ist <- getIState;
181 return (idris_erasureUsed ist)
183getExports :: Idris [Name]
184getExports = do ist <- getIState
185 return (idris_exports ist)
187totcheck :: (FC, Name) -> Idris ()
188totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
190defer_totcheck :: (FC, Name) -> Idris ()
193 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
195clear_totcheck :: Idris ()
196clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
198setFlags :: Name -> [FnOpt] -> Idris ()
199setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
201setFnInfo :: Name -> FnInfo -> Idris ()
202setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
204setAccessibility :: Name -> Accessibility -> Idris ()
207 let ctxt = setAccess n a (tt_ctxt i)
208 putIState $ i { tt_ctxt = ctxt }
210-- | get the accessibility of a name outside this module
211getFromHideList :: Name -> Idris (Maybe Accessibility)
212getFromHideList n = do i <- getIState
213 return $ lookupCtxtExact n (hide_list i)
215setTotality :: Name -> Totality -> Idris ()
218 let ctxt = setTotal n a (tt_ctxt i)
219 putIState $ i { tt_ctxt = ctxt }
221getTotality :: Name -> Idris Totality
224 case lookupTotal n (tt_ctxt i) of
226 _ -> return (Total [])
228-- Get coercions which might return the required type
229getCoercionsTo :: IState -> Type -> [Name]
231 let cs = idris_coercions i
232 (fn,_) = unApply (getRetTy ty) in
234 where findCoercions t [] = []
235 findCoercions t (n : ns) =
236 let ps = case lookupTy n (tt_ctxt i) of
237 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
238 (t', _) -> [n | t == t']
240 ps ++ findCoercions t ns
242addToCG :: Name -> CGInfo -> Idris ()
245 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
247addCalls :: Name -> [Name] -> Idris ()
250 case lookupCtxtExact n (idris_callgraph i) of
251 Nothing -> addToCG n (CGInfo calls [] [])
252 Just (CGInfo cs scg used) ->
253 addToCG n (CGInfo (nub (calls ++ cs)) scg used)
255addTyInferred :: Name -> Idris ()
258 putIState $ i { idris_tyinfodata =
259 addDef n TIPartial (idris_tyinfodata i) }
261addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
262addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
263 mapM_ addConstraint ts
265 where addConstraint (x, y) = findMVApps x y
268 = do let (fx, argsx) = unApply x
269 let (fy, argsy) = unApply y
274 else mapM_ addConstraint (zip argsx argsy)
276 tryAddMV (P _ mv _) y =
278 case lookup mv (idris_metavars ist) of
279 Just _ -> addConstraintRule mv y
281 tryAddMV _ _ = return ()
283 addConstraintRule :: Name -> Term -> Idris ()
284 addConstraintRule n t
286 logLvl 1 $ "TI constraint: " ++ show (n, t)
287 case lookupCtxt n (idris_tyinfodata ist) of
289 do mapM_ (checkConsistent t) ts
290 let ti' = addDef n (TISolution (t : ts))
291 (idris_tyinfodata ist)
292 put $ ist { idris_tyinfodata = ti' }
294 do let ti' = addDef n (TISolution [t])
295 (idris_tyinfodata ist)
296 put $ ist { idris_tyinfodata = ti' }
298 -- Check a solution is consistent with previous solutions
299 -- Meaning: If heads are both data types, they had better be the
301 checkConsistent :: Term -> Term -> Idris ()
302 checkConsistent x y =
303 do let (fx, _) = unApply x
304 let (fy, _) = unApply y
306 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
307 (P (TCon _ _) n _, Constant _) -> errWhen True
308 (Constant _, P (TCon _ _) n' _) -> errWhen True
309 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
314 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
315 errWhen False = return ()
317isTyInferred :: Name -> Idris Bool
320 case lookupCtxt n (idris_tyinfodata i) of
321 [TIPartial] -> return True
324-- | Adds error handlers for a particular function and argument. If names are
325-- ambiguous, all matching handlers are updated.
326addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
327addFunctionErrorHandlers f arg hs =
329 let oldHandlers = idris_function_errorhandlers i
330 let newHandlers = flip (addDef f) oldHandlers $
331 case lookupCtxtExact f oldHandlers of
332 Nothing -> M.singleton arg (S.fromList hs)
333 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
334 -- will always be one of those two, thus no extra case
335 putIState $ i { idris_function_errorhandlers = newHandlers }
337getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
338getFunctionErrorHandlers f arg = do i <- getIState
339 return . maybe [] S.toList $
340 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
343-- Trace all the names in a call graph starting at the given name
344getAllNames :: Name -> Idris [Name]
345getAllNames n = allNames [] n
347allNames :: [Name] -> Name -> Idris [Name]
348allNames ns n | n `elem` ns = return []
349allNames ns n = do i <- getIState
350 case lookupCtxtExact n (idris_callgraph i) of
351 Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')
352 return (nub (n : concat more))
355addCoercion :: Name -> Idris ()
356addCoercion n = do i <- getIState
357 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
359addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
362 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
364addNameHint :: Name -> Name -> Idris ()
367 ty' <- case lookupCtxtName ty (idris_implicits i) of
368 [(tyn, _)] -> return tyn
369 [] -> throwError (NoSuchVariable ty)
370 tyns -> throwError (CantResolveAlts (map fst tyns))
371 let ns' = case lookupCtxt ty' (idris_namehints i) of
374 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
376getNameHints :: IState -> Name -> [Name]
377getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
379 case lookupCtxt n (idris_namehints i) of
383addDeprecated :: Name -> String -> Idris ()
384addDeprecated n reason = do i <- getIState
385 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
387getDeprecated :: Name -> Idris (Maybe String)
388getDeprecated n = do i <- getIState
389 return $ lookupCtxtExact n (idris_deprecated i)
391push_estack :: Name -> Bool -> Idris ()
394 putIState (i { elab_stack = (n, inst) : elab_stack i })
396pop_estack :: Idris ()
397pop_estack = do i <- getIState
398 putIState (i { elab_stack = ptail (elab_stack i) })
402-- | Add a class instance function.
404-- Precondition: the instance should have the correct type.
406-- Dodgy hack 1: Put integer instances first in the list so they are
407-- resolved by default.
409-- Dodgy hack 2: put constraint chasers (@@) last
410addInstance :: Bool -- ^ whether the name is an Integer instance
411 -> Bool -- ^ whether to include the instance in instance search
412 -> Name -- ^ the name of the class
413 -> Name -- ^ the name of the instance
415addInstance int res n i
416 = do ist <- getIState
417 case lookupCtxt n (idris_classes ist) of
418 [CI a b c d e ins fds] ->
419 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
420 putIState $ ist { idris_classes = cs }
421 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)
422 putIState $ ist { idris_classes = cs }
423 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
424 addI i ins | int = (i, res) : ins
425 | chaser n = ins ++ [(i, res)]
426 | otherwise = insI i ins
427 insI i [] = [(i, res)]
428 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
429 | otherwise = n : insI i ns
432 | ('@':'@':_) <- str nm = True
433 chaser (NS n _) = chaser n
436addClass :: Name -> ClassInfo -> Idris ()
438 = do ist <- getIState
439 let i' = case lookupCtxt n (idris_classes ist) of
440 [c] -> c { class_instances = class_instances i }
442 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
444addRecord :: Name -> RecordInfo -> Idris ()
445addRecord n ri = do ist <- getIState
446 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
448addAutoHint :: Name -> Name -> Idris ()
451 case lookupCtxtExact n (idris_autohints ist) of
453 do let hs = addDef n [hint] (idris_autohints ist)
454 putIState $ ist { idris_autohints = hs }
456 do let hs = addDef n (hint : nhints) (idris_autohints ist)
457 putIState $ ist { idris_autohints = hs }
459getAutoHints :: Name -> Idris [Name]
460getAutoHints n = do ist <- getIState
461 case lookupCtxtExact n (idris_autohints ist) of
465addIBC :: IBCWrite -> Idris ()
468 when (notDef (ibc_write i)) $
469 putIState $ i { ibc_write = ibc : ibc_write i }
470 where notDef [] = True
471 notDef (IBCDef n': is) | n == n' = False
472 notDef (_ : is) = notDef is
473addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
476clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
477 idris_inmodule = S.empty }
479resetNameIdx :: Idris ()
480resetNameIdx = do i <- getIState
481 put (i { idris_nameIdx = (0, emptyContext) })
483-- Used to preserve sharing of names
484addNameIdx :: Name -> Idris (Int, Name)
485addNameIdx n = do i <- getIState
486 let (i', x) = addNameIdx' i n
490addNameIdx' :: IState -> Name -> (IState, (Int, Name))
492 = let idxs = snd (idris_nameIdx i) in
493 case lookupCtxt n idxs of
495 _ -> let i' = fst (idris_nameIdx i) + 1 in
496 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
498getSymbol :: Name -> Idris Name
499getSymbol n = do i <- getIState
500 case M.lookup n (idris_symbols i) of
502 Nothing -> do let sym' = M.insert n n (idris_symbols i)
503 put (i { idris_symbols = sym' })
506getHdrs :: Codegen -> Idris [String]
507getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
509getImported :: Idris [(FilePath, Bool)]
510getImported = do i <- getIState; return (idris_imported i)
512setErrSpan :: FC -> Idris ()
513setErrSpan x = do i <- getIState;
515 Nothing -> putIState $ i { errSpan = Just x }
519clearErr = do i <- getIState
520 putIState $ i { errSpan = Nothing }
522getSO :: Idris (Maybe String)
523getSO = do i <- getIState
524 return (compiled_so i)
526setSO :: Maybe String -> Idris ()
527setSO s = do i <- getIState
528 putIState $ (i { compiled_so = s })
530getIState :: Idris IState
533putIState :: IState -> Idris ()
536updateIState :: (IState -> IState) -> Idris ()
537updateIState f = do i <- getIState
540withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
541withContext ctx name dflt action = do
543 case lookupCtxt name (ctx ist) of
547withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
548withContext_ ctx name action = withContext ctx name () action
550-- | A version of liftIO that puts errors into the exception type of the Idris monad
551runIO :: IO a -> Idris a
552runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
553-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
555-- Issue #1738 on the issue tracker.
556-- https://github.com/idris-lang/Idris-dev/issues/1738
559getName = do i <- getIState;
560 let idx = idris_name i;
561 putIState $ (i { idris_name = idx + 1 })
564-- InternalApp keeps track of the real function application for making case splits from, not the application the
565-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
566addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
569 -- We canonicalise the path to make "./Test/Module.idr" equal
570 -- to "Test/Module.idr"
571 exists <- runIO $ doesFileExist fp
573 do fp' <- runIO $ canonicalizePath fp
574 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
576getInternalApp :: FilePath -> Int -> Idris PTerm
577getInternalApp fp l = do i <- getIState
578 -- We canonicalise the path to make
579 -- "./Test/Module.idr" equal to
581 exists <- runIO $ doesFileExist fp
583 then do fp' <- runIO $ canonicalizePath fp
584 case lookup (fp', l) (idris_lineapps i) of
586 Nothing -> return Placeholder
587 -- TODO: What if it's not there?
588 else return Placeholder
590-- Pattern definitions are only used for coverage checking, so erase them
592clearOrigPats :: Idris ()
593clearOrigPats = do i <- get
594 let ps = idris_patdefs i
595 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
596 put (i { idris_patdefs = ps' })
598-- Erase types from Ps in the context (basically ending up with what's in
599-- the .ibc, which is all we need after all the analysis is done)
600clearPTypes :: Idris ()
601clearPTypes = do i <- get
603 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
604 where pErase (CaseOp c t tys orig tot cds)
605 = CaseOp c t tys orig [] (pErase' cds)
607 pErase' (CaseDefs _ (cs, c) _ rs)
608 = let c' = (cs, fmap pEraseType c) in
611checkUndefined :: FC -> Name -> Idris ()
615 (_:_) -> throwError . Msg $ show fc ++ ":" ++
616 show n ++ " already defined"
619isUndefined :: FC -> Name -> Idris Bool
622 case lookupTyExact n i of
623 Just _ -> return False
626setContext :: Context -> Idris ()
627setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
629updateContext :: (Context -> Context) -> Idris ()
630updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
632addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
633addConstraints fc (v, cs)
636 let ctxt' = ctxt { next_tvar = v }
637 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
638 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
641 insertAll ((c, fc) : cs) ics
642 = insertAll cs $ S.insert (ConstraintFC c fc) ics
644addDeferred = addDeferred' Ref
645addDeferredTyCon = addDeferred' (TCon 0 0)
647-- | Save information about a name that is not yet defined
648addDeferred' :: NameType
649 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
650 -- ^ The Name is the name being made into a metavar,
651 -- the Int is the number of vars that are part of a
652 -- putative proof context, the Maybe Name is the
653 -- top-level function containing the new metavariable,
654 -- the Type is its type, and the Bool is whether :p is
658 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
659 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
661 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
662 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
665 -- 'tidyNames' is to generate user accessible names in case they are
666 -- needed in tactic scripts
667 tidyNames used (Bind (MN i x) b sc)
668 = let n' = uniqueNameSet (UN x) used in
669 Bind n' b $ tidyNames (S.insert n' used) sc
670 tidyNames used (Bind n b sc)
671 = let n' = uniqueNameSet n used in
672 Bind n' b $ tidyNames (S.insert n' used) sc
675solveDeferred :: FC -> Name -> Idris ()
678 case lookup n (idris_metavars i) of
679 Just (_, _, _, _, False) ->
680 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
681 _ -> putIState $ i { idris_metavars =
682 filter (\(n', _) -> n/=n')
685 filter (notMV n) (ibc_write i)
687 where notMV n (IBCMetavar n') = not (n == n')
690getUndefined :: Idris [Name]
691getUndefined = do i <- getIState
692 return (map fst (idris_metavars i) \\ primDefs)
694isMetavarName :: Name -> IState -> Bool
696 = case lookupNames n (tt_ctxt ist) of
697 (t:_) -> isJust $ lookup t (idris_metavars ist)
700getWidth :: Idris ConsoleWidth
701getWidth = fmap idris_consolewidth getIState
703setWidth :: ConsoleWidth -> Idris ()
704setWidth w = do ist <- getIState
705 put ist { idris_consolewidth = w }
707setDepth :: Maybe Int -> Idris ()
708setDepth d = do ist <- getIState
709 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
711typeDescription :: String
712typeDescription = "The type of types"
715type1Doc :: Doc OutputAnnotation
716type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
719isetPrompt :: String -> Idris ()
720isetPrompt p = do i <- getIState
721 case idris_outputmode i of
722 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
724-- | Tell clients how much was parsed and loaded
725isetLoadedRegion :: Idris ()
726isetLoadedRegion = do i <- getIState
727 let span = idris_parsedSpan i
730 case idris_outputmode i of
732 runIO . hPutStrLn h $
733 convSExp "set-loaded-region" fc n
736setLogLevel :: Int -> Idris ()
737setLogLevel l = do i <- getIState
738 let opts = idris_options i
739 let opt' = opts { opt_logLevel = l }
740 putIState $ i { idris_options = opt' }
742setLogCats :: [LogCat] -> Idris ()
745 let opts = idris_options i
746 let opt' = opts { opt_logcats = cs }
747 putIState $ i { idris_options = opt' }
749setCmdLine :: [Opt] -> Idris ()
750setCmdLine opts = do i <- getIState
751 let iopts = idris_options i
752 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
754getCmdLine :: Idris [Opt]
755getCmdLine = do i <- getIState
756 return (opt_cmdline (idris_options i))
758getDumpHighlighting :: Idris Bool
759getDumpHighlighting = do ist <- getIState
760 return (findC (opt_cmdline (idris_options ist)))
761 where findC = elem DumpHighlights
763getDumpDefun :: Idris (Maybe FilePath)
764getDumpDefun = do i <- getIState
765 return $ findC (opt_cmdline (idris_options i))
766 where findC [] = Nothing
767 findC (DumpDefun x : _) = Just x
768 findC (_ : xs) = findC xs
770getDumpCases :: Idris (Maybe FilePath)
771getDumpCases = do i <- getIState
772 return $ findC (opt_cmdline (idris_options i))
773 where findC [] = Nothing
774 findC (DumpCases x : _) = Just x
775 findC (_ : xs) = findC xs
778logLevel = do i <- getIState
779 return (opt_logLevel (idris_options i))
781setAutoImpls :: Bool -> Idris ()
782setAutoImpls b = do i <- getIState
783 let opts = idris_options i
784 let opt' = opts { opt_autoimpls = b }
785 putIState $ i { idris_options = opt' }
787getAutoImpls :: Idris Bool
788getAutoImpls = do i <- getIState
789 return (opt_autoimpls (idris_options i))
791setErrContext :: Bool -> Idris ()
792setErrContext t = do i <- getIState
793 let opts = idris_options i
794 let opts' = opts { opt_errContext = t }
795 putIState $ i { idris_options = opts' }
797errContext :: Idris Bool
798errContext = do i <- getIState
799 return (opt_errContext (idris_options i))
801getOptimise :: Idris [Optimisation]
802getOptimise = do i <- getIState
803 return (opt_optimise (idris_options i))
805setOptimise :: [Optimisation] -> Idris ()
806setOptimise newopts = do i <- getIState
807 let opts = idris_options i
808 let opts' = opts { opt_optimise = newopts }
809 putIState $ i { idris_options = opts' }
811addOptimise :: Optimisation -> Idris ()
812addOptimise opt = do opts <- getOptimise
813 setOptimise (nub (opt : opts))
815removeOptimise :: Optimisation -> Idris ()
816removeOptimise opt = do opts <- getOptimise
817 setOptimise ((nub opts) \\ [opt])
819-- Set appropriate optimisation set for the given level. We only have
820-- one optimisation that is configurable at the moment, however!
821setOptLevel :: Int -> Idris ()
822setOptLevel n | n <= 0 = setOptimise []
823setOptLevel 1 = setOptimise []
824setOptLevel 2 = setOptimise [PETransform]
825setOptLevel n | n >= 3 = setOptimise [PETransform]
828useREPL = do i <- getIState
829 return (opt_repl (idris_options i))
831setREPL :: Bool -> Idris ()
832setREPL t = do i <- getIState
833 let opts = idris_options i
834 let opt' = opts { opt_repl = t }
835 putIState $ i { idris_options = opt' }
837showOrigErr :: Idris Bool
838showOrigErr = do i <- getIState
839 return (opt_origerr (idris_options i))
841setShowOrigErr :: Bool -> Idris ()
842setShowOrigErr b = do i <- getIState
843 let opts = idris_options i
844 let opt' = opts { opt_origerr = b }
845 putIState $ i { idris_options = opt' }
847setAutoSolve :: Bool -> Idris ()
848setAutoSolve b = do i <- getIState
849 let opts = idris_options i
850 let opt' = opts { opt_autoSolve = b }
851 putIState $ i { idris_options = opt' }
853setNoBanner :: Bool -> Idris ()
854setNoBanner n = do i <- getIState
855 let opts = idris_options i
856 let opt' = opts { opt_nobanner = n }
857 putIState $ i { idris_options = opt' }
859getNoBanner :: Idris Bool
860getNoBanner = do i <- getIState
861 let opts = idris_options i
862 return (opt_nobanner opts)
864setEvalTypes :: Bool -> Idris ()
865setEvalTypes n = do i <- getIState
866 let opts = idris_options i
867 let opt' = opts { opt_evaltypes = n }
868 putIState $ i { idris_options = opt' }
870getDesugarNats :: Idris Bool
871getDesugarNats = do i <- getIState
872 let opts = idris_options i
873 return (opt_desugarnats opts)
876setDesugarNats :: Bool -> Idris ()
877setDesugarNats n = do i <- getIState
878 let opts = idris_options i
879 let opt' = opts { opt_desugarnats = n }
880 putIState $ i { idris_options = opt' }
882setQuiet :: Bool -> Idris ()
883setQuiet q = do i <- getIState
884 let opts = idris_options i
885 let opt' = opts { opt_quiet = q }
886 putIState $ i { idris_options = opt' }
888getQuiet :: Idris Bool
889getQuiet = do i <- getIState
890 let opts = idris_options i
891 return (opt_quiet opts)
893setCodegen :: Codegen -> Idris ()
894setCodegen t = do i <- getIState
895 let opts = idris_options i
896 let opt' = opts { opt_codegen = t }
897 putIState $ i { idris_options = opt' }
899codegen :: Idris Codegen
900codegen = do i <- getIState
901 return (opt_codegen (idris_options i))
903setOutputTy :: OutputType -> Idris ()
904setOutputTy t = do i <- getIState
905 let opts = idris_options i
906 let opt' = opts { opt_outputTy = t }
907 putIState $ i { idris_options = opt' }
909outputTy :: Idris OutputType
910outputTy = do i <- getIState
911 return $ opt_outputTy $ idris_options i
913setIdeMode :: Bool -> Handle -> Idris ()
914setIdeMode True h = do i <- getIState
915 putIState $ i { idris_outputmode = IdeMode 0 h
916 , idris_colourRepl = False
918setIdeMode False _ = return ()
920setTargetTriple :: String -> Idris ()
921setTargetTriple t = do i <- getIState
922 let opts = idris_options i
923 opt' = opts { opt_triple = t }
924 putIState $ i { idris_options = opt' }
926targetTriple :: Idris String
927targetTriple = do i <- getIState
928 return (opt_triple (idris_options i))
930setTargetCPU :: String -> Idris ()
931setTargetCPU t = do i <- getIState
932 let opts = idris_options i
933 opt' = opts { opt_cpu = t }
934 putIState $ i { idris_options = opt' }
936targetCPU :: Idris String
937targetCPU = do i <- getIState
938 return (opt_cpu (idris_options i))
941verbose = do i <- getIState
942 -- Quietness overrides verbosity
943 return (not (opt_quiet (idris_options i)) &&
944 opt_verbose (idris_options i))
946setVerbose :: Bool -> Idris ()
947setVerbose t = do i <- getIState
948 let opts = idris_options i
949 let opt' = opts { opt_verbose = t }
950 putIState $ i { idris_options = opt' }
952typeInType :: Idris Bool
953typeInType = do i <- getIState
954 return (opt_typeintype (idris_options i))
956setTypeInType :: Bool -> Idris ()
957setTypeInType t = do i <- getIState
958 let opts = idris_options i
959 let opt' = opts { opt_typeintype = t }
960 putIState $ i { idris_options = opt' }
962coverage :: Idris Bool
963coverage = do i <- getIState
964 return (opt_coverage (idris_options i))
966setCoverage :: Bool -> Idris ()
967setCoverage t = do i <- getIState
968 let opts = idris_options i
969 let opt' = opts { opt_coverage = t }
970 putIState $ i { idris_options = opt' }
972setIBCSubDir :: FilePath -> Idris ()
973setIBCSubDir fp = do i <- getIState
974 let opts = idris_options i
975 let opt' = opts { opt_ibcsubdir = fp }
976 putIState $ i { idris_options = opt' }
978valIBCSubDir :: IState -> Idris FilePath
979valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
981addImportDir :: FilePath -> Idris ()
982addImportDir fp = do i <- getIState
983 let opts = idris_options i
984 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
985 putIState $ i { idris_options = opt' }
987setImportDirs :: [FilePath] -> Idris ()
988setImportDirs fps = do i <- getIState
989 let opts = idris_options i
990 let opt' = opts { opt_importdirs = fps }
991 putIState $ i { idris_options = opt' }
993allImportDirs :: Idris [FilePath]
994allImportDirs = do i <- getIState
995 let optdirs = opt_importdirs (idris_options i)
996 return ("." : reverse optdirs)
998colourise :: Idris Bool
999colourise = do i <- getIState
1000 return $ idris_colourRepl i
1002setColourise :: Bool -> Idris ()
1003setColourise b = do i <- getIState
1004 putIState $ i { idris_colourRepl = b }
1006impShow :: Idris Bool
1007impShow = do i <- getIState
1008 return (opt_showimp (idris_options i))
1010setImpShow :: Bool -> Idris ()
1011setImpShow t = do i <- getIState
1012 let opts = idris_options i
1013 let opt' = opts { opt_showimp = t }
1014 putIState $ i { idris_options = opt' }
1016setColour :: ColourType -> IdrisColour -> Idris ()
1017setColour ct c = do i <- getIState
1018 let newTheme = setColour' ct c (idris_colourTheme i)
1019 putIState $ i { idris_colourTheme = newTheme }
1020 where setColour' KeywordColour c t = t { keywordColour = c }
1021 setColour' BoundVarColour c t = t { boundVarColour = c }
1022 setColour' ImplicitColour c t = t { implicitColour = c }
1023 setColour' FunctionColour c t = t { functionColour = c }
1024 setColour' TypeColour c t = t { typeColour = c }
1025 setColour' DataColour c t = t { dataColour = c }
1026 setColour' PromptColour c t = t { promptColour = c }
1027 setColour' PostulateColour c t = t { postulateColour = c }
1030logLvl :: Int -> String -> Idris ()
1031logLvl = logLvlCats []
1033logCoverage :: Int -> String -> Idris ()
1034logCoverage = logLvlCats [ICoverage]
1036logErasure :: Int -> String -> Idris ()
1037logErasure = logLvlCats [IErasure]
1039-- | Log an action of the parser
1040logParser :: Int -> String -> Idris ()
1041logParser = logLvlCats parserCats
1043-- | Log an action of the elaborator.
1044logElab :: Int -> String -> Idris ()
1045logElab = logLvlCats elabCats
1047-- | Log an action of the compiler.
1048logCodeGen :: Int -> String -> Idris ()
1049logCodeGen = logLvlCats codegenCats
1051logIBC :: Int -> String -> Idris ()
1052logIBC = logLvlCats [IIBC]
1054-- | Log aspect of Idris execution
1056-- An empty set of logging levels is used to denote all categories.
1058-- @TODO update IDE protocol
1059logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1060 -> Int -- ^ The Logging level the message should appear.
1061 -> String -- ^ The message to show the developer.
1063logLvlCats cs l str = do
1065 let lvl = opt_logLevel (idris_options i)
1066 let cats = opt_logcats (idris_options i)
1068 when (inCat cs cats || null cats) $
1069 case idris_outputmode i of
1071 runIO $ hPutStrLn h str
1073 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1074 runIO . hPutStrLn h $ convSExp "log" good n
1076 inCat :: [LogCat] -> [LogCat] -> Bool
1077 inCat cs cats = any (`elem` cats) cs
1079cmdOptType :: Opt -> Idris Bool
1080cmdOptType x = do i <- getIState
1081 return $ x `elem` opt_cmdline (idris_options i)
1083noErrors :: Idris Bool
1084noErrors = do i <- getIState
1086 Nothing -> return True
1089setTypeCase :: Bool -> Idris ()
1090setTypeCase t = do i <- getIState
1091 let opts = idris_options i
1092 let opt' = opts { opt_typecase = t }
1093 putIState $ i { idris_options = opt' }
1096-- Dealing with parameters
1098expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1099 [Name] -> -- all names
1100 [Name] -> -- names with no declaration
1102expandParams dec ps ns infs tm = en 0 tm
1104 -- if we shadow a name (say in a lambda binding) that is used in a call to
1105 -- a lifted function, we need access to both names - once in the scope of the
1106 -- binding and once to call the lifted functions. So we'll explicitly shadow
1107 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1108 -- but we didn't...)
1110 mkShadow (UN n) = MN 0 n
1111 mkShadow (MN i n) = MN (i+1) n
1112 mkShadow (NS x s) = NS (mkShadow x) s
1114 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1115 -- that are merely mentioned.
1117 en 0 (PLam fc n nfc t s)
1118 | n `elem` (map fst ps ++ ns)
1119 = let n' = mkShadow n in
1120 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1121 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1122 en 0 (PPi p n nfc t s)
1123 | n `elem` (map fst ps ++ ns)
1124 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1125 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1126 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1127 en 0 (PLet fc n nfc ty v s)
1128 | n `elem` (map fst ps ++ ns)
1129 = let n' = mkShadow n in
1130 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1131 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1132 -- FIXME: Should only do this in a type signature!
1133 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1134 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1135 = let n' = mkShadow n in
1136 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1137 en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1138 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1139 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1140 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1141 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1142 en 0 (PHidden t) = PHidden (en 0 t)
1143 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1144 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1145 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1146 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1147 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1148 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1150 en 0 (PQuote (Var n))
1151 | n `nselem` ns = PQuote (Var (dec n))
1152 en 0 (PApp fc (PInferRef fc' hl n) as)
1153 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1154 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1155 en 0 (PApp fc (PRef fc' hl n) as)
1156 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1157 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1158 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1159 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1160 en 0 (PAppBind fc (PRef fc' hl n) as)
1161 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1162 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1163 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1164 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1166 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1167 (map ((pexp . (PRef fc hl)) . fst) ps)
1168 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1169 (map ((pexp . (PRef fc hl)) . fst) ps)
1170 en 0 (PInferRef fc hl n)
1171 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1172 (map ((pexp . (PRef fc hl)) . fst) ps)
1173 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1174 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1175 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1176 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1177 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1178 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1180 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1181 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1183 en ql t = descend (en ql) t
1186 nselem x (y : xs) | nseq x y = True
1187 | otherwise = nselem x xs
1189 nseq x y = nsroot x == nsroot y
1191 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1192 enTacImp ql other = other
1194expandParamsD :: Bool -> -- True = RHS only
1196 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1197expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1198 = if n `elem` ns && (not rhsonly)
1199 then -- trace (show (n, expandParams dec ps ns ty)) $
1200 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1201 else --trace (show (n, expandParams dec ps ns ty)) $
1202 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1203expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1204 = if n `elem` ns && (not rhsonly)
1205 then -- trace (show (n, expandParams dec ps ns ty)) $
1206 PPostulate e doc syn fc nfc o (dec n)
1207 (piBind ps (expandParams dec ps ns [] ty))
1208 else --trace (show (n, expandParams dec ps ns ty)) $
1209 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1210expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1211 = let n' = if n `elem` ns then dec n else n in
1212 PClauses fc opts n' (map expandParamsC cs)
1214 expandParamsC (PClause fc n lhs ws rhs ds)
1215 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1216 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1217 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1218 n' = if n `elem` ns then dec n else n
1219 -- names bound on the lhs should not be expanded on the rhs
1220 ns' = removeBound lhs ns in
1222 (map (expandParams dec ps'' ns' []) ws)
1223 (expandParams dec ps'' ns' [] rhs)
1224 (map (expandParamsD True ist dec ps'' ns') ds)
1225 expandParamsC (PWith fc n lhs ws wval pn ds)
1226 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1227 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1228 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1229 n' = if n `elem` ns then dec n else n
1230 ns' = removeBound lhs ns in
1232 (map (expandParams dec ps'' ns' []) ws)
1233 (expandParams dec ps'' ns' [] wval)
1235 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1236 updateps yn nm [] = []
1237 updateps yn nm (((a, t), i):as)
1238 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1239 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1241 removeBound lhs ns = ns \\ nub (bnames lhs)
1243 bnames (PRef _ _ n) = [n]
1244 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1245 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1246 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1249-- | Expands parameters defined in parameter and where blocks inside of declarations
1250expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1251 = PData doc argDocs syn fc co (expandPData pd)
1253 -- just do the type decl, leave constructors alone (parameters will be
1254 -- added implicitly)
1255 expandPData (PDatadecl n nfc ty cons)
1257 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1259 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1260 econ (doc, argDocs, n, nfc, t, fc, fs)
1261 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1262expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1264expandParamsD rhs ist dec ps ns (PParams f params pds)
1265 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1266 (map (expandParamsD True ist dec ps ns) pds)
1267-- (map (expandParamsD ist dec ps ns) pds)
1268expandParamsD rhs ist dec ps ns (PMutual f pds)
1269 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1270expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1272 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1274 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1277 (map (expandParamsD rhs ist dec ps ns) decls)
1280expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params ty cn decls)
1281 = PInstance doc argDocs info f
1282 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1285 (map (expandParams dec ps ns []) params)
1286 (expandParams dec ps ns [] ty)
1288 (map (expandParamsD rhs ist dec ps ns) decls)
1289expandParamsD rhs ist dec ps ns d = d
1291mapsnd f (x, t) = (x, f t)
1293-- Calculate a priority for a type, for deciding elaboration order
1294-- * if it's just a type variable or concrete type, do it early (0)
1295-- * if there's only type variables and injective constructors, do it next (1)
1296-- * if there's a function type, next (2)
1297-- * finally, everything else (3)
1299getPriority :: IState -> PTerm -> Int
1300getPriority i tm = 1 -- pri tm
1303 case lookupP n (tt_ctxt i) of
1304 ((P (DCon _ _ _) _ _):_) -> 1
1305 ((P (TCon _ _) _ _):_) -> 1
1306 ((P Ref _ _):_) -> 1
1307 [] -> 0 -- must be locally bound, if it's not an error...
1308 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1310 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1311 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1312 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1313 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1314 pri (PTyped l r) = pri l
1315 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1316 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1317 pri (PAlternative _ a as) = maximum (map pri as)
1318 pri (PConstant _ _) = 0
1323addStatics :: Name -> Term -> PTerm -> Idris ()
1324addStatics n tm ptm =
1325 do let (statics, dynamics) = initStatics tm ptm
1328 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1329 Just p -> getNamesFrom 0 (fn_params p) tm ++
1330 concatMap (getParamNames ist . snd) statics
1331 _ -> concatMap (getParamNames ist . snd) statics
1333 let stnames = nub $ concatMap (freeArgNames . snd) statics
1334 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1336 -- also get the arguments which are 'uniquely inferrable' from
1337 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1338 -- or parameters to the type of a static
1339 let statics' = nub $ map fst statics ++
1340 filter (\x -> not (elem x dnames)) stnames
1341 let stpos = staticList statics' tm
1343 unless (null statics) $
1344 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1345 ++ showTmImpls ptm ++ "\n"
1346 ++ show statics ++ "\n" ++ show dynamics
1347 ++ "\n" ++ show paramnames
1348 ++ "\n" ++ show stpos
1349 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1350 addIBC (IBCStatic n)
1352 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1353 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1354 (static, (n, ty) : dynamic)
1355 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1356 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1357 if pstatic p == Static then ((n, ty) : static, dynamic)
1358 else if (not (searchArg p))
1359 then (static, (n, ty) : dynamic)
1360 else (static, dynamic)
1361 initStatics t pt = ([], [])
1363 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1364 = case lookupCtxtExact n (idris_datatypes ist) of
1365 Just ti -> getNamePos 0 (param_pos ti) args
1367 where getNamePos i ps [] = []
1368 getNamePos i ps (P _ n _ : as)
1369 | i `elem` ps = n : getNamePos (i + 1) ps as
1370 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1371 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1372 = n : getParamNames ist sc
1373 getParamNames ist _ = []
1375 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1376 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1377 | otherwise = getNamesFrom (i + 1) ps sc
1378 getNamesFrom i ps sc = []
1380 freeArgNames (Bind n (Pi _ ty _) sc)
1381 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1382 freeArgNames tm = let (_, args) = unApply tm in
1383 concatMap freeNames args
1385 -- if a name appears in a type class or tactic implicit index, it doesn't
1386 -- affect its 'uniquely inferrable' from a static status since these are
1387 -- resolved by searching.
1388 searchArg (Constraint _ _) = True
1389 searchArg (TacImp _ _ _) = True
1392 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1395-- Dealing with implicit arguments
1397-- Add some bound implicits to the using block if they aren't there already
1399addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1400addToUsing us [] = us
1401addToUsing us ((n, t) : ns)
1402 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1403 | otherwise = addToUsing us ns
1404 where impName (UImplicit n _) = Just n
1407-- Add constraint bindings from using block
1409addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1410addUsingConstraints syn fc t
1412 let ns = namesIn [] ist t
1413 let cs = getConstraints t -- check declared constraints
1414 let addconsts = uconsts \\ cs
1415 return (doAdd addconsts ns t)
1416 where uconsts = filter uconst (using syn)
1417 uconst (UConstraint _ _) = True
1421 -- if all of args in ns, then add it
1422 doAdd (UConstraint c args : cs) ns t
1423 | all (\n -> elem n ns) args
1424 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1425 (mkConst c args) (doAdd cs ns t)
1426 | otherwise = doAdd cs ns t
1428 mkConst c args = PApp fc (PRef fc [] c)
1429 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1431 getConstraints (PPi (Constraint _ _) _ _ c sc)
1432 = getcapp c ++ getConstraints sc
1433 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1434 getConstraints _ = []
1436 getcapp (PApp _ (PRef _ _ c) args)
1437 = do ns <- mapM getName args
1438 return (UConstraint c ns)
1441 getName (PExp _ _ _ (PRef _ _ n)) = return n
1444-- Add implicit bindings from using block, and bind any missing names
1445addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1446addUsingImpls syn n fc t
1447 = do ist <- getIState
1448 autoimpl <- getAutoImpls
1449 let ns_in = implicitNamesIn (map iname uimpls) ist t
1450 let ns = if autoimpl then ns_in
1451 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1453 let badnames = filter (\n -> not (implicitable n) &&
1454 n `notElem` (map iname uimpls)) ns
1455 unless (null badnames) $
1456 throwError (At fc (Elaborating "type of " n Nothing
1457 (NoSuchVariable (head badnames))))
1458 let cs = getArgnames t -- get already bound names
1459 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1460 -- if all names in the arguments of addconsts appear in ns,
1461 -- add the constraint implicitly
1462 return (bindFree ns (doAdd addimpls ns t))
1463 where uimpls = filter uimpl (using syn)
1464 uimpl (UImplicit _ _) = True
1467 iname (UImplicit n _) = n
1468 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1471 -- if all of args in ns, then add it
1472 doAdd (UImplicit n ty : cs) ns t
1474 = PPi (Imp [] Dynamic False Nothing False) n NoFC ty (doAdd cs ns t)
1475 | otherwise = doAdd cs ns t
1477 -- bind the free names which weren't in the using block
1480 | elem n (map iname uimpls) = bindFree ns tm
1482 = PPi (Imp [InaccessibleArg] Dynamic False Nothing False) n NoFC Placeholder (bindFree ns tm)
1484 getArgnames (PPi _ n _ c sc)
1485 = n : getArgnames sc
1488-- Given the original type and the elaborated type, return the implicitness
1489-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1491getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1492getUnboundImplicits i t tm = getImps t (collectImps tm)
1493 where collectImps (PPi p n _ t sc)
1494 = (n, (p, t)) : collectImps sc
1497 scopedimpl (Just i) = not (toplevel_imp i)
1498 scopedimpl _ = False
1500 getImps (Bind n (Pi i _ _) sc) imps
1501 | scopedimpl i = getImps sc imps
1502 getImps (Bind n (Pi _ t _) sc) imps
1503 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1505 argInfo n (Imp opt _ _ _ _) Placeholder
1506 = (True, PImp 0 True opt n Placeholder)
1507 argInfo n (Imp opt _ _ _ _) t'
1508 = (False, PImp (getPriority i t') True opt n t')
1509 argInfo n (Exp opt _ _) t'
1510 = (InaccessibleArg `elem` opt,
1511 PExp (getPriority i t') opt n t')
1512 argInfo n (Constraint opt _) t'
1513 = (InaccessibleArg `elem` opt,
1514 PConstraint 10 opt n t')
1515 argInfo n (TacImp opt _ scr) t'
1516 = (InaccessibleArg `elem` opt,
1517 PTacImplicit 10 opt n scr t')
1518 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1519 where impBind n t = (True, PImp 1 True [] n Placeholder)
1522-- Add implicit Pi bindings for any names in the term which appear in an
1523-- argument position.
1525-- This has become a right mess already. Better redo it some time...
1526-- TODO: This is obsoleted by the new way of elaborating types, (which
1527-- calls addUsingImpls) but there's still a couple of places which use
1528-- it. Clean them up!
1530-- Issue 1739 in the issue tracker
1531-- https://github.com/idris-lang/Idris-dev/issues/1739
1532implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1533implicit info syn n ptm = implicit' info syn [] n ptm
1535implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1536implicit' info syn ignore n ptm
1538 auto <- getAutoImpls
1539 let (tm', impdata) = implicitise auto syn ignore i ptm
1540 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1541-- let (tm'', spos) = findStatics i tm'
1542 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1544 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1546-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1549 -- Detect unknown names in default arguments and throw error if found.
1550 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1551 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1553 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1554 notFoundInDefault kns (PTacImplicit _ _ n script _)
1556 case notFound kns (namesIn [] i script) of
1557 Nothing -> return (n:kns)
1558 Just name -> throwError (NoSuchVariable name)
1559 notFoundInDefault kns p = return ((pname p):kns)
1561 notFound :: [Name] -> [Name] -> Maybe Name
1562 notFound kns [] = Nothing
1563 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1564 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1566-- Even if auto_implicits is off, we need to call this so we record which
1567-- arguments are implicit
1568implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1569implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1570 let (declimps, ns') = execState (imps True [] tm) ([], [])
1571 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1572 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1573 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1575 then (tm, reverse declimps)
1576 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1578 uvars = map ipair (filter uimplicit (using syn))
1579 pvars = syn_params syn
1581 inUsing n = n `elem` map fst uvars
1583 ipair (UImplicit x y) = (x, y)
1584 uimplicit (UImplicit _ _) = True
1587 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1588 | otherwise = x : dropAll xs ys
1591 -- Find names in argument position in a type, suitable for implicit
1593 -- Not the function position, but do everything else...
1594 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1595 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1597 imps top env ty@(PApp _ f as)
1598 = do (decls, ns) <- get
1599 let isn = nub (implNamesIn uvars ty)
1600 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1601 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1602 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1604 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1605 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1606 imps True (n:env) sc
1607 imps top env (PPi (Exp l _ _) n _ ty sc)
1608 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1609 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1611 (decls, ns) <- get -- ignore decls in HO types
1612 put (PExp (getPriority ist ty) l n Placeholder : decls,
1613 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1614 imps True (n:env) sc
1615 imps top env (PPi (Constraint l _) n _ ty sc)
1616 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1617 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1619 (decls, ns) <- get -- ignore decls in HO types
1620 put (PConstraint 10 l n Placeholder : decls,
1621 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1622 imps True (n:env) sc
1623 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1624 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1625 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1627 (decls, ns) <- get -- ignore decls in HO types
1628 put (PTacImplicit 10 l n scr Placeholder : decls,
1629 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1630 imps True (n:env) sc
1631 imps top env (PRewrite _ l r _)
1632 = do (decls, ns) <- get
1633 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1634 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1635 imps top env (PTyped l r)
1637 imps top env (PPair _ _ _ l r)
1638 = do (decls, ns) <- get
1639 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1640 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1641 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1642 = do (decls, ns) <- get
1643 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1644 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1645 imps top env (PDPair _ _ _ l t r)
1646 = do (decls, ns) <- get
1647 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1649 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1650 imps top env (PAlternative ms a as)
1651 = do (decls, ns) <- get
1652 let isn = concatMap (namesIn uvars ist) as
1653 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1654 imps top env (PLam fc n _ ty sc)
1655 = do imps False env ty
1656 imps False (n:env) sc
1657 imps top env (PHidden tm) = imps False env tm
1658 imps top env (PUnifyLog tm) = imps False env tm
1659 imps top env (PNoImplicits tm) = imps False env tm
1660 imps top env (PRunElab fc tm ns) = imps False env tm
1661 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1662 imps top env _ = return ()
1664 pibind using [] sc = sc
1665 pibind using (n:ns) sc
1666 = case lookup n using of
1667 Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)) False)
1668 n NoFC ty (pibind using ns sc)
1669 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False)
1670 n NoFC Placeholder (pibind using ns sc)
1672-- Add implicit arguments in function calls
1673addImplPat :: IState -> PTerm -> PTerm
1674addImplPat = addImpl' True [] [] []
1676addImplBound :: IState -> [Name] -> PTerm -> PTerm
1677addImplBound ist ns = addImpl' False ns [] [] ist
1679addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1680addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1682-- | Add the implicit arguments to applications in the term
1683-- [Name] gives the names to always expend, even when under a binder of
1684-- that name (this is to expand methods with implicit arguments in dependent
1686addImpl :: [Name] -> IState -> PTerm -> PTerm
1687addImpl = addImpl' False [] []
1689-- TODO: in patterns, don't add implicits to function names guarded by constructors
1690-- and *not* inside a PHidden
1692addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1693addImpl' inpat env infns imp_meths ist ptm
1694 = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1696 topname = case ptm of
1698 PApp _ (PRef _ _ n) _ -> n
1699 _ -> sUN "" -- doesn't matter then
1701 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1702 ai inpat qq env ds (PRef fc fcs f)
1703 | f `elem` infns = PInferRef fc fcs f
1704 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1705 ai inpat qq env ds (PHidden (PRef fc hl f))
1706 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1707 ai inpat qq env ds (PRewrite fc l r g)
1708 = let l' = ai inpat qq env ds l
1709 r' = ai inpat qq env ds r
1710 g' = fmap (ai inpat qq env ds) g in
1711 PRewrite fc l' r' g'
1712 ai inpat qq env ds (PTyped l r)
1713 = let l' = ai inpat qq env ds l
1714 r' = ai inpat qq env ds r in
1716 ai inpat qq env ds (PPair fc hls p l r)
1717 = let l' = ai inpat qq env ds l
1718 r' = ai inpat qq env ds r in
1719 PPair fc hls p l' r'
1720 ai inpat qq env ds (PDPair fc hls p l t r)
1721 = let l' = ai inpat qq env ds l
1722 t' = ai inpat qq env ds t
1723 r' = ai inpat qq env ds r in
1724 PDPair fc hls p l' t' r'
1725 ai inpat qq env ds (PAlternative ms a as)
1726 = let as' = map (ai inpat qq env ds) as in
1727 PAlternative ms a as'
1728 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1729 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1730 = let as' = map (fmap (ai inpat qq env ds)) as in
1731 PApp fc (PInferRef ffc hl f) as'
1732 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1733 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1734 | not (f `elem` map fst env)
1735 = let as' = map (fmap (ai inpat qq env ds)) as in
1736 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1737 | Just (Just ty) <- lookup f env =
1738 let as' = map (fmap (ai inpat qq env ds)) as
1739 arity = getPArity ty in
1740 mkPApp fc arity ftm as'
1741 ai inpat qq env ds (PApp fc f as)
1742 = let f' = ai inpat qq env ds f
1743 as' = map (fmap (ai inpat qq env ds)) as in
1745 ai inpat qq env ds (PCase fc c os)
1746 = let c' = ai inpat qq env ds c in
1747 -- leave os alone, because they get lifted into a new pattern match
1748 -- definition which is passed through addImpl agai inpatn with more scope
1752 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1753 (ai inpat qq env ds t)
1754 (ai inpat qq env ds f)
1756 -- If the name in a lambda is a constructor name, do this as a 'case'
1757 -- instead (it is harmless to do so, especially since the lambda will
1758 -- be lifted anyway!)
1759 ai inpat qq env ds (PLam fc n nfc ty sc)
1760 = case lookupDef n (tt_ctxt ist) of
1761 [] -> let ty' = ai inpat qq env ds ty
1762 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1763 PLam fc n nfc ty' sc'
1764 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1765 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1766 [(PRef fc [] n, sc)]))
1767 ai inpat qq env ds (PLet fc n nfc ty val sc)
1768 = case lookupDef n (tt_ctxt ist) of
1769 [] -> let ty' = ai inpat qq env ds ty
1770 val' = ai inpat qq env ds val
1771 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1772 PLet fc n nfc ty' val' sc'
1774 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1775 ai inpat qq env ds (PPi p n nfc ty sc)
1776 = let ty' = ai inpat qq env ds ty
1777 env' = if n `elem` imp_meths then env
1778 else ((n, Just ty) : env)
1779 sc' = ai inpat qq env' ds sc in
1781 ai inpat qq env ds (PGoal fc r n sc)
1782 = let r' = ai inpat qq env ds r
1783 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1785 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1786 -- Don't do PProof or PTactics since implicits get added when scope is
1787 -- properly known in ElabTerm.runTac
1788 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1789 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1790 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1791 (fmap (ai inpat True env ds) g)
1792 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1793 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1794 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1795 ai inpat qq env ds tm = tm
1797 handleErr (Left err) = PElabError err
1798 handleErr (Right x) = x
1800-- if in a pattern, and there are no arguments, and there's no possible
1801-- names with zero explicit arguments, don't add implicits.
1803aiFn :: Name -> Bool -> Bool -> Bool
1806 -> Name -- ^ function being applied
1808 -> [PArg] -- ^ initial arguments (if in a pattern)
1810aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1811 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1813 = case lookupDef f (tt_ctxt ist) of
1814 [] -> Right $ PPatvar ffc f
1815 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1816 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1817 if (not (vname f) || tcname f
1818 || any (conCaf (tt_ctxt ist)) ialts)
1819-- any constructor alts || any allImp ialts))
1820 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1821 else Right $ PPatvar ffc f
1822 where imp (PExp _ _ _ _) = False
1825 allImp xs = all imp xs
1827 unqualified (NS _ _) = False
1828 unqualified _ = True
1830 constructor (TyDecl (DCon _ _ _) _) = True
1831 constructor _ = False
1833 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1835 vname (UN n) = True -- non qualified
1838aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1839 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1840aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1841 -- This is where namespaces get resolved by adding PAlternative
1842 = do let ns = lookupCtxtName f (idris_implicits ist)
1843 let nh = filter (\(n, _) -> notHidden n) ns
1844 let ns' = case trimAlts ds nh of
1848 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1850 [] -> if f `elem` (map fst (idris_metavars ist))
1851 then Right $ PApp fc (PRef ffc [ffc] f) as
1852 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1854 PAlternative [] (ExactlyOne True) $
1855 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1856 (insertImpl ns as)) alts
1858 -- if the name is in imp_meths, we should actually refer to the bound
1859 -- name rather than the global one after expanding implicits
1860 isImpName f f' | f `elem` imp_meths = f
1863 trimAlts [] alts = alts
1865 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1870 notHidden n = case getAccessibility n of
1876 = case lookupDefAccExact n False (tt_ctxt ist) of
1880 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1881 -> [PArg] -- ^ given arguments
1884 = let (as', badimpls) = partition (impIn ps) as in
1885 map addUnknownImp badimpls ++
1886 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1888 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1889 -> [PArg] -- parameters
1890 -> [PArg] -- explicit arguments
1891 -> [PArg] -- implicits given
1893 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1894 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1895 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1896 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1897 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1898 let rtc = PResolveTC fc in
1899 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1900 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1901 case find n imps [] of
1903 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1905 PImp p True l n Placeholder :
1906 insImpAcc (M.insert n Placeholder pnas) ps given imps
1907 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1908 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1909 case find n imps [] of
1911 PTacImplicit p l n sc tm :
1912 insImpAcc (M.insert n tm pnas) ps given imps'
1915 then PTacImplicit p l n sc Placeholder :
1916 insImpAcc (M.insert n Placeholder pnas) ps given imps
1917 else PTacImplicit p l n sc sc :
1918 insImpAcc (M.insert n sc pnas) ps given imps
1919 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1920 insImpAcc _ _ given imps = given ++ imps
1922 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1924 find n [] acc = Nothing
1925 find n (PImp _ _ _ n' t : gs) acc
1926 | n == n' = Just (t, reverse acc ++ gs)
1927 find n (PTacImplicit _ _ n' _ t : gs) acc
1928 | n == n' = Just (t, reverse acc ++ gs)
1929 find n (g : gs) acc = find n gs (g : acc)
1931-- return True if the second argument is an implicit argument which is
1932-- expected in the implicits, or if it's not an implicit
1933impIn :: [PArg] -> PArg -> Bool
1934impIn ps (PExp _ _ _ _) = True
1935impIn ps (PConstraint _ _ _ _) = True
1936impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1938expArg (PExp _ _ _ _) = True
1939expArg (PConstraint _ _ _ _) = True
1942-- replace non-linear occurrences with _
1944stripLinear :: IState -> PTerm -> PTerm
1945stripLinear i tm = evalState (sl tm) [] where
1946 sl :: PTerm -> State [Name] PTerm
1948 | (_:_) <- lookupTy f (tt_ctxt i)
1949 = return $ PRef fc hl f
1950 | otherwise = do ns <- get
1952 then return $ PHidden (PRef fc hl f) -- Placeholder
1953 else do put (f : ns)
1954 return (PRef fc hl f)
1958 then return $ PHidden (PPatvar fc f) -- Placeholder
1959 else do put (f : ns)
1960 return (PPatvar fc f)
1961 -- Assumption is that variables are all the same in each alternative
1962 sl t@(PAlternative ms b as) = do ns <- get
1964 return (PAlternative ms b as')
1965 where slAlts ns (a : as) = do put ns
1969 slAlts ns [] = return []
1970 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1971 sl (PDPair fc hls p l t r) = do l' <- sl l
1974 return (PDPair fc hls p l' t' r')
1975 sl (PApp fc fn args) = do fn' <- case fn of
1976 -- Just the args, fn isn't matchable as a var
1977 PRef _ _ _ -> return fn
1979 args' <- mapM slA args
1980 return $ PApp fc fn' args'
1981 where slA (PImp p m l n t) = do t' <- sl t
1982 return $ PImp p m l n t'
1983 slA (PExp p l n t) = do t' <- sl t
1984 return $ PExp p l n t'
1985 slA (PConstraint p l n t)
1987 return $ PConstraint p l n t'
1988 slA (PTacImplicit p l n sc t)
1990 return $ PTacImplicit p l n sc t'
1993-- | Remove functions which aren't applied to anything, which must then
1994-- be resolved by unification. Assume names resolved and alternatives
1995-- filled in (so no ambiguity).
1996stripUnmatchable :: IState -> PTerm -> PTerm
1997stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1998 su :: PTerm -> PTerm
1999 su tm@(PRef fc hl f)
2000 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2002 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2003 not (implicitable f)
2005 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2006 not (implicitable f)
2008 su (PApp fc f@(PRef _ _ fn) args)
2009 -- here we use canBeDConName because the impossible pattern
2010 -- check will not necessarily fully resolve constructor names,
2011 -- and these bare names will otherwise get in the way of
2012 -- impossbility checking.
2013 | canBeDConName fn ctxt
2014 = PApp fc f (fmap (fmap su) args)
2016 = PHidden (PApp fc f args)
2017 su (PAlternative ms b alts)
2018 = let alts' = filter (/= Placeholder) (map su alts) in
2019 if null alts' then Placeholder
2020 else PAlternative ms b alts'
2021 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2022 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2023 su t@(PLam fc _ _ _ _) = PHidden t
2024 su t@(PPi _ _ _ _ _) = PHidden t
2025 su t@(PConstant _ c) | isTypeConst c = PHidden t
2030stripUnmatchable i tm = tm
2033mkPApp fc a f as = let rest = drop a as in
2034 if a == 0 then appRest fc f rest
2035 else appRest fc (PApp fc f (take a as)) rest
2038 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2040-- Find 'static' argument positions
2041-- (the declared ones, plus any names in argument position in the declared
2043-- FIXME: It's possible that this really has to happen after elaboration
2045findStatics :: IState -> PTerm -> (PTerm, [Bool])
2046findStatics ist tm = let (ns, ss) = fs tm
2047 in runState (pos ns ss tm) []
2048 where fs (PPi p n fc t sc)
2049 | Static <- pstatic p
2050 = let (ns, ss) = fs sc in
2051 (namesIn [] ist t : ns, n : ss)
2052 | otherwise = let (ns, ss) = fs sc in
2056 inOne n ns = length (filter id (map (elem n) ns)) == 1
2058 pos ns ss (PPi p n fc t sc)
2059 | elem n ss = do sc' <- pos ns ss sc
2062 return (PPi (p { pstatic = Static }) n fc t sc')
2063 | otherwise = do sc' <- pos ns ss sc
2066 return (PPi p n fc t sc')
2067 pos ns ss t = return t
2069-- for 6.12/7 compatibility
2070data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2072instance Applicative (EitherErr a) where
2076instance Monad (EitherErr a) where
2079 (LeftErr e) >>= k = LeftErr e
2080 RightOK v >>= k = k v
2082toEither (LeftErr e) = Left e
2083toEither (RightOK ho) = Right ho
2085-- | Syntactic match of a against b, returning pair of variables in a
2086-- and what they match. Returns the pair that failed if not a match.
2087matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2088matchClause = matchClause' False
2090matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2091matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2092 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2094 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2097 match' x y = match (fullApp x) (fullApp y)
2098 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2099 | fi == txt "fromInteger" && b == txt "builtins",
2100 PConstant _ (I _) <- getTm x = match (getTm x) x'
2101 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2102 | fi == txt "fromInteger" && b == txt "builtins",
2103 PConstant _ (I _) <- getTm x = match (getTm x) x'
2104 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2105 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2106 match (PApp _ f args) (PApp _ f' args')
2107 | length args == length args'
2108 = do mf <- match' f f'
2109 ms <- zipWithM matchArg args args'
2110 return (mf ++ concat ms)
2111 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2112 match (PPatvar f n) xr = match (PRef f [f] n) xr
2113 match xr (PPatvar f n) = match xr (PRef f [f] n)
2114 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2115 match (PRef _ _ n) tm@(PRef _ _ n')
2116 | n == n' && not names &&
2117 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2118 || tm == Placeholder)
2120 -- if one namespace is missing, drop the other
2121 | n == n' || n == dropNS n' || dropNS n == n' = return []
2122 where dropNS (NS n _) = n
2124 match (PRef _ _ n) tm
2125 | not names && (not (isConName n (tt_ctxt i) ||
2126 isFnName n (tt_ctxt i)) || tm == Placeholder)
2128 match (PRewrite _ l r _) (PRewrite _ l' r' _)
2129 = do ml <- match' l l'
2132 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2135 match (PTyped l r) x = match l x
2136 match x (PTyped l r) = match x l
2137 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2140 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2143 return (ml ++ mt ++ mr)
2144 match (PAlternative _ a as) (PAlternative _ a' as')
2145 = do ms <- zipWithM match' as as'
2147 match a@(PAlternative _ _ as) b
2148 = do let ms = zipWith match' as (repeat b)
2149 case (rights (map toEither ms)) of
2152 match (PCase _ _ _) _ = return [] -- lifted out
2153 match (PMetavar _ _) _ = return [] -- modified
2154 match (PInferRef _ _ _) _ = return [] -- modified
2155 match (PQuote _) _ = return []
2156 match (PProof _) _ = return []
2157 match (PTactics _) _ = return []
2158 match (PResolveTC _) (PResolveTC _) = return []
2159 match (PTrue _ _) (PTrue _ _) = return []
2160 match (PReturn _) (PReturn _) = return []
2161 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2164 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2167 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2168 mty <- match' ty ty'
2170 return (mt ++ mty ++ ms)
2171 match (PHidden x) (PHidden y)
2172 | RightOK xs <- match x y = return xs -- to collect variables
2173 | otherwise = return [] -- Otherwise hidden things are unmatchable
2175 | RightOK xs <- match x y = return xs
2176 | otherwise = return []
2178 | RightOK xs <- match x y = return xs
2179 | otherwise = return []
2180 match (PUnifyLog x) y = match' x y
2181 match x (PUnifyLog y) = match' x y
2182 match (PNoImplicits x) y = match' x y
2183 match x (PNoImplicits y) = match' x y
2184 match Placeholder _ = return []
2185 match _ Placeholder = return []
2186 match (PResolveTC _) _ = return []
2187 match a b | a == b = return []
2188 | otherwise = LeftErr (a, b)
2190 checkRpts (RightOK ms) = check ms where
2192 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2195 check (_:xs) = check xs
2197 checkRpts (LeftErr x) = Left x
2199substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2200substMatches ms = substMatchesShadow ms []
2202substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2203substMatchesShadow [] shs t = t
2204substMatchesShadow ((n,tm):ns) shs t
2205 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2207substMatch :: Name -> PTerm -> PTerm -> PTerm
2208substMatch n = substMatchShadow n []
2210substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2211substMatchShadow n shs tm t = sm shs t where
2212 sm xs (PRef _ _ n') | n == n' = tm
2213 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2214 sm xs (PPi p x fc t sc)
2216 = let x' = nextName x in
2217 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2218 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2219 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2220 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2221 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2222 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2223 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2225 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2226 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2227 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2228 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2229 sm xs (PHidden x) = PHidden (sm xs x)
2230 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2231 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2232 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2233 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2236 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2239shadow :: Name -> Name -> PTerm -> PTerm
2240shadow n n' t = sm 0 t where
2241 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2242 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2243 | otherwise = PLam fc x xfc (sm 0 t) sc
2244 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2245 | otherwise = PPi p x fc (sm 0 t) sc
2246 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2247 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2248 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2249 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2250 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2251 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2252 sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2253 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2254 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2255 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2256 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2257 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2258 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2259 sm 0 (PHidden x) = PHidden (sm 0 x)
2260 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2261 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2262 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2263 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2264 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2265 sm ql x = descend (sm ql) x
2267-- | Rename any binders which are repeated (so that we don't have to mess
2268-- about with shadowing anywhere else).
2269mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2270mkUniqueNames env shadows tm
2271 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2273 initMap = M.fromList shadows
2275 inScope :: S.Set Name
2276 inScope = S.fromList $ boundNamesIn tm
2278 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2279 return (arg { getTm = t' })
2281 -- Initialise the unique name with the environment length (so we're not
2282 -- looking for too long...)
2283 initN (UN n) l = UN $ txt (str n ++ show l)
2284 initN (MN i s) l = MN (i+l) s
2287 -- FIXME: Probably ought to do this for completeness! It's fine as
2288 -- long as there are no bindings inside tactics though.
2289 mkUniqT _ nmap tac = return tac
2291 mkUniq :: Int -- ^ The number of quotations that we're under
2292 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2293 mkUniq 0 nmap (PLam fc n nfc ty sc)
2297 then do let n' = uniqueNameSet (initN n (S.size env))
2298 (S.union env inScope)
2299 return (n', sc) -- shadow n n' sc)
2301 put (S.insert n' env)
2302 let nmap' = M.insert n n' nmap
2303 ty' <- mkUniq 0 nmap ty
2304 sc'' <- mkUniq 0 nmap' sc'
2305 return $! PLam fc n' nfc ty' sc''
2306 mkUniq 0 nmap (PPi p n fc ty sc)
2310 then do let n' = uniqueNameSet (initN n (S.size env))
2311 (S.union env inScope)
2312 return (n', sc) -- shadow n n' sc)
2314 put (S.insert n' env)
2315 let nmap' = M.insert n n' nmap
2316 ty' <- mkUniq 0 nmap ty
2317 sc'' <- mkUniq 0 nmap' sc'
2318 return $! PPi p n' fc ty' sc''
2319 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2323 then do let n' = uniqueNameSet (initN n (S.size env))
2324 (S.union env inScope)
2325 return (n', sc) -- shadow n n' sc)
2327 put (S.insert n' env)
2328 let nmap' = M.insert n n' nmap
2329 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2330 sc'' <- mkUniq 0 nmap' sc'
2331 return $! PLet fc n' nfc ty' val' sc''
2332 mkUniq 0 nmap (PApp fc t args)
2333 = do t' <- mkUniq 0 nmap t
2334 args' <- mapM (mkUniqA 0 nmap) args
2335 return $! PApp fc t' args'
2336 mkUniq 0 nmap (PAppBind fc t args)
2337 = do t' <- mkUniq 0 nmap t
2338 args' <- mapM (mkUniqA 0 nmap) args
2339 return $! PAppBind fc t' args'
2340 mkUniq 0 nmap (PCase fc t alts)
2341 = do t' <- mkUniq 0 nmap t
2342 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2343 return (x', y')) alts
2344 return $! PCase fc t' alts'
2345 mkUniq 0 nmap (PIfThenElse fc c t f)
2346 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2347 mkUniq 0 nmap (PPair fc hls p l r)
2348 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2349 return $! PPair fc hls p l' r'
2350 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2353 (n', sc') <- if n `S.member` env
2354 then do let n' = uniqueNameSet n (S.union env inScope)
2355 return (n', sc) -- shadow n n' sc)
2357 put (S.insert n' env)
2358 let nmap' = M.insert n n' nmap
2359 t' <- mkUniq 0 nmap t
2360 sc'' <- mkUniq 0 nmap' sc'
2361 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2362 mkUniq 0 nmap (PDPair fc hls p l t r)
2363 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2364 return $! PDPair fc hls p l' t' r'
2365 mkUniq 0 nmap (PAlternative ns b as)
2366 -- store the nmap and defer the rest until we've pruned the set
2367 -- during elaboration
2368 = return $ PAlternative (M.toList nmap ++ ns) b as
2369 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2370 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2371 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2372 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2373 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2374 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2375 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2376 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2377 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2378 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2381 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2383 mkUniq ql nmap (PQuasiquote tm ty) =
2384 do tm' <- mkUniq (ql + 1) nmap tm
2386 Nothing -> return Nothing
2387 Just t -> fmap Just $ mkUniq ql nmap t
2388 return $! PQuasiquote tm' ty'
2389 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2391 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