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) }
211setFnInfo :: Name -> FnInfo -> Idris ()
212setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
214setAccessibility :: Name -> Accessibility -> Idris ()
217 let ctxt = setAccess n a (tt_ctxt i)
218 putIState $ i { tt_ctxt = ctxt }
220-- | get the accessibility of a name outside this module
221getFromHideList :: Name -> Idris (Maybe Accessibility)
222getFromHideList n = do i <- getIState
223 return $ lookupCtxtExact n (hide_list i)
225setTotality :: Name -> Totality -> Idris ()
228 let ctxt = setTotal n a (tt_ctxt i)
229 putIState $ i { tt_ctxt = ctxt }
231setInjectivity :: Name -> Injectivity -> Idris ()
234 let ctxt = setInjective n a (tt_ctxt i)
235 putIState $ i { tt_ctxt = ctxt }
237getTotality :: Name -> Idris Totality
240 case lookupTotal n (tt_ctxt i) of
242 _ -> return (Total [])
244-- Get coercions which might return the required type
245getCoercionsTo :: IState -> Type -> [Name]
247 let cs = idris_coercions i
248 (fn,_) = unApply (getRetTy ty) in
250 where findCoercions t [] = []
251 findCoercions t (n : ns) =
252 let ps = case lookupTy n (tt_ctxt i) of
253 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
254 (t', _) -> [n | t == t']
256 ps ++ findCoercions t ns
258addToCG :: Name -> CGInfo -> Idris ()
261 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
263addCalls :: Name -> [Name] -> Idris ()
266 case lookupCtxtExact n (idris_callgraph i) of
267 Nothing -> addToCG n (CGInfo calls [] [])
268 Just (CGInfo cs scg used) ->
269 addToCG n (CGInfo (nub (calls ++ cs)) scg used)
271addTyInferred :: Name -> Idris ()
274 putIState $ i { idris_tyinfodata =
275 addDef n TIPartial (idris_tyinfodata i) }
277addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
278addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
279 mapM_ addConstraint ts
281 where addConstraint (x, y) = findMVApps x y
284 = do let (fx, argsx) = unApply x
285 let (fy, argsy) = unApply y
290 else mapM_ addConstraint (zip argsx argsy)
292 tryAddMV (P _ mv _) y =
294 case lookup mv (idris_metavars ist) of
295 Just _ -> addConstraintRule mv y
297 tryAddMV _ _ = return ()
299 addConstraintRule :: Name -> Term -> Idris ()
300 addConstraintRule n t
302 logLvl 1 $ "TI constraint: " ++ show (n, t)
303 case lookupCtxt n (idris_tyinfodata ist) of
305 do mapM_ (checkConsistent t) ts
306 let ti' = addDef n (TISolution (t : ts))
307 (idris_tyinfodata ist)
308 put $ ist { idris_tyinfodata = ti' }
310 do let ti' = addDef n (TISolution [t])
311 (idris_tyinfodata ist)
312 put $ ist { idris_tyinfodata = ti' }
314 -- Check a solution is consistent with previous solutions
315 -- Meaning: If heads are both data types, they had better be the
317 checkConsistent :: Term -> Term -> Idris ()
318 checkConsistent x y =
319 do let (fx, _) = unApply x
320 let (fy, _) = unApply y
322 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
323 (P (TCon _ _) n _, Constant _) -> errWhen True
324 (Constant _, P (TCon _ _) n' _) -> errWhen True
325 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
330 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
331 errWhen False = return ()
333isTyInferred :: Name -> Idris Bool
336 case lookupCtxt n (idris_tyinfodata i) of
337 [TIPartial] -> return True
340-- | Adds error handlers for a particular function and argument. If
341-- names are ambiguous, all matching handlers are updated.
342addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
343addFunctionErrorHandlers f arg hs =
345 let oldHandlers = idris_function_errorhandlers i
346 let newHandlers = flip (addDef f) oldHandlers $
347 case lookupCtxtExact f oldHandlers of
348 Nothing -> M.singleton arg (S.fromList hs)
349 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
350 -- will always be one of those two, thus no extra case
351 putIState $ i { idris_function_errorhandlers = newHandlers }
353getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
354getFunctionErrorHandlers f arg = do i <- getIState
355 return . maybe [] S.toList $
356 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
359-- | Trace all the names in a call graph starting at the given name
360getAllNames :: Name -> Idris [Name]
361getAllNames n = allNames [] n
363allNames :: [Name] -> Name -> Idris [Name]
364allNames ns n | n `elem` ns = return []
365allNames ns n = do i <- getIState
366 case lookupCtxtExact n (idris_callgraph i) of
367 Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')
368 return (nub (n : concat more))
371addCoercion :: Name -> Idris ()
372addCoercion n = do i <- getIState
373 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
375addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
378 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
380addNameHint :: Name -> Name -> Idris ()
383 ty' <- case lookupCtxtName ty (idris_implicits i) of
384 [(tyn, _)] -> return tyn
385 [] -> throwError (NoSuchVariable ty)
386 tyns -> throwError (CantResolveAlts (map fst tyns))
387 let ns' = case lookupCtxt ty' (idris_namehints i) of
390 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
392getNameHints :: IState -> Name -> [Name]
393getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
395 case lookupCtxt n (idris_namehints i) of
399addDeprecated :: Name -> String -> Idris ()
400addDeprecated n reason = do
402 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
404getDeprecated :: Name -> Idris (Maybe String)
407 return $ lookupCtxtExact n (idris_deprecated i)
410addFragile :: Name -> String -> Idris ()
411addFragile n reason = do
413 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
415getFragile :: Name -> Idris (Maybe String)
418 return $ lookupCtxtExact n (idris_fragile i)
420push_estack :: Name -> Bool -> Idris ()
423 putIState (i { elab_stack = (n, impl) : elab_stack i })
425pop_estack :: Idris ()
426pop_estack = do i <- getIState
427 putIState (i { elab_stack = ptail (elab_stack i) })
431-- | Add an interface implementation function.
433-- Precondition: the implementation should have the correct type.
435-- Dodgy hack 1: Put integer implementations first in the list so they are
436-- resolved by default.
438-- Dodgy hack 2: put constraint chasers (ParentN) last
439addImplementation :: Bool -- ^ whether the name is an Integer implementation
440 -> Bool -- ^ whether to include the implementation in implementation search
441 -> Name -- ^ the name of the interface
442 -> Name -- ^ the name of the implementation
444addImplementation int res n i
445 = do ist <- getIState
446 case lookupCtxt n (idris_interfaces ist) of
447 [CI a b c d e f g ins fds] ->
448 do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
449 putIState $ ist { idris_interfaces = cs }
450 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
451 putIState $ ist { idris_interfaces = cs }
452 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
453 addI i ins | int = (i, res) : ins
454 | chaser n = ins ++ [(i, res)]
455 | otherwise = insI i ins
456 insI i [] = [(i, res)]
457 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
458 | otherwise = n : insI i ns
460 chaser (SN (ParentN _ _)) = True
461 chaser (NS n _) = chaser n
464-- | Add a privileged implementation - one which implementation search will
465-- happily resolve immediately if it is type correct This is used for
466-- naming parent implementations when defining an implementation with
467-- constraints. Returns the old list, so we can revert easily at the
469addOpenImpl :: [Name] -> Idris [Name]
470addOpenImpl ns = do ist <- getIState
471 ns' <- mapM (checkValid ist) ns
472 let open = idris_openimpls ist
473 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
477 = case lookupCtxtName n (idris_implicits ist) of
478 [(n', _)] -> return n'
479 [] -> throwError (NoSuchVariable n)
480 more -> throwError (CantResolveAlts (map fst more))
482setOpenImpl :: [Name] -> Idris ()
483setOpenImpl ns = do ist <- getIState
484 putIState $ ist { idris_openimpls = ns }
486getOpenImpl :: Idris [Name]
487getOpenImpl = do ist <- getIState
488 return (idris_openimpls ist)
490addInterface :: Name -> InterfaceInfo -> Idris ()
492 = do ist <- getIState
493 let i' = case lookupCtxt n (idris_interfaces ist) of
494 [c] -> c { interface_implementations = interface_implementations i }
496 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
498addRecord :: Name -> RecordInfo -> Idris ()
499addRecord n ri = do ist <- getIState
500 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
502addAutoHint :: Name -> Name -> Idris ()
505 case lookupCtxtExact n (idris_autohints ist) of
507 do let hs = addDef n [hint] (idris_autohints ist)
508 putIState $ ist { idris_autohints = hs }
510 do let hs = addDef n (hint : nhints) (idris_autohints ist)
511 putIState $ ist { idris_autohints = hs }
513getAutoHints :: Name -> Idris [Name]
514getAutoHints n = do ist <- getIState
515 case lookupCtxtExact n (idris_autohints ist) of
519addIBC :: IBCWrite -> Idris ()
522 when (notDef (ibc_write i)) $
523 putIState $ i { ibc_write = ibc : ibc_write i }
524 where notDef [] = True
525 notDef (IBCDef n': is) | n == n' = False
526 notDef (_ : is) = notDef is
527addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
530clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
531 idris_inmodule = S.empty }
533resetNameIdx :: Idris ()
534resetNameIdx = do i <- getIState
535 put (i { idris_nameIdx = (0, emptyContext) })
537-- | Used to preserve sharing of names
538addNameIdx :: Name -> Idris (Int, Name)
539addNameIdx n = do i <- getIState
540 let (i', x) = addNameIdx' i n
544addNameIdx' :: IState -> Name -> (IState, (Int, Name))
546 = let idxs = snd (idris_nameIdx i) in
547 case lookupCtxt n idxs of
549 _ -> let i' = fst (idris_nameIdx i) + 1 in
550 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
552getSymbol :: Name -> Idris Name
553getSymbol n = do i <- getIState
554 case M.lookup n (idris_symbols i) of
556 Nothing -> do let sym' = M.insert n n (idris_symbols i)
557 put (i { idris_symbols = sym' })
560getHdrs :: Codegen -> Idris [String]
561getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
563getImported :: Idris [(FilePath, Bool)]
564getImported = do i <- getIState; return (idris_imported i)
566setErrSpan :: FC -> Idris ()
567setErrSpan x = do i <- getIState;
569 Nothing -> putIState $ i { errSpan = Just x }
573clearErr = do i <- getIState
574 putIState $ i { errSpan = Nothing }
576getSO :: Idris (Maybe String)
577getSO = do i <- getIState
578 return (compiled_so i)
580setSO :: Maybe String -> Idris ()
581setSO s = do i <- getIState
582 putIState (i { compiled_so = s })
584getIState :: Idris IState
587putIState :: IState -> Idris ()
590updateIState :: (IState -> IState) -> Idris ()
591updateIState f = do i <- getIState
594withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
595withContext ctx name dflt action = do
597 case lookupCtxt name (ctx ist) of
601withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
602withContext_ ctx name action = withContext ctx name () action
604-- | A version of liftIO that puts errors into the exception type of
606runIO :: IO a -> Idris a
607runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
608-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
610-- Issue #1738 on the issue tracker.
611-- https://github.com/idris-lang/Idris-dev/issues/1738
614getName = do i <- getIState;
615 let idx = idris_name i;
616 putIState (i { idris_name = idx + 1 })
619-- | InternalApp keeps track of the real function application for
620-- making case splits from, not the application the programmer wrote,
621-- which doesn't have the whole context in any case other than top
623addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
626 -- We canonicalise the path to make "./Test/Module.idr" equal
627 -- to "Test/Module.idr"
628 exists <- runIO $ doesFileExist fp
630 do fp' <- runIO $ canonicalizePath fp
631 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
633getInternalApp :: FilePath -> Int -> Idris PTerm
634getInternalApp fp l = do i <- getIState
635 -- We canonicalise the path to make
636 -- "./Test/Module.idr" equal to
638 exists <- runIO $ doesFileExist fp
640 then do fp' <- runIO $ canonicalizePath fp
641 case lookup (fp', l) (idris_lineapps i) of
643 Nothing -> return Placeholder
644 -- TODO: What if it's not there?
645 else return Placeholder
647-- | Pattern definitions are only used for coverage checking, so erase
648-- them when we're done
649clearOrigPats :: Idris ()
650clearOrigPats = do i <- get
651 let ps = idris_patdefs i
652 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
653 put (i { idris_patdefs = ps' })
655-- | Erase types from Ps in the context (basically ending up with
656-- what's in the .ibc, which is all we need after all the analysis is
658clearPTypes :: Idris ()
659clearPTypes = do i <- get
661 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
662 where pErase (CaseOp c t tys orig tot cds)
663 = CaseOp c t tys orig [] (pErase' cds)
665 pErase' (CaseDefs _ (cs, c) _ rs)
666 = let c' = (cs, fmap pEraseType c) in
669checkUndefined :: FC -> Name -> Idris ()
673 (_:_) -> throwError . Msg $ show fc ++ ":" ++
674 show n ++ " already defined"
677isUndefined :: FC -> Name -> Idris Bool
680 case lookupTyExact n i of
681 Just _ -> return False
684setContext :: Context -> Idris ()
685setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
687updateContext :: (Context -> Context) -> Idris ()
688updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
690addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
691addConstraints fc (v, cs)
692 = do tit <- typeInType
696 let ctxt' = ctxt { next_tvar = v }
697 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
698 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
701 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
702 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
703 insertAll ((c, fc) : cs) ics
704 = insertAll cs $ S.insert (ConstraintFC c fc) ics
706addDeferred = addDeferred' Ref
707addDeferredTyCon = addDeferred' (TCon 0 0)
709-- | Save information about a name that is not yet defined
710addDeferred' :: NameType
711 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
712 -- ^ The Name is the name being made into a metavar,
713 -- the Int is the number of vars that are part of a
714 -- putative proof context, the Maybe Name is the
715 -- top-level function containing the new metavariable,
716 -- the Type is its type, and the Bool is whether :p is
720 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
721 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
723 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
724 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
727 -- 'tidyNames' is to generate user accessible names in case they are
728 -- needed in tactic scripts
729 tidyNames used (Bind (MN i x) b sc)
730 = let n' = uniqueNameSet (UN x) used in
731 Bind n' b $ tidyNames (S.insert n' used) sc
732 tidyNames used (Bind n b sc)
733 = let n' = uniqueNameSet n used in
734 Bind n' b $ tidyNames (S.insert n' used) sc
737solveDeferred :: FC -> Name -> Idris ()
740 case lookup n (idris_metavars i) of
741 Just (_, _, _, _, False) ->
742 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
743 _ -> putIState $ i { idris_metavars =
744 filter (\(n', _) -> n/=n')
747 filter (notMV n) (ibc_write i)
749 where notMV n (IBCMetavar n') = not (n == n')
752getUndefined :: Idris [Name]
753getUndefined = do i <- getIState
754 return (map fst (idris_metavars i) \\ primDefs)
756isMetavarName :: Name -> IState -> Bool
758 = case lookupNames n (tt_ctxt ist) of
759 (t:_) -> isJust $ lookup t (idris_metavars ist)
762getWidth :: Idris ConsoleWidth
763getWidth = fmap idris_consolewidth getIState
765setWidth :: ConsoleWidth -> Idris ()
766setWidth w = do ist <- getIState
767 put ist { idris_consolewidth = w }
769setDepth :: Maybe Int -> Idris ()
770setDepth d = do ist <- getIState
771 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
773typeDescription :: String
774typeDescription = "The type of types"
777type1Doc :: Doc OutputAnnotation
778type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
781isetPrompt :: String -> Idris ()
782isetPrompt p = do i <- getIState
783 case idris_outputmode i of
784 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
786-- | Tell clients how much was parsed and loaded
787isetLoadedRegion :: Idris ()
788isetLoadedRegion = do i <- getIState
789 let span = idris_parsedSpan i
792 case idris_outputmode i of
794 runIO . hPutStrLn h $
795 convSExp "set-loaded-region" fc n
798setLogLevel :: Int -> Idris ()
799setLogLevel l = do i <- getIState
800 let opts = idris_options i
801 let opt' = opts { opt_logLevel = l }
802 putIState $ i { idris_options = opt' }
804setLogCats :: [LogCat] -> Idris ()
807 let opts = idris_options i
808 let opt' = opts { opt_logcats = cs }
809 putIState $ i { idris_options = opt' }
811setCmdLine :: [Opt] -> Idris ()
812setCmdLine opts = do i <- getIState
813 let iopts = idris_options i
814 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
816getCmdLine :: Idris [Opt]
817getCmdLine = do i <- getIState
818 return (opt_cmdline (idris_options i))
820getDumpHighlighting :: Idris Bool
821getDumpHighlighting = do ist <- getIState
822 return (findC (opt_cmdline (idris_options ist)))
823 where findC = elem DumpHighlights
825getDumpDefun :: Idris (Maybe FilePath)
826getDumpDefun = do i <- getIState
827 return $ findC (opt_cmdline (idris_options i))
828 where findC [] = Nothing
829 findC (DumpDefun x : _) = Just x
830 findC (_ : xs) = findC xs
832getDumpCases :: Idris (Maybe FilePath)
833getDumpCases = do i <- getIState
834 return $ findC (opt_cmdline (idris_options i))
835 where findC [] = Nothing
836 findC (DumpCases x : _) = Just x
837 findC (_ : xs) = findC xs
840logLevel = do i <- getIState
841 return (opt_logLevel (idris_options i))
843setAutoImpls :: Bool -> Idris ()
844setAutoImpls b = do i <- getIState
845 let opts = idris_options i
846 let opt' = opts { opt_autoimpls = b }
847 putIState $ i { idris_options = opt' }
849getAutoImpls :: Idris Bool
850getAutoImpls = do i <- getIState
851 return (opt_autoimpls (idris_options i))
853setErrContext :: Bool -> Idris ()
854setErrContext t = do i <- getIState
855 let opts = idris_options i
856 let opts' = opts { opt_errContext = t }
857 putIState $ i { idris_options = opts' }
859errContext :: Idris Bool
860errContext = do i <- getIState
861 return (opt_errContext (idris_options i))
863getOptimise :: Idris [Optimisation]
864getOptimise = do i <- getIState
865 return (opt_optimise (idris_options i))
867setOptimise :: [Optimisation] -> Idris ()
868setOptimise newopts = do i <- getIState
869 let opts = idris_options i
870 let opts' = opts { opt_optimise = newopts }
871 putIState $ i { idris_options = opts' }
873addOptimise :: Optimisation -> Idris ()
874addOptimise opt = do opts <- getOptimise
875 setOptimise (nub (opt : opts))
877removeOptimise :: Optimisation -> Idris ()
878removeOptimise opt = do opts <- getOptimise
879 setOptimise ((nub opts) \\ [opt])
881-- | Set appropriate optimisation set for the given level. We only
882-- have one optimisation that is configurable at the moment, however!
883setOptLevel :: Int -> Idris ()
884setOptLevel n | n <= 0 = setOptimise []
885setOptLevel 1 = setOptimise []
886setOptLevel 2 = setOptimise [PETransform]
887setOptLevel n | n >= 3 = setOptimise [PETransform]
890useREPL = do i <- getIState
891 return (opt_repl (idris_options i))
893setREPL :: Bool -> Idris ()
894setREPL t = do i <- getIState
895 let opts = idris_options i
896 let opt' = opts { opt_repl = t }
897 putIState $ i { idris_options = opt' }
899showOrigErr :: Idris Bool
900showOrigErr = do i <- getIState
901 return (opt_origerr (idris_options i))
903setShowOrigErr :: Bool -> Idris ()
904setShowOrigErr b = do i <- getIState
905 let opts = idris_options i
906 let opt' = opts { opt_origerr = b }
907 putIState $ i { idris_options = opt' }
909setAutoSolve :: Bool -> Idris ()
910setAutoSolve b = do i <- getIState
911 let opts = idris_options i
912 let opt' = opts { opt_autoSolve = b }
913 putIState $ i { idris_options = opt' }
915setNoBanner :: Bool -> Idris ()
916setNoBanner n = do i <- getIState
917 let opts = idris_options i
918 let opt' = opts { opt_nobanner = n }
919 putIState $ i { idris_options = opt' }
921getNoBanner :: Idris Bool
922getNoBanner = do i <- getIState
923 let opts = idris_options i
924 return (opt_nobanner opts)
926setEvalTypes :: Bool -> Idris ()
927setEvalTypes n = do i <- getIState
928 let opts = idris_options i
929 let opt' = opts { opt_evaltypes = n }
930 putIState $ i { idris_options = opt' }
932getDesugarNats :: Idris Bool
933getDesugarNats = do i <- getIState
934 let opts = idris_options i
935 return (opt_desugarnats opts)
938setDesugarNats :: Bool -> Idris ()
939setDesugarNats n = do i <- getIState
940 let opts = idris_options i
941 let opt' = opts { opt_desugarnats = n }
942 putIState $ i { idris_options = opt' }
944setQuiet :: Bool -> Idris ()
945setQuiet q = do i <- getIState
946 let opts = idris_options i
947 let opt' = opts { opt_quiet = q }
948 putIState $ i { idris_options = opt' }
950getQuiet :: Idris Bool
951getQuiet = do i <- getIState
952 let opts = idris_options i
953 return (opt_quiet opts)
955setCodegen :: Codegen -> Idris ()
956setCodegen t = do i <- getIState
957 let opts = idris_options i
958 let opt' = opts { opt_codegen = t }
959 putIState $ i { idris_options = opt' }
961codegen :: Idris Codegen
962codegen = do i <- getIState
963 return (opt_codegen (idris_options i))
966setOutputTy :: OutputType -> Idris ()
967setOutputTy t = do i <- getIState
968 let opts = idris_options i
969 let opt' = opts { opt_outputTy = t }
970 putIState $ i { idris_options = opt' }
972outputTy :: Idris OutputType
973outputTy = do i <- getIState
974 return $ opt_outputTy $ idris_options i
976setIdeMode :: Bool -> Handle -> Idris ()
977setIdeMode True h = do i <- getIState
978 putIState $ i { idris_outputmode = IdeMode 0 h
979 , idris_colourRepl = False
981setIdeMode False _ = return ()
983setTargetTriple :: String -> Idris ()
984setTargetTriple t = do i <- getIState
985 let opts = idris_options i
986 opt' = opts { opt_triple = t }
987 putIState $ i { idris_options = opt' }
989targetTriple :: Idris String
990targetTriple = do i <- getIState
991 return (opt_triple (idris_options i))
993setTargetCPU :: String -> Idris ()
994setTargetCPU t = do i <- getIState
995 let opts = idris_options i
996 opt' = opts { opt_cpu = t }
997 putIState $ i { idris_options = opt' }
999targetCPU :: Idris String
1000targetCPU = do i <- getIState
1001 return (opt_cpu (idris_options i))
1003verbose :: Idris Bool
1004verbose = do i <- getIState
1005 -- Quietness overrides verbosity
1006 return (not (opt_quiet (idris_options i)) &&
1007 opt_verbose (idris_options i))
1009setVerbose :: Bool -> Idris ()
1010setVerbose t = do i <- getIState
1011 let opts = idris_options i
1012 let opt' = opts { opt_verbose = t }
1013 putIState $ i { idris_options = opt' }
1015typeInType :: Idris Bool
1016typeInType = do i <- getIState
1017 return (opt_typeintype (idris_options i))
1019setTypeInType :: Bool -> Idris ()
1020setTypeInType t = do i <- getIState
1021 let opts = idris_options i
1022 let opt' = opts { opt_typeintype = t }
1023 putIState $ i { idris_options = opt' }
1025coverage :: Idris Bool
1026coverage = do i <- getIState
1027 return (opt_coverage (idris_options i))
1029setCoverage :: Bool -> Idris ()
1030setCoverage t = do i <- getIState
1031 let opts = idris_options i
1032 let opt' = opts { opt_coverage = t }
1033 putIState $ i { idris_options = opt' }
1035setIBCSubDir :: FilePath -> Idris ()
1036setIBCSubDir fp = do i <- getIState
1037 let opts = idris_options i
1038 let opt' = opts { opt_ibcsubdir = fp }
1039 putIState $ i { idris_options = opt' }
1041valIBCSubDir :: IState -> Idris FilePath
1042valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1044addImportDir :: FilePath -> Idris ()
1045addImportDir fp = do i <- getIState
1046 let opts = idris_options i
1047 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1048 putIState $ i { idris_options = opt' }
1050setImportDirs :: [FilePath] -> Idris ()
1051setImportDirs fps = do i <- getIState
1052 let opts = idris_options i
1053 let opt' = opts { opt_importdirs = fps }
1054 putIState $ i { idris_options = opt' }
1056allImportDirs :: Idris [FilePath]
1057allImportDirs = do i <- getIState
1058 let optdirs = opt_importdirs (idris_options i)
1059 return ("." : reverse optdirs)
1061addSourceDir :: FilePath -> Idris ()
1062addSourceDir fp = do i <- getIState
1063 let opts = idris_options i
1064 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1065 putIState $ i { idris_options = opts' }
1067setSourceDirs :: [FilePath] -> Idris ()
1068setSourceDirs fps = do i <- getIState
1069 let opts = idris_options i
1070 let opts' = opts { opt_sourcedirs = nub $ fps }
1071 putIState $ i { idris_options = opts' }
1073allSourceDirs :: Idris [FilePath]
1074allSourceDirs = do i <- getIState
1075 let optdirs = opt_sourcedirs (idris_options i)
1076 return ("." : reverse optdirs)
1078colourise :: Idris Bool
1079colourise = do i <- getIState
1080 return $ idris_colourRepl i
1082setColourise :: Bool -> Idris ()
1083setColourise b = do i <- getIState
1084 putIState $ i { idris_colourRepl = b }
1086impShow :: Idris Bool
1087impShow = do i <- getIState
1088 return (opt_showimp (idris_options i))
1090setImpShow :: Bool -> Idris ()
1091setImpShow t = do i <- getIState
1092 let opts = idris_options i
1093 let opt' = opts { opt_showimp = t }
1094 putIState $ i { idris_options = opt' }
1096setColour :: ColourType -> IdrisColour -> Idris ()
1097setColour ct c = do i <- getIState
1098 let newTheme = setColour' ct c (idris_colourTheme i)
1099 putIState $ i { idris_colourTheme = newTheme }
1100 where setColour' KeywordColour c t = t { keywordColour = c }
1101 setColour' BoundVarColour c t = t { boundVarColour = c }
1102 setColour' ImplicitColour c t = t { implicitColour = c }
1103 setColour' FunctionColour c t = t { functionColour = c }
1104 setColour' TypeColour c t = t { typeColour = c }
1105 setColour' DataColour c t = t { dataColour = c }
1106 setColour' PromptColour c t = t { promptColour = c }
1107 setColour' PostulateColour c t = t { postulateColour = c }
1110logLvl :: Int -> String -> Idris ()
1111logLvl = logLvlCats []
1113logCoverage :: Int -> String -> Idris ()
1114logCoverage = logLvlCats [ICoverage]
1116logErasure :: Int -> String -> Idris ()
1117logErasure = logLvlCats [IErasure]
1119-- | Log an action of the parser
1120logParser :: Int -> String -> Idris ()
1121logParser = logLvlCats parserCats
1123-- | Log an action of the elaborator.
1124logElab :: Int -> String -> Idris ()
1125logElab = logLvlCats elabCats
1127-- | Log an action of the compiler.
1128logCodeGen :: Int -> String -> Idris ()
1129logCodeGen = logLvlCats codegenCats
1131logIBC :: Int -> String -> Idris ()
1132logIBC = logLvlCats [IIBC]
1134-- | Log aspect of Idris execution
1136-- An empty set of logging levels is used to denote all categories.
1138-- @TODO update IDE protocol
1139logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1140 -> Int -- ^ The Logging level the message should appear.
1141 -> String -- ^ The message to show the developer.
1143logLvlCats cs l str = do
1145 let lvl = opt_logLevel (idris_options i)
1146 let cats = opt_logcats (idris_options i)
1148 when (inCat cs cats || null cats) $
1149 case idris_outputmode i of
1151 runIO $ hPutStrLn h str
1153 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1154 runIO . hPutStrLn h $ convSExp "log" good n
1156 inCat :: [LogCat] -> [LogCat] -> Bool
1157 inCat cs cats = any (`elem` cats) cs
1159cmdOptType :: Opt -> Idris Bool
1160cmdOptType x = do i <- getIState
1161 return $ x `elem` opt_cmdline (idris_options i)
1163noErrors :: Idris Bool
1164noErrors = do i <- getIState
1166 Nothing -> return True
1169setTypeCase :: Bool -> Idris ()
1170setTypeCase t = do i <- getIState
1171 let opts = idris_options i
1172 let opt' = opts { opt_typecase = t }
1173 putIState $ i { idris_options = opt' }
1176-- Dealing with parameters
1178expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1179 [Name] -> -- all names
1180 [Name] -> -- names with no declaration
1182expandParams dec ps ns infs tm = en 0 tm
1184 -- if we shadow a name (say in a lambda binding) that is used in a call to
1185 -- a lifted function, we need access to both names - once in the scope of the
1186 -- binding and once to call the lifted functions. So we'll explicitly shadow
1187 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1188 -- but we didn't...)
1190 mkShadow (UN n) = MN 0 n
1191 mkShadow (MN i n) = MN (i+1) n
1192 mkShadow (NS x s) = NS (mkShadow x) s
1194 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1195 -- that are merely mentioned.
1197 en 0 (PLam fc n nfc t s)
1198 | n `elem` (map fst ps ++ ns)
1199 = let n' = mkShadow n in
1200 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1201 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1202 en 0 (PPi p n nfc t s)
1203 | n `elem` (map fst ps ++ ns)
1204 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1205 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1206 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1207 en 0 (PLet fc n nfc ty v s)
1208 | n `elem` (map fst ps ++ ns)
1209 = let n' = mkShadow n in
1210 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1211 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1212 -- FIXME: Should only do this in a type signature!
1213 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1214 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1215 = let n' = mkShadow n in
1216 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1217 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1218 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1219 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1220 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1221 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1222 en 0 (PHidden t) = PHidden (en 0 t)
1223 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1224 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1225 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1226 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1227 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1228 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1230 en 0 (PQuote (Var n))
1231 | n `nselem` ns = PQuote (Var (dec n))
1232 en 0 (PApp fc (PInferRef fc' hl n) as)
1233 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1234 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1235 en 0 (PApp fc (PRef fc' hl n) as)
1236 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1237 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1238 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1239 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1240 en 0 (PAppBind fc (PRef fc' hl n) as)
1241 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1242 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1243 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1244 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1246 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1247 (map ((pexp . (PRef fc hl)) . fst) ps)
1248 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1249 (map ((pexp . (PRef fc hl)) . fst) ps)
1250 en 0 (PInferRef fc hl n)
1251 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1252 (map ((pexp . (PRef fc hl)) . fst) ps)
1253 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1254 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1255 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1256 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1257 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1258 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1260 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1261 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1263 en ql t = descend (en ql) t
1266 nselem x (y : xs) | nseq x y = True
1267 | otherwise = nselem x xs
1269 nseq x y = nsroot x == nsroot y
1271 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1272 enTacImp ql other = other
1274expandParamsD :: Bool -> -- True = RHS only
1276 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1277expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1278 = if n `elem` ns && (not rhsonly)
1279 then -- trace (show (n, expandParams dec ps ns ty)) $
1280 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1281 else --trace (show (n, expandParams dec ps ns ty)) $
1282 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1283expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1284 = if n `elem` ns && (not rhsonly)
1285 then -- trace (show (n, expandParams dec ps ns ty)) $
1286 PPostulate e doc syn fc nfc o (dec n)
1287 (piBind ps (expandParams dec ps ns [] ty))
1288 else --trace (show (n, expandParams dec ps ns ty)) $
1289 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1290expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1291 = let n' = if n `elem` ns then dec n else n in
1292 PClauses fc opts n' (map expandParamsC cs)
1294 expandParamsC (PClause fc n lhs ws rhs ds)
1295 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1296 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1297 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1298 n' = if n `elem` ns then dec n else n
1299 -- names bound on the lhs should not be expanded on the rhs
1300 ns' = removeBound lhs ns in
1302 (map (expandParams dec ps'' ns' []) ws)
1303 (expandParams dec ps'' ns' [] rhs)
1304 (map (expandParamsD True ist dec ps'' ns') ds)
1305 expandParamsC (PWith fc n lhs ws wval pn ds)
1306 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1307 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1308 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1309 n' = if n `elem` ns then dec n else n
1310 ns' = removeBound lhs ns in
1312 (map (expandParams dec ps'' ns' []) ws)
1313 (expandParams dec ps'' ns' [] wval)
1315 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1316 updateps yn nm [] = []
1317 updateps yn nm (((a, t), i):as)
1318 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1319 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1321 removeBound lhs ns = ns \\ nub (bnames lhs)
1323 bnames (PRef _ _ n) = [n]
1324 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1325 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1326 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1329-- | Expands parameters defined in parameter and where blocks inside of declarations
1330expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1331 = PData doc argDocs syn fc co (expandPData pd)
1333 -- just do the type decl, leave constructors alone (parameters will be
1334 -- added implicitly)
1335 expandPData (PDatadecl n nfc ty cons)
1337 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1339 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1340 econ (doc, argDocs, n, nfc, t, fc, fs)
1341 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1342expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1344expandParamsD rhs ist dec ps ns (PParams f params pds)
1345 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1346 (map (expandParamsD True ist dec ps ns) pds)
1347-- (map (expandParamsD ist dec ps ns) pds)
1348expandParamsD rhs ist dec ps ns (PMutual f pds)
1349 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1350expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1351 = PInterface doc info f
1352 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1354 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1357 (map (expandParamsD rhs ist dec ps ns) decls)
1360expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1361 = let cn' = case cn of
1362 Just n -> if n `elem` ns then Just (dec n) else Just n
1363 Nothing -> Nothing in
1364 PImplementation doc argDocs info f
1365 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1368 (map (expandParams dec ps ns []) params)
1369 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1370 (expandParams dec ps ns [] ty)
1372 (map (expandParamsD True ist dec ps ns) decls)
1373expandParamsD rhs ist dec ps ns d = d
1375mapsnd f (x, t) = (x, f t)
1377expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1378 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1380expandImplementationScope ist dec ps ns d = d
1382-- | Calculate a priority for a type, for deciding elaboration order
1383-- * if it's just a type variable or concrete type, do it early (0)
1384-- * if there's only type variables and injective constructors, do it next (1)
1385-- * if there's a function type, next (2)
1386-- * finally, everything else (3)
1387getPriority :: IState -> PTerm -> Int
1388getPriority i tm = 1 -- pri tm
1391 case lookupP n (tt_ctxt i) of
1392 ((P (DCon _ _ _) _ _):_) -> 1
1393 ((P (TCon _ _) _ _):_) -> 1
1394 ((P Ref _ _):_) -> 1
1395 [] -> 0 -- must be locally bound, if it's not an error...
1396 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1398 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1399 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1400 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1401 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1402 pri (PTyped l r) = pri l
1403 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1404 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1405 pri (PAlternative _ a as) = maximum (map pri as)
1406 pri (PConstant _ _) = 0
1411addStatics :: Name -> Term -> PTerm -> Idris ()
1412addStatics n tm ptm =
1413 do let (statics, dynamics) = initStatics tm ptm
1416 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1417 Just p -> getNamesFrom 0 (fn_params p) tm ++
1418 concatMap (getParamNames ist . snd) statics
1419 _ -> concatMap (getParamNames ist . snd) statics
1421 let stnames = nub $ concatMap (freeArgNames . snd) statics
1422 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1424 -- also get the arguments which are 'uniquely inferrable' from
1425 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1426 -- or parameters to the type of a static
1427 let statics' = nub $ map fst statics ++
1428 filter (\x -> not (elem x dnames)) stnames
1429 let stpos = staticList statics' tm
1431 unless (null statics) $
1432 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1433 ++ showTmImpls ptm ++ "\n"
1434 ++ show statics ++ "\n" ++ show dynamics
1435 ++ "\n" ++ show paramnames
1436 ++ "\n" ++ show stpos
1437 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1438 addIBC (IBCStatic n)
1440 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1441 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1442 (static, (n, ty) : dynamic)
1443 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1444 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1445 if pstatic p == Static then ((n, ty) : static, dynamic)
1446 else if (not (searchArg p))
1447 then (static, (n, ty) : dynamic)
1448 else (static, dynamic)
1449 initStatics t pt = ([], [])
1451 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1452 = case lookupCtxtExact n (idris_datatypes ist) of
1453 Just ti -> getNamePos 0 (param_pos ti) args
1455 where getNamePos i ps [] = []
1456 getNamePos i ps (P _ n _ : as)
1457 | i `elem` ps = n : getNamePos (i + 1) ps as
1458 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1459 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1460 = n : getParamNames ist sc
1461 getParamNames ist _ = []
1463 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1464 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1465 | otherwise = getNamesFrom (i + 1) ps sc
1466 getNamesFrom i ps sc = []
1468 freeArgNames (Bind n (Pi _ ty _) sc)
1469 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1470 freeArgNames tm = let (_, args) = unApply tm in
1471 concatMap freeNames args
1473 -- if a name appears in an interface or tactic implicit index, it doesn't
1474 -- affect its 'uniquely inferrable' from a static status since these are
1475 -- resolved by searching.
1476 searchArg (Constraint _ _) = True
1477 searchArg (TacImp _ _ _) = True
1480 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1483-- Dealing with implicit arguments
1485-- Add some bound implicits to the using block if they aren't there already
1487addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1488addToUsing us [] = us
1489addToUsing us ((n, t) : ns)
1490 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1491 | otherwise = addToUsing us ns
1492 where impName (UImplicit n _) = Just n
1495-- Add constraint bindings from using block
1497addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1498addUsingConstraints syn fc t
1500 let ns = namesIn [] ist t
1501 let cs = getConstraints t -- check declared constraints
1502 let addconsts = uconsts \\ cs
1503 return (doAdd addconsts ns t)
1504 where uconsts = filter uconst (using syn)
1505 uconst (UConstraint _ _) = True
1509 -- if all of args in ns, then add it
1510 doAdd (UConstraint c args : cs) ns t
1511 | all (\n -> elem n ns) args
1512 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1513 (mkConst c args) (doAdd cs ns t)
1514 | otherwise = doAdd cs ns t
1516 mkConst c args = PApp fc (PRef fc [] c)
1517 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1519 getConstraints (PPi (Constraint _ _) _ _ c sc)
1520 = getcapp c ++ getConstraints sc
1521 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1522 getConstraints _ = []
1524 getcapp (PApp _ (PRef _ _ c) args)
1525 = do ns <- mapM getName args
1526 return (UConstraint c ns)
1529 getName (PExp _ _ _ (PRef _ _ n)) = return n
1532-- | Add implicit bindings from using block, and bind any missing names
1533addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1534addUsingImpls syn n fc t
1535 = do ist <- getIState
1536 autoimpl <- getAutoImpls
1537 let ns_in = implicitNamesIn (map iname uimpls) ist t
1538 let ns = if autoimpl then ns_in
1539 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1541 let badnames = filter (\n -> not (implicitable n) &&
1542 n `notElem` (map iname uimpls)) ns
1543 unless (null badnames) $
1544 throwError (At fc (Elaborating "type of " n Nothing
1545 (NoSuchVariable (head badnames))))
1546 let cs = getArgnames t -- get already bound names
1547 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1548 -- if all names in the arguments of addconsts appear in ns,
1549 -- add the constraint implicitly
1550 return (bindFree ns (doAdd addimpls ns t))
1551 where uimpls = filter uimpl (using syn)
1552 uimpl (UImplicit _ _) = True
1555 iname (UImplicit n _) = n
1556 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1559 -- if all of args in ns, then add it
1560 doAdd (UImplicit n ty : cs) ns t
1562 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1563 | otherwise = doAdd cs ns t
1565 -- bind the free names which weren't in the using block
1568 | elem n (map iname uimpls) = bindFree ns tm
1570 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1572 getArgnames (PPi _ n _ c sc)
1573 = n : getArgnames sc
1576-- Given the original type and the elaborated type, return the implicitness
1577-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1579getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1580getUnboundImplicits i t tm = getImps t (collectImps tm)
1581 where collectImps (PPi p n _ t sc)
1582 = (n, (p, t)) : collectImps sc
1585 scopedimpl (Just i) = not (toplevel_imp i)
1586 scopedimpl _ = False
1588 getImps (Bind n (Pi i _ _) sc) imps
1589 | scopedimpl i = getImps sc imps
1590 getImps (Bind n (Pi _ t _) sc) imps
1591 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1593 argInfo n (Imp opt _ _ _ _) Placeholder
1594 = (True, PImp 0 True opt n Placeholder)
1595 argInfo n (Imp opt _ _ _ _) t'
1596 = (False, PImp (getPriority i t') True opt n t')
1597 argInfo n (Exp opt _ _) t'
1598 = (InaccessibleArg `elem` opt,
1599 PExp (getPriority i t') opt n t')
1600 argInfo n (Constraint opt _) t'
1601 = (InaccessibleArg `elem` opt,
1602 PConstraint 10 opt n t')
1603 argInfo n (TacImp opt _ scr) t'
1604 = (InaccessibleArg `elem` opt,
1605 PTacImplicit 10 opt n scr t')
1606 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1607 where impBind n t = (True, PImp 1 True [] n Placeholder)
1610-- Add implicit Pi bindings for any names in the term which appear in an
1611-- argument position.
1613-- This has become a right mess already. Better redo it some time...
1614-- TODO: This is obsoleted by the new way of elaborating types, (which
1615-- calls addUsingImpls) but there's still a couple of places which use
1616-- it. Clean them up!
1618-- Issue 1739 in the issue tracker
1619-- https://github.com/idris-lang/Idris-dev/issues/1739
1620implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1621implicit info syn n ptm = implicit' info syn [] n ptm
1623implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1624implicit' info syn ignore n ptm
1626 auto <- getAutoImpls
1627 let (tm', impdata) = implicitise auto syn ignore i ptm
1628 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1629-- let (tm'', spos) = findStatics i tm'
1630 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1632 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1634-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1637 -- Detect unknown names in default arguments and throw error if found.
1638 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1639 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1641 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1642 notFoundInDefault kns (PTacImplicit _ _ n script _)
1644 case notFound kns (namesIn [] i script) of
1645 Nothing -> return (n:kns)
1646 Just name -> throwError (NoSuchVariable name)
1647 notFoundInDefault kns p = return ((pname p):kns)
1649 notFound :: [Name] -> [Name] -> Maybe Name
1650 notFound kns [] = Nothing
1651 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1652 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1654-- | Even if auto_implicits is off, we need to call this so we record
1655-- which arguments are implicit
1656implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1657implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1658 let (declimps, ns') = execState (imps True [] tm) ([], [])
1659 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1660 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1661 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1663 then (tm, reverse declimps)
1664 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1666 uvars = map ipair (filter uimplicit (using syn))
1667 pvars = syn_params syn
1669 inUsing n = n `elem` map fst uvars
1671 ipair (UImplicit x y) = (x, y)
1672 uimplicit (UImplicit _ _) = True
1675 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1676 | otherwise = x : dropAll xs ys
1679 -- Find names in argument position in a type, suitable for implicit
1681 -- Not the function position, but do everything else...
1682 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1683 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1685 imps top env ty@(PApp _ f as)
1686 = do (decls, ns) <- get
1687 let isn = nub (implNamesIn uvars ty)
1688 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1689 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1690 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1692 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1693 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1694 imps True (n:env) sc
1695 imps top env (PPi (Exp l _ _) n _ ty sc)
1696 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1697 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1699 (decls, ns) <- get -- ignore decls in HO types
1700 put (PExp (getPriority ist ty) l n Placeholder : decls,
1701 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1702 imps True (n:env) sc
1703 imps top env (PPi (Constraint l _) n _ ty sc)
1704 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1705 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1707 (decls, ns) <- get -- ignore decls in HO types
1708 put (PConstraint 10 l n Placeholder : decls,
1709 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1710 imps True (n:env) sc
1711 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1712 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1713 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1715 (decls, ns) <- get -- ignore decls in HO types
1716 put (PTacImplicit 10 l n scr Placeholder : decls,
1717 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1718 imps True (n:env) sc
1719 imps top env (PRewrite _ _ l r _)
1720 = do (decls, ns) <- get
1721 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1722 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1723 imps top env (PTyped l r)
1725 imps top env (PPair _ _ _ l r)
1726 = do (decls, ns) <- get
1727 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1728 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1729 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1730 = do (decls, ns) <- get
1731 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1732 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1733 imps top env (PDPair _ _ _ l t r)
1734 = do (decls, ns) <- get
1735 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1737 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1738 imps top env (PAlternative ms a as)
1739 = do (decls, ns) <- get
1740 let isn = concatMap (namesIn uvars ist) as
1741 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1742 imps top env (PLam fc n _ ty sc)
1743 = do imps False env ty
1744 imps False (n:env) sc
1745 imps top env (PHidden tm) = imps False env tm
1746 imps top env (PUnifyLog tm) = imps False env tm
1747 imps top env (PNoImplicits tm) = imps False env tm
1748 imps top env (PRunElab fc tm ns) = imps False env tm
1749 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1750 imps top env _ = return ()
1752 pibind using [] sc = sc
1753 pibind using (n:ns) sc
1754 = case lookup n using of
1755 Just ty -> PPi impl_gen
1756 n NoFC ty (pibind using ns sc)
1757 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1758 n NoFC Placeholder (pibind using ns sc)
1760-- | Add implicit arguments in function calls
1761addImplPat :: IState -> PTerm -> PTerm
1762addImplPat = addImpl' True [] [] []
1764addImplBound :: IState -> [Name] -> PTerm -> PTerm
1765addImplBound ist ns = addImpl' False ns [] [] ist
1767addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1768addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1770-- | Add the implicit arguments to applications in the term [Name]
1771-- gives the names to always expend, even when under a binder of that
1772-- name (this is to expand methods with implicit arguments in
1773-- dependent interfaces).
1774addImpl :: [Name] -> IState -> PTerm -> PTerm
1775addImpl = addImpl' False [] []
1777-- TODO: in patterns, don't add implicits to function names guarded by constructors
1778-- and *not* inside a PHidden
1780addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1781addImpl' inpat env infns imp_meths ist ptm
1782 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1784 topname = case ptm of
1786 PApp _ (PRef _ _ n) _ -> n
1787 _ -> sUN "" -- doesn't matter then
1789 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1790 ai inpat qq env ds (PRef fc fcs f)
1791 | f `elem` infns = PInferRef fc fcs f
1792 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1793 ai inpat qq env ds (PHidden (PRef fc hl f))
1794 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1795 ai inpat qq env ds (PRewrite fc by l r g)
1796 = let l' = ai inpat qq env ds l
1797 r' = ai inpat qq env ds r
1798 g' = fmap (ai inpat qq env ds) g in
1799 PRewrite fc by l' r' g'
1800 ai inpat qq env ds (PTyped l r)
1801 = let l' = ai inpat qq env ds l
1802 r' = ai inpat qq env ds r in
1804 ai inpat qq env ds (PPair fc hls p l r)
1805 = let l' = ai inpat qq env ds l
1806 r' = ai inpat qq env ds r in
1807 PPair fc hls p l' r'
1808 ai inpat qq env ds (PDPair fc hls p l t r)
1809 = let l' = ai inpat qq env ds l
1810 t' = ai inpat qq env ds t
1811 r' = ai inpat qq env ds r in
1812 PDPair fc hls p l' t' r'
1813 ai inpat qq env ds (PAlternative ms a as)
1814 = let as' = map (ai inpat qq env ds) as in
1815 PAlternative ms a as'
1816 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1817 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1818 = let as' = map (fmap (ai inpat qq env ds)) as in
1819 PApp fc (PInferRef ffc hl f) as'
1820 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1821 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1822 | not (f `elem` map fst env)
1823 = let as' = map (fmap (ai inpat qq env ds)) as in
1824 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1825 | Just (Just ty) <- lookup f env =
1826 let as' = map (fmap (ai inpat qq env ds)) as
1827 arity = getPArity ty in
1828 mkPApp fc arity ftm as'
1829 ai inpat qq env ds (PApp fc f as)
1830 = let f' = ai inpat qq env ds f
1831 as' = map (fmap (ai inpat qq env ds)) as in
1833 ai inpat qq env ds (PWithApp fc f a)
1834 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1835 ai inpat qq env ds (PCase fc c os)
1836 = let c' = ai inpat qq env ds c in
1837 -- leave lhs alone, because they get lifted into a new pattern match
1838 -- definition which is passed through addImpl again
1839 PCase fc c' (map aiCase os)
1842 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1844 -- Anything beginning with a lower case letter, not applied,
1845 -- and no namespace is a pattern variable
1846 patnames (PApp _ (PRef _ _ f) [])
1847 | implicitable f = [(f, Nothing)]
1848 patnames (PRef _ _ f)
1849 | implicitable f = [(f, Nothing)]
1850 patnames (PApp _ (PRef _ _ _) args)
1851 = concatMap patnames (map getTm args)
1852 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1853 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1854 patnames (PAs _ _ t) = patnames t
1855 patnames (PAlternative _ _ ts) = concatMap patnames ts
1859 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1860 (ai inpat qq env ds t)
1861 (ai inpat qq env ds f)
1863 -- If the name in a lambda is an unapplied data constructor name, do this
1864 -- as a 'case' instead because we'll expect to match on it
1865 ai inpat qq env ds (PLam fc n nfc ty sc)
1866 = if canBeDConName n (tt_ctxt ist)
1867 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1868 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1869 [(PRef fc [] n, sc)]))
1870 else let ty' = ai inpat qq env ds ty
1871 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1872 PLam fc n nfc ty' sc'
1873 ai inpat qq env ds (PLet fc n nfc ty val sc)
1874 = if canBeDConName n (tt_ctxt ist)
1875 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1876 else let ty' = ai inpat qq env ds ty
1877 val' = ai inpat qq env ds val
1878 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1879 PLet fc n nfc ty' val' sc'
1880 ai inpat qq env ds (PPi p n nfc ty sc)
1881 = let ty' = ai inpat qq env ds ty
1882 env' = if n `elem` imp_meths then env
1883 else ((n, Just ty) : env)
1884 sc' = ai inpat qq env' ds sc in
1886 ai inpat qq env ds (PGoal fc r n sc)
1887 = let r' = ai inpat qq env ds r
1888 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1890 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1891 -- Don't do PProof or PTactics since implicits get added when scope is
1892 -- properly known in ElabTerm.runTac
1893 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1894 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1895 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1896 (fmap (ai inpat True env ds) g)
1897 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1898 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1899 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1900 ai inpat qq env ds tm = tm
1902 handleErr (Left err) = PElabError err
1903 handleErr (Right x) = x
1905-- if in a pattern, and there are no arguments, and there's no possible
1906-- names with zero explicit arguments, don't add implicits.
1908aiFn :: Name -> Bool -> Bool -> Bool
1911 -> Name -- ^ function being applied
1913 -> [PArg] -- ^ initial arguments (if in a pattern)
1915aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1916 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1918 = case lookupDef f (tt_ctxt ist) of
1919 [] -> Right $ PPatvar ffc f
1920 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1921 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1922 if (not (vname f) || tcname f
1923 || any (conCaf (tt_ctxt ist)) ialts)
1924-- any constructor alts || any allImp ialts))
1925 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1926 else Right $ PPatvar ffc f
1927 where imp (PExp _ _ _ _) = False
1930 allImp xs = all imp xs
1932 unqualified (NS _ _) = False
1933 unqualified _ = True
1935 constructor (TyDecl (DCon _ _ _) _) = True
1936 constructor _ = False
1938 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1940 vname (UN n) = True -- non qualified
1943aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1944 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1945aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1946 -- This is where namespaces get resolved by adding PAlternative
1947 = do let ns = lookupCtxtName f (idris_implicits ist)
1948 let nh = filter (\(n, _) -> notHidden n) ns
1949 let ns' = case trimAlts ds nh of
1953 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1955 [] -> case metaVar f (map fst (idris_metavars ist)) of
1956 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1957 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1959 PAlternative [] (ExactlyOne True) $
1960 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1961 (insertImpl ns as)) alts
1963 -- if the name is in imp_meths, we should actually refer to the bound
1964 -- name rather than the global one after expanding implicits
1965 isImpName f f' | f `elem` imp_meths = f
1968 -- If it's a metavariable name, try to qualify it from the list of
1969 -- unsolved metavariables
1970 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1971 metaVar f (_ : ns) = metaVar f ns
1972 metaVar f [] = Nothing
1974 trimAlts [] alts = alts
1976 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1981 notHidden n = case getAccessibility n of
1987 = case lookupDefAccExact n False (tt_ctxt ist) of
1991 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1992 -> [PArg] -- ^ given arguments
1995 = let (as', badimpls) = partition (impIn ps) as in
1996 map addUnknownImp badimpls ++
1997 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1999 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2000 -> [PArg] -- parameters
2001 -> [PArg] -- explicit arguments
2002 -> [PArg] -- implicits given
2004 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2005 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2006 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2007 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2008 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2009 let rtc = PResolveTC fc in
2010 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2011 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2012 case find n imps [] of
2014 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2016 PImp p True l n Placeholder :
2017 insImpAcc (M.insert n Placeholder pnas) ps given imps
2018 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2019 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2020 case find n imps [] of
2022 PTacImplicit p l n sc tm :
2023 insImpAcc (M.insert n tm pnas) ps given imps'
2026 then PTacImplicit p l n sc Placeholder :
2027 insImpAcc (M.insert n Placeholder pnas) ps given imps
2028 else PTacImplicit p l n sc sc :
2029 insImpAcc (M.insert n sc pnas) ps given imps
2030 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2031 insImpAcc _ _ given imps = given ++ imps
2033 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2035 find n [] acc = Nothing
2036 find n (PImp _ _ _ n' t : gs) acc
2037 | n == n' = Just (t, reverse acc ++ gs)
2038 find n (PTacImplicit _ _ n' _ t : gs) acc
2039 | n == n' = Just (t, reverse acc ++ gs)
2040 find n (g : gs) acc = find n gs (g : acc)
2042-- | return True if the second argument is an implicit argument which
2043-- is expected in the implicits, or if it's not an implicit
2044impIn :: [PArg] -> PArg -> Bool
2045impIn ps (PExp _ _ _ _) = True
2046impIn ps (PConstraint _ _ _ _) = True
2047impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2049expArg (PExp _ _ _ _) = True
2050expArg (PConstraint _ _ _ _) = True
2053-- replace non-linear occurrences with _
2055stripLinear :: IState -> PTerm -> PTerm
2056stripLinear i tm = evalState (sl tm) [] where
2057 sl :: PTerm -> State [Name] PTerm
2059 | (_:_) <- lookupTy f (tt_ctxt i)
2060 = return $ PRef fc hl f
2061 | otherwise = do ns <- get
2063 then return $ PHidden (PRef fc hl f) -- Placeholder
2064 else do put (f : ns)
2065 return (PRef fc hl f)
2069 then return $ PHidden (PPatvar fc f) -- Placeholder
2070 else do put (f : ns)
2071 return (PPatvar fc f)
2072 -- Assumption is that variables are all the same in each alternative
2073 sl t@(PAlternative ms b as) = do ns <- get
2075 return (PAlternative ms b as')
2076 where slAlts ns (a : as) = do put ns
2080 slAlts ns [] = return []
2081 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2082 sl (PDPair fc hls p l t r) = do l' <- sl l
2085 return (PDPair fc hls p l' t' r')
2086 sl (PApp fc fn args) = do fn' <- case fn of
2087 -- Just the args, fn isn't matchable as a var
2088 PRef _ _ _ -> return fn
2090 args' <- mapM slA args
2091 return $ PApp fc fn' args'
2092 where slA (PImp p m l n t) = do t' <- sl t
2093 return $ PImp p m l n t'
2094 slA (PExp p l n t) = do t' <- sl t
2095 return $ PExp p l n t'
2096 slA (PConstraint p l n t)
2098 return $ PConstraint p l n t'
2099 slA (PTacImplicit p l n sc t)
2101 return $ PTacImplicit p l n sc t'
2104-- | Remove functions which aren't applied to anything, which must then
2105-- be resolved by unification. Assume names resolved and alternatives
2106-- filled in (so no ambiguity).
2107stripUnmatchable :: IState -> PTerm -> PTerm
2108stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2109 su :: PTerm -> PTerm
2110 su tm@(PRef fc hl f)
2111 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2113 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2114 not (implicitable f)
2116 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2117 not (implicitable f)
2119 su (PApp fc f@(PRef _ _ fn) args)
2120 -- here we use canBeDConName because the impossible pattern
2121 -- check will not necessarily fully resolve constructor names,
2122 -- and these bare names will otherwise get in the way of
2123 -- impossbility checking.
2124 | canBeDConName fn ctxt
2125 = PApp fc f (fmap (fmap su) args)
2127 = PHidden (PApp fc f args)
2128 su (PAlternative ms b alts)
2129 = let alts' = filter (/= Placeholder) (map su alts) in
2130 if null alts' then Placeholder
2131 else PAlternative ms b alts'
2132 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2133 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2134 su t@(PLam fc _ _ _ _) = PHidden t
2135 su t@(PPi _ _ _ _ _) = PHidden t
2136 su t@(PConstant _ c) | isTypeConst c = PHidden t
2141stripUnmatchable i tm = tm
2144mkPApp fc a f as = let rest = drop a as in
2145 if a == 0 then appRest fc f rest
2146 else appRest fc (PApp fc f (take a as)) rest
2149 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2153-- | Find 'static' argument positions
2154-- (the declared ones, plus any names in argument position in the declared
2156-- FIXME: It's possible that this really has to happen after elaboration
2157findStatics :: IState -> PTerm -> (PTerm, [Bool])
2158findStatics ist tm = let (ns, ss) = fs tm
2159 in runState (pos ns ss tm) []
2160 where fs (PPi p n fc t sc)
2161 | Static <- pstatic p
2162 = let (ns, ss) = fs sc in
2163 (namesIn [] ist t : ns, n : ss)
2164 | otherwise = let (ns, ss) = fs sc in
2168 inOne n ns = length (filter id (map (elem n) ns)) == 1
2170 pos ns ss (PPi p n fc t sc)
2171 | elem n ss = do sc' <- pos ns ss sc
2174 return (PPi (p { pstatic = Static }) n fc t sc')
2175 | otherwise = do sc' <- pos ns ss sc
2178 return (PPi p n fc t sc')
2179 pos ns ss t = return t
2181-- for 6.12/7 compatibility
2182data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2184instance Applicative (EitherErr a) where
2188instance Monad (EitherErr a) where
2191 (LeftErr e) >>= k = LeftErr e
2192 RightOK v >>= k = k v
2194toEither (LeftErr e) = Left e
2195toEither (RightOK ho) = Right ho
2197-- | Syntactic match of a against b, returning pair of variables in a
2198-- and what they match. Returns the pair that failed if not a match.
2199matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2200matchClause = matchClause' False
2202matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2203matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2204 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2206 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2209 match' x y = match (fullApp x) (fullApp y)
2210 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2211 | fi == txt "fromInteger" && b == txt "builtins",
2212 PConstant _ (I _) <- getTm x = match (getTm x) x'
2213 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2214 | fi == txt "fromInteger" && b == txt "builtins",
2215 PConstant _ (I _) <- getTm x = match (getTm x) x'
2216 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2217 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2218 match (PApp _ f args) (PApp _ f' args')
2219 | length args == length args'
2220 = do mf <- match' f f'
2221 ms <- zipWithM matchArg args args'
2222 return (mf ++ concat ms)
2223 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2224 match (PPatvar f n) xr = match (PRef f [f] n) xr
2225 match xr (PPatvar f n) = match xr (PRef f [f] n)
2226 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2227 match (PRef _ _ n) tm@(PRef _ _ n')
2228 | n == n' && not names &&
2229 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2230 || tm == Placeholder)
2232 -- if one namespace is missing, drop the other
2233 | n == n' || n == dropNS n' || dropNS n == n' = return []
2234 where dropNS (NS n _) = n
2236 match (PRef _ _ n) tm
2237 | not names && (not (isConName n (tt_ctxt i) ||
2238 isFnName n (tt_ctxt i)) || tm == Placeholder)
2240 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2241 = do ml <- match' l l'
2244 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2247 match (PTyped l r) x = match l x
2248 match x (PTyped l r) = match x l
2249 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2252 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2255 return (ml ++ mt ++ mr)
2256 match (PAlternative _ a as) (PAlternative _ a' as')
2257 = do ms <- zipWithM match' as as'
2259 match a@(PAlternative _ _ as) b
2260 = do let ms = zipWith match' as (repeat b)
2261 case (rights (map toEither ms)) of
2264 match (PCase _ _ _) _ = return [] -- lifted out
2265 match (PMetavar _ _) _ = return [] -- modified
2266 match (PInferRef _ _ _) _ = return [] -- modified
2267 match (PQuote _) _ = return []
2268 match (PProof _) _ = return []
2269 match (PTactics _) _ = return []
2270 match (PResolveTC _) (PResolveTC _) = return []
2271 match (PTrue _ _) (PTrue _ _) = return []
2272 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2275 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2278 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2279 mty <- match' ty ty'
2281 return (mt ++ mty ++ ms)
2282 match (PHidden x) (PHidden y)
2283 | RightOK xs <- match x y = return xs -- to collect variables
2284 | otherwise = return [] -- Otherwise hidden things are unmatchable
2286 | RightOK xs <- match x y = return xs
2287 | otherwise = return []
2289 | RightOK xs <- match x y = return xs
2290 | otherwise = return []
2291 match (PUnifyLog x) y = match' x y
2292 match x (PUnifyLog y) = match' x y
2293 match (PNoImplicits x) y = match' x y
2294 match x (PNoImplicits y) = match' x y
2295 match Placeholder _ = return []
2296 match _ Placeholder = return []
2297 match (PResolveTC _) _ = return []
2298 match a b | a == b = return []
2299 | otherwise = LeftErr (a, b)
2301 checkRpts (RightOK ms) = check ms where
2303 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2306 check (_:xs) = check xs
2308 checkRpts (LeftErr x) = Left x
2310substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2311substMatches ms = substMatchesShadow ms []
2313-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2314-- substMatchesShadow [] shs t = t
2315-- substMatchesShadow ((n,tm):ns) shs t
2316-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2318substMatch :: Name -> PTerm -> PTerm -> PTerm
2319substMatch n = substMatchShadow n []
2321substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2322substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2324substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2325substMatchesShadow nmap shs t = sm shs t where
2326 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2327 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2328 sm xs (PPi p x fc t sc)
2330 = let x' = nextName x in
2331 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2332 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2333 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2334 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2335 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2336 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2337 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2339 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2340 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2341 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2342 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2343 sm xs (PHidden x) = PHidden (sm xs x)
2344 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2345 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2346 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2347 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2350 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2353shadow :: Name -> Name -> PTerm -> PTerm
2354shadow n n' t = sm 0 t where
2355 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2356 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2357 | otherwise = PLam fc x xfc (sm 0 t) sc
2358 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2359 | otherwise = PPi p x fc (sm 0 t) sc
2360 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2361 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2362 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2363 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2364 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2365 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2366 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2367 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2368 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2369 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2370 sm 0 (PAlternative ms a as)
2371 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2372 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2373 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2374 sm 0 (PHidden x) = PHidden (sm 0 x)
2375 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2376 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2377 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2378 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2379 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2380 sm ql x = descend (sm ql) x
2382 shadowAlt p@(x, oldn) = (update x, update oldn)
2383 update oldn | n == oldn = n'
2386-- | Rename any binders which are repeated (so that we don't have to
2387-- mess about with shadowing anywhere else).
2388mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2389mkUniqueNames env shadows tm
2390 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2392 initMap = M.fromList shadows
2394 inScope :: S.Set Name
2395 inScope = S.fromList $ boundNamesIn tm
2397 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2398 return (arg { getTm = t' })
2400 -- Initialise the unique name with the environment length (so we're not
2401 -- looking for too long...)
2402 initN (UN n) l = UN $ txt (str n ++ show l)
2403 initN (MN i s) l = MN (i+l) s
2406 -- FIXME: Probably ought to do this for completeness! It's fine as
2407 -- long as there are no bindings inside tactics though.
2408 mkUniqT _ nmap tac = return tac
2410 mkUniq :: Int -- ^ The number of quotations that we're under
2411 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2412 mkUniq 0 nmap (PLam fc n nfc ty sc)
2416 then do let n' = uniqueNameSet (initN n (S.size env))
2417 (S.union env inScope)
2418 return (n', sc) -- shadow n n' sc)
2420 put (S.insert n' env)
2421 let nmap' = M.insert n n' nmap
2422 ty' <- mkUniq 0 nmap ty
2423 sc'' <- mkUniq 0 nmap' sc'
2424 return $! PLam fc n' nfc ty' sc''
2425 mkUniq 0 nmap (PPi p n fc ty sc)
2429 then do let n' = uniqueNameSet (initN n (S.size env))
2430 (S.union env inScope)
2431 return (n', sc) -- shadow n n' sc)
2433 put (S.insert n' env)
2434 let nmap' = M.insert n n' nmap
2435 ty' <- mkUniq 0 nmap ty
2436 sc'' <- mkUniq 0 nmap' sc'
2437 return $! PPi p n' fc ty' sc''
2438 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2442 then do let n' = uniqueNameSet (initN n (S.size env))
2443 (S.union env inScope)
2444 return (n', sc) -- shadow n n' sc)
2446 put (S.insert n' env)
2447 let nmap' = M.insert n n' nmap
2448 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2449 sc'' <- mkUniq 0 nmap' sc'
2450 return $! PLet fc n' nfc ty' val' sc''
2451 mkUniq 0 nmap (PApp fc t args)
2452 = do t' <- mkUniq 0 nmap t
2453 args' <- mapM (mkUniqA 0 nmap) args
2454 return $! PApp fc t' args'
2455 mkUniq 0 nmap (PAppBind fc t args)
2456 = do t' <- mkUniq 0 nmap t
2457 args' <- mapM (mkUniqA 0 nmap) args
2458 return $! PAppBind fc t' args'
2459 mkUniq 0 nmap (PCase fc t alts)
2460 = do t' <- mkUniq 0 nmap t
2461 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2462 return (x', y')) alts
2463 return $! PCase fc t' alts'
2464 mkUniq 0 nmap (PIfThenElse fc c t f)
2465 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2466 mkUniq 0 nmap (PPair fc hls p l r)
2467 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2468 return $! PPair fc hls p l' r'
2469 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2472 (n', sc') <- if n `S.member` env
2473 then do let n' = uniqueNameSet n (S.union env inScope)
2474 return (n', sc) -- shadow n n' sc)
2476 put (S.insert n' env)
2477 let nmap' = M.insert n n' nmap
2478 t' <- mkUniq 0 nmap t
2479 sc'' <- mkUniq 0 nmap' sc'
2480 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2481 mkUniq 0 nmap (PDPair fc hls p l t r)
2482 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2483 return $! PDPair fc hls p l' t' r'
2484 mkUniq 0 nmap (PAlternative ns b as)
2485 -- store the nmap and defer the rest until we've pruned the set
2486 -- during elaboration
2487 = return $ PAlternative (ns ++ M.toList nmap) b as
2488 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2489 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2490 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2491 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2492 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2493 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2494 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2495 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2496 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2497 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2500 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2502 mkUniq ql nmap (PQuasiquote tm ty) =
2503 do tm' <- mkUniq (ql + 1) nmap tm
2505 Nothing -> return Nothing
2506 Just t -> fmap Just $ mkUniq ql nmap t
2507 return $! PQuasiquote tm' ty'
2508 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2510 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2513getFile :: Opt -> Maybe String
2514getFile (Filename str) = Just str
2517getBC :: Opt -> Maybe String
2518getBC (BCAsm str) = Just str
2521getOutput :: Opt -> Maybe String
2522getOutput (Output str) = Just str
2523getOutput _ = Nothing
2525getIBCSubDir :: Opt -> Maybe String
2526getIBCSubDir (IBCSubDir str) = Just str
2527getIBCSubDir _ = Nothing
2529getImportDir :: Opt -> Maybe String
2530getImportDir (ImportDir str) = Just str
2531getImportDir _ = Nothing
2533getSourceDir :: Opt -> Maybe String
2534getSourceDir (SourceDir str) = Just str
2535getSourceDir _ = Nothing
2537getPkgDir :: Opt -> Maybe String
2538getPkgDir (Pkg str) = Just str
2539getPkgDir _ = Nothing
2541getPkg :: Opt -> Maybe (Bool, String)
2542getPkg (PkgBuild str) = Just (False, str)
2543getPkg (PkgInstall str) = Just (True, str)
2546getPkgClean :: Opt -> Maybe String
2547getPkgClean (PkgClean str) = Just str
2548getPkgClean _ = Nothing
2550getPkgREPL :: Opt -> Maybe String
2551getPkgREPL (PkgREPL str) = Just str
2552getPkgREPL _ = Nothing
2554getPkgCheck :: Opt -> Maybe String
2555getPkgCheck (PkgCheck str) = Just str
2556getPkgCheck _ = Nothing
2558-- | Returns None if given an Opt which is not PkgMkDoc
2559-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2560getPkgMkDoc :: Opt -- ^ Opt to extract
2561 -> Maybe (Bool, String) -- ^ Result
2562getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2563getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2564getPkgMkDoc _ = Nothing
2566getPkgTest :: Opt -- ^ the option to extract
2567 -> Maybe String -- ^ the package file to test
2568getPkgTest (PkgTest f) = Just f
2569getPkgTest _ = Nothing
2571getCodegen :: Opt -> Maybe Codegen
2572getCodegen (UseCodegen x) = Just x
2573getCodegen _ = Nothing
2575getCodegenArgs :: Opt -> Maybe String
2576getCodegenArgs (CodegenArgs args) = Just args
2577getCodegenArgs _ = Nothing
2579getConsoleWidth :: Opt -> Maybe ConsoleWidth
2580getConsoleWidth (UseConsoleWidth x) = Just x
2581getConsoleWidth _ = Nothing
2584getExecScript :: Opt -> Maybe String
2585getExecScript (InterpretScript expr) = Just expr
2586getExecScript _ = Nothing
2588getPkgIndex :: Opt -> Maybe FilePath
2589getPkgIndex (PkgIndex file) = Just file
2590getPkgIndex _ = Nothing
2592getEvalExpr :: Opt -> Maybe String
2593getEvalExpr (EvalExpr expr) = Just expr
2594getEvalExpr _ = Nothing
2596getOutputTy :: Opt -> Maybe OutputType
2597getOutputTy (OutputTy t) = Just t
2598getOutputTy _ = Nothing
2600getLanguageExt :: Opt -> Maybe LanguageExt
2601getLanguageExt (Extension e) = Just e
2602getLanguageExt _ = Nothing
2604getTriple :: Opt -> Maybe String
2605getTriple (TargetTriple x) = Just x
2606getTriple _ = Nothing
2608getCPU :: Opt -> Maybe String
2609getCPU (TargetCPU x) = Just x
2612getOptLevel :: Opt -> Maybe Int
2613getOptLevel (OptLevel x) = Just x
2614getOptLevel _ = Nothing
2616getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2617getOptimisation (AddOpt p) = Just (True, p)
2618getOptimisation (RemoveOpt p) = Just (False, p)
2619getOptimisation _ = Nothing
2621getColour :: Opt -> Maybe Bool
2622getColour (ColourREPL b) = Just b
2623getColour _ = Nothing
2625getClient :: Opt -> Maybe String
2626getClient (Client x) = Just x
2627getClient _ = Nothing
2629-- Get the first valid port
2630getPort :: [Opt] -> Maybe REPLPort
2632getPort (Port p : xs) = Just p
2633getPort (_ : xs) = getPort xs
2635opt :: (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