2Module : Idris.AbsSyntax
3Description : Provides Idris' core data definitions and utility code.
6Maintainer : The Idris Community.
8{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
9 PatternGuards, TypeSynonymInstances #-}
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
13 , module Idris.AbsSyntaxTree
16import Idris.AbsSyntaxTree
18import Idris.Core.Elaborate hiding (Tactic(..))
19import Idris.Core.Evaluate
21import Idris.Core.Typecheck
22import Idris.Docstrings
23import Idris.IdeMode hiding (Opt(..))
24import IRTS.CodegenCommon
26import Util.DynamicLinker
31import Control.Applicative
32import Control.Monad (liftM3)
33import Control.Monad.State
36import Data.Generics.Uniplate.Data (descend, descendM)
37import Data.List hiding (insert, union)
38import qualified Data.Map as M
40import qualified Data.Set as S
41import qualified Data.Text as T
42import Data.Word (Word)
44import Network (PortID(PortNumber))
45import System.Console.Haskeline
46import System.Directory (canonicalizePath, doesFileExist)
48import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)
50getContext :: Idris Context
51getContext = do i <- getIState; return (tt_ctxt i)
53forCodegen :: Codegen -> [(Codegen, a)] -> [a]
54forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
56 eqLang (Via _ x) (Via _ y) = x == y
57 eqLang Bytecode Bytecode = True
60getObjectFiles :: Codegen -> Idris [FilePath]
61getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
63addObjectFile :: Codegen -> FilePath -> Idris ()
64addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
66getLibs :: Codegen -> Idris [String]
67getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
69addLib :: Codegen -> String -> Idris ()
70addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
72getFlags :: Codegen -> Idris [String]
73getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
75addFlag :: Codegen -> String -> Idris ()
76addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
78addDyLib :: [String] -> Idris (Either DynamicLib String)
79addDyLib libs = do i <- getIState
80 let ls = idris_dynamic_libs i
81 let importdirs = opt_importdirs (idris_options i)
82 case mapMaybe (findDyLib ls) libs of
83 x:_ -> return (Left x)
85 handle <- lift . lift .
86 mapM (\l -> catchIO (tryLoadLib importdirs l)
87 (\_ -> return Nothing)) $ libs
89 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
90 intercalate "," libs ++ "\"")
91 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
93 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
94 findDyLib [] l = Nothing
95 findDyLib (lib:libs) l | l == lib_name lib = Just lib
96 | otherwise = findDyLib libs l
98getAutoImports :: Idris [FilePath]
99getAutoImports = do i <- getIState
100 return (opt_autoImport (idris_options i))
102addAutoImport :: FilePath -> Idris ()
103addAutoImport fp = do i <- getIState
104 let opts = idris_options i
105 let autoimps = opt_autoImport opts
106 put (i { idris_options = opts { opt_autoImport =
107 fp : opt_autoImport opts } } )
109addDefinedName :: Name -> Idris ()
110addDefinedName n = do ist <- getIState
111 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
113getDefinedNames :: Idris [Name]
114getDefinedNames = do ist <- getIState
115 return (S.toList (idris_inmodule ist))
117addTT :: Term -> Idris (Maybe Term)
118addTT t = do ist <- getIState
119 case M.lookup t (idris_ttstats ist) of
120 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
121 putIState $ ist { idris_ttstats = tt' }
123 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
124 putIState $ ist { idris_ttstats = tt' }
128dumpTT = do ist <- get
129 let sts = sortBy count (M.toList (idris_ttstats ist))
133 count (_,x) (_,y) = compare y x
134 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
136addHdr :: Codegen -> String -> Idris ()
137addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
139addImported :: Bool -> FilePath -> Idris ()
142 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
144addLangExt :: LanguageExt -> Idris ()
145addLangExt TypeProviders = do i <- getIState
147 idris_language_extensions = TypeProviders : idris_language_extensions i
149addLangExt ErrorReflection = do i <- getIState
151 idris_language_extensions = ErrorReflection : idris_language_extensions i
154-- | Transforms are organised by the function being applied on the lhs
155-- of the transform, to make looking up appropriate transforms quicker
156addTrans :: Name -> (Term, Term) -> Idris ()
159 let t' = case lookupCtxtExact basefn (idris_transforms i) of
160 Just def -> (t : def)
162 putIState $ i { idris_transforms = addDef basefn t'
163 (idris_transforms i) }
165addErrRev :: (Term, Term) -> Idris ()
166addErrRev t = do i <- getIState
167 putIState $ i { idris_errRev = t : idris_errRev i }
169addErasureUsage :: Name -> Int -> Idris ()
170addErasureUsage n i = do ist <- getIState
171 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
173addExport :: Name -> Idris ()
174addExport n = do ist <- getIState
175 putIState $ ist { idris_exports = n : idris_exports ist }
177addUsedName :: FC -> Name -> Name -> Idris ()
179 = do ist <- getIState
180 case lookupTyName n (tt_ctxt ist) of
181 [(n', ty)] -> addUsage n' 0 ty
182 [] -> throwError (At fc (NoSuchVariable n))
183 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
184 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
186 | otherwise = addUsage n (i + 1) sc
187 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
189getErasureUsage :: Idris [(Name, Int)]
190getErasureUsage = do ist <- getIState;
191 return (idris_erasureUsed ist)
193getExports :: Idris [Name]
194getExports = do ist <- getIState
195 return (idris_exports ist)
197totcheck :: (FC, Name) -> Idris ()
198totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
200defer_totcheck :: (FC, Name) -> Idris ()
203 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
205clear_totcheck :: Idris ()
206clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
208setFlags :: Name -> [FnOpt] -> Idris ()
209setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
211addFnOpt :: Name -> FnOpt -> Idris ()
212addFnOpt n f = do i <- getIState
213 let fls = case lookupCtxtExact n (idris_flags i) of
218setFnInfo :: Name -> FnInfo -> Idris ()
219setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
221setAccessibility :: Name -> Accessibility -> Idris ()
224 let ctxt = setAccess n a (tt_ctxt i)
225 putIState $ i { tt_ctxt = ctxt }
227-- | get the accessibility of a name outside this module
228getFromHideList :: Name -> Idris (Maybe Accessibility)
229getFromHideList n = do i <- getIState
230 return $ lookupCtxtExact n (hide_list i)
232setTotality :: Name -> Totality -> Idris ()
235 let ctxt = setTotal n a (tt_ctxt i)
236 putIState $ i { tt_ctxt = ctxt }
238setInjectivity :: Name -> Injectivity -> Idris ()
241 let ctxt = setInjective n a (tt_ctxt i)
242 putIState $ i { tt_ctxt = ctxt }
244getTotality :: Name -> Idris Totality
247 case lookupTotal n (tt_ctxt i) of
249 _ -> return (Total [])
251-- Get coercions which might return the required type
252getCoercionsTo :: IState -> Type -> [Name]
254 let cs = idris_coercions i
255 (fn,_) = unApply (getRetTy ty) in
257 where findCoercions t [] = []
258 findCoercions t (n : ns) =
259 let ps = case lookupTy n (tt_ctxt i) of
260 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
261 (t', _) -> [n | t == t']
263 ps ++ findCoercions t ns
265addToCG :: Name -> CGInfo -> Idris ()
268 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
270addCalls :: Name -> [Name] -> Idris ()
273 case lookupCtxtExact n (idris_callgraph i) of
274 Nothing -> addToCG n (CGInfo calls [] [])
275 Just (CGInfo cs scg used) ->
276 addToCG n (CGInfo (nub (calls ++ cs)) scg used)
278addTyInferred :: Name -> Idris ()
281 putIState $ i { idris_tyinfodata =
282 addDef n TIPartial (idris_tyinfodata i) }
284addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
285addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
286 mapM_ addConstraint ts
288 where addConstraint (x, y) = findMVApps x y
291 = do let (fx, argsx) = unApply x
292 let (fy, argsy) = unApply y
297 else mapM_ addConstraint (zip argsx argsy)
299 tryAddMV (P _ mv _) y =
301 case lookup mv (idris_metavars ist) of
302 Just _ -> addConstraintRule mv y
304 tryAddMV _ _ = return ()
306 addConstraintRule :: Name -> Term -> Idris ()
307 addConstraintRule n t
309 logLvl 1 $ "TI constraint: " ++ show (n, t)
310 case lookupCtxt n (idris_tyinfodata ist) of
312 do mapM_ (checkConsistent t) ts
313 let ti' = addDef n (TISolution (t : ts))
314 (idris_tyinfodata ist)
315 put $ ist { idris_tyinfodata = ti' }
317 do let ti' = addDef n (TISolution [t])
318 (idris_tyinfodata ist)
319 put $ ist { idris_tyinfodata = ti' }
321 -- Check a solution is consistent with previous solutions
322 -- Meaning: If heads are both data types, they had better be the
324 checkConsistent :: Term -> Term -> Idris ()
325 checkConsistent x y =
326 do let (fx, _) = unApply x
327 let (fy, _) = unApply y
329 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
330 (P (TCon _ _) n _, Constant _) -> errWhen True
331 (Constant _, P (TCon _ _) n' _) -> errWhen True
332 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
337 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
338 errWhen False = return ()
340isTyInferred :: Name -> Idris Bool
343 case lookupCtxt n (idris_tyinfodata i) of
344 [TIPartial] -> return True
347-- | Adds error handlers for a particular function and argument. If
348-- names are ambiguous, all matching handlers are updated.
349addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
350addFunctionErrorHandlers f arg hs =
352 let oldHandlers = idris_function_errorhandlers i
353 let newHandlers = flip (addDef f) oldHandlers $
354 case lookupCtxtExact f oldHandlers of
355 Nothing -> M.singleton arg (S.fromList hs)
356 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
357 -- will always be one of those two, thus no extra case
358 putIState $ i { idris_function_errorhandlers = newHandlers }
360getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
361getFunctionErrorHandlers f arg = do i <- getIState
362 return . maybe [] S.toList $
363 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
366-- | Trace all the names in a call graph starting at the given name
367getAllNames :: Name -> Idris [Name]
368getAllNames n = allNames [] n
370allNames :: [Name] -> Name -> Idris [Name]
371allNames ns n | n `elem` ns = return []
372allNames ns n = do i <- getIState
373 case lookupCtxtExact n (idris_callgraph i) of
374 Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')
375 return (nub (n : concat more))
378addCoercion :: Name -> Idris ()
379addCoercion n = do i <- getIState
380 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
382addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
385 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
387addNameHint :: Name -> Name -> Idris ()
390 ty' <- case lookupCtxtName ty (idris_implicits i) of
391 [(tyn, _)] -> return tyn
392 [] -> throwError (NoSuchVariable ty)
393 tyns -> throwError (CantResolveAlts (map fst tyns))
394 let ns' = case lookupCtxt ty' (idris_namehints i) of
397 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
399getNameHints :: IState -> Name -> [Name]
400getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
402 case lookupCtxt n (idris_namehints i) of
406addDeprecated :: Name -> String -> Idris ()
407addDeprecated n reason = do
409 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
411getDeprecated :: Name -> Idris (Maybe String)
414 return $ lookupCtxtExact n (idris_deprecated i)
417addFragile :: Name -> String -> Idris ()
418addFragile n reason = do
420 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
422getFragile :: Name -> Idris (Maybe String)
425 return $ lookupCtxtExact n (idris_fragile i)
427push_estack :: Name -> Bool -> Idris ()
430 putIState (i { elab_stack = (n, impl) : elab_stack i })
432pop_estack :: Idris ()
433pop_estack = do i <- getIState
434 putIState (i { elab_stack = ptail (elab_stack i) })
438-- | Add an interface implementation function.
440-- Precondition: the implementation should have the correct type.
442-- Dodgy hack 1: Put integer implementations first in the list so they are
443-- resolved by default.
445-- Dodgy hack 2: put constraint chasers (ParentN) last
446addImplementation :: Bool -- ^ whether the name is an Integer implementation
447 -> Bool -- ^ whether to include the implementation in implementation search
448 -> Name -- ^ the name of the interface
449 -> Name -- ^ the name of the implementation
451addImplementation int res n i
452 = do ist <- getIState
453 case lookupCtxt n (idris_interfaces ist) of
454 [CI a b c d e f g ins fds] ->
455 do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
456 putIState $ ist { idris_interfaces = cs }
457 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
458 putIState $ ist { idris_interfaces = cs }
459 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
460 addI i ins | int = (i, res) : ins
461 | chaser n = ins ++ [(i, res)]
462 | otherwise = insI i ins
463 insI i [] = [(i, res)]
464 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
465 | otherwise = n : insI i ns
467 chaser (SN (ParentN _ _)) = True
468 chaser (NS n _) = chaser n
471-- | Add a privileged implementation - one which implementation search will
472-- happily resolve immediately if it is type correct This is used for
473-- naming parent implementations when defining an implementation with
474-- constraints. Returns the old list, so we can revert easily at the
476addOpenImpl :: [Name] -> Idris [Name]
477addOpenImpl ns = do ist <- getIState
478 ns' <- mapM (checkValid ist) ns
479 let open = idris_openimpls ist
480 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
484 = case lookupCtxtName n (idris_implicits ist) of
485 [(n', _)] -> return n'
486 [] -> throwError (NoSuchVariable n)
487 more -> throwError (CantResolveAlts (map fst more))
489setOpenImpl :: [Name] -> Idris ()
490setOpenImpl ns = do ist <- getIState
491 putIState $ ist { idris_openimpls = ns }
493getOpenImpl :: Idris [Name]
494getOpenImpl = do ist <- getIState
495 return (idris_openimpls ist)
497addInterface :: Name -> InterfaceInfo -> Idris ()
499 = do ist <- getIState
500 let i' = case lookupCtxt n (idris_interfaces ist) of
501 [c] -> c { interface_implementations = interface_implementations i }
503 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
505addRecord :: Name -> RecordInfo -> Idris ()
506addRecord n ri = do ist <- getIState
507 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
509addAutoHint :: Name -> Name -> Idris ()
512 case lookupCtxtExact n (idris_autohints ist) of
514 do let hs = addDef n [hint] (idris_autohints ist)
515 putIState $ ist { idris_autohints = hs }
517 do let hs = addDef n (hint : nhints) (idris_autohints ist)
518 putIState $ ist { idris_autohints = hs }
520getAutoHints :: Name -> Idris [Name]
521getAutoHints n = do ist <- getIState
522 case lookupCtxtExact n (idris_autohints ist) of
526addIBC :: IBCWrite -> Idris ()
529 when (notDef (ibc_write i)) $
530 putIState $ i { ibc_write = ibc : ibc_write i }
531 where notDef [] = True
532 notDef (IBCDef n': is) | n == n' = False
533 notDef (_ : is) = notDef is
534addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
537clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
538 idris_inmodule = S.empty }
540resetNameIdx :: Idris ()
541resetNameIdx = do i <- getIState
542 put (i { idris_nameIdx = (0, emptyContext) })
544-- | Used to preserve sharing of names
545addNameIdx :: Name -> Idris (Int, Name)
546addNameIdx n = do i <- getIState
547 let (i', x) = addNameIdx' i n
551addNameIdx' :: IState -> Name -> (IState, (Int, Name))
553 = let idxs = snd (idris_nameIdx i) in
554 case lookupCtxt n idxs of
556 _ -> let i' = fst (idris_nameIdx i) + 1 in
557 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
559getSymbol :: Name -> Idris Name
560getSymbol n = do i <- getIState
561 case M.lookup n (idris_symbols i) of
563 Nothing -> do let sym' = M.insert n n (idris_symbols i)
564 put (i { idris_symbols = sym' })
567getHdrs :: Codegen -> Idris [String]
568getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
570getImported :: Idris [(FilePath, Bool)]
571getImported = do i <- getIState; return (idris_imported i)
573setErrSpan :: FC -> Idris ()
574setErrSpan x = do i <- getIState;
576 Nothing -> putIState $ i { errSpan = Just x }
580clearErr = do i <- getIState
581 putIState $ i { errSpan = Nothing }
583getSO :: Idris (Maybe String)
584getSO = do i <- getIState
585 return (compiled_so i)
587setSO :: Maybe String -> Idris ()
588setSO s = do i <- getIState
589 putIState (i { compiled_so = s })
591getIState :: Idris IState
594putIState :: IState -> Idris ()
597updateIState :: (IState -> IState) -> Idris ()
598updateIState f = do i <- getIState
601withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
602withContext ctx name dflt action = do
604 case lookupCtxt name (ctx ist) of
608withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
609withContext_ ctx name action = withContext ctx name () action
611-- | A version of liftIO that puts errors into the exception type of
613runIO :: IO a -> Idris a
614runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
615-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
617-- Issue #1738 on the issue tracker.
618-- https://github.com/idris-lang/Idris-dev/issues/1738
621getName = do i <- getIState;
622 let idx = idris_name i;
623 putIState (i { idris_name = idx + 1 })
626-- | InternalApp keeps track of the real function application for
627-- making case splits from, not the application the programmer wrote,
628-- which doesn't have the whole context in any case other than top
630addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
633 -- We canonicalise the path to make "./Test/Module.idr" equal
634 -- to "Test/Module.idr"
635 exists <- runIO $ doesFileExist fp
637 do fp' <- runIO $ canonicalizePath fp
638 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
640getInternalApp :: FilePath -> Int -> Idris PTerm
641getInternalApp fp l = do i <- getIState
642 -- We canonicalise the path to make
643 -- "./Test/Module.idr" equal to
645 exists <- runIO $ doesFileExist fp
647 then do fp' <- runIO $ canonicalizePath fp
648 case lookup (fp', l) (idris_lineapps i) of
650 Nothing -> return Placeholder
651 -- TODO: What if it's not there?
652 else return Placeholder
654-- | Pattern definitions are only used for coverage checking, so erase
655-- them when we're done
656clearOrigPats :: Idris ()
657clearOrigPats = do i <- get
658 let ps = idris_patdefs i
659 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
660 put (i { idris_patdefs = ps' })
662-- | Erase types from Ps in the context (basically ending up with
663-- what's in the .ibc, which is all we need after all the analysis is
665clearPTypes :: Idris ()
666clearPTypes = do i <- get
668 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
669 where pErase (CaseOp c t tys orig tot cds)
670 = CaseOp c t tys orig [] (pErase' cds)
672 pErase' (CaseDefs (cs, c) rs)
673 = let c' = (cs, fmap pEraseType c) in
676checkUndefined :: FC -> Name -> Idris ()
680 (_:_) -> throwError . Msg $ show fc ++ ":" ++
681 show n ++ " already defined"
684isUndefined :: FC -> Name -> Idris Bool
687 case lookupTyExact n i of
688 Just _ -> return False
691setContext :: Context -> Idris ()
692setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
694updateContext :: (Context -> Context) -> Idris ()
695updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
697addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
698addConstraints fc (v, cs)
699 = do tit <- typeInType
703 let ctxt' = ctxt { next_tvar = v }
704 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
705 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
708 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
709 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
710 insertAll ((c, fc) : cs) ics
711 = insertAll cs $ S.insert (ConstraintFC c fc) ics
713addDeferred = addDeferred' Ref
714addDeferredTyCon = addDeferred' (TCon 0 0)
716-- | Save information about a name that is not yet defined
717addDeferred' :: NameType
718 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
719 -- ^ The Name is the name being made into a metavar,
720 -- the Int is the number of vars that are part of a
721 -- putative proof context, the Maybe Name is the
722 -- top-level function containing the new metavariable,
723 -- the Type is its type, and the Bool is whether :p is
727 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
728 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
730 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
731 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
734 -- 'tidyNames' is to generate user accessible names in case they are
735 -- needed in tactic scripts
736 tidyNames used (Bind (MN i x) b sc)
737 = let n' = uniqueNameSet (UN x) used in
738 Bind n' b $ tidyNames (S.insert n' used) sc
739 tidyNames used (Bind n b sc)
740 = let n' = uniqueNameSet n used in
741 Bind n' b $ tidyNames (S.insert n' used) sc
744solveDeferred :: FC -> Name -> Idris ()
747 case lookup n (idris_metavars i) of
748 Just (_, _, _, _, False) ->
749 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
750 _ -> putIState $ i { idris_metavars =
751 filter (\(n', _) -> n/=n')
754 filter (notMV n) (ibc_write i)
756 where notMV n (IBCMetavar n') = not (n == n')
759getUndefined :: Idris [Name]
760getUndefined = do i <- getIState
761 return (map fst (idris_metavars i) \\ primDefs)
763isMetavarName :: Name -> IState -> Bool
765 = case lookupNames n (tt_ctxt ist) of
766 (t:_) -> isJust $ lookup t (idris_metavars ist)
769getWidth :: Idris ConsoleWidth
770getWidth = fmap idris_consolewidth getIState
772setWidth :: ConsoleWidth -> Idris ()
773setWidth w = do ist <- getIState
774 put ist { idris_consolewidth = w }
776setDepth :: Maybe Int -> Idris ()
777setDepth d = do ist <- getIState
778 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
780typeDescription :: String
781typeDescription = "The type of types"
784type1Doc :: Doc OutputAnnotation
785type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
788isetPrompt :: String -> Idris ()
789isetPrompt p = do i <- getIState
790 case idris_outputmode i of
791 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
793-- | Tell clients how much was parsed and loaded
794isetLoadedRegion :: Idris ()
795isetLoadedRegion = do i <- getIState
796 let span = idris_parsedSpan i
799 case idris_outputmode i of
801 runIO . hPutStrLn h $
802 convSExp "set-loaded-region" fc n
805setLogLevel :: Int -> Idris ()
806setLogLevel l = do i <- getIState
807 let opts = idris_options i
808 let opt' = opts { opt_logLevel = l }
809 putIState $ i { idris_options = opt' }
811setLogCats :: [LogCat] -> Idris ()
814 let opts = idris_options i
815 let opt' = opts { opt_logcats = cs }
816 putIState $ i { idris_options = opt' }
818setCmdLine :: [Opt] -> Idris ()
819setCmdLine opts = do i <- getIState
820 let iopts = idris_options i
821 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
823getCmdLine :: Idris [Opt]
824getCmdLine = do i <- getIState
825 return (opt_cmdline (idris_options i))
827getDumpHighlighting :: Idris Bool
828getDumpHighlighting = do ist <- getIState
829 return (findC (opt_cmdline (idris_options ist)))
830 where findC = elem DumpHighlights
832getDumpDefun :: Idris (Maybe FilePath)
833getDumpDefun = do i <- getIState
834 return $ findC (opt_cmdline (idris_options i))
835 where findC [] = Nothing
836 findC (DumpDefun x : _) = Just x
837 findC (_ : xs) = findC xs
839getDumpCases :: Idris (Maybe FilePath)
840getDumpCases = do i <- getIState
841 return $ findC (opt_cmdline (idris_options i))
842 where findC [] = Nothing
843 findC (DumpCases x : _) = Just x
844 findC (_ : xs) = findC xs
847logLevel = do i <- getIState
848 return (opt_logLevel (idris_options i))
850setAutoImpls :: Bool -> Idris ()
851setAutoImpls b = do i <- getIState
852 let opts = idris_options i
853 let opt' = opts { opt_autoimpls = b }
854 putIState $ i { idris_options = opt' }
856getAutoImpls :: Idris Bool
857getAutoImpls = do i <- getIState
858 return (opt_autoimpls (idris_options i))
860setErrContext :: Bool -> Idris ()
861setErrContext t = do i <- getIState
862 let opts = idris_options i
863 let opts' = opts { opt_errContext = t }
864 putIState $ i { idris_options = opts' }
866errContext :: Idris Bool
867errContext = do i <- getIState
868 return (opt_errContext (idris_options i))
870getOptimise :: Idris [Optimisation]
871getOptimise = do i <- getIState
872 return (opt_optimise (idris_options i))
874setOptimise :: [Optimisation] -> Idris ()
875setOptimise newopts = do i <- getIState
876 let opts = idris_options i
877 let opts' = opts { opt_optimise = newopts }
878 putIState $ i { idris_options = opts' }
880addOptimise :: Optimisation -> Idris ()
881addOptimise opt = do opts <- getOptimise
882 setOptimise (nub (opt : opts))
884removeOptimise :: Optimisation -> Idris ()
885removeOptimise opt = do opts <- getOptimise
886 setOptimise ((nub opts) \\ [opt])
888-- | Set appropriate optimisation set for the given level. We only
889-- have one optimisation that is configurable at the moment, however!
890setOptLevel :: Int -> Idris ()
891setOptLevel n | n <= 0 = setOptimise []
892setOptLevel 1 = setOptimise []
893setOptLevel 2 = setOptimise [PETransform]
894setOptLevel n | n >= 3 = setOptimise [PETransform]
897useREPL = do i <- getIState
898 return (opt_repl (idris_options i))
900setREPL :: Bool -> Idris ()
901setREPL t = do i <- getIState
902 let opts = idris_options i
903 let opt' = opts { opt_repl = t }
904 putIState $ i { idris_options = opt' }
906showOrigErr :: Idris Bool
907showOrigErr = do i <- getIState
908 return (opt_origerr (idris_options i))
910setShowOrigErr :: Bool -> Idris ()
911setShowOrigErr b = do i <- getIState
912 let opts = idris_options i
913 let opt' = opts { opt_origerr = b }
914 putIState $ i { idris_options = opt' }
916setAutoSolve :: Bool -> Idris ()
917setAutoSolve b = do i <- getIState
918 let opts = idris_options i
919 let opt' = opts { opt_autoSolve = b }
920 putIState $ i { idris_options = opt' }
922setNoBanner :: Bool -> Idris ()
923setNoBanner n = do i <- getIState
924 let opts = idris_options i
925 let opt' = opts { opt_nobanner = n }
926 putIState $ i { idris_options = opt' }
928getNoBanner :: Idris Bool
929getNoBanner = do i <- getIState
930 let opts = idris_options i
931 return (opt_nobanner opts)
933setEvalTypes :: Bool -> Idris ()
934setEvalTypes n = do i <- getIState
935 let opts = idris_options i
936 let opt' = opts { opt_evaltypes = n }
937 putIState $ i { idris_options = opt' }
939getDesugarNats :: Idris Bool
940getDesugarNats = do i <- getIState
941 let opts = idris_options i
942 return (opt_desugarnats opts)
945setDesugarNats :: Bool -> Idris ()
946setDesugarNats n = do i <- getIState
947 let opts = idris_options i
948 let opt' = opts { opt_desugarnats = n }
949 putIState $ i { idris_options = opt' }
951setQuiet :: Bool -> Idris ()
952setQuiet q = do i <- getIState
953 let opts = idris_options i
954 let opt' = opts { opt_quiet = q }
955 putIState $ i { idris_options = opt' }
957getQuiet :: Idris Bool
958getQuiet = do i <- getIState
959 let opts = idris_options i
960 return (opt_quiet opts)
962setCodegen :: Codegen -> Idris ()
963setCodegen t = do i <- getIState
964 let opts = idris_options i
965 let opt' = opts { opt_codegen = t }
966 putIState $ i { idris_options = opt' }
968codegen :: Idris Codegen
969codegen = do i <- getIState
970 return (opt_codegen (idris_options i))
973setOutputTy :: OutputType -> Idris ()
974setOutputTy t = do i <- getIState
975 let opts = idris_options i
976 let opt' = opts { opt_outputTy = t }
977 putIState $ i { idris_options = opt' }
979outputTy :: Idris OutputType
980outputTy = do i <- getIState
981 return $ opt_outputTy $ idris_options i
983setIdeMode :: Bool -> Handle -> Idris ()
984setIdeMode True h = do i <- getIState
985 putIState $ i { idris_outputmode = IdeMode 0 h
986 , idris_colourRepl = False
988setIdeMode False _ = return ()
990setTargetTriple :: String -> Idris ()
991setTargetTriple t = do i <- getIState
992 let opts = idris_options i
993 opt' = opts { opt_triple = t }
994 putIState $ i { idris_options = opt' }
996targetTriple :: Idris String
997targetTriple = do i <- getIState
998 return (opt_triple (idris_options i))
1000setTargetCPU :: String -> Idris ()
1001setTargetCPU t = do i <- getIState
1002 let opts = idris_options i
1003 opt' = opts { opt_cpu = t }
1004 putIState $ i { idris_options = opt' }
1006targetCPU :: Idris String
1007targetCPU = do i <- getIState
1008 return (opt_cpu (idris_options i))
1010verbose :: Idris Bool
1011verbose = do i <- getIState
1012 -- Quietness overrides verbosity
1013 return (not (opt_quiet (idris_options i)) &&
1014 opt_verbose (idris_options i))
1016setVerbose :: Bool -> Idris ()
1017setVerbose t = do i <- getIState
1018 let opts = idris_options i
1019 let opt' = opts { opt_verbose = t }
1020 putIState $ i { idris_options = opt' }
1022typeInType :: Idris Bool
1023typeInType = do i <- getIState
1024 return (opt_typeintype (idris_options i))
1026setTypeInType :: Bool -> Idris ()
1027setTypeInType t = do i <- getIState
1028 let opts = idris_options i
1029 let opt' = opts { opt_typeintype = t }
1030 putIState $ i { idris_options = opt' }
1032coverage :: Idris Bool
1033coverage = do i <- getIState
1034 return (opt_coverage (idris_options i))
1036setCoverage :: Bool -> Idris ()
1037setCoverage t = do i <- getIState
1038 let opts = idris_options i
1039 let opt' = opts { opt_coverage = t }
1040 putIState $ i { idris_options = opt' }
1042setIBCSubDir :: FilePath -> Idris ()
1043setIBCSubDir fp = do i <- getIState
1044 let opts = idris_options i
1045 let opt' = opts { opt_ibcsubdir = fp }
1046 putIState $ i { idris_options = opt' }
1048valIBCSubDir :: IState -> Idris FilePath
1049valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1051addImportDir :: FilePath -> Idris ()
1052addImportDir fp = do i <- getIState
1053 let opts = idris_options i
1054 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1055 putIState $ i { idris_options = opt' }
1057setImportDirs :: [FilePath] -> Idris ()
1058setImportDirs fps = do i <- getIState
1059 let opts = idris_options i
1060 let opt' = opts { opt_importdirs = fps }
1061 putIState $ i { idris_options = opt' }
1063allImportDirs :: Idris [FilePath]
1064allImportDirs = do i <- getIState
1065 let optdirs = opt_importdirs (idris_options i)
1066 return ("." : reverse optdirs)
1068addSourceDir :: FilePath -> Idris ()
1069addSourceDir fp = do i <- getIState
1070 let opts = idris_options i
1071 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1072 putIState $ i { idris_options = opts' }
1074setSourceDirs :: [FilePath] -> Idris ()
1075setSourceDirs fps = do i <- getIState
1076 let opts = idris_options i
1077 let opts' = opts { opt_sourcedirs = nub $ fps }
1078 putIState $ i { idris_options = opts' }
1080allSourceDirs :: Idris [FilePath]
1081allSourceDirs = do i <- getIState
1082 let optdirs = opt_sourcedirs (idris_options i)
1083 return ("." : reverse optdirs)
1085colourise :: Idris Bool
1086colourise = do i <- getIState
1087 return $ idris_colourRepl i
1089setColourise :: Bool -> Idris ()
1090setColourise b = do i <- getIState
1091 putIState $ i { idris_colourRepl = b }
1093impShow :: Idris Bool
1094impShow = do i <- getIState
1095 return (opt_showimp (idris_options i))
1097setImpShow :: Bool -> Idris ()
1098setImpShow t = do i <- getIState
1099 let opts = idris_options i
1100 let opt' = opts { opt_showimp = t }
1101 putIState $ i { idris_options = opt' }
1103setColour :: ColourType -> IdrisColour -> Idris ()
1104setColour ct c = do i <- getIState
1105 let newTheme = setColour' ct c (idris_colourTheme i)
1106 putIState $ i { idris_colourTheme = newTheme }
1107 where setColour' KeywordColour c t = t { keywordColour = c }
1108 setColour' BoundVarColour c t = t { boundVarColour = c }
1109 setColour' ImplicitColour c t = t { implicitColour = c }
1110 setColour' FunctionColour c t = t { functionColour = c }
1111 setColour' TypeColour c t = t { typeColour = c }
1112 setColour' DataColour c t = t { dataColour = c }
1113 setColour' PromptColour c t = t { promptColour = c }
1114 setColour' PostulateColour c t = t { postulateColour = c }
1117logLvl :: Int -> String -> Idris ()
1118logLvl = logLvlCats []
1120logCoverage :: Int -> String -> Idris ()
1121logCoverage = logLvlCats [ICoverage]
1123logErasure :: Int -> String -> Idris ()
1124logErasure = logLvlCats [IErasure]
1126-- | Log an action of the parser
1127logParser :: Int -> String -> Idris ()
1128logParser = logLvlCats parserCats
1130-- | Log an action of the elaborator.
1131logElab :: Int -> String -> Idris ()
1132logElab = logLvlCats elabCats
1134-- | Log an action of the compiler.
1135logCodeGen :: Int -> String -> Idris ()
1136logCodeGen = logLvlCats codegenCats
1138logIBC :: Int -> String -> Idris ()
1139logIBC = logLvlCats [IIBC]
1141-- | Log aspect of Idris execution
1143-- An empty set of logging levels is used to denote all categories.
1145-- @TODO update IDE protocol
1146logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1147 -> Int -- ^ The Logging level the message should appear.
1148 -> String -- ^ The message to show the developer.
1150logLvlCats cs l str = do
1152 let lvl = opt_logLevel (idris_options i)
1153 let cats = opt_logcats (idris_options i)
1155 when (inCat cs cats || null cats) $
1156 case idris_outputmode i of
1158 runIO $ hPutStrLn h str
1160 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1161 runIO . hPutStrLn h $ convSExp "log" good n
1163 inCat :: [LogCat] -> [LogCat] -> Bool
1164 inCat cs cats = any (`elem` cats) cs
1166cmdOptType :: Opt -> Idris Bool
1167cmdOptType x = do i <- getIState
1168 return $ x `elem` opt_cmdline (idris_options i)
1170noErrors :: Idris Bool
1171noErrors = do i <- getIState
1173 Nothing -> return True
1176setTypeCase :: Bool -> Idris ()
1177setTypeCase t = do i <- getIState
1178 let opts = idris_options i
1179 let opt' = opts { opt_typecase = t }
1180 putIState $ i { idris_options = opt' }
1183-- Dealing with parameters
1185expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1186 [Name] -> -- all names
1187 [Name] -> -- names with no declaration
1189expandParams dec ps ns infs tm = en 0 tm
1191 -- if we shadow a name (say in a lambda binding) that is used in a call to
1192 -- a lifted function, we need access to both names - once in the scope of the
1193 -- binding and once to call the lifted functions. So we'll explicitly shadow
1194 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1195 -- but we didn't...)
1197 mkShadow (UN n) = MN 0 n
1198 mkShadow (MN i n) = MN (i+1) n
1199 mkShadow (NS x s) = NS (mkShadow x) s
1201 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1202 -- that are merely mentioned.
1204 en 0 (PLam fc n nfc t s)
1205 | n `elem` (map fst ps ++ ns)
1206 = let n' = mkShadow n in
1207 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1208 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1209 en 0 (PPi p n nfc t s)
1210 | n `elem` (map fst ps ++ ns)
1211 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1212 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1213 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1214 en 0 (PLet fc n nfc ty v s)
1215 | n `elem` (map fst ps ++ ns)
1216 = let n' = mkShadow n in
1217 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1218 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1219 -- FIXME: Should only do this in a type signature!
1220 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1221 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1222 = let n' = mkShadow n in
1223 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1224 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1225 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1226 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1227 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1228 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1229 en 0 (PHidden t) = PHidden (en 0 t)
1230 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1231 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1232 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1233 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1234 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1235 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1237 en 0 (PQuote (Var n))
1238 | n `nselem` ns = PQuote (Var (dec n))
1239 en 0 (PApp fc (PInferRef fc' hl n) as)
1240 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1241 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1242 en 0 (PApp fc (PRef fc' hl n) as)
1243 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1244 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1245 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1246 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1247 en 0 (PAppBind fc (PRef fc' hl n) as)
1248 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1249 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1250 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1251 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1253 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1254 (map ((pexp . (PRef fc hl)) . fst) ps)
1255 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1256 (map ((pexp . (PRef fc hl)) . fst) ps)
1257 en 0 (PInferRef fc hl n)
1258 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1259 (map ((pexp . (PRef fc hl)) . fst) ps)
1260 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1261 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1262 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1263 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1264 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1265 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1267 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1268 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1270 en ql t = descend (en ql) t
1273 nselem x (y : xs) | nseq x y = True
1274 | otherwise = nselem x xs
1276 nseq x y = nsroot x == nsroot y
1278 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1279 enTacImp ql other = other
1281expandParamsD :: Bool -> -- True = RHS only
1283 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1284expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1285 = if n `elem` ns && (not rhsonly)
1286 then -- trace (show (n, expandParams dec ps ns ty)) $
1287 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1288 else --trace (show (n, expandParams dec ps ns ty)) $
1289 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1290expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1291 = if n `elem` ns && (not rhsonly)
1292 then -- trace (show (n, expandParams dec ps ns ty)) $
1293 PPostulate e doc syn fc nfc o (dec n)
1294 (piBind ps (expandParams dec ps ns [] ty))
1295 else --trace (show (n, expandParams dec ps ns ty)) $
1296 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1297expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1298 = let n' = if n `elem` ns then dec n else n in
1299 PClauses fc opts n' (map expandParamsC cs)
1301 expandParamsC (PClause fc n lhs ws rhs ds)
1302 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1303 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1304 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1305 n' = if n `elem` ns then dec n else n
1306 -- names bound on the lhs should not be expanded on the rhs
1307 ns' = removeBound lhs ns in
1309 (map (expandParams dec ps'' ns' []) ws)
1310 (expandParams dec ps'' ns' [] rhs)
1311 (map (expandParamsD True ist dec ps'' ns') ds)
1312 expandParamsC (PWith fc n lhs ws wval pn ds)
1313 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1314 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1315 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1316 n' = if n `elem` ns then dec n else n
1317 ns' = removeBound lhs ns in
1319 (map (expandParams dec ps'' ns' []) ws)
1320 (expandParams dec ps'' ns' [] wval)
1322 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1323 updateps yn nm [] = []
1324 updateps yn nm (((a, t), i):as)
1325 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1326 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1328 removeBound lhs ns = ns \\ nub (bnames lhs)
1330 bnames (PRef _ _ n) = [n]
1331 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1332 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1333 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1336-- | Expands parameters defined in parameter and where blocks inside of declarations
1337expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1338 = PData doc argDocs syn fc co (expandPData pd)
1340 -- just do the type decl, leave constructors alone (parameters will be
1341 -- added implicitly)
1342 expandPData (PDatadecl n nfc ty cons)
1344 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1346 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1347 econ (doc, argDocs, n, nfc, t, fc, fs)
1348 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1349expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1351expandParamsD rhs ist dec ps ns (PParams f params pds)
1352 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1353 (map (expandParamsD True ist dec ps ns) pds)
1354-- (map (expandParamsD ist dec ps ns) pds)
1355expandParamsD rhs ist dec ps ns (PMutual f pds)
1356 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1357expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1358 = PInterface doc info f
1359 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1361 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1364 (map (expandParamsD rhs ist dec ps ns) decls)
1367expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1368 = let cn' = case cn of
1369 Just n -> if n `elem` ns then Just (dec n) else Just n
1370 Nothing -> Nothing in
1371 PImplementation doc argDocs info f
1372 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1375 (map (expandParams dec ps ns []) params)
1376 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1377 (expandParams dec ps ns [] ty)
1379 (map (expandParamsD True ist dec ps ns) decls)
1380expandParamsD rhs ist dec ps ns d = d
1382mapsnd f (x, t) = (x, f t)
1384expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1385 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1387expandImplementationScope ist dec ps ns d = d
1389-- | Calculate a priority for a type, for deciding elaboration order
1390-- * if it's just a type variable or concrete type, do it early (0)
1391-- * if there's only type variables and injective constructors, do it next (1)
1392-- * if there's a function type, next (2)
1393-- * finally, everything else (3)
1394getPriority :: IState -> PTerm -> Int
1395getPriority i tm = 1 -- pri tm
1398 case lookupP n (tt_ctxt i) of
1399 ((P (DCon _ _ _) _ _):_) -> 1
1400 ((P (TCon _ _) _ _):_) -> 1
1401 ((P Ref _ _):_) -> 1
1402 [] -> 0 -- must be locally bound, if it's not an error...
1403 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1405 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1406 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1407 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1408 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1409 pri (PTyped l r) = pri l
1410 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1411 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1412 pri (PAlternative _ a as) = maximum (map pri as)
1413 pri (PConstant _ _) = 0
1418addStatics :: Name -> Term -> PTerm -> Idris ()
1419addStatics n tm ptm =
1420 do let (statics, dynamics) = initStatics tm ptm
1423 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1424 Just p -> getNamesFrom 0 (fn_params p) tm ++
1425 concatMap (getParamNames ist . snd) statics
1426 _ -> concatMap (getParamNames ist . snd) statics
1428 let stnames = nub $ concatMap (freeArgNames . snd) statics
1429 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1431 -- also get the arguments which are 'uniquely inferrable' from
1432 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1433 -- or parameters to the type of a static
1434 let statics' = nub $ map fst statics ++
1435 filter (\x -> not (elem x dnames)) stnames
1436 let stpos = staticList statics' tm
1438 unless (null statics) $
1439 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1440 ++ showTmImpls ptm ++ "\n"
1441 ++ show statics ++ "\n" ++ show dynamics
1442 ++ "\n" ++ show paramnames
1443 ++ "\n" ++ show stpos
1444 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1445 addIBC (IBCStatic n)
1447 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1448 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1449 (static, (n, ty) : dynamic)
1450 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1451 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1452 if pstatic p == Static then ((n, ty) : static, dynamic)
1453 else if (not (searchArg p))
1454 then (static, (n, ty) : dynamic)
1455 else (static, dynamic)
1456 initStatics t pt = ([], [])
1458 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1459 = case lookupCtxtExact n (idris_datatypes ist) of
1460 Just ti -> getNamePos 0 (param_pos ti) args
1462 where getNamePos i ps [] = []
1463 getNamePos i ps (P _ n _ : as)
1464 | i `elem` ps = n : getNamePos (i + 1) ps as
1465 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1466 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1467 = n : getParamNames ist sc
1468 getParamNames ist _ = []
1470 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1471 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1472 | otherwise = getNamesFrom (i + 1) ps sc
1473 getNamesFrom i ps sc = []
1475 freeArgNames (Bind n (Pi _ ty _) sc)
1476 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1477 freeArgNames tm = let (_, args) = unApply tm in
1478 concatMap freeNames args
1480 -- if a name appears in an interface or tactic implicit index, it doesn't
1481 -- affect its 'uniquely inferrable' from a static status since these are
1482 -- resolved by searching.
1483 searchArg (Constraint _ _) = True
1484 searchArg (TacImp _ _ _) = True
1487 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1490-- Dealing with implicit arguments
1492-- Add some bound implicits to the using block if they aren't there already
1494addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1495addToUsing us [] = us
1496addToUsing us ((n, t) : ns)
1497 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1498 | otherwise = addToUsing us ns
1499 where impName (UImplicit n _) = Just n
1502-- Add constraint bindings from using block
1504addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1505addUsingConstraints syn fc t
1507 let ns = namesIn [] ist t
1508 let cs = getConstraints t -- check declared constraints
1509 let addconsts = uconsts \\ cs
1510 return (doAdd addconsts ns t)
1511 where uconsts = filter uconst (using syn)
1512 uconst (UConstraint _ _) = True
1516 -- if all of args in ns, then add it
1517 doAdd (UConstraint c args : cs) ns t
1518 | all (\n -> elem n ns) args
1519 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1520 (mkConst c args) (doAdd cs ns t)
1521 | otherwise = doAdd cs ns t
1523 mkConst c args = PApp fc (PRef fc [] c)
1524 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1526 getConstraints (PPi (Constraint _ _) _ _ c sc)
1527 = getcapp c ++ getConstraints sc
1528 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1529 getConstraints _ = []
1531 getcapp (PApp _ (PRef _ _ c) args)
1532 = do ns <- mapM getName args
1533 return (UConstraint c ns)
1536 getName (PExp _ _ _ (PRef _ _ n)) = return n
1539-- | Add implicit bindings from using block, and bind any missing names
1540addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1541addUsingImpls syn n fc t
1542 = do ist <- getIState
1543 autoimpl <- getAutoImpls
1544 let ns_in = implicitNamesIn (map iname uimpls) ist t
1545 let ns = if autoimpl then ns_in
1546 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1548 let badnames = filter (\n -> not (implicitable n) &&
1549 n `notElem` (map iname uimpls)) ns
1550 unless (null badnames) $
1551 throwError (At fc (Elaborating "type of " n Nothing
1552 (NoSuchVariable (head badnames))))
1553 let cs = getArgnames t -- get already bound names
1554 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1555 -- if all names in the arguments of addconsts appear in ns,
1556 -- add the constraint implicitly
1557 return (bindFree ns (doAdd addimpls ns t))
1558 where uimpls = filter uimpl (using syn)
1559 uimpl (UImplicit _ _) = True
1562 iname (UImplicit n _) = n
1563 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1566 -- if all of args in ns, then add it
1567 doAdd (UImplicit n ty : cs) ns t
1569 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1570 | otherwise = doAdd cs ns t
1572 -- bind the free names which weren't in the using block
1575 | elem n (map iname uimpls) = bindFree ns tm
1577 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1579 getArgnames (PPi _ n _ c sc)
1580 = n : getArgnames sc
1583-- Given the original type and the elaborated type, return the implicitness
1584-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1586getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1587getUnboundImplicits i t tm = getImps t (collectImps tm)
1588 where collectImps (PPi p n _ t sc)
1589 = (n, (p, t)) : collectImps sc
1592 scopedimpl (Just i) = not (toplevel_imp i)
1593 scopedimpl _ = False
1595 getImps (Bind n (Pi i _ _) sc) imps
1596 | scopedimpl i = getImps sc imps
1597 getImps (Bind n (Pi _ t _) sc) imps
1598 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1600 argInfo n (Imp opt _ _ _ _) Placeholder
1601 = (True, PImp 0 True opt n Placeholder)
1602 argInfo n (Imp opt _ _ _ _) t'
1603 = (False, PImp (getPriority i t') True opt n t')
1604 argInfo n (Exp opt _ _) t'
1605 = (InaccessibleArg `elem` opt,
1606 PExp (getPriority i t') opt n t')
1607 argInfo n (Constraint opt _) t'
1608 = (InaccessibleArg `elem` opt,
1609 PConstraint 10 opt n t')
1610 argInfo n (TacImp opt _ scr) t'
1611 = (InaccessibleArg `elem` opt,
1612 PTacImplicit 10 opt n scr t')
1613 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1614 where impBind n t = (True, PImp 1 True [] n Placeholder)
1617-- Add implicit Pi bindings for any names in the term which appear in an
1618-- argument position.
1620-- This has become a right mess already. Better redo it some time...
1621-- TODO: This is obsoleted by the new way of elaborating types, (which
1622-- calls addUsingImpls) but there's still a couple of places which use
1623-- it. Clean them up!
1625-- Issue 1739 in the issue tracker
1626-- https://github.com/idris-lang/Idris-dev/issues/1739
1627implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1628implicit info syn n ptm = implicit' info syn [] n ptm
1630implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1631implicit' info syn ignore n ptm
1633 auto <- getAutoImpls
1634 let (tm', impdata) = implicitise auto syn ignore i ptm
1635 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1636-- let (tm'', spos) = findStatics i tm'
1637 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1639 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1641-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1644 -- Detect unknown names in default arguments and throw error if found.
1645 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1646 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1648 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1649 notFoundInDefault kns (PTacImplicit _ _ n script _)
1651 case notFound kns (namesIn [] i script) of
1652 Nothing -> return (n:kns)
1653 Just name -> throwError (NoSuchVariable name)
1654 notFoundInDefault kns p = return ((pname p):kns)
1656 notFound :: [Name] -> [Name] -> Maybe Name
1657 notFound kns [] = Nothing
1658 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1659 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1661-- | Even if auto_implicits is off, we need to call this so we record
1662-- which arguments are implicit
1663implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1664implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1665 let (declimps, ns') = execState (imps True [] tm) ([], [])
1666 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1667 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1668 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1670 then (tm, reverse declimps)
1671 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1673 uvars = map ipair (filter uimplicit (using syn))
1674 pvars = syn_params syn
1676 inUsing n = n `elem` map fst uvars
1678 ipair (UImplicit x y) = (x, y)
1679 uimplicit (UImplicit _ _) = True
1682 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1683 | otherwise = x : dropAll xs ys
1686 -- Find names in argument position in a type, suitable for implicit
1688 -- Not the function position, but do everything else...
1689 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1690 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1692 imps top env ty@(PApp _ f as)
1693 = do (decls, ns) <- get
1694 let isn = nub (implNamesIn uvars ty)
1695 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1696 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1697 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1699 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1700 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1701 imps True (n:env) sc
1702 imps top env (PPi (Exp l _ _) n _ ty sc)
1703 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1704 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1706 (decls, ns) <- get -- ignore decls in HO types
1707 put (PExp (getPriority ist ty) l n Placeholder : decls,
1708 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1709 imps True (n:env) sc
1710 imps top env (PPi (Constraint l _) n _ ty sc)
1711 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1712 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1714 (decls, ns) <- get -- ignore decls in HO types
1715 put (PConstraint 10 l n Placeholder : decls,
1716 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1717 imps True (n:env) sc
1718 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1719 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1720 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1722 (decls, ns) <- get -- ignore decls in HO types
1723 put (PTacImplicit 10 l n scr Placeholder : decls,
1724 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1725 imps True (n:env) sc
1726 imps top env (PRewrite _ _ l r _)
1727 = do (decls, ns) <- get
1728 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1729 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1730 imps top env (PTyped l r)
1732 imps top env (PPair _ _ _ l r)
1733 = do (decls, ns) <- get
1734 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1735 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1736 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1737 = do (decls, ns) <- get
1738 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1739 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1740 imps top env (PDPair _ _ _ l t r)
1741 = do (decls, ns) <- get
1742 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1744 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1745 imps top env (PAlternative ms a as)
1746 = do (decls, ns) <- get
1747 let isn = concatMap (namesIn uvars ist) as
1748 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1749 imps top env (PLam fc n _ ty sc)
1750 = do imps False env ty
1751 imps False (n:env) sc
1752 imps top env (PHidden tm) = imps False env tm
1753 imps top env (PUnifyLog tm) = imps False env tm
1754 imps top env (PNoImplicits tm) = imps False env tm
1755 imps top env (PRunElab fc tm ns) = imps False env tm
1756 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1757 imps top env _ = return ()
1759 pibind using [] sc = sc
1760 pibind using (n:ns) sc
1761 = case lookup n using of
1762 Just ty -> PPi impl_gen
1763 n NoFC ty (pibind using ns sc)
1764 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1765 n NoFC Placeholder (pibind using ns sc)
1767-- | Add implicit arguments in function calls
1768addImplPat :: IState -> PTerm -> PTerm
1769addImplPat = addImpl' True [] [] []
1771addImplBound :: IState -> [Name] -> PTerm -> PTerm
1772addImplBound ist ns = addImpl' False ns [] [] ist
1774addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1775addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1777-- | Add the implicit arguments to applications in the term [Name]
1778-- gives the names to always expend, even when under a binder of that
1779-- name (this is to expand methods with implicit arguments in
1780-- dependent interfaces).
1781addImpl :: [Name] -> IState -> PTerm -> PTerm
1782addImpl = addImpl' False [] []
1784-- TODO: in patterns, don't add implicits to function names guarded by constructors
1785-- and *not* inside a PHidden
1787addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1788addImpl' inpat env infns imp_meths ist ptm
1789 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1791 topname = case ptm of
1793 PApp _ (PRef _ _ n) _ -> n
1794 _ -> sUN "" -- doesn't matter then
1796 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1797 ai inpat qq env ds (PRef fc fcs f)
1798 | f `elem` infns = PInferRef fc fcs f
1799 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1800 ai inpat qq env ds (PHidden (PRef fc hl f))
1801 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1802 ai inpat qq env ds (PRewrite fc by l r g)
1803 = let l' = ai inpat qq env ds l
1804 r' = ai inpat qq env ds r
1805 g' = fmap (ai inpat qq env ds) g in
1806 PRewrite fc by l' r' g'
1807 ai inpat qq env ds (PTyped l r)
1808 = let l' = ai inpat qq env ds l
1809 r' = ai inpat qq env ds r in
1811 ai inpat qq env ds (PPair fc hls p l r)
1812 = let l' = ai inpat qq env ds l
1813 r' = ai inpat qq env ds r in
1814 PPair fc hls p l' r'
1815 ai inpat qq env ds (PDPair fc hls p l t r)
1816 = let l' = ai inpat qq env ds l
1817 t' = ai inpat qq env ds t
1818 r' = ai inpat qq env ds r in
1819 PDPair fc hls p l' t' r'
1820 ai inpat qq env ds (PAlternative ms a as)
1821 = let as' = map (ai inpat qq env ds) as in
1822 PAlternative ms a as'
1823 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1824 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1825 = let as' = map (fmap (ai inpat qq env ds)) as in
1826 PApp fc (PInferRef ffc hl f) as'
1827 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1828 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1829 | not (f `elem` map fst env)
1830 = let as' = map (fmap (ai inpat qq env ds)) as in
1831 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1832 | Just (Just ty) <- lookup f env =
1833 let as' = map (fmap (ai inpat qq env ds)) as
1834 arity = getPArity ty in
1835 mkPApp fc arity ftm as'
1836 ai inpat qq env ds (PApp fc f as)
1837 = let f' = ai inpat qq env ds f
1838 as' = map (fmap (ai inpat qq env ds)) as in
1840 ai inpat qq env ds (PWithApp fc f a)
1841 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1842 ai inpat qq env ds (PCase fc c os)
1843 = let c' = ai inpat qq env ds c in
1844 -- leave lhs alone, because they get lifted into a new pattern match
1845 -- definition which is passed through addImpl again
1846 PCase fc c' (map aiCase os)
1849 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1851 -- Anything beginning with a lower case letter, not applied,
1852 -- and no namespace is a pattern variable
1853 patnames (PApp _ (PRef _ _ f) [])
1854 | implicitable f = [(f, Nothing)]
1855 patnames (PRef _ _ f)
1856 | implicitable f = [(f, Nothing)]
1857 patnames (PApp _ (PRef _ _ _) args)
1858 = concatMap patnames (map getTm args)
1859 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1860 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1861 patnames (PAs _ _ t) = patnames t
1862 patnames (PAlternative _ _ ts) = concatMap patnames ts
1866 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1867 (ai inpat qq env ds t)
1868 (ai inpat qq env ds f)
1870 -- If the name in a lambda is an unapplied data constructor name, do this
1871 -- as a 'case' instead because we'll expect to match on it
1872 ai inpat qq env ds (PLam fc n nfc ty sc)
1873 = if canBeDConName n (tt_ctxt ist)
1874 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1875 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1876 [(PRef fc [] n, sc)]))
1877 else let ty' = ai inpat qq env ds ty
1878 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1879 PLam fc n nfc ty' sc'
1880 ai inpat qq env ds (PLet fc n nfc ty val sc)
1881 = if canBeDConName n (tt_ctxt ist)
1882 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1883 else let ty' = ai inpat qq env ds ty
1884 val' = ai inpat qq env ds val
1885 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1886 PLet fc n nfc ty' val' sc'
1887 ai inpat qq env ds (PPi p n nfc ty sc)
1888 = let ty' = ai inpat qq env ds ty
1889 env' = if n `elem` imp_meths then env
1890 else ((n, Just ty) : env)
1891 sc' = ai inpat qq env' ds sc in
1893 ai inpat qq env ds (PGoal fc r n sc)
1894 = let r' = ai inpat qq env ds r
1895 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1897 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1898 -- Don't do PProof or PTactics since implicits get added when scope is
1899 -- properly known in ElabTerm.runTac
1900 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1901 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1902 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1903 (fmap (ai inpat True env ds) g)
1904 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1905 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1906 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1907 ai inpat qq env ds tm = tm
1909 handleErr (Left err) = PElabError err
1910 handleErr (Right x) = x
1912-- if in a pattern, and there are no arguments, and there's no possible
1913-- names with zero explicit arguments, don't add implicits.
1915aiFn :: Name -> Bool -> Bool -> Bool
1918 -> Name -- ^ function being applied
1920 -> [PArg] -- ^ initial arguments (if in a pattern)
1922aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1923 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1925 = case lookupDef f (tt_ctxt ist) of
1926 [] -> Right $ PPatvar ffc f
1927 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1928 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1929 if (not (vname f) || tcname f
1930 || any (conCaf (tt_ctxt ist)) ialts)
1931-- any constructor alts || any allImp ialts))
1932 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1933 else Right $ PPatvar ffc f
1934 where imp (PExp _ _ _ _) = False
1937 allImp xs = all imp xs
1939 unqualified (NS _ _) = False
1940 unqualified _ = True
1942 constructor (TyDecl (DCon _ _ _) _) = True
1943 constructor _ = False
1945 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1947 vname (UN n) = True -- non qualified
1950aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1951 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1952aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1953 -- This is where namespaces get resolved by adding PAlternative
1954 = do let ns = lookupCtxtName f (idris_implicits ist)
1955 let nh = filter (\(n, _) -> notHidden n) ns
1956 let ns' = case trimAlts ds nh of
1960 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1962 [] -> case metaVar f (map fst (idris_metavars ist)) of
1963 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1964 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1966 PAlternative [] (ExactlyOne True) $
1967 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1968 (insertImpl ns as)) alts
1970 -- if the name is in imp_meths, we should actually refer to the bound
1971 -- name rather than the global one after expanding implicits
1972 isImpName f f' | f `elem` imp_meths = f
1975 -- If it's a metavariable name, try to qualify it from the list of
1976 -- unsolved metavariables
1977 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1978 metaVar f (_ : ns) = metaVar f ns
1979 metaVar f [] = Nothing
1981 trimAlts [] alts = alts
1983 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1988 notHidden n = case getAccessibility n of
1994 = case lookupDefAccExact n False (tt_ctxt ist) of
1998 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1999 -> [PArg] -- ^ given arguments
2002 = let (as', badimpls) = partition (impIn ps) as in
2003 map addUnknownImp badimpls ++
2004 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
2006 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2007 -> [PArg] -- parameters
2008 -> [PArg] -- explicit arguments
2009 -> [PArg] -- implicits given
2011 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2012 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2013 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2014 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2015 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2016 let rtc = PResolveTC fc in
2017 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2018 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2019 case find n imps [] of
2021 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2023 PImp p True l n Placeholder :
2024 insImpAcc (M.insert n Placeholder pnas) ps given imps
2025 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2026 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2027 case find n imps [] of
2029 PTacImplicit p l n sc tm :
2030 insImpAcc (M.insert n tm pnas) ps given imps'
2033 then PTacImplicit p l n sc Placeholder :
2034 insImpAcc (M.insert n Placeholder pnas) ps given imps
2035 else PTacImplicit p l n sc sc :
2036 insImpAcc (M.insert n sc pnas) ps given imps
2037 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2038 insImpAcc _ _ given imps = given ++ imps
2040 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2042 find n [] acc = Nothing
2043 find n (PImp _ _ _ n' t : gs) acc
2044 | n == n' = Just (t, reverse acc ++ gs)
2045 find n (PTacImplicit _ _ n' _ t : gs) acc
2046 | n == n' = Just (t, reverse acc ++ gs)
2047 find n (g : gs) acc = find n gs (g : acc)
2049-- | return True if the second argument is an implicit argument which
2050-- is expected in the implicits, or if it's not an implicit
2051impIn :: [PArg] -> PArg -> Bool
2052impIn ps (PExp _ _ _ _) = True
2053impIn ps (PConstraint _ _ _ _) = True
2054impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2056expArg (PExp _ _ _ _) = True
2057expArg (PConstraint _ _ _ _) = True
2060-- replace non-linear occurrences with _
2062stripLinear :: IState -> PTerm -> PTerm
2063stripLinear i tm = evalState (sl tm) [] where
2064 sl :: PTerm -> State [Name] PTerm
2066 | (_:_) <- lookupTy f (tt_ctxt i)
2067 = return $ PRef fc hl f
2068 | otherwise = do ns <- get
2070 then return $ PHidden (PRef fc hl f) -- Placeholder
2071 else do put (f : ns)
2072 return (PRef fc hl f)
2076 then return $ PHidden (PPatvar fc f) -- Placeholder
2077 else do put (f : ns)
2078 return (PPatvar fc f)
2079 -- Assumption is that variables are all the same in each alternative
2080 sl t@(PAlternative ms b as) = do ns <- get
2082 return (PAlternative ms b as')
2083 where slAlts ns (a : as) = do put ns
2087 slAlts ns [] = return []
2088 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2089 sl (PDPair fc hls p l t r) = do l' <- sl l
2092 return (PDPair fc hls p l' t' r')
2093 sl (PApp fc fn args) = do fn' <- case fn of
2094 -- Just the args, fn isn't matchable as a var
2095 PRef _ _ _ -> return fn
2097 args' <- mapM slA args
2098 return $ PApp fc fn' args'
2099 where slA (PImp p m l n t) = do t' <- sl t
2100 return $ PImp p m l n t'
2101 slA (PExp p l n t) = do t' <- sl t
2102 return $ PExp p l n t'
2103 slA (PConstraint p l n t)
2105 return $ PConstraint p l n t'
2106 slA (PTacImplicit p l n sc t)
2108 return $ PTacImplicit p l n sc t'
2111-- | Remove functions which aren't applied to anything, which must then
2112-- be resolved by unification. Assume names resolved and alternatives
2113-- filled in (so no ambiguity).
2114stripUnmatchable :: IState -> PTerm -> PTerm
2115stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2116 su :: PTerm -> PTerm
2117 su tm@(PRef fc hl f)
2118 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2120 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2121 not (implicitable f)
2123 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2124 not (implicitable f)
2126 su (PApp fc f@(PRef _ _ fn) args)
2127 -- here we use canBeDConName because the impossible pattern
2128 -- check will not necessarily fully resolve constructor names,
2129 -- and these bare names will otherwise get in the way of
2130 -- impossbility checking.
2131 | canBeDConName fn ctxt
2132 = PApp fc f (fmap (fmap su) args)
2134 = PHidden (PApp fc f args)
2135 su (PAlternative ms b alts)
2136 = let alts' = filter (/= Placeholder) (map su alts) in
2137 if null alts' then Placeholder
2138 else PAlternative ms b alts'
2139 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2140 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2141 su t@(PLam fc _ _ _ _) = PHidden t
2142 su t@(PPi _ _ _ _ _) = PHidden t
2143 su t@(PConstant _ c) | isTypeConst c = PHidden t
2148stripUnmatchable i tm = tm
2151mkPApp fc a f as = let rest = drop a as in
2152 if a == 0 then appRest fc f rest
2153 else appRest fc (PApp fc f (take a as)) rest
2156 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2160-- | Find 'static' argument positions
2161-- (the declared ones, plus any names in argument position in the declared
2163-- FIXME: It's possible that this really has to happen after elaboration
2164findStatics :: IState -> PTerm -> (PTerm, [Bool])
2165findStatics ist tm = let (ns, ss) = fs tm
2166 in runState (pos ns ss tm) []
2167 where fs (PPi p n fc t sc)
2168 | Static <- pstatic p
2169 = let (ns, ss) = fs sc in
2170 (namesIn [] ist t : ns, n : ss)
2171 | otherwise = let (ns, ss) = fs sc in
2175 inOne n ns = length (filter id (map (elem n) ns)) == 1
2177 pos ns ss (PPi p n fc t sc)
2178 | elem n ss = do sc' <- pos ns ss sc
2181 return (PPi (p { pstatic = Static }) n fc t sc')
2182 | otherwise = do sc' <- pos ns ss sc
2185 return (PPi p n fc t sc')
2186 pos ns ss t = return t
2188-- for 6.12/7 compatibility
2189data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2191instance Applicative (EitherErr a) where
2195instance Monad (EitherErr a) where
2198 (LeftErr e) >>= k = LeftErr e
2199 RightOK v >>= k = k v
2201toEither (LeftErr e) = Left e
2202toEither (RightOK ho) = Right ho
2204-- | Syntactic match of a against b, returning pair of variables in a
2205-- and what they match. Returns the pair that failed if not a match.
2206matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2207matchClause = matchClause' False
2209matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2210matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2211 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2213 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2216 match' x y = match (fullApp x) (fullApp y)
2217 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2218 | fi == txt "fromInteger" && b == txt "builtins",
2219 PConstant _ (I _) <- getTm x = match (getTm x) x'
2220 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2221 | fi == txt "fromInteger" && b == txt "builtins",
2222 PConstant _ (I _) <- getTm x = match (getTm x) x'
2223 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2224 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2225 match (PApp _ f args) (PApp _ f' args')
2226 | length args == length args'
2227 = do mf <- match' f f'
2228 ms <- zipWithM matchArg args args'
2229 return (mf ++ concat ms)
2230 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2231 match (PPatvar f n) xr = match (PRef f [f] n) xr
2232 match xr (PPatvar f n) = match xr (PRef f [f] n)
2233 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2234 match (PRef _ _ n) tm@(PRef _ _ n')
2235 | n == n' && not names &&
2236 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2237 || tm == Placeholder)
2239 -- if one namespace is missing, drop the other
2240 | n == n' || n == dropNS n' || dropNS n == n' = return []
2241 where dropNS (NS n _) = n
2243 match (PRef _ _ n) tm
2244 | not names && (not (isConName n (tt_ctxt i) ||
2245 isFnName n (tt_ctxt i)) || tm == Placeholder)
2247 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2248 = do ml <- match' l l'
2251 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2254 match (PTyped l r) x = match l x
2255 match x (PTyped l r) = match x l
2256 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2259 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2262 return (ml ++ mt ++ mr)
2263 match (PAlternative _ a as) (PAlternative _ a' as')
2264 = do ms <- zipWithM match' as as'
2266 match a@(PAlternative _ _ as) b
2267 = do let ms = zipWith match' as (repeat b)
2268 case (rights (map toEither ms)) of
2271 match (PCase _ _ _) _ = return [] -- lifted out
2272 match (PMetavar _ _) _ = return [] -- modified
2273 match (PInferRef _ _ _) _ = return [] -- modified
2274 match (PQuote _) _ = return []
2275 match (PProof _) _ = return []
2276 match (PTactics _) _ = return []
2277 match (PResolveTC _) (PResolveTC _) = return []
2278 match (PTrue _ _) (PTrue _ _) = return []
2279 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2282 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2285 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2286 mty <- match' ty ty'
2288 return (mt ++ mty ++ ms)
2289 match (PHidden x) (PHidden y)
2290 | RightOK xs <- match x y = return xs -- to collect variables
2291 | otherwise = return [] -- Otherwise hidden things are unmatchable
2293 | RightOK xs <- match x y = return xs
2294 | otherwise = return []
2296 | RightOK xs <- match x y = return xs
2297 | otherwise = return []
2298 match (PUnifyLog x) y = match' x y
2299 match x (PUnifyLog y) = match' x y
2300 match (PNoImplicits x) y = match' x y
2301 match x (PNoImplicits y) = match' x y
2302 match Placeholder _ = return []
2303 match _ Placeholder = return []
2304 match (PResolveTC _) _ = return []
2305 match a b | a == b = return []
2306 | otherwise = LeftErr (a, b)
2308 checkRpts (RightOK ms) = check ms where
2310 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2313 check (_:xs) = check xs
2315 checkRpts (LeftErr x) = Left x
2317substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2318substMatches ms = substMatchesShadow ms []
2320-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2321-- substMatchesShadow [] shs t = t
2322-- substMatchesShadow ((n,tm):ns) shs t
2323-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2325substMatch :: Name -> PTerm -> PTerm -> PTerm
2326substMatch n = substMatchShadow n []
2328substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2329substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2331substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2332substMatchesShadow nmap shs t = sm shs t where
2333 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2334 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2335 sm xs (PPi p x fc t sc)
2337 = let x' = nextName x in
2338 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2339 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2340 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2341 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2342 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2343 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2344 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2346 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2347 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2348 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2349 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2350 sm xs (PHidden x) = PHidden (sm xs x)
2351 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2352 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2353 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2354 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2357 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2360shadow :: Name -> Name -> PTerm -> PTerm
2361shadow n n' t = sm 0 t where
2362 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2363 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2364 | otherwise = PLam fc x xfc (sm 0 t) sc
2365 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2366 | otherwise = PPi p x fc (sm 0 t) sc
2367 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2368 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2369 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2370 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2371 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2372 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2373 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2374 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2375 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2376 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2377 sm 0 (PAlternative ms a as)
2378 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2379 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2380 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2381 sm 0 (PHidden x) = PHidden (sm 0 x)
2382 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2383 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2384 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2385 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2386 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2387 sm ql x = descend (sm ql) x
2389 shadowAlt p@(x, oldn) = (update x, update oldn)
2390 update oldn | n == oldn = n'
2393-- | Rename any binders which are repeated (so that we don't have to
2394-- mess about with shadowing anywhere else).
2395mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2396mkUniqueNames env shadows tm
2397 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2399 initMap = M.fromList shadows
2401 inScope :: S.Set Name
2402 inScope = S.fromList $ boundNamesIn tm
2404 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2405 return (arg { getTm = t' })
2407 -- Initialise the unique name with the environment length (so we're not
2408 -- looking for too long...)
2409 initN (UN n) l = UN $ txt (str n ++ show l)
2410 initN (MN i s) l = MN (i+l) s
2413 -- FIXME: Probably ought to do this for completeness! It's fine as
2414 -- long as there are no bindings inside tactics though.
2415 mkUniqT _ nmap tac = return tac
2417 mkUniq :: Int -- ^ The number of quotations that we're under
2418 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2419 mkUniq 0 nmap (PLam fc n nfc ty sc)
2423 then do let n' = uniqueNameSet (initN n (S.size env))
2424 (S.union env inScope)
2425 return (n', sc) -- shadow n n' sc)
2427 put (S.insert n' env)
2428 let nmap' = M.insert n n' nmap
2429 ty' <- mkUniq 0 nmap ty
2430 sc'' <- mkUniq 0 nmap' sc'
2431 return $! PLam fc n' nfc ty' sc''
2432 mkUniq 0 nmap (PPi p n fc ty sc)
2436 then do let n' = uniqueNameSet (initN n (S.size env))
2437 (S.union env inScope)
2438 return (n', sc) -- shadow n n' sc)
2440 put (S.insert n' env)
2441 let nmap' = M.insert n n' nmap
2442 ty' <- mkUniq 0 nmap ty
2443 sc'' <- mkUniq 0 nmap' sc'
2444 return $! PPi p n' fc ty' sc''
2445 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2449 then do let n' = uniqueNameSet (initN n (S.size env))
2450 (S.union env inScope)
2451 return (n', sc) -- shadow n n' sc)
2453 put (S.insert n' env)
2454 let nmap' = M.insert n n' nmap
2455 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2456 sc'' <- mkUniq 0 nmap' sc'
2457 return $! PLet fc n' nfc ty' val' sc''
2458 mkUniq 0 nmap (PApp fc t args)
2459 = do t' <- mkUniq 0 nmap t
2460 args' <- mapM (mkUniqA 0 nmap) args
2461 return $! PApp fc t' args'
2462 mkUniq 0 nmap (PAppBind fc t args)
2463 = do t' <- mkUniq 0 nmap t
2464 args' <- mapM (mkUniqA 0 nmap) args
2465 return $! PAppBind fc t' args'
2466 mkUniq 0 nmap (PCase fc t alts)
2467 = do t' <- mkUniq 0 nmap t
2468 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2469 return (x', y')) alts
2470 return $! PCase fc t' alts'
2471 mkUniq 0 nmap (PIfThenElse fc c t f)
2472 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2473 mkUniq 0 nmap (PPair fc hls p l r)
2474 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2475 return $! PPair fc hls p l' r'
2476 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2479 (n', sc') <- if n `S.member` env
2480 then do let n' = uniqueNameSet n (S.union env inScope)
2481 return (n', sc) -- shadow n n' sc)
2483 put (S.insert n' env)
2484 let nmap' = M.insert n n' nmap
2485 t' <- mkUniq 0 nmap t
2486 sc'' <- mkUniq 0 nmap' sc'
2487 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2488 mkUniq 0 nmap (PDPair fc hls p l t r)
2489 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2490 return $! PDPair fc hls p l' t' r'
2491 mkUniq 0 nmap (PAlternative ns b as)
2492 -- store the nmap and defer the rest until we've pruned the set
2493 -- during elaboration
2494 = return $ PAlternative (ns ++ M.toList nmap) b as
2495 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2496 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2497 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2498 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2499 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2500 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2501 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2502 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2503 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2504 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2507 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2509 mkUniq ql nmap (PQuasiquote tm ty) =
2510 do tm' <- mkUniq (ql + 1) nmap tm
2512 Nothing -> return Nothing
2513 Just t -> fmap Just $ mkUniq ql nmap t
2514 return $! PQuasiquote tm' ty'
2515 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2517 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2520getFile :: Opt -> Maybe String
2521getFile (Filename str) = Just str
2524getBC :: Opt -> Maybe String
2525getBC (BCAsm str) = Just str
2528getOutput :: Opt -> Maybe String
2529getOutput (Output str) = Just str
2530getOutput _ = Nothing
2532getIBCSubDir :: Opt -> Maybe String
2533getIBCSubDir (IBCSubDir str) = Just str
2534getIBCSubDir _ = Nothing
2536getImportDir :: Opt -> Maybe String
2537getImportDir (ImportDir str) = Just str
2538getImportDir _ = Nothing
2540getSourceDir :: Opt -> Maybe String
2541getSourceDir (SourceDir str) = Just str
2542getSourceDir _ = Nothing
2544getPkgDir :: Opt -> Maybe String
2545getPkgDir (Pkg str) = Just str
2546getPkgDir _ = Nothing
2548getPkg :: Opt -> Maybe (Bool, String)
2549getPkg (PkgBuild str) = Just (False, str)
2550getPkg (PkgInstall str) = Just (True, str)
2553getPkgClean :: Opt -> Maybe String
2554getPkgClean (PkgClean str) = Just str
2555getPkgClean _ = Nothing
2557getPkgREPL :: Opt -> Maybe String
2558getPkgREPL (PkgREPL str) = Just str
2559getPkgREPL _ = Nothing
2561getPkgCheck :: Opt -> Maybe String
2562getPkgCheck (PkgCheck str) = Just str
2563getPkgCheck _ = Nothing
2565-- | Returns None if given an Opt which is not PkgMkDoc
2566-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2567getPkgMkDoc :: Opt -- ^ Opt to extract
2568 -> Maybe (Bool, String) -- ^ Result
2569getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2570getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2571getPkgMkDoc _ = Nothing
2573getPkgTest :: Opt -- ^ the option to extract
2574 -> Maybe String -- ^ the package file to test
2575getPkgTest (PkgTest f) = Just f
2576getPkgTest _ = Nothing
2578getCodegen :: Opt -> Maybe Codegen
2579getCodegen (UseCodegen x) = Just x
2580getCodegen _ = Nothing
2582getCodegenArgs :: Opt -> Maybe String
2583getCodegenArgs (CodegenArgs args) = Just args
2584getCodegenArgs _ = Nothing
2586getConsoleWidth :: Opt -> Maybe ConsoleWidth
2587getConsoleWidth (UseConsoleWidth x) = Just x
2588getConsoleWidth _ = Nothing
2591getExecScript :: Opt -> Maybe String
2592getExecScript (InterpretScript expr) = Just expr
2593getExecScript _ = Nothing
2595getPkgIndex :: Opt -> Maybe FilePath
2596getPkgIndex (PkgIndex file) = Just file
2597getPkgIndex _ = Nothing
2599getEvalExpr :: Opt -> Maybe String
2600getEvalExpr (EvalExpr expr) = Just expr
2601getEvalExpr _ = Nothing
2603getOutputTy :: Opt -> Maybe OutputType
2604getOutputTy (OutputTy t) = Just t
2605getOutputTy _ = Nothing
2607getLanguageExt :: Opt -> Maybe LanguageExt
2608getLanguageExt (Extension e) = Just e
2609getLanguageExt _ = Nothing
2611getTriple :: Opt -> Maybe String
2612getTriple (TargetTriple x) = Just x
2613getTriple _ = Nothing
2615getCPU :: Opt -> Maybe String
2616getCPU (TargetCPU x) = Just x
2619getOptLevel :: Opt -> Maybe Int
2620getOptLevel (OptLevel x) = Just x
2621getOptLevel _ = Nothing
2623getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2624getOptimisation (AddOpt p) = Just (True, p)
2625getOptimisation (RemoveOpt p) = Just (False, p)
2626getOptimisation _ = Nothing
2628getColour :: Opt -> Maybe Bool
2629getColour (ColourREPL b) = Just b
2630getColour _ = Nothing
2632getClient :: Opt -> Maybe String
2633getClient (Client x) = Just x
2634getClient _ = Nothing
2636-- Get the first valid port
2637getPort :: [Opt] -> Maybe REPLPort
2639getPort (Port p : xs) = Just p
2640getPort (_ : xs) = getPort xs
2642opt :: (Opt -> Maybe a) -> [Opt] -> [a]
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