2Module : Idris.AbsSyntax
3Description : Provides Idris' core data definitions and utility code.
6Maintainer : The Idris Community.
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
9 TypeSynonymInstances, PatternGuards #-}
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
13 , module Idris.AbsSyntaxTree
17import Idris.Core.Evaluate
18import Idris.Core.Elaborate hiding (Tactic(..))
19import Idris.Core.Typecheck
20import Idris.AbsSyntaxTree
22import Idris.Docstrings
23import Idris.IdeMode hiding (Opt(..))
24import IRTS.CodegenCommon
25import Util.DynamicLinker
27import System.Console.Haskeline
29import System.Directory (canonicalizePath, doesFileExist)
31import Control.Applicative
32import Control.Monad (liftM3)
33import Control.Monad.State
35import Data.List hiding (insert,union)
37import qualified Data.Text as T
39import qualified Data.Map as M
41import qualified Data.Set as S
42import Data.Word (Word)
44import Data.Generics.Uniplate.Data (descend, descendM)
48import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
50import Network (PortID(PortNumber))
56getContext :: Idris Context
57getContext = do i <- getIState; return (tt_ctxt i)
59forCodegen :: Codegen -> [(Codegen, a)] -> [a]
60forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
62 eqLang (Via _ x) (Via _ y) = x == y
63 eqLang Bytecode Bytecode = True
66getObjectFiles :: Codegen -> Idris [FilePath]
67getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
69addObjectFile :: Codegen -> FilePath -> Idris ()
70addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
72getLibs :: Codegen -> Idris [String]
73getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
75addLib :: Codegen -> String -> Idris ()
76addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
78getFlags :: Codegen -> Idris [String]
79getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
81addFlag :: Codegen -> String -> Idris ()
82addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
84addDyLib :: [String] -> Idris (Either DynamicLib String)
85addDyLib libs = do i <- getIState
86 let ls = idris_dynamic_libs i
87 let importdirs = opt_importdirs (idris_options i)
88 case mapMaybe (findDyLib ls) libs of
89 x:_ -> return (Left x)
91 handle <- lift . lift .
92 mapM (\l -> catchIO (tryLoadLib importdirs l)
93 (\_ -> return Nothing)) $ libs
95 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
96 intercalate "," libs ++ "\"")
97 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
99 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
100 findDyLib [] l = Nothing
101 findDyLib (lib:libs) l | l == lib_name lib = Just lib
102 | otherwise = findDyLib libs l
104getAutoImports :: Idris [FilePath]
105getAutoImports = do i <- getIState
106 return (opt_autoImport (idris_options i))
108addAutoImport :: FilePath -> Idris ()
109addAutoImport fp = do i <- getIState
110 let opts = idris_options i
111 let autoimps = opt_autoImport opts
112 put (i { idris_options = opts { opt_autoImport =
113 fp : opt_autoImport opts } } )
115addDefinedName :: Name -> Idris ()
116addDefinedName n = do ist <- getIState
117 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
119getDefinedNames :: Idris [Name]
120getDefinedNames = do ist <- getIState
121 return (S.toList (idris_inmodule ist))
123addTT :: Term -> Idris (Maybe Term)
124addTT t = do ist <- getIState
125 case M.lookup t (idris_ttstats ist) of
126 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
127 putIState $ ist { idris_ttstats = tt' }
129 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
130 putIState $ ist { idris_ttstats = tt' }
134dumpTT = do ist <- get
135 let sts = sortBy count (M.toList (idris_ttstats ist))
139 count (_,x) (_,y) = compare y x
140 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
142addHdr :: Codegen -> String -> Idris ()
143addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
145addImported :: Bool -> FilePath -> Idris ()
148 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
150addLangExt :: LanguageExt -> Idris ()
151addLangExt TypeProviders = do i <- getIState
153 idris_language_extensions = TypeProviders : idris_language_extensions i
155addLangExt ErrorReflection = do i <- getIState
157 idris_language_extensions = ErrorReflection : idris_language_extensions i
160-- | Transforms are organised by the function being applied on the lhs
161-- of the transform, to make looking up appropriate transforms quicker
162addTrans :: Name -> (Term, Term) -> Idris ()
165 let t' = case lookupCtxtExact basefn (idris_transforms i) of
166 Just def -> (t : def)
168 putIState $ i { idris_transforms = addDef basefn t'
169 (idris_transforms i) }
171addErrRev :: (Term, Term) -> Idris ()
172addErrRev t = do i <- getIState
173 putIState $ i { idris_errRev = t : idris_errRev i }
175addErasureUsage :: Name -> Int -> Idris ()
176addErasureUsage n i = do ist <- getIState
177 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
179addExport :: Name -> Idris ()
180addExport n = do ist <- getIState
181 putIState $ ist { idris_exports = n : idris_exports ist }
183addUsedName :: FC -> Name -> Name -> Idris ()
185 = do ist <- getIState
186 case lookupTyName n (tt_ctxt ist) of
187 [(n', ty)] -> addUsage n' 0 ty
188 [] -> throwError (At fc (NoSuchVariable n))
189 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
190 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
192 | otherwise = addUsage n (i + 1) sc
193 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
195getErasureUsage :: Idris [(Name, Int)]
196getErasureUsage = do ist <- getIState;
197 return (idris_erasureUsed ist)
199getExports :: Idris [Name]
200getExports = do ist <- getIState
201 return (idris_exports ist)
203totcheck :: (FC, Name) -> Idris ()
204totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
206defer_totcheck :: (FC, Name) -> Idris ()
209 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
211clear_totcheck :: Idris ()
212clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
214setFlags :: Name -> [FnOpt] -> Idris ()
215setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
217setFnInfo :: Name -> FnInfo -> Idris ()
218setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
220setAccessibility :: Name -> Accessibility -> Idris ()
223 let ctxt = setAccess n a (tt_ctxt i)
224 putIState $ i { tt_ctxt = ctxt }
226-- | get the accessibility of a name outside this module
227getFromHideList :: Name -> Idris (Maybe Accessibility)
228getFromHideList n = do i <- getIState
229 return $ lookupCtxtExact n (hide_list i)
231setTotality :: Name -> Totality -> Idris ()
234 let ctxt = setTotal n a (tt_ctxt i)
235 putIState $ i { tt_ctxt = ctxt }
237setInjectivity :: Name -> Injectivity -> Idris ()
240 let ctxt = setInjective n a (tt_ctxt i)
241 putIState $ i { tt_ctxt = ctxt }
243getTotality :: Name -> Idris Totality
246 case lookupTotal n (tt_ctxt i) of
248 _ -> return (Total [])
250-- Get coercions which might return the required type
251getCoercionsTo :: IState -> Type -> [Name]
253 let cs = idris_coercions i
254 (fn,_) = unApply (getRetTy ty) in
256 where findCoercions t [] = []
257 findCoercions t (n : ns) =
258 let ps = case lookupTy n (tt_ctxt i) of
259 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
260 (t', _) -> [n | t == t']
262 ps ++ findCoercions t ns
264addToCG :: Name -> CGInfo -> Idris ()
267 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
269addCalls :: Name -> [Name] -> Idris ()
272 case lookupCtxtExact n (idris_callgraph i) of
273 Nothing -> addToCG n (CGInfo calls [] [])
274 Just (CGInfo cs scg used) ->
275 addToCG n (CGInfo (nub (calls ++ cs)) scg used)
277addTyInferred :: Name -> Idris ()
280 putIState $ i { idris_tyinfodata =
281 addDef n TIPartial (idris_tyinfodata i) }
283addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
284addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
285 mapM_ addConstraint ts
287 where addConstraint (x, y) = findMVApps x y
290 = do let (fx, argsx) = unApply x
291 let (fy, argsy) = unApply y
296 else mapM_ addConstraint (zip argsx argsy)
298 tryAddMV (P _ mv _) y =
300 case lookup mv (idris_metavars ist) of
301 Just _ -> addConstraintRule mv y
303 tryAddMV _ _ = return ()
305 addConstraintRule :: Name -> Term -> Idris ()
306 addConstraintRule n t
308 logLvl 1 $ "TI constraint: " ++ show (n, t)
309 case lookupCtxt n (idris_tyinfodata ist) of
311 do mapM_ (checkConsistent t) ts
312 let ti' = addDef n (TISolution (t : ts))
313 (idris_tyinfodata ist)
314 put $ ist { idris_tyinfodata = ti' }
316 do let ti' = addDef n (TISolution [t])
317 (idris_tyinfodata ist)
318 put $ ist { idris_tyinfodata = ti' }
320 -- Check a solution is consistent with previous solutions
321 -- Meaning: If heads are both data types, they had better be the
323 checkConsistent :: Term -> Term -> Idris ()
324 checkConsistent x y =
325 do let (fx, _) = unApply x
326 let (fy, _) = unApply y
328 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
329 (P (TCon _ _) n _, Constant _) -> errWhen True
330 (Constant _, P (TCon _ _) n' _) -> errWhen True
331 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
336 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
337 errWhen False = return ()
339isTyInferred :: Name -> Idris Bool
342 case lookupCtxt n (idris_tyinfodata i) of
343 [TIPartial] -> return True
346-- | Adds error handlers for a particular function and argument. If
347-- names are ambiguous, all matching handlers are updated.
348addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
349addFunctionErrorHandlers f arg hs =
351 let oldHandlers = idris_function_errorhandlers i
352 let newHandlers = flip (addDef f) oldHandlers $
353 case lookupCtxtExact f oldHandlers of
354 Nothing -> M.singleton arg (S.fromList hs)
355 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
356 -- will always be one of those two, thus no extra case
357 putIState $ i { idris_function_errorhandlers = newHandlers }
359getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
360getFunctionErrorHandlers f arg = do i <- getIState
361 return . maybe [] S.toList $
362 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
365-- | Trace all the names in a call graph starting at the given name
366getAllNames :: Name -> Idris [Name]
367getAllNames n = allNames [] n
369allNames :: [Name] -> Name -> Idris [Name]
370allNames ns n | n `elem` ns = return []
371allNames ns n = do i <- getIState
372 case lookupCtxtExact n (idris_callgraph i) of
373 Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')
374 return (nub (n : concat more))
377addCoercion :: Name -> Idris ()
378addCoercion n = do i <- getIState
379 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
381addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
384 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
386addNameHint :: Name -> Name -> Idris ()
389 ty' <- case lookupCtxtName ty (idris_implicits i) of
390 [(tyn, _)] -> return tyn
391 [] -> throwError (NoSuchVariable ty)
392 tyns -> throwError (CantResolveAlts (map fst tyns))
393 let ns' = case lookupCtxt ty' (idris_namehints i) of
396 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
398getNameHints :: IState -> Name -> [Name]
399getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
401 case lookupCtxt n (idris_namehints i) of
405addDeprecated :: Name -> String -> Idris ()
406addDeprecated n reason = do
408 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
410getDeprecated :: Name -> Idris (Maybe String)
413 return $ lookupCtxtExact n (idris_deprecated i)
416addFragile :: Name -> String -> Idris ()
417addFragile n reason = do
419 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
421getFragile :: Name -> Idris (Maybe String)
424 return $ lookupCtxtExact n (idris_fragile i)
426push_estack :: Name -> Bool -> Idris ()
429 putIState (i { elab_stack = (n, impl) : elab_stack i })
431pop_estack :: Idris ()
432pop_estack = do i <- getIState
433 putIState (i { elab_stack = ptail (elab_stack i) })
437-- | Add an interface implementation function.
439-- Precondition: the implementation should have the correct type.
441-- Dodgy hack 1: Put integer implementations first in the list so they are
442-- resolved by default.
444-- Dodgy hack 2: put constraint chasers (ParentN) last
445addImplementation :: Bool -- ^ whether the name is an Integer implementation
446 -> Bool -- ^ whether to include the implementation in implementation search
447 -> Name -- ^ the name of the interface
448 -> Name -- ^ the name of the implementation
450addImplementation int res n i
451 = do ist <- getIState
452 case lookupCtxt n (idris_interfaces ist) of
453 [CI a b c d e ins fds] ->
454 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_interfaces ist)
455 putIState $ ist { idris_interfaces = cs }
456 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_interfaces ist)
457 putIState $ ist { idris_interfaces = cs }
458 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
459 addI i ins | int = (i, res) : ins
460 | chaser n = ins ++ [(i, res)]
461 | otherwise = insI i ins
462 insI i [] = [(i, res)]
463 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
464 | otherwise = n : insI i ns
466 chaser (SN (ParentN _ _)) = True
467 chaser (NS n _) = chaser n
470-- | Add a privileged implementation - one which implementation search will
471-- happily resolve immediately if it is type correct This is used for
472-- naming parent implementations when defining an implementation with
473-- constraints. Returns the old list, so we can revert easily at the
475addOpenImpl :: [Name] -> Idris [Name]
476addOpenImpl ns = do ist <- getIState
477 ns' <- mapM (checkValid ist) ns
478 let open = idris_openimpls ist
479 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
483 = case lookupCtxtName n (idris_implicits ist) of
484 [(n', _)] -> return n'
485 [] -> throwError (NoSuchVariable n)
486 more -> throwError (CantResolveAlts (map fst more))
488setOpenImpl :: [Name] -> Idris ()
489setOpenImpl ns = do ist <- getIState
490 putIState $ ist { idris_openimpls = ns }
492getOpenImpl :: Idris [Name]
493getOpenImpl = do ist <- getIState
494 return (idris_openimpls ist)
496addInterface :: Name -> InterfaceInfo -> Idris ()
498 = do ist <- getIState
499 let i' = case lookupCtxt n (idris_interfaces ist) of
500 [c] -> c { interface_implementations = interface_implementations i }
502 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
504addRecord :: Name -> RecordInfo -> Idris ()
505addRecord n ri = do ist <- getIState
506 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
508addAutoHint :: Name -> Name -> Idris ()
511 case lookupCtxtExact n (idris_autohints ist) of
513 do let hs = addDef n [hint] (idris_autohints ist)
514 putIState $ ist { idris_autohints = hs }
516 do let hs = addDef n (hint : nhints) (idris_autohints ist)
517 putIState $ ist { idris_autohints = hs }
519getAutoHints :: Name -> Idris [Name]
520getAutoHints n = do ist <- getIState
521 case lookupCtxtExact n (idris_autohints ist) of
525addIBC :: IBCWrite -> Idris ()
528 when (notDef (ibc_write i)) $
529 putIState $ i { ibc_write = ibc : ibc_write i }
530 where notDef [] = True
531 notDef (IBCDef n': is) | n == n' = False
532 notDef (_ : is) = notDef is
533addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
536clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
537 idris_inmodule = S.empty }
539resetNameIdx :: Idris ()
540resetNameIdx = do i <- getIState
541 put (i { idris_nameIdx = (0, emptyContext) })
543-- | Used to preserve sharing of names
544addNameIdx :: Name -> Idris (Int, Name)
545addNameIdx n = do i <- getIState
546 let (i', x) = addNameIdx' i n
550addNameIdx' :: IState -> Name -> (IState, (Int, Name))
552 = let idxs = snd (idris_nameIdx i) in
553 case lookupCtxt n idxs of
555 _ -> let i' = fst (idris_nameIdx i) + 1 in
556 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
558getSymbol :: Name -> Idris Name
559getSymbol n = do i <- getIState
560 case M.lookup n (idris_symbols i) of
562 Nothing -> do let sym' = M.insert n n (idris_symbols i)
563 put (i { idris_symbols = sym' })
566getHdrs :: Codegen -> Idris [String]
567getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
569getImported :: Idris [(FilePath, Bool)]
570getImported = do i <- getIState; return (idris_imported i)
572setErrSpan :: FC -> Idris ()
573setErrSpan x = do i <- getIState;
575 Nothing -> putIState $ i { errSpan = Just x }
579clearErr = do i <- getIState
580 putIState $ i { errSpan = Nothing }
582getSO :: Idris (Maybe String)
583getSO = do i <- getIState
584 return (compiled_so i)
586setSO :: Maybe String -> Idris ()
587setSO s = do i <- getIState
588 putIState (i { compiled_so = s })
590getIState :: Idris IState
593putIState :: IState -> Idris ()
596updateIState :: (IState -> IState) -> Idris ()
597updateIState f = do i <- getIState
600withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
601withContext ctx name dflt action = do
603 case lookupCtxt name (ctx ist) of
607withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
608withContext_ ctx name action = withContext ctx name () action
610-- | A version of liftIO that puts errors into the exception type of
612runIO :: IO a -> Idris a
613runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
614-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
616-- Issue #1738 on the issue tracker.
617-- https://github.com/idris-lang/Idris-dev/issues/1738
620getName = do i <- getIState;
621 let idx = idris_name i;
622 putIState (i { idris_name = idx + 1 })
625-- | InternalApp keeps track of the real function application for
626-- making case splits from, not the application the programmer wrote,
627-- which doesn't have the whole context in any case other than top
629addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
632 -- We canonicalise the path to make "./Test/Module.idr" equal
633 -- to "Test/Module.idr"
634 exists <- runIO $ doesFileExist fp
636 do fp' <- runIO $ canonicalizePath fp
637 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
639getInternalApp :: FilePath -> Int -> Idris PTerm
640getInternalApp fp l = do i <- getIState
641 -- We canonicalise the path to make
642 -- "./Test/Module.idr" equal to
644 exists <- runIO $ doesFileExist fp
646 then do fp' <- runIO $ canonicalizePath fp
647 case lookup (fp', l) (idris_lineapps i) of
649 Nothing -> return Placeholder
650 -- TODO: What if it's not there?
651 else return Placeholder
653-- | Pattern definitions are only used for coverage checking, so erase
654-- them when we're done
655clearOrigPats :: Idris ()
656clearOrigPats = do i <- get
657 let ps = idris_patdefs i
658 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
659 put (i { idris_patdefs = ps' })
661-- | Erase types from Ps in the context (basically ending up with
662-- what's in the .ibc, which is all we need after all the analysis is
664clearPTypes :: Idris ()
665clearPTypes = do i <- get
667 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
668 where pErase (CaseOp c t tys orig tot cds)
669 = CaseOp c t tys orig [] (pErase' cds)
671 pErase' (CaseDefs _ (cs, c) _ rs)
672 = let c' = (cs, fmap pEraseType c) in
675checkUndefined :: FC -> Name -> Idris ()
679 (_:_) -> throwError . Msg $ show fc ++ ":" ++
680 show n ++ " already defined"
683isUndefined :: FC -> Name -> Idris Bool
686 case lookupTyExact n i of
687 Just _ -> return False
690setContext :: Context -> Idris ()
691setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
693updateContext :: (Context -> Context) -> Idris ()
694updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
696addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
697addConstraints fc (v, cs)
698 = do tit <- typeInType
702 let ctxt' = ctxt { next_tvar = v }
703 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
704 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
707 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
708 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
709 insertAll ((c, fc) : cs) ics
710 = insertAll cs $ S.insert (ConstraintFC c fc) ics
712addDeferred = addDeferred' Ref
713addDeferredTyCon = addDeferred' (TCon 0 0)
715-- | Save information about a name that is not yet defined
716addDeferred' :: NameType
717 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
718 -- ^ The Name is the name being made into a metavar,
719 -- the Int is the number of vars that are part of a
720 -- putative proof context, the Maybe Name is the
721 -- top-level function containing the new metavariable,
722 -- the Type is its type, and the Bool is whether :p is
726 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
727 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
729 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
730 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
733 -- 'tidyNames' is to generate user accessible names in case they are
734 -- needed in tactic scripts
735 tidyNames used (Bind (MN i x) b sc)
736 = let n' = uniqueNameSet (UN x) used in
737 Bind n' b $ tidyNames (S.insert n' used) sc
738 tidyNames used (Bind n b sc)
739 = let n' = uniqueNameSet n used in
740 Bind n' b $ tidyNames (S.insert n' used) sc
743solveDeferred :: FC -> Name -> Idris ()
746 case lookup n (idris_metavars i) of
747 Just (_, _, _, _, False) ->
748 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
749 _ -> putIState $ i { idris_metavars =
750 filter (\(n', _) -> n/=n')
753 filter (notMV n) (ibc_write i)
755 where notMV n (IBCMetavar n') = not (n == n')
758getUndefined :: Idris [Name]
759getUndefined = do i <- getIState
760 return (map fst (idris_metavars i) \\ primDefs)
762isMetavarName :: Name -> IState -> Bool
764 = case lookupNames n (tt_ctxt ist) of
765 (t:_) -> isJust $ lookup t (idris_metavars ist)
768getWidth :: Idris ConsoleWidth
769getWidth = fmap idris_consolewidth getIState
771setWidth :: ConsoleWidth -> Idris ()
772setWidth w = do ist <- getIState
773 put ist { idris_consolewidth = w }
775setDepth :: Maybe Int -> Idris ()
776setDepth d = do ist <- getIState
777 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
779typeDescription :: String
780typeDescription = "The type of types"
783type1Doc :: Doc OutputAnnotation
784type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
787isetPrompt :: String -> Idris ()
788isetPrompt p = do i <- getIState
789 case idris_outputmode i of
790 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
792-- | Tell clients how much was parsed and loaded
793isetLoadedRegion :: Idris ()
794isetLoadedRegion = do i <- getIState
795 let span = idris_parsedSpan i
798 case idris_outputmode i of
800 runIO . hPutStrLn h $
801 convSExp "set-loaded-region" fc n
804setLogLevel :: Int -> Idris ()
805setLogLevel l = do i <- getIState
806 let opts = idris_options i
807 let opt' = opts { opt_logLevel = l }
808 putIState $ i { idris_options = opt' }
810setLogCats :: [LogCat] -> Idris ()
813 let opts = idris_options i
814 let opt' = opts { opt_logcats = cs }
815 putIState $ i { idris_options = opt' }
817setCmdLine :: [Opt] -> Idris ()
818setCmdLine opts = do i <- getIState
819 let iopts = idris_options i
820 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
822getCmdLine :: Idris [Opt]
823getCmdLine = do i <- getIState
824 return (opt_cmdline (idris_options i))
826getDumpHighlighting :: Idris Bool
827getDumpHighlighting = do ist <- getIState
828 return (findC (opt_cmdline (idris_options ist)))
829 where findC = elem DumpHighlights
831getDumpDefun :: Idris (Maybe FilePath)
832getDumpDefun = do i <- getIState
833 return $ findC (opt_cmdline (idris_options i))
834 where findC [] = Nothing
835 findC (DumpDefun x : _) = Just x
836 findC (_ : xs) = findC xs
838getDumpCases :: Idris (Maybe FilePath)
839getDumpCases = do i <- getIState
840 return $ findC (opt_cmdline (idris_options i))
841 where findC [] = Nothing
842 findC (DumpCases x : _) = Just x
843 findC (_ : xs) = findC xs
846logLevel = do i <- getIState
847 return (opt_logLevel (idris_options i))
849setAutoImpls :: Bool -> Idris ()
850setAutoImpls b = do i <- getIState
851 let opts = idris_options i
852 let opt' = opts { opt_autoimpls = b }
853 putIState $ i { idris_options = opt' }
855getAutoImpls :: Idris Bool
856getAutoImpls = do i <- getIState
857 return (opt_autoimpls (idris_options i))
859setErrContext :: Bool -> Idris ()
860setErrContext t = do i <- getIState
861 let opts = idris_options i
862 let opts' = opts { opt_errContext = t }
863 putIState $ i { idris_options = opts' }
865errContext :: Idris Bool
866errContext = do i <- getIState
867 return (opt_errContext (idris_options i))
869getOptimise :: Idris [Optimisation]
870getOptimise = do i <- getIState
871 return (opt_optimise (idris_options i))
873setOptimise :: [Optimisation] -> Idris ()
874setOptimise newopts = do i <- getIState
875 let opts = idris_options i
876 let opts' = opts { opt_optimise = newopts }
877 putIState $ i { idris_options = opts' }
879addOptimise :: Optimisation -> Idris ()
880addOptimise opt = do opts <- getOptimise
881 setOptimise (nub (opt : opts))
883removeOptimise :: Optimisation -> Idris ()
884removeOptimise opt = do opts <- getOptimise
885 setOptimise ((nub opts) \\ [opt])
887-- | Set appropriate optimisation set for the given level. We only
888-- have one optimisation that is configurable at the moment, however!
889setOptLevel :: Int -> Idris ()
890setOptLevel n | n <= 0 = setOptimise []
891setOptLevel 1 = setOptimise []
892setOptLevel 2 = setOptimise [PETransform]
893setOptLevel n | n >= 3 = setOptimise [PETransform]
896useREPL = do i <- getIState
897 return (opt_repl (idris_options i))
899setREPL :: Bool -> Idris ()
900setREPL t = do i <- getIState
901 let opts = idris_options i
902 let opt' = opts { opt_repl = t }
903 putIState $ i { idris_options = opt' }
905showOrigErr :: Idris Bool
906showOrigErr = do i <- getIState
907 return (opt_origerr (idris_options i))
909setShowOrigErr :: Bool -> Idris ()
910setShowOrigErr b = do i <- getIState
911 let opts = idris_options i
912 let opt' = opts { opt_origerr = b }
913 putIState $ i { idris_options = opt' }
915setAutoSolve :: Bool -> Idris ()
916setAutoSolve b = do i <- getIState
917 let opts = idris_options i
918 let opt' = opts { opt_autoSolve = b }
919 putIState $ i { idris_options = opt' }
921setNoBanner :: Bool -> Idris ()
922setNoBanner n = do i <- getIState
923 let opts = idris_options i
924 let opt' = opts { opt_nobanner = n }
925 putIState $ i { idris_options = opt' }
927getNoBanner :: Idris Bool
928getNoBanner = do i <- getIState
929 let opts = idris_options i
930 return (opt_nobanner opts)
932setEvalTypes :: Bool -> Idris ()
933setEvalTypes n = do i <- getIState
934 let opts = idris_options i
935 let opt' = opts { opt_evaltypes = n }
936 putIState $ i { idris_options = opt' }
938getDesugarNats :: Idris Bool
939getDesugarNats = do i <- getIState
940 let opts = idris_options i
941 return (opt_desugarnats opts)
944setDesugarNats :: Bool -> Idris ()
945setDesugarNats n = do i <- getIState
946 let opts = idris_options i
947 let opt' = opts { opt_desugarnats = n }
948 putIState $ i { idris_options = opt' }
950setQuiet :: Bool -> Idris ()
951setQuiet q = do i <- getIState
952 let opts = idris_options i
953 let opt' = opts { opt_quiet = q }
954 putIState $ i { idris_options = opt' }
956getQuiet :: Idris Bool
957getQuiet = do i <- getIState
958 let opts = idris_options i
959 return (opt_quiet opts)
961setCodegen :: Codegen -> Idris ()
962setCodegen t = do i <- getIState
963 let opts = idris_options i
964 let opt' = opts { opt_codegen = t }
965 putIState $ i { idris_options = opt' }
967codegen :: Idris Codegen
968codegen = do i <- getIState
969 return (opt_codegen (idris_options i))
972setOutputTy :: OutputType -> Idris ()
973setOutputTy t = do i <- getIState
974 let opts = idris_options i
975 let opt' = opts { opt_outputTy = t }
976 putIState $ i { idris_options = opt' }
978outputTy :: Idris OutputType
979outputTy = do i <- getIState
980 return $ opt_outputTy $ idris_options i
982setIdeMode :: Bool -> Handle -> Idris ()
983setIdeMode True h = do i <- getIState
984 putIState $ i { idris_outputmode = IdeMode 0 h
985 , idris_colourRepl = False
987setIdeMode False _ = return ()
989setTargetTriple :: String -> Idris ()
990setTargetTriple t = do i <- getIState
991 let opts = idris_options i
992 opt' = opts { opt_triple = t }
993 putIState $ i { idris_options = opt' }
995targetTriple :: Idris String
996targetTriple = do i <- getIState
997 return (opt_triple (idris_options i))
999setTargetCPU :: String -> Idris ()
1000setTargetCPU t = do i <- getIState
1001 let opts = idris_options i
1002 opt' = opts { opt_cpu = t }
1003 putIState $ i { idris_options = opt' }
1005targetCPU :: Idris String
1006targetCPU = do i <- getIState
1007 return (opt_cpu (idris_options i))
1009verbose :: Idris Bool
1010verbose = do i <- getIState
1011 -- Quietness overrides verbosity
1012 return (not (opt_quiet (idris_options i)) &&
1013 opt_verbose (idris_options i))
1015setVerbose :: Bool -> Idris ()
1016setVerbose t = do i <- getIState
1017 let opts = idris_options i
1018 let opt' = opts { opt_verbose = t }
1019 putIState $ i { idris_options = opt' }
1021typeInType :: Idris Bool
1022typeInType = do i <- getIState
1023 return (opt_typeintype (idris_options i))
1025setTypeInType :: Bool -> Idris ()
1026setTypeInType t = do i <- getIState
1027 let opts = idris_options i
1028 let opt' = opts { opt_typeintype = t }
1029 putIState $ i { idris_options = opt' }
1031coverage :: Idris Bool
1032coverage = do i <- getIState
1033 return (opt_coverage (idris_options i))
1035setCoverage :: Bool -> Idris ()
1036setCoverage t = do i <- getIState
1037 let opts = idris_options i
1038 let opt' = opts { opt_coverage = t }
1039 putIState $ i { idris_options = opt' }
1041setIBCSubDir :: FilePath -> Idris ()
1042setIBCSubDir fp = do i <- getIState
1043 let opts = idris_options i
1044 let opt' = opts { opt_ibcsubdir = fp }
1045 putIState $ i { idris_options = opt' }
1047valIBCSubDir :: IState -> Idris FilePath
1048valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1050addImportDir :: FilePath -> Idris ()
1051addImportDir fp = do i <- getIState
1052 let opts = idris_options i
1053 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1054 putIState $ i { idris_options = opt' }
1056setImportDirs :: [FilePath] -> Idris ()
1057setImportDirs fps = do i <- getIState
1058 let opts = idris_options i
1059 let opt' = opts { opt_importdirs = fps }
1060 putIState $ i { idris_options = opt' }
1062allImportDirs :: Idris [FilePath]
1063allImportDirs = do i <- getIState
1064 let optdirs = opt_importdirs (idris_options i)
1065 return ("." : reverse optdirs)
1067addSourceDir :: FilePath -> Idris ()
1068addSourceDir fp = do i <- getIState
1069 let opts = idris_options i
1070 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1071 putIState $ i { idris_options = opts' }
1073setSourceDirs :: [FilePath] -> Idris ()
1074setSourceDirs fps = do i <- getIState
1075 let opts = idris_options i
1076 let opts' = opts { opt_sourcedirs = nub $ fps }
1077 putIState $ i { idris_options = opts' }
1079allSourceDirs :: Idris [FilePath]
1080allSourceDirs = do i <- getIState
1081 let optdirs = opt_sourcedirs (idris_options i)
1082 return ("." : reverse optdirs)
1084colourise :: Idris Bool
1085colourise = do i <- getIState
1086 return $ idris_colourRepl i
1088setColourise :: Bool -> Idris ()
1089setColourise b = do i <- getIState
1090 putIState $ i { idris_colourRepl = b }
1092impShow :: Idris Bool
1093impShow = do i <- getIState
1094 return (opt_showimp (idris_options i))
1096setImpShow :: Bool -> Idris ()
1097setImpShow t = do i <- getIState
1098 let opts = idris_options i
1099 let opt' = opts { opt_showimp = t }
1100 putIState $ i { idris_options = opt' }
1102setColour :: ColourType -> IdrisColour -> Idris ()
1103setColour ct c = do i <- getIState
1104 let newTheme = setColour' ct c (idris_colourTheme i)
1105 putIState $ i { idris_colourTheme = newTheme }
1106 where setColour' KeywordColour c t = t { keywordColour = c }
1107 setColour' BoundVarColour c t = t { boundVarColour = c }
1108 setColour' ImplicitColour c t = t { implicitColour = c }
1109 setColour' FunctionColour c t = t { functionColour = c }
1110 setColour' TypeColour c t = t { typeColour = c }
1111 setColour' DataColour c t = t { dataColour = c }
1112 setColour' PromptColour c t = t { promptColour = c }
1113 setColour' PostulateColour c t = t { postulateColour = c }
1116logLvl :: Int -> String -> Idris ()
1117logLvl = logLvlCats []
1119logCoverage :: Int -> String -> Idris ()
1120logCoverage = logLvlCats [ICoverage]
1122logErasure :: Int -> String -> Idris ()
1123logErasure = logLvlCats [IErasure]
1125-- | Log an action of the parser
1126logParser :: Int -> String -> Idris ()
1127logParser = logLvlCats parserCats
1129-- | Log an action of the elaborator.
1130logElab :: Int -> String -> Idris ()
1131logElab = logLvlCats elabCats
1133-- | Log an action of the compiler.
1134logCodeGen :: Int -> String -> Idris ()
1135logCodeGen = logLvlCats codegenCats
1137logIBC :: Int -> String -> Idris ()
1138logIBC = logLvlCats [IIBC]
1140-- | Log aspect of Idris execution
1142-- An empty set of logging levels is used to denote all categories.
1144-- @TODO update IDE protocol
1145logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1146 -> Int -- ^ The Logging level the message should appear.
1147 -> String -- ^ The message to show the developer.
1149logLvlCats cs l str = do
1151 let lvl = opt_logLevel (idris_options i)
1152 let cats = opt_logcats (idris_options i)
1154 when (inCat cs cats || null cats) $
1155 case idris_outputmode i of
1157 runIO $ hPutStrLn h str
1159 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1160 runIO . hPutStrLn h $ convSExp "log" good n
1162 inCat :: [LogCat] -> [LogCat] -> Bool
1163 inCat cs cats = any (`elem` cats) cs
1165cmdOptType :: Opt -> Idris Bool
1166cmdOptType x = do i <- getIState
1167 return $ x `elem` opt_cmdline (idris_options i)
1169noErrors :: Idris Bool
1170noErrors = do i <- getIState
1172 Nothing -> return True
1175setTypeCase :: Bool -> Idris ()
1176setTypeCase t = do i <- getIState
1177 let opts = idris_options i
1178 let opt' = opts { opt_typecase = t }
1179 putIState $ i { idris_options = opt' }
1182-- Dealing with parameters
1184expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1185 [Name] -> -- all names
1186 [Name] -> -- names with no declaration
1188expandParams dec ps ns infs tm = en 0 tm
1190 -- if we shadow a name (say in a lambda binding) that is used in a call to
1191 -- a lifted function, we need access to both names - once in the scope of the
1192 -- binding and once to call the lifted functions. So we'll explicitly shadow
1193 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1194 -- but we didn't...)
1196 mkShadow (UN n) = MN 0 n
1197 mkShadow (MN i n) = MN (i+1) n
1198 mkShadow (NS x s) = NS (mkShadow x) s
1200 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1201 -- that are merely mentioned.
1203 en 0 (PLam fc n nfc t s)
1204 | n `elem` (map fst ps ++ ns)
1205 = let n' = mkShadow n in
1206 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1207 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1208 en 0 (PPi p n nfc t s)
1209 | n `elem` (map fst ps ++ ns)
1210 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1211 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1212 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1213 en 0 (PLet fc n nfc ty v s)
1214 | n `elem` (map fst ps ++ ns)
1215 = let n' = mkShadow n in
1216 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1217 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1218 -- FIXME: Should only do this in a type signature!
1219 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1220 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1221 = let n' = mkShadow n in
1222 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1223 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1224 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1225 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1226 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1227 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1228 en 0 (PHidden t) = PHidden (en 0 t)
1229 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1230 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1231 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1232 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1233 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1234 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1236 en 0 (PQuote (Var n))
1237 | n `nselem` ns = PQuote (Var (dec n))
1238 en 0 (PApp fc (PInferRef fc' hl n) as)
1239 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1240 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1241 en 0 (PApp fc (PRef fc' hl n) as)
1242 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1243 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1244 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1245 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1246 en 0 (PAppBind fc (PRef fc' hl n) as)
1247 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1248 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1249 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1250 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1252 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1253 (map ((pexp . (PRef fc hl)) . fst) ps)
1254 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1255 (map ((pexp . (PRef fc hl)) . fst) ps)
1256 en 0 (PInferRef fc hl n)
1257 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1258 (map ((pexp . (PRef fc hl)) . fst) ps)
1259 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1260 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1261 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1262 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1263 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1264 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1266 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1267 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1269 en ql t = descend (en ql) t
1272 nselem x (y : xs) | nseq x y = True
1273 | otherwise = nselem x xs
1275 nseq x y = nsroot x == nsroot y
1277 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1278 enTacImp ql other = other
1280expandParamsD :: Bool -> -- True = RHS only
1282 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1283expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1284 = if n `elem` ns && (not rhsonly)
1285 then -- trace (show (n, expandParams dec ps ns ty)) $
1286 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1287 else --trace (show (n, expandParams dec ps ns ty)) $
1288 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1289expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1290 = if n `elem` ns && (not rhsonly)
1291 then -- trace (show (n, expandParams dec ps ns ty)) $
1292 PPostulate e doc syn fc nfc o (dec n)
1293 (piBind ps (expandParams dec ps ns [] ty))
1294 else --trace (show (n, expandParams dec ps ns ty)) $
1295 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1296expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1297 = let n' = if n `elem` ns then dec n else n in
1298 PClauses fc opts n' (map expandParamsC cs)
1300 expandParamsC (PClause fc n lhs ws rhs ds)
1301 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1302 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1303 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1304 n' = if n `elem` ns then dec n else n
1305 -- names bound on the lhs should not be expanded on the rhs
1306 ns' = removeBound lhs ns in
1308 (map (expandParams dec ps'' ns' []) ws)
1309 (expandParams dec ps'' ns' [] rhs)
1310 (map (expandParamsD True ist dec ps'' ns') ds)
1311 expandParamsC (PWith fc n lhs ws wval pn ds)
1312 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1313 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1314 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1315 n' = if n `elem` ns then dec n else n
1316 ns' = removeBound lhs ns in
1318 (map (expandParams dec ps'' ns' []) ws)
1319 (expandParams dec ps'' ns' [] wval)
1321 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1322 updateps yn nm [] = []
1323 updateps yn nm (((a, t), i):as)
1324 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1325 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1327 removeBound lhs ns = ns \\ nub (bnames lhs)
1329 bnames (PRef _ _ n) = [n]
1330 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1331 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1332 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1335-- | Expands parameters defined in parameter and where blocks inside of declarations
1336expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1337 = PData doc argDocs syn fc co (expandPData pd)
1339 -- just do the type decl, leave constructors alone (parameters will be
1340 -- added implicitly)
1341 expandPData (PDatadecl n nfc ty cons)
1343 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1345 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1346 econ (doc, argDocs, n, nfc, t, fc, fs)
1347 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1348expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1350expandParamsD rhs ist dec ps ns (PParams f params pds)
1351 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1352 (map (expandParamsD True ist dec ps ns) pds)
1353-- (map (expandParamsD ist dec ps ns) pds)
1354expandParamsD rhs ist dec ps ns (PMutual f pds)
1355 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1356expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1357 = PInterface doc info f
1358 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1360 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1363 (map (expandParamsD rhs ist dec ps ns) decls)
1366expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1367 = let cn' = case cn of
1368 Just n -> if n `elem` ns then Just (dec n) else Just n
1369 Nothing -> Nothing in
1370 PImplementation doc argDocs info f
1371 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1374 (map (expandParams dec ps ns []) params)
1375 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1376 (expandParams dec ps ns [] ty)
1378 (map (expandParamsD True ist dec ps ns) decls)
1379expandParamsD rhs ist dec ps ns d = d
1381mapsnd f (x, t) = (x, f t)
1383expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1384 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1386expandImplementationScope ist dec ps ns d = d
1388-- | Calculate a priority for a type, for deciding elaboration order
1389-- * if it's just a type variable or concrete type, do it early (0)
1390-- * if there's only type variables and injective constructors, do it next (1)
1391-- * if there's a function type, next (2)
1392-- * finally, everything else (3)
1393getPriority :: IState -> PTerm -> Int
1394getPriority i tm = 1 -- pri tm
1397 case lookupP n (tt_ctxt i) of
1398 ((P (DCon _ _ _) _ _):_) -> 1
1399 ((P (TCon _ _) _ _):_) -> 1
1400 ((P Ref _ _):_) -> 1
1401 [] -> 0 -- must be locally bound, if it's not an error...
1402 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1404 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1405 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1406 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1407 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1408 pri (PTyped l r) = pri l
1409 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1410 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1411 pri (PAlternative _ a as) = maximum (map pri as)
1412 pri (PConstant _ _) = 0
1417addStatics :: Name -> Term -> PTerm -> Idris ()
1418addStatics n tm ptm =
1419 do let (statics, dynamics) = initStatics tm ptm
1422 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1423 Just p -> getNamesFrom 0 (fn_params p) tm ++
1424 concatMap (getParamNames ist . snd) statics
1425 _ -> concatMap (getParamNames ist . snd) statics
1427 let stnames = nub $ concatMap (freeArgNames . snd) statics
1428 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1430 -- also get the arguments which are 'uniquely inferrable' from
1431 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1432 -- or parameters to the type of a static
1433 let statics' = nub $ map fst statics ++
1434 filter (\x -> not (elem x dnames)) stnames
1435 let stpos = staticList statics' tm
1437 unless (null statics) $
1438 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1439 ++ showTmImpls ptm ++ "\n"
1440 ++ show statics ++ "\n" ++ show dynamics
1441 ++ "\n" ++ show paramnames
1442 ++ "\n" ++ show stpos
1443 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1444 addIBC (IBCStatic n)
1446 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1447 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1448 (static, (n, ty) : dynamic)
1449 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1450 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1451 if pstatic p == Static then ((n, ty) : static, dynamic)
1452 else if (not (searchArg p))
1453 then (static, (n, ty) : dynamic)
1454 else (static, dynamic)
1455 initStatics t pt = ([], [])
1457 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1458 = case lookupCtxtExact n (idris_datatypes ist) of
1459 Just ti -> getNamePos 0 (param_pos ti) args
1461 where getNamePos i ps [] = []
1462 getNamePos i ps (P _ n _ : as)
1463 | i `elem` ps = n : getNamePos (i + 1) ps as
1464 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1465 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1466 = n : getParamNames ist sc
1467 getParamNames ist _ = []
1469 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1470 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1471 | otherwise = getNamesFrom (i + 1) ps sc
1472 getNamesFrom i ps sc = []
1474 freeArgNames (Bind n (Pi _ ty _) sc)
1475 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1476 freeArgNames tm = let (_, args) = unApply tm in
1477 concatMap freeNames args
1479 -- if a name appears in an interface or tactic implicit index, it doesn't
1480 -- affect its 'uniquely inferrable' from a static status since these are
1481 -- resolved by searching.
1482 searchArg (Constraint _ _) = True
1483 searchArg (TacImp _ _ _) = True
1486 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1489-- Dealing with implicit arguments
1491-- Add some bound implicits to the using block if they aren't there already
1493addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1494addToUsing us [] = us
1495addToUsing us ((n, t) : ns)
1496 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1497 | otherwise = addToUsing us ns
1498 where impName (UImplicit n _) = Just n
1501-- Add constraint bindings from using block
1503addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1504addUsingConstraints syn fc t
1506 let ns = namesIn [] ist t
1507 let cs = getConstraints t -- check declared constraints
1508 let addconsts = uconsts \\ cs
1509 return (doAdd addconsts ns t)
1510 where uconsts = filter uconst (using syn)
1511 uconst (UConstraint _ _) = True
1515 -- if all of args in ns, then add it
1516 doAdd (UConstraint c args : cs) ns t
1517 | all (\n -> elem n ns) args
1518 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1519 (mkConst c args) (doAdd cs ns t)
1520 | otherwise = doAdd cs ns t
1522 mkConst c args = PApp fc (PRef fc [] c)
1523 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1525 getConstraints (PPi (Constraint _ _) _ _ c sc)
1526 = getcapp c ++ getConstraints sc
1527 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1528 getConstraints _ = []
1530 getcapp (PApp _ (PRef _ _ c) args)
1531 = do ns <- mapM getName args
1532 return (UConstraint c ns)
1535 getName (PExp _ _ _ (PRef _ _ n)) = return n
1538-- | Add implicit bindings from using block, and bind any missing names
1539addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1540addUsingImpls syn n fc t
1541 = do ist <- getIState
1542 autoimpl <- getAutoImpls
1543 let ns_in = implicitNamesIn (map iname uimpls) ist t
1544 let ns = if autoimpl then ns_in
1545 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1547 let badnames = filter (\n -> not (implicitable n) &&
1548 n `notElem` (map iname uimpls)) ns
1549 unless (null badnames) $
1550 throwError (At fc (Elaborating "type of " n Nothing
1551 (NoSuchVariable (head badnames))))
1552 let cs = getArgnames t -- get already bound names
1553 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1554 -- if all names in the arguments of addconsts appear in ns,
1555 -- add the constraint implicitly
1556 return (bindFree ns (doAdd addimpls ns t))
1557 where uimpls = filter uimpl (using syn)
1558 uimpl (UImplicit _ _) = True
1561 iname (UImplicit n _) = n
1562 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1565 -- if all of args in ns, then add it
1566 doAdd (UImplicit n ty : cs) ns t
1568 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1569 | otherwise = doAdd cs ns t
1571 -- bind the free names which weren't in the using block
1574 | elem n (map iname uimpls) = bindFree ns tm
1576 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1578 getArgnames (PPi _ n _ c sc)
1579 = n : getArgnames sc
1582-- Given the original type and the elaborated type, return the implicitness
1583-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1585getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1586getUnboundImplicits i t tm = getImps t (collectImps tm)
1587 where collectImps (PPi p n _ t sc)
1588 = (n, (p, t)) : collectImps sc
1591 scopedimpl (Just i) = not (toplevel_imp i)
1592 scopedimpl _ = False
1594 getImps (Bind n (Pi i _ _) sc) imps
1595 | scopedimpl i = getImps sc imps
1596 getImps (Bind n (Pi _ t _) sc) imps
1597 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1599 argInfo n (Imp opt _ _ _ _) Placeholder
1600 = (True, PImp 0 True opt n Placeholder)
1601 argInfo n (Imp opt _ _ _ _) t'
1602 = (False, PImp (getPriority i t') True opt n t')
1603 argInfo n (Exp opt _ _) t'
1604 = (InaccessibleArg `elem` opt,
1605 PExp (getPriority i t') opt n t')
1606 argInfo n (Constraint opt _) t'
1607 = (InaccessibleArg `elem` opt,
1608 PConstraint 10 opt n t')
1609 argInfo n (TacImp opt _ scr) t'
1610 = (InaccessibleArg `elem` opt,
1611 PTacImplicit 10 opt n scr t')
1612 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1613 where impBind n t = (True, PImp 1 True [] n Placeholder)
1616-- Add implicit Pi bindings for any names in the term which appear in an
1617-- argument position.
1619-- This has become a right mess already. Better redo it some time...
1620-- TODO: This is obsoleted by the new way of elaborating types, (which
1621-- calls addUsingImpls) but there's still a couple of places which use
1622-- it. Clean them up!
1624-- Issue 1739 in the issue tracker
1625-- https://github.com/idris-lang/Idris-dev/issues/1739
1626implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1627implicit info syn n ptm = implicit' info syn [] n ptm
1629implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1630implicit' info syn ignore n ptm
1632 auto <- getAutoImpls
1633 let (tm', impdata) = implicitise auto syn ignore i ptm
1634 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1635-- let (tm'', spos) = findStatics i tm'
1636 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1638 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1640-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1643 -- Detect unknown names in default arguments and throw error if found.
1644 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1645 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1647 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1648 notFoundInDefault kns (PTacImplicit _ _ n script _)
1650 case notFound kns (namesIn [] i script) of
1651 Nothing -> return (n:kns)
1652 Just name -> throwError (NoSuchVariable name)
1653 notFoundInDefault kns p = return ((pname p):kns)
1655 notFound :: [Name] -> [Name] -> Maybe Name
1656 notFound kns [] = Nothing
1657 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1658 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1660-- | Even if auto_implicits is off, we need to call this so we record
1661-- which arguments are implicit
1662implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1663implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1664 let (declimps, ns') = execState (imps True [] tm) ([], [])
1665 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1666 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1667 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1669 then (tm, reverse declimps)
1670 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1672 uvars = map ipair (filter uimplicit (using syn))
1673 pvars = syn_params syn
1675 inUsing n = n `elem` map fst uvars
1677 ipair (UImplicit x y) = (x, y)
1678 uimplicit (UImplicit _ _) = True
1681 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1682 | otherwise = x : dropAll xs ys
1685 -- Find names in argument position in a type, suitable for implicit
1687 -- Not the function position, but do everything else...
1688 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1689 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1691 imps top env ty@(PApp _ f as)
1692 = do (decls, ns) <- get
1693 let isn = nub (implNamesIn uvars ty)
1694 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1695 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1696 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1698 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1699 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1700 imps True (n:env) sc
1701 imps top env (PPi (Exp l _ _) n _ ty sc)
1702 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1703 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1705 (decls, ns) <- get -- ignore decls in HO types
1706 put (PExp (getPriority ist ty) l n Placeholder : decls,
1707 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1708 imps True (n:env) sc
1709 imps top env (PPi (Constraint l _) n _ ty sc)
1710 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1711 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1713 (decls, ns) <- get -- ignore decls in HO types
1714 put (PConstraint 10 l n Placeholder : decls,
1715 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1716 imps True (n:env) sc
1717 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1718 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1719 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1721 (decls, ns) <- get -- ignore decls in HO types
1722 put (PTacImplicit 10 l n scr Placeholder : decls,
1723 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1724 imps True (n:env) sc
1725 imps top env (PRewrite _ _ 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 (PTyped l r)
1731 imps top env (PPair _ _ _ l r)
1732 = do (decls, ns) <- get
1733 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1734 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1735 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1736 = do (decls, ns) <- get
1737 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1738 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1739 imps top env (PDPair _ _ _ l t r)
1740 = do (decls, ns) <- get
1741 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1743 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1744 imps top env (PAlternative ms a as)
1745 = do (decls, ns) <- get
1746 let isn = concatMap (namesIn uvars ist) as
1747 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1748 imps top env (PLam fc n _ ty sc)
1749 = do imps False env ty
1750 imps False (n:env) sc
1751 imps top env (PHidden tm) = imps False env tm
1752 imps top env (PUnifyLog tm) = imps False env tm
1753 imps top env (PNoImplicits tm) = imps False env tm
1754 imps top env (PRunElab fc tm ns) = imps False env tm
1755 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1756 imps top env _ = return ()
1758 pibind using [] sc = sc
1759 pibind using (n:ns) sc
1760 = case lookup n using of
1761 Just ty -> PPi impl_gen
1762 n NoFC ty (pibind using ns sc)
1763 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1764 n NoFC Placeholder (pibind using ns sc)
1766-- | Add implicit arguments in function calls
1767addImplPat :: IState -> PTerm -> PTerm
1768addImplPat = addImpl' True [] [] []
1770addImplBound :: IState -> [Name] -> PTerm -> PTerm
1771addImplBound ist ns = addImpl' False ns [] [] ist
1773addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1774addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1776-- | Add the implicit arguments to applications in the term [Name]
1777-- gives the names to always expend, even when under a binder of that
1778-- name (this is to expand methods with implicit arguments in
1779-- dependent interfaces).
1780addImpl :: [Name] -> IState -> PTerm -> PTerm
1781addImpl = addImpl' False [] []
1783-- TODO: in patterns, don't add implicits to function names guarded by constructors
1784-- and *not* inside a PHidden
1786addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1787addImpl' inpat env infns imp_meths ist ptm
1788 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1790 topname = case ptm of
1792 PApp _ (PRef _ _ n) _ -> n
1793 _ -> sUN "" -- doesn't matter then
1795 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1796 ai inpat qq env ds (PRef fc fcs f)
1797 | f `elem` infns = PInferRef fc fcs f
1798 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1799 ai inpat qq env ds (PHidden (PRef fc hl f))
1800 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1801 ai inpat qq env ds (PRewrite fc by l r g)
1802 = let l' = ai inpat qq env ds l
1803 r' = ai inpat qq env ds r
1804 g' = fmap (ai inpat qq env ds) g in
1805 PRewrite fc by l' r' g'
1806 ai inpat qq env ds (PTyped l r)
1807 = let l' = ai inpat qq env ds l
1808 r' = ai inpat qq env ds r in
1810 ai inpat qq env ds (PPair fc hls p l r)
1811 = let l' = ai inpat qq env ds l
1812 r' = ai inpat qq env ds r in
1813 PPair fc hls p l' r'
1814 ai inpat qq env ds (PDPair fc hls p l t r)
1815 = let l' = ai inpat qq env ds l
1816 t' = ai inpat qq env ds t
1817 r' = ai inpat qq env ds r in
1818 PDPair fc hls p l' t' r'
1819 ai inpat qq env ds (PAlternative ms a as)
1820 = let as' = map (ai inpat qq env ds) as in
1821 PAlternative ms a as'
1822 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1823 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1824 = let as' = map (fmap (ai inpat qq env ds)) as in
1825 PApp fc (PInferRef ffc hl f) as'
1826 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1827 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1828 | not (f `elem` map fst env)
1829 = let as' = map (fmap (ai inpat qq env ds)) as in
1830 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1831 | Just (Just ty) <- lookup f env =
1832 let as' = map (fmap (ai inpat qq env ds)) as
1833 arity = getPArity ty in
1834 mkPApp fc arity ftm as'
1835 ai inpat qq env ds (PApp fc f as)
1836 = let f' = ai inpat qq env ds f
1837 as' = map (fmap (ai inpat qq env ds)) as in
1839 ai inpat qq env ds (PWithApp fc f a)
1840 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1841 ai inpat qq env ds (PCase fc c os)
1842 = let c' = ai inpat qq env ds c in
1843 -- leave lhs alone, because they get lifted into a new pattern match
1844 -- definition which is passed through addImpl again
1845 PCase fc c' (map aiCase os)
1848 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1850 -- Anything beginning with a lower case letter, not applied,
1851 -- and no namespace is a pattern variable
1852 patnames (PApp _ (PRef _ _ f) [])
1853 | implicitable f = [(f, Nothing)]
1854 patnames (PRef _ _ f)
1855 | implicitable f = [(f, Nothing)]
1856 patnames (PApp _ (PRef _ _ _) args)
1857 = concatMap patnames (map getTm args)
1858 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1859 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1860 patnames (PAs _ _ t) = patnames t
1861 patnames (PAlternative _ _ ts) = concatMap patnames ts
1865 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1866 (ai inpat qq env ds t)
1867 (ai inpat qq env ds f)
1869 -- If the name in a lambda is an unapplied data constructor name, do this
1870 -- as a 'case' instead because we'll expect to match on it
1871 ai inpat qq env ds (PLam fc n nfc ty sc)
1872 = if canBeDConName n (tt_ctxt ist)
1873 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1874 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1875 [(PRef fc [] n, sc)]))
1876 else let ty' = ai inpat qq env ds ty
1877 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1878 PLam fc n nfc ty' sc'
1879 ai inpat qq env ds (PLet fc n nfc ty val sc)
1880 = if canBeDConName n (tt_ctxt ist)
1881 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1882 else let ty' = ai inpat qq env ds ty
1883 val' = ai inpat qq env ds val
1884 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1885 PLet fc n nfc ty' val' sc'
1886 ai inpat qq env ds (PPi p n nfc ty sc)
1887 = let ty' = ai inpat qq env ds ty
1888 env' = if n `elem` imp_meths then env
1889 else ((n, Just ty) : env)
1890 sc' = ai inpat qq env' ds sc in
1892 ai inpat qq env ds (PGoal fc r n sc)
1893 = let r' = ai inpat qq env ds r
1894 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1896 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1897 -- Don't do PProof or PTactics since implicits get added when scope is
1898 -- properly known in ElabTerm.runTac
1899 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1900 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1901 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1902 (fmap (ai inpat True env ds) g)
1903 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1904 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1905 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1906 ai inpat qq env ds tm = tm
1908 handleErr (Left err) = PElabError err
1909 handleErr (Right x) = x
1911-- if in a pattern, and there are no arguments, and there's no possible
1912-- names with zero explicit arguments, don't add implicits.
1914aiFn :: Name -> Bool -> Bool -> Bool
1917 -> Name -- ^ function being applied
1919 -> [PArg] -- ^ initial arguments (if in a pattern)
1921aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1922 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1924 = case lookupDef f (tt_ctxt ist) of
1925 [] -> Right $ PPatvar ffc f
1926 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1927 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1928 if (not (vname f) || tcname f
1929 || any (conCaf (tt_ctxt ist)) ialts)
1930-- any constructor alts || any allImp ialts))
1931 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1932 else Right $ PPatvar ffc f
1933 where imp (PExp _ _ _ _) = False
1936 allImp xs = all imp xs
1938 unqualified (NS _ _) = False
1939 unqualified _ = True
1941 constructor (TyDecl (DCon _ _ _) _) = True
1942 constructor _ = False
1944 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1946 vname (UN n) = True -- non qualified
1949aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1950 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1951aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1952 -- This is where namespaces get resolved by adding PAlternative
1953 = do let ns = lookupCtxtName f (idris_implicits ist)
1954 let nh = filter (\(n, _) -> notHidden n) ns
1955 let ns' = case trimAlts ds nh of
1959 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1961 [] -> case metaVar f (map fst (idris_metavars ist)) of
1962 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1963 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1965 PAlternative [] (ExactlyOne True) $
1966 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1967 (insertImpl ns as)) alts
1969 -- if the name is in imp_meths, we should actually refer to the bound
1970 -- name rather than the global one after expanding implicits
1971 isImpName f f' | f `elem` imp_meths = f
1974 -- If it's a metavariable name, try to qualify it from the list of
1975 -- unsolved metavariables
1976 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1977 metaVar f (_ : ns) = metaVar f ns
1978 metaVar f [] = Nothing
1980 trimAlts [] alts = alts
1982 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1987 notHidden n = case getAccessibility n of
1993 = case lookupDefAccExact n False (tt_ctxt ist) of
1997 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1998 -> [PArg] -- ^ given arguments
2001 = let (as', badimpls) = partition (impIn ps) as in
2002 map addUnknownImp badimpls ++
2003 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
2005 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2006 -> [PArg] -- parameters
2007 -> [PArg] -- explicit arguments
2008 -> [PArg] -- implicits given
2010 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2011 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2012 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2013 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2014 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2015 let rtc = PResolveTC fc in
2016 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2017 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2018 case find n imps [] of
2020 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2022 PImp p True l n Placeholder :
2023 insImpAcc (M.insert n Placeholder pnas) ps given imps
2024 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2025 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2026 case find n imps [] of
2028 PTacImplicit p l n sc tm :
2029 insImpAcc (M.insert n tm pnas) ps given imps'
2032 then PTacImplicit p l n sc Placeholder :
2033 insImpAcc (M.insert n Placeholder pnas) ps given imps
2034 else PTacImplicit p l n sc sc :
2035 insImpAcc (M.insert n sc pnas) ps given imps
2036 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2037 insImpAcc _ _ given imps = given ++ imps
2039 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2041 find n [] acc = Nothing
2042 find n (PImp _ _ _ n' t : gs) acc
2043 | n == n' = Just (t, reverse acc ++ gs)
2044 find n (PTacImplicit _ _ n' _ t : gs) acc
2045 | n == n' = Just (t, reverse acc ++ gs)
2046 find n (g : gs) acc = find n gs (g : acc)
2048-- | return True if the second argument is an implicit argument which
2049-- is expected in the implicits, or if it's not an implicit
2050impIn :: [PArg] -> PArg -> Bool
2051impIn ps (PExp _ _ _ _) = True
2052impIn ps (PConstraint _ _ _ _) = True
2053impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2055expArg (PExp _ _ _ _) = True
2056expArg (PConstraint _ _ _ _) = True
2059-- replace non-linear occurrences with _
2061stripLinear :: IState -> PTerm -> PTerm
2062stripLinear i tm = evalState (sl tm) [] where
2063 sl :: PTerm -> State [Name] PTerm
2065 | (_:_) <- lookupTy f (tt_ctxt i)
2066 = return $ PRef fc hl f
2067 | otherwise = do ns <- get
2069 then return $ PHidden (PRef fc hl f) -- Placeholder
2070 else do put (f : ns)
2071 return (PRef fc hl f)
2075 then return $ PHidden (PPatvar fc f) -- Placeholder
2076 else do put (f : ns)
2077 return (PPatvar fc f)
2078 -- Assumption is that variables are all the same in each alternative
2079 sl t@(PAlternative ms b as) = do ns <- get
2081 return (PAlternative ms b as')
2082 where slAlts ns (a : as) = do put ns
2086 slAlts ns [] = return []
2087 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2088 sl (PDPair fc hls p l t r) = do l' <- sl l
2091 return (PDPair fc hls p l' t' r')
2092 sl (PApp fc fn args) = do fn' <- case fn of
2093 -- Just the args, fn isn't matchable as a var
2094 PRef _ _ _ -> return fn
2096 args' <- mapM slA args
2097 return $ PApp fc fn' args'
2098 where slA (PImp p m l n t) = do t' <- sl t
2099 return $ PImp p m l n t'
2100 slA (PExp p l n t) = do t' <- sl t
2101 return $ PExp p l n t'
2102 slA (PConstraint p l n t)
2104 return $ PConstraint p l n t'
2105 slA (PTacImplicit p l n sc t)
2107 return $ PTacImplicit p l n sc t'
2110-- | Remove functions which aren't applied to anything, which must then
2111-- be resolved by unification. Assume names resolved and alternatives
2112-- filled in (so no ambiguity).
2113stripUnmatchable :: IState -> PTerm -> PTerm
2114stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2115 su :: PTerm -> PTerm
2116 su tm@(PRef fc hl f)
2117 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2119 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2120 not (implicitable f)
2122 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2123 not (implicitable f)
2125 su (PApp fc f@(PRef _ _ fn) args)
2126 -- here we use canBeDConName because the impossible pattern
2127 -- check will not necessarily fully resolve constructor names,
2128 -- and these bare names will otherwise get in the way of
2129 -- impossbility checking.
2130 | canBeDConName fn ctxt
2131 = PApp fc f (fmap (fmap su) args)
2133 = PHidden (PApp fc f args)
2134 su (PAlternative ms b alts)
2135 = let alts' = filter (/= Placeholder) (map su alts) in
2136 if null alts' then Placeholder
2137 else PAlternative ms b alts'
2138 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2139 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2140 su t@(PLam fc _ _ _ _) = PHidden t
2141 su t@(PPi _ _ _ _ _) = PHidden t
2142 su t@(PConstant _ c) | isTypeConst c = PHidden t
2147stripUnmatchable i tm = tm
2150mkPApp fc a f as = let rest = drop a as in
2151 if a == 0 then appRest fc f rest
2152 else appRest fc (PApp fc f (take a as)) rest
2155 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2159-- | Find 'static' argument positions
2160-- (the declared ones, plus any names in argument position in the declared
2162-- FIXME: It's possible that this really has to happen after elaboration
2163findStatics :: IState -> PTerm -> (PTerm, [Bool])
2164findStatics ist tm = let (ns, ss) = fs tm
2165 in runState (pos ns ss tm) []
2166 where fs (PPi p n fc t sc)
2167 | Static <- pstatic p
2168 = let (ns, ss) = fs sc in
2169 (namesIn [] ist t : ns, n : ss)
2170 | otherwise = let (ns, ss) = fs sc in
2174 inOne n ns = length (filter id (map (elem n) ns)) == 1
2176 pos ns ss (PPi p n fc t sc)
2177 | elem n ss = do sc' <- pos ns ss sc
2180 return (PPi (p { pstatic = Static }) n fc t sc')
2181 | otherwise = do sc' <- pos ns ss sc
2184 return (PPi p n fc t sc')
2185 pos ns ss t = return t
2187-- for 6.12/7 compatibility
2188data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2190instance Applicative (EitherErr a) where
2194instance Monad (EitherErr a) where
2197 (LeftErr e) >>= k = LeftErr e
2198 RightOK v >>= k = k v
2200toEither (LeftErr e) = Left e
2201toEither (RightOK ho) = Right ho
2203-- | Syntactic match of a against b, returning pair of variables in a
2204-- and what they match. Returns the pair that failed if not a match.
2205matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2206matchClause = matchClause' False
2208matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2209matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2210 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2212 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2215 match' x y = match (fullApp x) (fullApp y)
2216 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2217 | fi == txt "fromInteger" && b == txt "builtins",
2218 PConstant _ (I _) <- getTm x = match (getTm x) x'
2219 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2220 | fi == txt "fromInteger" && b == txt "builtins",
2221 PConstant _ (I _) <- getTm x = match (getTm x) x'
2222 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2223 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2224 match (PApp _ f args) (PApp _ f' args')
2225 | length args == length args'
2226 = do mf <- match' f f'
2227 ms <- zipWithM matchArg args args'
2228 return (mf ++ concat ms)
2229 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2230 match (PPatvar f n) xr = match (PRef f [f] n) xr
2231 match xr (PPatvar f n) = match xr (PRef f [f] n)
2232 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2233 match (PRef _ _ n) tm@(PRef _ _ n')
2234 | n == n' && not names &&
2235 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2236 || tm == Placeholder)
2238 -- if one namespace is missing, drop the other
2239 | n == n' || n == dropNS n' || dropNS n == n' = return []
2240 where dropNS (NS n _) = n
2242 match (PRef _ _ n) tm
2243 | not names && (not (isConName n (tt_ctxt i) ||
2244 isFnName n (tt_ctxt i)) || tm == Placeholder)
2246 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2247 = do ml <- match' l l'
2250 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2253 match (PTyped l r) x = match l x
2254 match x (PTyped l r) = match x l
2255 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2258 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2261 return (ml ++ mt ++ mr)
2262 match (PAlternative _ a as) (PAlternative _ a' as')
2263 = do ms <- zipWithM match' as as'
2265 match a@(PAlternative _ _ as) b
2266 = do let ms = zipWith match' as (repeat b)
2267 case (rights (map toEither ms)) of
2270 match (PCase _ _ _) _ = return [] -- lifted out
2271 match (PMetavar _ _) _ = return [] -- modified
2272 match (PInferRef _ _ _) _ = return [] -- modified
2273 match (PQuote _) _ = return []
2274 match (PProof _) _ = return []
2275 match (PTactics _) _ = return []
2276 match (PResolveTC _) (PResolveTC _) = return []
2277 match (PTrue _ _) (PTrue _ _) = return []
2278 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2281 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2284 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2285 mty <- match' ty ty'
2287 return (mt ++ mty ++ ms)
2288 match (PHidden x) (PHidden y)
2289 | RightOK xs <- match x y = return xs -- to collect variables
2290 | otherwise = return [] -- Otherwise hidden things are unmatchable
2292 | RightOK xs <- match x y = return xs
2293 | otherwise = return []
2295 | RightOK xs <- match x y = return xs
2296 | otherwise = return []
2297 match (PUnifyLog x) y = match' x y
2298 match x (PUnifyLog y) = match' x y
2299 match (PNoImplicits x) y = match' x y
2300 match x (PNoImplicits y) = match' x y
2301 match Placeholder _ = return []
2302 match _ Placeholder = return []
2303 match (PResolveTC _) _ = return []
2304 match a b | a == b = return []
2305 | otherwise = LeftErr (a, b)
2307 checkRpts (RightOK ms) = check ms where
2309 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2312 check (_:xs) = check xs
2314 checkRpts (LeftErr x) = Left x
2316substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2317substMatches ms = substMatchesShadow ms []
2319-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2320-- substMatchesShadow [] shs t = t
2321-- substMatchesShadow ((n,tm):ns) shs t
2322-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2324substMatch :: Name -> PTerm -> PTerm -> PTerm
2325substMatch n = substMatchShadow n []
2327substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2328substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2330substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2331substMatchesShadow nmap shs t = sm shs t where
2332 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2333 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2334 sm xs (PPi p x fc t sc)
2336 = let x' = nextName x in
2337 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2338 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2339 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2340 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2341 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2342 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2343 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2345 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2346 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2347 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2348 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2349 sm xs (PHidden x) = PHidden (sm xs x)
2350 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2351 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2352 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2353 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2356 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2359shadow :: Name -> Name -> PTerm -> PTerm
2360shadow n n' t = sm 0 t where
2361 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2362 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2363 | otherwise = PLam fc x xfc (sm 0 t) sc
2364 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2365 | otherwise = PPi p x fc (sm 0 t) sc
2366 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2367 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2368 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2369 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2370 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2371 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2372 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2373 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2374 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2375 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2376 sm 0 (PAlternative ms a as)
2377 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2378 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2379 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2380 sm 0 (PHidden x) = PHidden (sm 0 x)
2381 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2382 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2383 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2384 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2385 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2386 sm ql x = descend (sm ql) x
2388 shadowAlt p@(x, oldn) = (update x, update oldn)
2389 update oldn | n == oldn = n'
2392-- | Rename any binders which are repeated (so that we don't have to
2393-- mess about with shadowing anywhere else).
2394mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2395mkUniqueNames env shadows tm
2396 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2398 initMap = M.fromList shadows
2400 inScope :: S.Set Name
2401 inScope = S.fromList $ boundNamesIn tm
2403 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2404 return (arg { getTm = t' })
2406 -- Initialise the unique name with the environment length (so we're not
2407 -- looking for too long...)
2408 initN (UN n) l = UN $ txt (str n ++ show l)
2409 initN (MN i s) l = MN (i+l) s
2412 -- FIXME: Probably ought to do this for completeness! It's fine as
2413 -- long as there are no bindings inside tactics though.
2414 mkUniqT _ nmap tac = return tac
2416 mkUniq :: Int -- ^ The number of quotations that we're under
2417 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2418 mkUniq 0 nmap (PLam fc n nfc ty sc)
2422 then do let n' = uniqueNameSet (initN n (S.size env))
2423 (S.union env inScope)
2424 return (n', sc) -- shadow n n' sc)
2426 put (S.insert n' env)
2427 let nmap' = M.insert n n' nmap
2428 ty' <- mkUniq 0 nmap ty
2429 sc'' <- mkUniq 0 nmap' sc'
2430 return $! PLam fc n' nfc ty' sc''
2431 mkUniq 0 nmap (PPi p n fc ty sc)
2435 then do let n' = uniqueNameSet (initN n (S.size env))
2436 (S.union env inScope)
2437 return (n', sc) -- shadow n n' sc)
2439 put (S.insert n' env)
2440 let nmap' = M.insert n n' nmap
2441 ty' <- mkUniq 0 nmap ty
2442 sc'' <- mkUniq 0 nmap' sc'
2443 return $! PPi p n' fc ty' sc''
2444 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2448 then do let n' = uniqueNameSet (initN n (S.size env))
2449 (S.union env inScope)
2450 return (n', sc) -- shadow n n' sc)
2452 put (S.insert n' env)
2453 let nmap' = M.insert n n' nmap
2454 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2455 sc'' <- mkUniq 0 nmap' sc'
2456 return $! PLet fc n' nfc ty' val' sc''
2457 mkUniq 0 nmap (PApp fc t args)
2458 = do t' <- mkUniq 0 nmap t
2459 args' <- mapM (mkUniqA 0 nmap) args
2460 return $! PApp fc t' args'
2461 mkUniq 0 nmap (PAppBind fc t args)
2462 = do t' <- mkUniq 0 nmap t
2463 args' <- mapM (mkUniqA 0 nmap) args
2464 return $! PAppBind fc t' args'
2465 mkUniq 0 nmap (PCase fc t alts)
2466 = do t' <- mkUniq 0 nmap t
2467 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2468 return (x', y')) alts
2469 return $! PCase fc t' alts'
2470 mkUniq 0 nmap (PIfThenElse fc c t f)
2471 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2472 mkUniq 0 nmap (PPair fc hls p l r)
2473 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2474 return $! PPair fc hls p l' r'
2475 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2478 (n', sc') <- if n `S.member` env
2479 then do let n' = uniqueNameSet n (S.union env inScope)
2480 return (n', sc) -- shadow n n' sc)
2482 put (S.insert n' env)
2483 let nmap' = M.insert n n' nmap
2484 t' <- mkUniq 0 nmap t
2485 sc'' <- mkUniq 0 nmap' sc'
2486 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2487 mkUniq 0 nmap (PDPair fc hls p l t r)
2488 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2489 return $! PDPair fc hls p l' t' r'
2490 mkUniq 0 nmap (PAlternative ns b as)
2491 -- store the nmap and defer the rest until we've pruned the set
2492 -- during elaboration
2493 = return $ PAlternative (ns ++ M.toList nmap) b as
2494 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2495 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2496 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2497 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2498 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2499 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2500 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2501 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2502 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2503 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2506 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2508 mkUniq ql nmap (PQuasiquote tm ty) =
2509 do tm' <- mkUniq (ql + 1) nmap tm
2511 Nothing -> return Nothing
2512 Just t -> fmap Just $ mkUniq ql nmap t
2513 return $! PQuasiquote tm' ty'
2514 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2516 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2519getFile :: Opt -> Maybe String
2520getFile (Filename str) = Just str
2523getBC :: Opt -> Maybe String
2524getBC (BCAsm str) = Just str
2527getOutput :: Opt -> Maybe String
2528getOutput (Output str) = Just str
2529getOutput _ = Nothing
2531getIBCSubDir :: Opt -> Maybe String
2532getIBCSubDir (IBCSubDir str) = Just str
2533getIBCSubDir _ = Nothing
2535getImportDir :: Opt -> Maybe String
2536getImportDir (ImportDir str) = Just str
2537getImportDir _ = Nothing
2539getSourceDir :: Opt -> Maybe String
2540getSourceDir (SourceDir str) = Just str
2541getSourceDir _ = Nothing
2543getPkgDir :: Opt -> Maybe String
2544getPkgDir (Pkg str) = Just str
2545getPkgDir _ = Nothing
2547getPkg :: Opt -> Maybe (Bool, String)
2548getPkg (PkgBuild str) = Just (False, str)
2549getPkg (PkgInstall str) = Just (True, str)
2552getPkgClean :: Opt -> Maybe String
2553getPkgClean (PkgClean str) = Just str
2554getPkgClean _ = Nothing
2556getPkgREPL :: Opt -> Maybe String
2557getPkgREPL (PkgREPL str) = Just str
2558getPkgREPL _ = Nothing
2560getPkgCheck :: Opt -> Maybe String
2561getPkgCheck (PkgCheck str) = Just str
2562getPkgCheck _ = Nothing
2564-- | Returns None if given an Opt which is not PkgMkDoc
2565-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2566getPkgMkDoc :: Opt -- ^ Opt to extract
2567 -> Maybe String -- ^ Result
2568getPkgMkDoc (PkgMkDoc str) = Just str
2569getPkgMkDoc _ = Nothing
2571getPkgTest :: Opt -- ^ the option to extract
2572 -> Maybe String -- ^ the package file to test
2573getPkgTest (PkgTest f) = Just f
2574getPkgTest _ = Nothing
2576getCodegen :: Opt -> Maybe Codegen
2577getCodegen (UseCodegen x) = Just x
2578getCodegen _ = Nothing
2580getCodegenArgs :: Opt -> Maybe String
2581getCodegenArgs (CodegenArgs args) = Just args
2582getCodegenArgs _ = Nothing
2584getConsoleWidth :: Opt -> Maybe ConsoleWidth
2585getConsoleWidth (UseConsoleWidth x) = Just x
2586getConsoleWidth _ = Nothing
2589getExecScript :: Opt -> Maybe String
2590getExecScript (InterpretScript expr) = Just expr
2591getExecScript _ = Nothing
2593getPkgIndex :: Opt -> Maybe FilePath
2594getPkgIndex (PkgIndex file) = Just file
2595getPkgIndex _ = Nothing
2597getEvalExpr :: Opt -> Maybe String
2598getEvalExpr (EvalExpr expr) = Just expr
2599getEvalExpr _ = Nothing
2601getOutputTy :: Opt -> Maybe OutputType
2602getOutputTy (OutputTy t) = Just t
2603getOutputTy _ = Nothing
2605getLanguageExt :: Opt -> Maybe LanguageExt
2606getLanguageExt (Extension e) = Just e
2607getLanguageExt _ = Nothing
2609getTriple :: Opt -> Maybe String
2610getTriple (TargetTriple x) = Just x
2611getTriple _ = Nothing
2613getCPU :: Opt -> Maybe String
2614getCPU (TargetCPU x) = Just x
2617getOptLevel :: Opt -> Maybe Int
2618getOptLevel (OptLevel x) = Just x
2619getOptLevel _ = Nothing
2621getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2622getOptimisation (AddOpt p) = Just (True, p)
2623getOptimisation (RemoveOpt p) = Just (False, p)
2624getOptimisation _ = Nothing
2626getColour :: Opt -> Maybe Bool
2627getColour (ColourREPL b) = Just b
2628getColour _ = Nothing
2630getClient :: Opt -> Maybe String
2631getClient (Client x) = Just x
2632getClient _ = Nothing
2634-- Get the first valid port
2635getPort :: [Opt] -> Maybe REPLPort
2637getPort (Port p : xs) = Just p
2638getPort (_ : xs) = getPort xs
2640opt :: (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