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 by l r g) = PRewrite f by (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 by 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 by 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 (PWithApp fc f a)
1746 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1747 ai inpat qq env ds (PCase fc c os)
1748 = let c' = ai inpat qq env ds c in
1749 -- leave os alone, because they get lifted into a new pattern match
1750 -- definition which is passed through addImpl agai inpatn with more scope
1754 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1755 (ai inpat qq env ds t)
1756 (ai inpat qq env ds f)
1758 -- If the name in a lambda is a constructor name, do this as a 'case'
1759 -- instead (it is harmless to do so, especially since the lambda will
1760 -- be lifted anyway!)
1761 ai inpat qq env ds (PLam fc n nfc ty sc)
1762 = case lookupDef n (tt_ctxt ist) of
1763 [] -> let ty' = ai inpat qq env ds ty
1764 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1765 PLam fc n nfc ty' sc'
1766 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1767 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1768 [(PRef fc [] n, sc)]))
1769 ai inpat qq env ds (PLet fc n nfc ty val sc)
1770 = case lookupDef n (tt_ctxt ist) of
1771 [] -> let ty' = ai inpat qq env ds ty
1772 val' = ai inpat qq env ds val
1773 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1774 PLet fc n nfc ty' val' sc'
1776 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1777 ai inpat qq env ds (PPi p n nfc ty sc)
1778 = let ty' = ai inpat qq env ds ty
1779 env' = if n `elem` imp_meths then env
1780 else ((n, Just ty) : env)
1781 sc' = ai inpat qq env' ds sc in
1783 ai inpat qq env ds (PGoal fc r n sc)
1784 = let r' = ai inpat qq env ds r
1785 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1787 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1788 -- Don't do PProof or PTactics since implicits get added when scope is
1789 -- properly known in ElabTerm.runTac
1790 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1791 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1792 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1793 (fmap (ai inpat True env ds) g)
1794 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1795 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1796 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1797 ai inpat qq env ds tm = tm
1799 handleErr (Left err) = PElabError err
1800 handleErr (Right x) = x
1802-- if in a pattern, and there are no arguments, and there's no possible
1803-- names with zero explicit arguments, don't add implicits.
1805aiFn :: Name -> Bool -> Bool -> Bool
1808 -> Name -- ^ function being applied
1810 -> [PArg] -- ^ initial arguments (if in a pattern)
1812aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1813 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1815 = case lookupDef f (tt_ctxt ist) of
1816 [] -> Right $ PPatvar ffc f
1817 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1818 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1819 if (not (vname f) || tcname f
1820 || any (conCaf (tt_ctxt ist)) ialts)
1821-- any constructor alts || any allImp ialts))
1822 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1823 else Right $ PPatvar ffc f
1824 where imp (PExp _ _ _ _) = False
1827 allImp xs = all imp xs
1829 unqualified (NS _ _) = False
1830 unqualified _ = True
1832 constructor (TyDecl (DCon _ _ _) _) = True
1833 constructor _ = False
1835 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1837 vname (UN n) = True -- non qualified
1840aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1841 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1842aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1843 -- This is where namespaces get resolved by adding PAlternative
1844 = do let ns = lookupCtxtName f (idris_implicits ist)
1845 let nh = filter (\(n, _) -> notHidden n) ns
1846 let ns' = case trimAlts ds nh of
1850 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1852 [] -> if f `elem` (map fst (idris_metavars ist))
1853 then Right $ PApp fc (PRef ffc [ffc] f) as
1854 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1856 PAlternative [] (ExactlyOne True) $
1857 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1858 (insertImpl ns as)) alts
1860 -- if the name is in imp_meths, we should actually refer to the bound
1861 -- name rather than the global one after expanding implicits
1862 isImpName f f' | f `elem` imp_meths = f
1865 trimAlts [] alts = alts
1867 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1872 notHidden n = case getAccessibility n of
1878 = case lookupDefAccExact n False (tt_ctxt ist) of
1882 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1883 -> [PArg] -- ^ given arguments
1886 = let (as', badimpls) = partition (impIn ps) as in
1887 map addUnknownImp badimpls ++
1888 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1890 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1891 -> [PArg] -- parameters
1892 -> [PArg] -- explicit arguments
1893 -> [PArg] -- implicits given
1895 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1896 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1897 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1898 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1899 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1900 let rtc = PResolveTC fc in
1901 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1902 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1903 case find n imps [] of
1905 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1907 PImp p True l n Placeholder :
1908 insImpAcc (M.insert n Placeholder pnas) ps given imps
1909 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1910 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1911 case find n imps [] of
1913 PTacImplicit p l n sc tm :
1914 insImpAcc (M.insert n tm pnas) ps given imps'
1917 then PTacImplicit p l n sc Placeholder :
1918 insImpAcc (M.insert n Placeholder pnas) ps given imps
1919 else PTacImplicit p l n sc sc :
1920 insImpAcc (M.insert n sc pnas) ps given imps
1921 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1922 insImpAcc _ _ given imps = given ++ imps
1924 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1926 find n [] acc = Nothing
1927 find n (PImp _ _ _ n' t : gs) acc
1928 | n == n' = Just (t, reverse acc ++ gs)
1929 find n (PTacImplicit _ _ n' _ t : gs) acc
1930 | n == n' = Just (t, reverse acc ++ gs)
1931 find n (g : gs) acc = find n gs (g : acc)
1933-- return True if the second argument is an implicit argument which is
1934-- expected in the implicits, or if it's not an implicit
1935impIn :: [PArg] -> PArg -> Bool
1936impIn ps (PExp _ _ _ _) = True
1937impIn ps (PConstraint _ _ _ _) = True
1938impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1940expArg (PExp _ _ _ _) = True
1941expArg (PConstraint _ _ _ _) = True
1944-- replace non-linear occurrences with _
1946stripLinear :: IState -> PTerm -> PTerm
1947stripLinear i tm = evalState (sl tm) [] where
1948 sl :: PTerm -> State [Name] PTerm
1950 | (_:_) <- lookupTy f (tt_ctxt i)
1951 = return $ PRef fc hl f
1952 | otherwise = do ns <- get
1954 then return $ PHidden (PRef fc hl f) -- Placeholder
1955 else do put (f : ns)
1956 return (PRef fc hl f)
1960 then return $ PHidden (PPatvar fc f) -- Placeholder
1961 else do put (f : ns)
1962 return (PPatvar fc f)
1963 -- Assumption is that variables are all the same in each alternative
1964 sl t@(PAlternative ms b as) = do ns <- get
1966 return (PAlternative ms b as')
1967 where slAlts ns (a : as) = do put ns
1971 slAlts ns [] = return []
1972 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1973 sl (PDPair fc hls p l t r) = do l' <- sl l
1976 return (PDPair fc hls p l' t' r')
1977 sl (PApp fc fn args) = do fn' <- case fn of
1978 -- Just the args, fn isn't matchable as a var
1979 PRef _ _ _ -> return fn
1981 args' <- mapM slA args
1982 return $ PApp fc fn' args'
1983 where slA (PImp p m l n t) = do t' <- sl t
1984 return $ PImp p m l n t'
1985 slA (PExp p l n t) = do t' <- sl t
1986 return $ PExp p l n t'
1987 slA (PConstraint p l n t)
1989 return $ PConstraint p l n t'
1990 slA (PTacImplicit p l n sc t)
1992 return $ PTacImplicit p l n sc t'
1995-- | Remove functions which aren't applied to anything, which must then
1996-- be resolved by unification. Assume names resolved and alternatives
1997-- filled in (so no ambiguity).
1998stripUnmatchable :: IState -> PTerm -> PTerm
1999stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2000 su :: PTerm -> PTerm
2001 su tm@(PRef fc hl f)
2002 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2004 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2005 not (implicitable f)
2007 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2008 not (implicitable f)
2010 su (PApp fc f@(PRef _ _ fn) args)
2011 -- here we use canBeDConName because the impossible pattern
2012 -- check will not necessarily fully resolve constructor names,
2013 -- and these bare names will otherwise get in the way of
2014 -- impossbility checking.
2015 | canBeDConName fn ctxt
2016 = PApp fc f (fmap (fmap su) args)
2018 = PHidden (PApp fc f args)
2019 su (PAlternative ms b alts)
2020 = let alts' = filter (/= Placeholder) (map su alts) in
2021 if null alts' then Placeholder
2022 else PAlternative ms b alts'
2023 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2024 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2025 su t@(PLam fc _ _ _ _) = PHidden t
2026 su t@(PPi _ _ _ _ _) = PHidden t
2027 su t@(PConstant _ c) | isTypeConst c = PHidden t
2032stripUnmatchable i tm = tm
2035mkPApp fc a f as = let rest = drop a as in
2036 if a == 0 then appRest fc f rest
2037 else appRest fc (PApp fc f (take a as)) rest
2040 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2042-- Find 'static' argument positions
2043-- (the declared ones, plus any names in argument position in the declared
2045-- FIXME: It's possible that this really has to happen after elaboration
2047findStatics :: IState -> PTerm -> (PTerm, [Bool])
2048findStatics ist tm = let (ns, ss) = fs tm
2049 in runState (pos ns ss tm) []
2050 where fs (PPi p n fc t sc)
2051 | Static <- pstatic p
2052 = let (ns, ss) = fs sc in
2053 (namesIn [] ist t : ns, n : ss)
2054 | otherwise = let (ns, ss) = fs sc in
2058 inOne n ns = length (filter id (map (elem n) ns)) == 1
2060 pos ns ss (PPi p n fc t sc)
2061 | elem n ss = do sc' <- pos ns ss sc
2064 return (PPi (p { pstatic = Static }) n fc t sc')
2065 | otherwise = do sc' <- pos ns ss sc
2068 return (PPi p n fc t sc')
2069 pos ns ss t = return t
2071-- for 6.12/7 compatibility
2072data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2074instance Applicative (EitherErr a) where
2078instance Monad (EitherErr a) where
2081 (LeftErr e) >>= k = LeftErr e
2082 RightOK v >>= k = k v
2084toEither (LeftErr e) = Left e
2085toEither (RightOK ho) = Right ho
2087-- | Syntactic match of a against b, returning pair of variables in a
2088-- and what they match. Returns the pair that failed if not a match.
2089matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2090matchClause = matchClause' False
2092matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2093matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2094 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2096 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2099 match' x y = match (fullApp x) (fullApp y)
2100 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2101 | fi == txt "fromInteger" && b == txt "builtins",
2102 PConstant _ (I _) <- getTm x = match (getTm x) x'
2103 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2104 | fi == txt "fromInteger" && b == txt "builtins",
2105 PConstant _ (I _) <- getTm x = match (getTm x) x'
2106 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2107 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2108 match (PApp _ f args) (PApp _ f' args')
2109 | length args == length args'
2110 = do mf <- match' f f'
2111 ms <- zipWithM matchArg args args'
2112 return (mf ++ concat ms)
2113 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2114 match (PPatvar f n) xr = match (PRef f [f] n) xr
2115 match xr (PPatvar f n) = match xr (PRef f [f] n)
2116 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2117 match (PRef _ _ n) tm@(PRef _ _ n')
2118 | n == n' && not names &&
2119 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2120 || tm == Placeholder)
2122 -- if one namespace is missing, drop the other
2123 | n == n' || n == dropNS n' || dropNS n == n' = return []
2124 where dropNS (NS n _) = n
2126 match (PRef _ _ n) tm
2127 | not names && (not (isConName n (tt_ctxt i) ||
2128 isFnName n (tt_ctxt i)) || tm == Placeholder)
2130 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2131 = do ml <- match' l l'
2134 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2137 match (PTyped l r) x = match l x
2138 match x (PTyped l r) = match x l
2139 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2142 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2145 return (ml ++ mt ++ mr)
2146 match (PAlternative _ a as) (PAlternative _ a' as')
2147 = do ms <- zipWithM match' as as'
2149 match a@(PAlternative _ _ as) b
2150 = do let ms = zipWith match' as (repeat b)
2151 case (rights (map toEither ms)) of
2154 match (PCase _ _ _) _ = return [] -- lifted out
2155 match (PMetavar _ _) _ = return [] -- modified
2156 match (PInferRef _ _ _) _ = return [] -- modified
2157 match (PQuote _) _ = return []
2158 match (PProof _) _ = return []
2159 match (PTactics _) _ = return []
2160 match (PResolveTC _) (PResolveTC _) = return []
2161 match (PTrue _ _) (PTrue _ _) = return []
2162 match (PReturn _) (PReturn _) = return []
2163 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2166 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2169 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2170 mty <- match' ty ty'
2172 return (mt ++ mty ++ ms)
2173 match (PHidden x) (PHidden y)
2174 | RightOK xs <- match x y = return xs -- to collect variables
2175 | otherwise = return [] -- Otherwise hidden things are unmatchable
2177 | RightOK xs <- match x y = return xs
2178 | otherwise = return []
2180 | RightOK xs <- match x y = return xs
2181 | otherwise = return []
2182 match (PUnifyLog x) y = match' x y
2183 match x (PUnifyLog y) = match' x y
2184 match (PNoImplicits x) y = match' x y
2185 match x (PNoImplicits y) = match' x y
2186 match Placeholder _ = return []
2187 match _ Placeholder = return []
2188 match (PResolveTC _) _ = return []
2189 match a b | a == b = return []
2190 | otherwise = LeftErr (a, b)
2192 checkRpts (RightOK ms) = check ms where
2194 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2197 check (_:xs) = check xs
2199 checkRpts (LeftErr x) = Left x
2201substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2202substMatches ms = substMatchesShadow ms []
2204substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2205substMatchesShadow [] shs t = t
2206substMatchesShadow ((n,tm):ns) shs t
2207 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2209substMatch :: Name -> PTerm -> PTerm -> PTerm
2210substMatch n = substMatchShadow n []
2212substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2213substMatchShadow n shs tm t = sm shs t where
2214 sm xs (PRef _ _ n') | n == n' = tm
2215 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2216 sm xs (PPi p x fc t sc)
2218 = let x' = nextName x in
2219 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2220 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2221 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2222 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2223 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2224 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2225 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2227 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2228 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2229 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2230 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2231 sm xs (PHidden x) = PHidden (sm xs x)
2232 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2233 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2234 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2235 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2238 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2241shadow :: Name -> Name -> PTerm -> PTerm
2242shadow n n' t = sm 0 t where
2243 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2244 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2245 | otherwise = PLam fc x xfc (sm 0 t) sc
2246 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2247 | otherwise = PPi p x fc (sm 0 t) sc
2248 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2249 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2250 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2251 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2252 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2253 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2254 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2255 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2256 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2257 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2258 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2259 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2260 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2261 sm 0 (PHidden x) = PHidden (sm 0 x)
2262 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2263 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2264 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2265 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2266 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2267 sm ql x = descend (sm ql) x
2269-- | Rename any binders which are repeated (so that we don't have to mess
2270-- about with shadowing anywhere else).
2271mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2272mkUniqueNames env shadows tm
2273 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2275 initMap = M.fromList shadows
2277 inScope :: S.Set Name
2278 inScope = S.fromList $ boundNamesIn tm
2280 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2281 return (arg { getTm = t' })
2283 -- Initialise the unique name with the environment length (so we're not
2284 -- looking for too long...)
2285 initN (UN n) l = UN $ txt (str n ++ show l)
2286 initN (MN i s) l = MN (i+l) s
2289 -- FIXME: Probably ought to do this for completeness! It's fine as
2290 -- long as there are no bindings inside tactics though.
2291 mkUniqT _ nmap tac = return tac
2293 mkUniq :: Int -- ^ The number of quotations that we're under
2294 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2295 mkUniq 0 nmap (PLam fc n nfc ty sc)
2299 then do let n' = uniqueNameSet (initN n (S.size env))
2300 (S.union env inScope)
2301 return (n', sc) -- shadow n n' sc)
2303 put (S.insert n' env)
2304 let nmap' = M.insert n n' nmap
2305 ty' <- mkUniq 0 nmap ty
2306 sc'' <- mkUniq 0 nmap' sc'
2307 return $! PLam fc n' nfc ty' sc''
2308 mkUniq 0 nmap (PPi p n fc ty sc)
2312 then do let n' = uniqueNameSet (initN n (S.size env))
2313 (S.union env inScope)
2314 return (n', sc) -- shadow n n' sc)
2316 put (S.insert n' env)
2317 let nmap' = M.insert n n' nmap
2318 ty' <- mkUniq 0 nmap ty
2319 sc'' <- mkUniq 0 nmap' sc'
2320 return $! PPi p n' fc ty' sc''
2321 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2325 then do let n' = uniqueNameSet (initN n (S.size env))
2326 (S.union env inScope)
2327 return (n', sc) -- shadow n n' sc)
2329 put (S.insert n' env)
2330 let nmap' = M.insert n n' nmap
2331 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2332 sc'' <- mkUniq 0 nmap' sc'
2333 return $! PLet fc n' nfc ty' val' sc''
2334 mkUniq 0 nmap (PApp fc t args)
2335 = do t' <- mkUniq 0 nmap t
2336 args' <- mapM (mkUniqA 0 nmap) args
2337 return $! PApp fc t' args'
2338 mkUniq 0 nmap (PAppBind fc t args)
2339 = do t' <- mkUniq 0 nmap t
2340 args' <- mapM (mkUniqA 0 nmap) args
2341 return $! PAppBind fc t' args'
2342 mkUniq 0 nmap (PCase fc t alts)
2343 = do t' <- mkUniq 0 nmap t
2344 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2345 return (x', y')) alts
2346 return $! PCase fc t' alts'
2347 mkUniq 0 nmap (PIfThenElse fc c t f)
2348 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2349 mkUniq 0 nmap (PPair fc hls p l r)
2350 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2351 return $! PPair fc hls p l' r'
2352 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2355 (n', sc') <- if n `S.member` env
2356 then do let n' = uniqueNameSet n (S.union env inScope)
2357 return (n', sc) -- shadow n n' sc)
2359 put (S.insert n' env)
2360 let nmap' = M.insert n n' nmap
2361 t' <- mkUniq 0 nmap t
2362 sc'' <- mkUniq 0 nmap' sc'
2363 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2364 mkUniq 0 nmap (PDPair fc hls p l t r)
2365 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2366 return $! PDPair fc hls p l' t' r'
2367 mkUniq 0 nmap (PAlternative ns b as)
2368 -- store the nmap and defer the rest until we've pruned the set
2369 -- during elaboration
2370 = return $ PAlternative (M.toList nmap ++ ns) b as
2371 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2372 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2373 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2374 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2375 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2376 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2377 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2378 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2379 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2380 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2383 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2385 mkUniq ql nmap (PQuasiquote tm ty) =
2386 do tm' <- mkUniq (ql + 1) nmap tm
2388 Nothing -> return Nothing
2389 Just t -> fmap Just $ mkUniq ql nmap t
2390 return $! PQuasiquote tm' ty'
2391 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2393 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