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) 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) 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
1542 let (tm', impdata) = implicitise syn ignore i ptm
1543 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1544 -- let (tm'', spos) = findStatics i tm'
1545 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1547 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1549 -- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1552 -- Detect unknown names in default arguments and throw error if found.
1553 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1554 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1556 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1557 notFoundInDefault kns (PTacImplicit _ _ n script _)
1559 case notFound kns (namesIn [] i script) of
1560 Nothing -> return (n:kns)
1561 Just name -> throwError (NoSuchVariable name)
1562 notFoundInDefault kns p = return ((pname p):kns)
1564 notFound :: [Name] -> [Name] -> Maybe Name
1565 notFound kns [] = Nothing
1566 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1567 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1569implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1570implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1571 let (declimps, ns') = execState (imps True [] tm) ([], [])
1572 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1573 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1574 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1576 then (tm, reverse declimps)
1577 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1579 uvars = map ipair (filter uimplicit (using syn))
1580 pvars = syn_params syn
1582 inUsing n = n `elem` map fst uvars
1584 ipair (UImplicit x y) = (x, y)
1585 uimplicit (UImplicit _ _) = True
1588 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1589 | otherwise = x : dropAll xs ys
1592 -- Find names in argument position in a type, suitable for implicit
1594 -- Not the function position, but do everything else...
1595 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1596 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1598 imps top env ty@(PApp _ f as)
1599 = do (decls, ns) <- get
1600 let isn = nub (implNamesIn uvars ty)
1601 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1602 imps top env (PPi (Imp l _ _ _) n _ ty sc)
1603 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1605 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1606 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1607 imps True (n:env) sc
1608 imps top env (PPi (Exp l _ _) n _ ty sc)
1609 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1610 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1612 (decls, ns) <- get -- ignore decls in HO types
1613 put (PExp (getPriority ist ty) l n Placeholder : decls,
1614 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1615 imps True (n:env) sc
1616 imps top env (PPi (Constraint l _) n _ ty sc)
1617 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1618 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1620 (decls, ns) <- get -- ignore decls in HO types
1621 put (PConstraint 10 l n Placeholder : decls,
1622 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1623 imps True (n:env) sc
1624 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1625 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1626 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1628 (decls, ns) <- get -- ignore decls in HO types
1629 put (PTacImplicit 10 l n scr Placeholder : decls,
1630 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1631 imps True (n:env) sc
1632 imps top env (PRewrite _ l r _)
1633 = do (decls, ns) <- get
1634 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1635 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1636 imps top env (PTyped l r)
1638 imps top env (PPair _ _ _ l r)
1639 = do (decls, ns) <- get
1640 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1641 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1642 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1643 = do (decls, ns) <- get
1644 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1645 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1646 imps top env (PDPair _ _ _ l t r)
1647 = do (decls, ns) <- get
1648 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1650 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1651 imps top env (PAlternative ms a as)
1652 = do (decls, ns) <- get
1653 let isn = concatMap (namesIn uvars ist) as
1654 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1655 imps top env (PLam fc n _ ty sc)
1656 = do imps False env ty
1657 imps False (n:env) sc
1658 imps top env (PHidden tm) = imps False env tm
1659 imps top env (PUnifyLog tm) = imps False env tm
1660 imps top env (PNoImplicits tm) = imps False env tm
1661 imps top env (PRunElab fc tm ns) = imps False env tm
1662 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1663 imps top env _ = return ()
1665 pibind using [] sc = sc
1666 pibind using (n:ns) sc
1667 = case lookup n using of
1668 Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))
1669 n NoFC ty (pibind using ns sc)
1670 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))
1671 n NoFC Placeholder (pibind using ns sc)
1673-- Add implicit arguments in function calls
1674addImplPat :: IState -> PTerm -> PTerm
1675addImplPat = addImpl' True [] [] []
1677addImplBound :: IState -> [Name] -> PTerm -> PTerm
1678addImplBound ist ns = addImpl' False ns [] [] ist
1680addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1681addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1683-- | Add the implicit arguments to applications in the term
1684-- [Name] gives the names to always expend, even when under a binder of
1685-- that name (this is to expand methods with implicit arguments in dependent
1687addImpl :: [Name] -> IState -> PTerm -> PTerm
1688addImpl = addImpl' False [] []
1690-- TODO: in patterns, don't add implicits to function names guarded by constructors
1691-- and *not* inside a PHidden
1693addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1694addImpl' inpat env infns imp_meths ist ptm
1695 = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1697 topname = case ptm of
1699 PApp _ (PRef _ _ n) _ -> n
1700 _ -> sUN "" -- doesn't matter then
1702 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1703 ai inpat qq env ds (PRef fc fcs f)
1704 | f `elem` infns = PInferRef fc fcs f
1705 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1706 ai inpat qq env ds (PHidden (PRef fc hl f))
1707 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1708 ai inpat qq env ds (PRewrite fc l r g)
1709 = let l' = ai inpat qq env ds l
1710 r' = ai inpat qq env ds r
1711 g' = fmap (ai inpat qq env ds) g in
1712 PRewrite fc l' r' g'
1713 ai inpat qq env ds (PTyped l r)
1714 = let l' = ai inpat qq env ds l
1715 r' = ai inpat qq env ds r in
1717 ai inpat qq env ds (PPair fc hls p l r)
1718 = let l' = ai inpat qq env ds l
1719 r' = ai inpat qq env ds r in
1720 PPair fc hls p l' r'
1721 ai inpat qq env ds (PDPair fc hls p l t r)
1722 = let l' = ai inpat qq env ds l
1723 t' = ai inpat qq env ds t
1724 r' = ai inpat qq env ds r in
1725 PDPair fc hls p l' t' r'
1726 ai inpat qq env ds (PAlternative ms a as)
1727 = let as' = map (ai inpat qq env ds) as in
1728 PAlternative ms a as'
1729 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1730 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1731 = let as' = map (fmap (ai inpat qq env ds)) as in
1732 PApp fc (PInferRef ffc hl f) as'
1733 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1734 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1735 | not (f `elem` map fst env)
1736 = let as' = map (fmap (ai inpat qq env ds)) as in
1737 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1738 | Just (Just ty) <- lookup f env =
1739 let as' = map (fmap (ai inpat qq env ds)) as
1740 arity = getPArity ty in
1741 mkPApp fc arity ftm as'
1742 ai inpat qq env ds (PApp fc f as)
1743 = let f' = ai inpat qq env ds f
1744 as' = map (fmap (ai inpat qq env ds)) as in
1746 ai inpat qq env ds (PCase fc c os)
1747 = let c' = ai inpat qq env ds c in
1748 -- leave os alone, because they get lifted into a new pattern match
1749 -- definition which is passed through addImpl agai inpatn with more scope
1753 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1754 (ai inpat qq env ds t)
1755 (ai inpat qq env ds f)
1757 -- If the name in a lambda is a constructor name, do this as a 'case'
1758 -- instead (it is harmless to do so, especially since the lambda will
1759 -- be lifted anyway!)
1760 ai inpat qq env ds (PLam fc n nfc ty sc)
1761 = case lookupDef n (tt_ctxt ist) of
1762 [] -> let ty' = ai inpat qq env ds ty
1763 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1764 PLam fc n nfc ty' sc'
1765 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1766 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1767 [(PRef fc [] n, sc)]))
1768 ai inpat qq env ds (PLet fc n nfc ty val sc)
1769 = case lookupDef n (tt_ctxt ist) of
1770 [] -> let ty' = ai inpat qq env ds ty
1771 val' = ai inpat qq env ds val
1772 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1773 PLet fc n nfc ty' val' sc'
1775 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1776 ai inpat qq env ds (PPi p n nfc ty sc)
1777 = let ty' = ai inpat qq env ds ty
1778 env' = if n `elem` imp_meths then env
1779 else ((n, Just ty) : env)
1780 sc' = ai inpat qq env' ds sc in
1782 ai inpat qq env ds (PGoal fc r n sc)
1783 = let r' = ai inpat qq env ds r
1784 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1786 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1787 -- Don't do PProof or PTactics since implicits get added when scope is
1788 -- properly known in ElabTerm.runTac
1789 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1790 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1791 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1792 (fmap (ai inpat True env ds) g)
1793 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1794 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1795 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1796 ai inpat qq env ds tm = tm
1798 handleErr (Left err) = PElabError err
1799 handleErr (Right x) = x
1801-- if in a pattern, and there are no arguments, and there's no possible
1802-- names with zero explicit arguments, don't add implicits.
1804aiFn :: Name -> Bool -> Bool -> Bool
1807 -> Name -- ^ function being applied
1809 -> [PArg] -- ^ initial arguments (if in a pattern)
1811aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1812 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1814 = case lookupDef f (tt_ctxt ist) of
1815 [] -> Right $ PPatvar ffc f
1816 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1817 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1818 if (not (vname f) || tcname f
1819 || any (conCaf (tt_ctxt ist)) ialts)
1820-- any constructor alts || any allImp ialts))
1821 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1822 else Right $ PPatvar ffc f
1823 where imp (PExp _ _ _ _) = False
1826 allImp xs = all imp xs
1828 unqualified (NS _ _) = False
1829 unqualified _ = True
1831 constructor (TyDecl (DCon _ _ _) _) = True
1832 constructor _ = False
1834 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1836 vname (UN n) = True -- non qualified
1839aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1840 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1841aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1842 -- This is where namespaces get resolved by adding PAlternative
1843 = do let ns = lookupCtxtName f (idris_implicits ist)
1844 let nh = filter (\(n, _) -> notHidden n) ns
1845 let ns' = case trimAlts ds nh of
1849 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1851 [] -> if f `elem` (map fst (idris_metavars ist))
1852 then Right $ PApp fc (PRef ffc [ffc] f) as
1853 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1855 PAlternative [] (ExactlyOne True) $
1856 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1857 (insertImpl ns as)) alts
1859 -- if the name is in imp_meths, we should actually refer to the bound
1860 -- name rather than the global one after expanding implicits
1861 isImpName f f' | f `elem` imp_meths = f
1864 trimAlts [] alts = alts
1866 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1871 notHidden n = case getAccessibility n of
1877 = case lookupDefAccExact n False (tt_ctxt ist) of
1881 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1882 -> [PArg] -- ^ given arguments
1885 = let (as', badimpls) = partition (impIn ps) as in
1886 map addUnknownImp badimpls ++
1887 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1889 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1890 -> [PArg] -- parameters
1891 -> [PArg] -- explicit arguments
1892 -> [PArg] -- implicits given
1894 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1895 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1896 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1897 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1898 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1899 let rtc = PResolveTC fc in
1900 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1901 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1902 case find n imps [] of
1904 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1906 PImp p True l n Placeholder :
1907 insImpAcc (M.insert n Placeholder pnas) ps given imps
1908 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1909 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1910 case find n imps [] of
1912 PTacImplicit p l n sc tm :
1913 insImpAcc (M.insert n tm pnas) ps given imps'
1916 then PTacImplicit p l n sc Placeholder :
1917 insImpAcc (M.insert n Placeholder pnas) ps given imps
1918 else PTacImplicit p l n sc sc :
1919 insImpAcc (M.insert n sc pnas) ps given imps
1920 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1921 insImpAcc _ _ given imps = given ++ imps
1923 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1925 find n [] acc = Nothing
1926 find n (PImp _ _ _ n' t : gs) acc
1927 | n == n' = Just (t, reverse acc ++ gs)
1928 find n (PTacImplicit _ _ n' _ t : gs) acc
1929 | n == n' = Just (t, reverse acc ++ gs)
1930 find n (g : gs) acc = find n gs (g : acc)
1932-- return True if the second argument is an implicit argument which is
1933-- expected in the implicits, or if it's not an implicit
1934impIn :: [PArg] -> PArg -> Bool
1935impIn ps (PExp _ _ _ _) = True
1936impIn ps (PConstraint _ _ _ _) = True
1937impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1939expArg (PExp _ _ _ _) = True
1940expArg (PConstraint _ _ _ _) = True
1943-- replace non-linear occurrences with _
1945stripLinear :: IState -> PTerm -> PTerm
1946stripLinear i tm = evalState (sl tm) [] where
1947 sl :: PTerm -> State [Name] PTerm
1949 | (_:_) <- lookupTy f (tt_ctxt i)
1950 = return $ PRef fc hl f
1951 | otherwise = do ns <- get
1953 then return $ PHidden (PRef fc hl f) -- Placeholder
1954 else do put (f : ns)
1955 return (PRef fc hl f)
1959 then return $ PHidden (PPatvar fc f) -- Placeholder
1960 else do put (f : ns)
1961 return (PPatvar fc f)
1962 -- Assumption is that variables are all the same in each alternative
1963 sl t@(PAlternative ms b as) = do ns <- get
1965 return (PAlternative ms b as')
1966 where slAlts ns (a : as) = do put ns
1970 slAlts ns [] = return []
1971 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1972 sl (PDPair fc hls p l t r) = do l' <- sl l
1975 return (PDPair fc hls p l' t' r')
1976 sl (PApp fc fn args) = do fn' <- case fn of
1977 -- Just the args, fn isn't matchable as a var
1978 PRef _ _ _ -> return fn
1980 args' <- mapM slA args
1981 return $ PApp fc fn' args'
1982 where slA (PImp p m l n t) = do t' <- sl t
1983 return $ PImp p m l n t'
1984 slA (PExp p l n t) = do t' <- sl t
1985 return $ PExp p l n t'
1986 slA (PConstraint p l n t)
1988 return $ PConstraint p l n t'
1989 slA (PTacImplicit p l n sc t)
1991 return $ PTacImplicit p l n sc t'
1994-- | Remove functions which aren't applied to anything, which must then
1995-- be resolved by unification. Assume names resolved and alternatives
1996-- filled in (so no ambiguity).
1997stripUnmatchable :: IState -> PTerm -> PTerm
1998stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1999 su :: PTerm -> PTerm
2000 su tm@(PRef fc hl f)
2001 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2003 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2004 not (implicitable f)
2006 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2007 not (implicitable f)
2009 su (PApp fc f@(PRef _ _ fn) args)
2010 -- here we use canBeDConName because the impossible pattern
2011 -- check will not necessarily fully resolve constructor names,
2012 -- and these bare names will otherwise get in the way of
2013 -- impossbility checking.
2014 | canBeDConName fn ctxt
2015 = PApp fc f (fmap (fmap su) args)
2017 = PHidden (PApp fc f args)
2018 su (PAlternative ms b alts)
2019 = let alts' = filter (/= Placeholder) (map su alts) in
2020 if null alts' then Placeholder
2021 else PAlternative ms b alts'
2022 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2023 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2024 su t@(PLam fc _ _ _ _) = PHidden t
2025 su t@(PPi _ _ _ _ _) = PHidden t
2026 su t@(PConstant _ c) | isTypeConst c = PHidden t
2031stripUnmatchable i tm = tm
2034mkPApp fc a f as = let rest = drop a as in
2035 if a == 0 then appRest fc f rest
2036 else appRest fc (PApp fc f (take a as)) rest
2039 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2041-- Find 'static' argument positions
2042-- (the declared ones, plus any names in argument position in the declared
2044-- FIXME: It's possible that this really has to happen after elaboration
2046findStatics :: IState -> PTerm -> (PTerm, [Bool])
2047findStatics ist tm = let (ns, ss) = fs tm
2048 in runState (pos ns ss tm) []
2049 where fs (PPi p n fc t sc)
2050 | Static <- pstatic p
2051 = let (ns, ss) = fs sc in
2052 (namesIn [] ist t : ns, n : ss)
2053 | otherwise = let (ns, ss) = fs sc in
2057 inOne n ns = length (filter id (map (elem n) ns)) == 1
2059 pos ns ss (PPi p n fc t sc)
2060 | elem n ss = do sc' <- pos ns ss sc
2063 return (PPi (p { pstatic = Static }) n fc t sc')
2064 | otherwise = do sc' <- pos ns ss sc
2067 return (PPi p n fc t sc')
2068 pos ns ss t = return t
2070-- for 6.12/7 compatibility
2071data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2073instance Applicative (EitherErr a) where
2077instance Monad (EitherErr a) where
2080 (LeftErr e) >>= k = LeftErr e
2081 RightOK v >>= k = k v
2083toEither (LeftErr e) = Left e
2084toEither (RightOK ho) = Right ho
2086-- | Syntactic match of a against b, returning pair of variables in a
2087-- and what they match. Returns the pair that failed if not a match.
2088matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2089matchClause = matchClause' False
2091matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2092matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2093 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2095 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2098 match' x y = match (fullApp x) (fullApp y)
2099 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2100 | fi == txt "fromInteger" && b == txt "builtins",
2101 PConstant _ (I _) <- getTm x = match (getTm x) x'
2102 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2103 | fi == txt "fromInteger" && b == txt "builtins",
2104 PConstant _ (I _) <- getTm x = match (getTm x) x'
2105 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2106 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2107 match (PApp _ f args) (PApp _ f' args')
2108 | length args == length args'
2109 = do mf <- match' f f'
2110 ms <- zipWithM matchArg args args'
2111 return (mf ++ concat ms)
2112 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2113 match (PPatvar f n) xr = match (PRef f [f] n) xr
2114 match xr (PPatvar f n) = match xr (PRef f [f] n)
2115 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2116 match (PRef _ _ n) tm@(PRef _ _ n')
2117 | n == n' && not names &&
2118 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2119 || tm == Placeholder)
2121 -- if one namespace is missing, drop the other
2122 | n == n' || n == dropNS n' || dropNS n == n' = return []
2123 where dropNS (NS n _) = n
2125 match (PRef _ _ n) tm
2126 | not names && (not (isConName n (tt_ctxt i) ||
2127 isFnName n (tt_ctxt i)) || tm == Placeholder)
2129 match (PRewrite _ l r _) (PRewrite _ l' r' _)
2130 = do ml <- match' l l'
2133 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2136 match (PTyped l r) x = match l x
2137 match x (PTyped l r) = match x l
2138 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2141 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2144 return (ml ++ mt ++ mr)
2145 match (PAlternative _ a as) (PAlternative _ a' as')
2146 = do ms <- zipWithM match' as as'
2148 match a@(PAlternative _ _ as) b
2149 = do let ms = zipWith match' as (repeat b)
2150 case (rights (map toEither ms)) of
2153 match (PCase _ _ _) _ = return [] -- lifted out
2154 match (PMetavar _ _) _ = return [] -- modified
2155 match (PInferRef _ _ _) _ = return [] -- modified
2156 match (PQuote _) _ = return []
2157 match (PProof _) _ = return []
2158 match (PTactics _) _ = return []
2159 match (PResolveTC _) (PResolveTC _) = return []
2160 match (PTrue _ _) (PTrue _ _) = return []
2161 match (PReturn _) (PReturn _) = return []
2162 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2165 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2168 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2169 mty <- match' ty ty'
2171 return (mt ++ mty ++ ms)
2172 match (PHidden x) (PHidden y)
2173 | RightOK xs <- match x y = return xs -- to collect variables
2174 | otherwise = return [] -- Otherwise hidden things are unmatchable
2176 | RightOK xs <- match x y = return xs
2177 | otherwise = return []
2179 | RightOK xs <- match x y = return xs
2180 | otherwise = return []
2181 match (PUnifyLog x) y = match' x y
2182 match x (PUnifyLog y) = match' x y
2183 match (PNoImplicits x) y = match' x y
2184 match x (PNoImplicits y) = match' x y
2185 match Placeholder _ = return []
2186 match _ Placeholder = return []
2187 match (PResolveTC _) _ = return []
2188 match a b | a == b = return []
2189 | otherwise = LeftErr (a, b)
2191 checkRpts (RightOK ms) = check ms where
2193 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2196 check (_:xs) = check xs
2198 checkRpts (LeftErr x) = Left x
2200substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2201substMatches ms = substMatchesShadow ms []
2203substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2204substMatchesShadow [] shs t = t
2205substMatchesShadow ((n,tm):ns) shs t
2206 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2208substMatch :: Name -> PTerm -> PTerm -> PTerm
2209substMatch n = substMatchShadow n []
2211substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2212substMatchShadow n shs tm t = sm shs t where
2213 sm xs (PRef _ _ n') | n == n' = tm
2214 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2215 sm xs (PPi p x fc t sc)
2217 = let x' = nextName x in
2218 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2219 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2220 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2221 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2222 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2223 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2224 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2226 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2227 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2228 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2229 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2230 sm xs (PHidden x) = PHidden (sm xs x)
2231 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2232 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2233 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2234 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2237 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2240shadow :: Name -> Name -> PTerm -> PTerm
2241shadow n n' t = sm 0 t where
2242 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2243 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2244 | otherwise = PLam fc x xfc (sm 0 t) sc
2245 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2246 | otherwise = PPi p x fc (sm 0 t) sc
2247 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2248 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2249 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2250 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2251 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2252 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2253 sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2254 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2255 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2256 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2257 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2258 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2259 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2260 sm 0 (PHidden x) = PHidden (sm 0 x)
2261 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2262 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2263 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2264 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2265 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2266 sm ql x = descend (sm ql) x
2268-- | Rename any binders which are repeated (so that we don't have to mess
2269-- about with shadowing anywhere else).
2270mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2271mkUniqueNames env shadows tm
2272 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2274 initMap = M.fromList shadows
2276 inScope :: S.Set Name
2277 inScope = S.fromList $ boundNamesIn tm
2279 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2280 return (arg { getTm = t' })
2282 -- Initialise the unique name with the environment length (so we're not
2283 -- looking for too long...)
2284 initN (UN n) l = UN $ txt (str n ++ show l)
2285 initN (MN i s) l = MN (i+l) s
2288 -- FIXME: Probably ought to do this for completeness! It's fine as
2289 -- long as there are no bindings inside tactics though.
2290 mkUniqT _ nmap tac = return tac
2292 mkUniq :: Int -- ^ The number of quotations that we're under
2293 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2294 mkUniq 0 nmap (PLam fc n nfc ty sc)
2298 then do let n' = uniqueNameSet (initN n (S.size env))
2299 (S.union env inScope)
2300 return (n', sc) -- shadow n n' sc)
2302 put (S.insert n' env)
2303 let nmap' = M.insert n n' nmap
2304 ty' <- mkUniq 0 nmap ty
2305 sc'' <- mkUniq 0 nmap' sc'
2306 return $! PLam fc n' nfc ty' sc''
2307 mkUniq 0 nmap (PPi p n fc ty sc)
2311 then do let n' = uniqueNameSet (initN n (S.size env))
2312 (S.union env inScope)
2313 return (n', sc) -- shadow n n' sc)
2315 put (S.insert n' env)
2316 let nmap' = M.insert n n' nmap
2317 ty' <- mkUniq 0 nmap ty
2318 sc'' <- mkUniq 0 nmap' sc'
2319 return $! PPi p n' fc ty' sc''
2320 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2324 then do let n' = uniqueNameSet (initN n (S.size env))
2325 (S.union env inScope)
2326 return (n', sc) -- shadow n n' sc)
2328 put (S.insert n' env)
2329 let nmap' = M.insert n n' nmap
2330 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2331 sc'' <- mkUniq 0 nmap' sc'
2332 return $! PLet fc n' nfc ty' val' sc''
2333 mkUniq 0 nmap (PApp fc t args)
2334 = do t' <- mkUniq 0 nmap t
2335 args' <- mapM (mkUniqA 0 nmap) args
2336 return $! PApp fc t' args'
2337 mkUniq 0 nmap (PAppBind fc t args)
2338 = do t' <- mkUniq 0 nmap t
2339 args' <- mapM (mkUniqA 0 nmap) args
2340 return $! PAppBind fc t' args'
2341 mkUniq 0 nmap (PCase fc t alts)
2342 = do t' <- mkUniq 0 nmap t
2343 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2344 return (x', y')) alts
2345 return $! PCase fc t' alts'
2346 mkUniq 0 nmap (PIfThenElse fc c t f)
2347 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2348 mkUniq 0 nmap (PPair fc hls p l r)
2349 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2350 return $! PPair fc hls p l' r'
2351 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2354 (n', sc') <- if n `S.member` env
2355 then do let n' = uniqueNameSet n (S.union env inScope)
2356 return (n', sc) -- shadow n n' sc)
2358 put (S.insert n' env)
2359 let nmap' = M.insert n n' nmap
2360 t' <- mkUniq 0 nmap t
2361 sc'' <- mkUniq 0 nmap' sc'
2362 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2363 mkUniq 0 nmap (PDPair fc hls p l t r)
2364 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2365 return $! PDPair fc hls p l' t' r'
2366 mkUniq 0 nmap (PAlternative ns b as)
2367 -- store the nmap and defer the rest until we've pruned the set
2368 -- during elaboration
2369 = return $ PAlternative (M.toList nmap ++ ns) b as
2370 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2371 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2372 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2373 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2374 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2375 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2376 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2377 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2378 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2379 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2382 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2384 mkUniq ql nmap (PQuasiquote tm ty) =
2385 do tm' <- mkUniq (ql + 1) nmap tm
2387 Nothing -> return Nothing
2388 Just t -> fmap Just $ mkUniq ql nmap t
2389 return $! PQuasiquote tm' ty'
2390 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2392 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