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 e = do i <- getIState
147 idris_language_extensions = e : idris_language_extensions i
150-- | Transforms are organised by the function being applied on the lhs
151-- of the transform, to make looking up appropriate transforms quicker
152addTrans :: Name -> (Term, Term) -> Idris ()
155 let t' = case lookupCtxtExact basefn (idris_transforms i) of
156 Just def -> (t : def)
158 putIState $ i { idris_transforms = addDef basefn t'
159 (idris_transforms i) }
161addErrRev :: (Term, Term) -> Idris ()
162addErrRev t = do i <- getIState
163 putIState $ i { idris_errRev = t : idris_errRev i }
165addErasureUsage :: Name -> Int -> Idris ()
166addErasureUsage n i = do ist <- getIState
167 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
169addExport :: Name -> Idris ()
170addExport n = do ist <- getIState
171 putIState $ ist { idris_exports = n : idris_exports ist }
173addUsedName :: FC -> Name -> Name -> Idris ()
175 = do ist <- getIState
176 case lookupTyName n (tt_ctxt ist) of
177 [(n', ty)] -> addUsage n' 0 ty
178 [] -> throwError (At fc (NoSuchVariable n))
179 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
180 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
182 | otherwise = addUsage n (i + 1) sc
183 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
185getErasureUsage :: Idris [(Name, Int)]
186getErasureUsage = do ist <- getIState;
187 return (idris_erasureUsed ist)
189getExports :: Idris [Name]
190getExports = do ist <- getIState
191 return (idris_exports ist)
193totcheck :: (FC, Name) -> Idris ()
194totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
196defer_totcheck :: (FC, Name) -> Idris ()
199 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
201clear_totcheck :: Idris ()
202clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
204setFlags :: Name -> [FnOpt] -> Idris ()
205setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
207addFnOpt :: Name -> FnOpt -> Idris ()
208addFnOpt n f = do i <- getIState
209 let fls = case lookupCtxtExact n (idris_flags i) of
214setFnInfo :: Name -> FnInfo -> Idris ()
215setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
217setAccessibility :: Name -> Accessibility -> Idris ()
220 let ctxt = setAccess n a (tt_ctxt i)
221 putIState $ i { tt_ctxt = ctxt }
223-- | get the accessibility of a name outside this module
224getFromHideList :: Name -> Idris (Maybe Accessibility)
225getFromHideList n = do i <- getIState
226 return $ lookupCtxtExact n (hide_list i)
228setTotality :: Name -> Totality -> Idris ()
231 let ctxt = setTotal n a (tt_ctxt i)
232 putIState $ i { tt_ctxt = ctxt }
234setInjectivity :: Name -> Injectivity -> Idris ()
237 let ctxt = setInjective n a (tt_ctxt i)
238 putIState $ i { tt_ctxt = ctxt }
240getTotality :: Name -> Idris Totality
243 case lookupTotal n (tt_ctxt i) of
245 _ -> return (Total [])
247-- Get coercions which might return the required type
248getCoercionsTo :: IState -> Type -> [Name]
250 let cs = idris_coercions i
251 (fn,_) = unApply (getRetTy ty) in
253 where findCoercions t [] = []
254 findCoercions t (n : ns) =
255 let ps = case lookupTy n (tt_ctxt i) of
256 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
257 (t', _) -> [n | t == t']
259 ps ++ findCoercions t ns
261addToCG :: Name -> CGInfo -> Idris ()
264 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
266addCalls :: Name -> [Name] -> Idris ()
269 case lookupCtxtExact n (idris_callgraph i) of
270 Nothing -> addToCG n (CGInfo calls Nothing [] [])
271 Just (CGInfo cs ans scg used) ->
272 addToCG n (CGInfo (nub (calls ++ cs)) ans scg used)
274addTyInferred :: Name -> Idris ()
277 putIState $ i { idris_tyinfodata =
278 addDef n TIPartial (idris_tyinfodata i) }
280addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
281addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
282 mapM_ addConstraint ts
284 where addConstraint (x, y) = findMVApps x y
287 = do let (fx, argsx) = unApply x
288 let (fy, argsy) = unApply y
293 else mapM_ addConstraint (zip argsx argsy)
295 tryAddMV (P _ mv _) y =
297 case lookup mv (idris_metavars ist) of
298 Just _ -> addConstraintRule mv y
300 tryAddMV _ _ = return ()
302 addConstraintRule :: Name -> Term -> Idris ()
303 addConstraintRule n t
305 logLvl 1 $ "TI constraint: " ++ show (n, t)
306 case lookupCtxt n (idris_tyinfodata ist) of
308 do mapM_ (checkConsistent t) ts
309 let ti' = addDef n (TISolution (t : ts))
310 (idris_tyinfodata ist)
311 put $ ist { idris_tyinfodata = ti' }
313 do let ti' = addDef n (TISolution [t])
314 (idris_tyinfodata ist)
315 put $ ist { idris_tyinfodata = ti' }
317 -- Check a solution is consistent with previous solutions
318 -- Meaning: If heads are both data types, they had better be the
320 checkConsistent :: Term -> Term -> Idris ()
321 checkConsistent x y =
322 do let (fx, _) = unApply x
323 let (fy, _) = unApply y
325 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
326 (P (TCon _ _) n _, Constant _) -> errWhen True
327 (Constant _, P (TCon _ _) n' _) -> errWhen True
328 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
333 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
334 errWhen False = return ()
336isTyInferred :: Name -> Idris Bool
339 case lookupCtxt n (idris_tyinfodata i) of
340 [TIPartial] -> return True
343-- | Adds error handlers for a particular function and argument. If
344-- names are ambiguous, all matching handlers are updated.
345addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
346addFunctionErrorHandlers f arg hs =
348 let oldHandlers = idris_function_errorhandlers i
349 let newHandlers = flip (addDef f) oldHandlers $
350 case lookupCtxtExact f oldHandlers of
351 Nothing -> M.singleton arg (S.fromList hs)
352 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
353 -- will always be one of those two, thus no extra case
354 putIState $ i { idris_function_errorhandlers = newHandlers }
356getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
357getFunctionErrorHandlers f arg = do i <- getIState
358 return . maybe [] S.toList $
359 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
362-- | Trace all the names in a call graph starting at the given name
363getAllNames :: Name -> Idris [Name]
364getAllNames n = do i <- getIState
365 case getCGAllNames i n of
367 Nothing -> do ns <- allNames [] n
371getCGAllNames :: IState -> Name -> Maybe [Name]
372getCGAllNames i n = case lookupCtxtExact n (idris_callgraph i) of
373 Just ci -> allCalls ci
376addCGAllNames :: IState -> Name -> [Name] -> Idris ()
378 = case lookupCtxtExact n (idris_callgraph i) of
379 Just ci -> addToCG n (ci { allCalls = Just ns })
380 _ -> addToCG n (CGInfo [] (Just ns) [] [])
382allNames :: [Name] -> Name -> Idris [Name]
383allNames ns n | n `elem` ns = return []
384allNames ns n = do i <- getIState
385 case getCGAllNames i n of
387 Nothing -> case lookupCtxtExact n (idris_callgraph i) of
389 do more <- mapM (allNames (n:ns)) (calls ci)
390 let ns' = nub (n : concat more)
391 addCGAllNames i n ns'
395addCoercion :: Name -> Idris ()
396addCoercion n = do i <- getIState
397 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
399addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
402 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
404addNameHint :: Name -> Name -> Idris ()
407 ty' <- case lookupCtxtName ty (idris_implicits i) of
408 [(tyn, _)] -> return tyn
409 [] -> throwError (NoSuchVariable ty)
410 tyns -> throwError (CantResolveAlts (map fst tyns))
411 let ns' = case lookupCtxt ty' (idris_namehints i) of
414 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
416getNameHints :: IState -> Name -> [Name]
417getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
419 case lookupCtxt n (idris_namehints i) of
423addDeprecated :: Name -> String -> Idris ()
424addDeprecated n reason = do
426 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
428getDeprecated :: Name -> Idris (Maybe String)
431 return $ lookupCtxtExact n (idris_deprecated i)
434addFragile :: Name -> String -> Idris ()
435addFragile n reason = do
437 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
439getFragile :: Name -> Idris (Maybe String)
442 return $ lookupCtxtExact n (idris_fragile i)
444push_estack :: Name -> Bool -> Idris ()
447 putIState (i { elab_stack = (n, impl) : elab_stack i })
449pop_estack :: Idris ()
450pop_estack = do i <- getIState
451 putIState (i { elab_stack = ptail (elab_stack i) })
455-- | Add an interface implementation function.
457-- Precondition: the implementation should have the correct type.
459-- Dodgy hack 1: Put integer implementations first in the list so they are
460-- resolved by default.
462-- Dodgy hack 2: put constraint chasers (ParentN) last
463addImplementation :: Bool -- ^ whether the name is an Integer implementation
464 -> Bool -- ^ whether to include the implementation in implementation search
465 -> Name -- ^ the name of the interface
466 -> Name -- ^ the name of the implementation
468addImplementation int res n i
469 = do ist <- getIState
470 case lookupCtxt n (idris_interfaces ist) of
471 [CI a b c d e f g ins fds] ->
472 do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
473 putIState $ ist { idris_interfaces = cs }
474 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
475 putIState $ ist { idris_interfaces = cs }
476 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
477 addI i ins | int = (i, res) : ins
478 | chaser n = ins ++ [(i, res)]
479 | otherwise = insI i ins
480 insI i [] = [(i, res)]
481 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
482 | otherwise = n : insI i ns
484 chaser (SN (ParentN _ _)) = True
485 chaser (NS n _) = chaser n
488-- | Add a privileged implementation - one which implementation search will
489-- happily resolve immediately if it is type correct This is used for
490-- naming parent implementations when defining an implementation with
491-- constraints. Returns the old list, so we can revert easily at the
493addOpenImpl :: [Name] -> Idris [Name]
494addOpenImpl ns = do ist <- getIState
495 ns' <- mapM (checkValid ist) ns
496 let open = idris_openimpls ist
497 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
501 = case lookupCtxtName n (idris_implicits ist) of
502 [(n', _)] -> return n'
503 [] -> throwError (NoSuchVariable n)
504 more -> throwError (CantResolveAlts (map fst more))
506setOpenImpl :: [Name] -> Idris ()
507setOpenImpl ns = do ist <- getIState
508 putIState $ ist { idris_openimpls = ns }
510getOpenImpl :: Idris [Name]
511getOpenImpl = do ist <- getIState
512 return (idris_openimpls ist)
514addInterface :: Name -> InterfaceInfo -> Idris ()
516 = do ist <- getIState
517 let i' = case lookupCtxt n (idris_interfaces ist) of
518 [c] -> c { interface_implementations = interface_implementations i }
520 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
522addRecord :: Name -> RecordInfo -> Idris ()
523addRecord n ri = do ist <- getIState
524 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
526addAutoHint :: Name -> Name -> Idris ()
529 case lookupCtxtExact n (idris_autohints ist) of
531 do let hs = addDef n [hint] (idris_autohints ist)
532 putIState $ ist { idris_autohints = hs }
534 do let hs = addDef n (hint : nhints) (idris_autohints ist)
535 putIState $ ist { idris_autohints = hs }
537getAutoHints :: Name -> Idris [Name]
538getAutoHints n = do ist <- getIState
539 case lookupCtxtExact n (idris_autohints ist) of
543addIBC :: IBCWrite -> Idris ()
546 when (notDef (ibc_write i)) $
547 putIState $ i { ibc_write = ibc : ibc_write i }
548 where notDef [] = True
549 notDef (IBCDef n': is) | n == n' = False
550 notDef (_ : is) = notDef is
551addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
554clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
555 idris_inmodule = S.empty }
557resetNameIdx :: Idris ()
558resetNameIdx = do i <- getIState
559 put (i { idris_nameIdx = (0, emptyContext) })
561-- | Used to preserve sharing of names
562addNameIdx :: Name -> Idris (Int, Name)
563addNameIdx n = do i <- getIState
564 let (i', x) = addNameIdx' i n
568addNameIdx' :: IState -> Name -> (IState, (Int, Name))
570 = let idxs = snd (idris_nameIdx i) in
571 case lookupCtxt n idxs of
573 _ -> let i' = fst (idris_nameIdx i) + 1 in
574 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
576getSymbol :: Name -> Idris Name
577getSymbol n = do i <- getIState
578 case M.lookup n (idris_symbols i) of
580 Nothing -> do let sym' = M.insert n n (idris_symbols i)
581 put (i { idris_symbols = sym' })
584getHdrs :: Codegen -> Idris [String]
585getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
587getImported :: Idris [(FilePath, Bool)]
588getImported = do i <- getIState; return (idris_imported i)
590setErrSpan :: FC -> Idris ()
591setErrSpan x = do i <- getIState;
593 Nothing -> putIState $ i { errSpan = Just x }
597clearErr = do i <- getIState
598 putIState $ i { errSpan = Nothing }
600getSO :: Idris (Maybe String)
601getSO = do i <- getIState
602 return (compiled_so i)
604setSO :: Maybe String -> Idris ()
605setSO s = do i <- getIState
606 putIState (i { compiled_so = s })
608getIState :: Idris IState
611putIState :: IState -> Idris ()
614updateIState :: (IState -> IState) -> Idris ()
615updateIState f = do i <- getIState
618withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
619withContext ctx name dflt action = do
621 case lookupCtxt name (ctx ist) of
625withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
626withContext_ ctx name action = withContext ctx name () action
628-- | A version of liftIO that puts errors into the exception type of
630runIO :: IO a -> Idris a
631runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
632-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
634-- Issue #1738 on the issue tracker.
635-- https://github.com/idris-lang/Idris-dev/issues/1738
638getName = do i <- getIState;
639 let idx = idris_name i;
640 putIState (i { idris_name = idx + 1 })
643-- | InternalApp keeps track of the real function application for
644-- making case splits from, not the application the programmer wrote,
645-- which doesn't have the whole context in any case other than top
647addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
650 -- We canonicalise the path to make "./Test/Module.idr" equal
651 -- to "Test/Module.idr"
652 exists <- runIO $ doesFileExist fp
654 do fp' <- runIO $ canonicalizePath fp
655 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
657getInternalApp :: FilePath -> Int -> Idris PTerm
658getInternalApp fp l = do i <- getIState
659 -- We canonicalise the path to make
660 -- "./Test/Module.idr" equal to
662 exists <- runIO $ doesFileExist fp
664 then do fp' <- runIO $ canonicalizePath fp
665 case lookup (fp', l) (idris_lineapps i) of
667 Nothing -> return Placeholder
668 -- TODO: What if it's not there?
669 else return Placeholder
671-- | Pattern definitions are only used for coverage checking, so erase
672-- them when we're done
673clearOrigPats :: Idris ()
674clearOrigPats = do i <- get
675 let ps = idris_patdefs i
676 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
677 put (i { idris_patdefs = ps' })
679-- | Erase types from Ps in the context (basically ending up with
680-- what's in the .ibc, which is all we need after all the analysis is
682clearPTypes :: Idris ()
683clearPTypes = do i <- get
685 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
686 where pErase (CaseOp c t tys orig tot cds)
687 = CaseOp c t tys orig [] (pErase' cds)
689 pErase' (CaseDefs (cs, c) rs)
690 = let c' = (cs, fmap pEraseType c) in
693checkUndefined :: FC -> Name -> Idris ()
697 (_:_) -> throwError . Msg $ show fc ++ ":" ++
698 show n ++ " already defined"
701isUndefined :: FC -> Name -> Idris Bool
704 case lookupTyExact n i of
705 Just _ -> return False
708setContext :: Context -> Idris ()
709setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
711updateContext :: (Context -> Context) -> Idris ()
712updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
714addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
715addConstraints fc (v, cs)
716 = do tit <- typeInType
720 let ctxt' = ctxt { next_tvar = v }
721 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
722 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
725 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
726 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
727 insertAll ((c, fc) : cs) ics
728 = insertAll cs $ S.insert (ConstraintFC c fc) ics
730addDeferred = addDeferred' Ref
731addDeferredTyCon = addDeferred' (TCon 0 0)
733-- | Save information about a name that is not yet defined
734addDeferred' :: NameType
735 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
736 -- ^ The Name is the name being made into a metavar,
737 -- the Int is the number of vars that are part of a
738 -- putative proof context, the Maybe Name is the
739 -- top-level function containing the new metavariable,
740 -- the Type is its type, and the Bool is whether :p is
744 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
745 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
747 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
748 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
751 -- 'tidyNames' is to generate user accessible names in case they are
752 -- needed in tactic scripts
753 tidyNames used (Bind (MN i x) b sc)
754 = let n' = uniqueNameSet (UN x) used in
755 Bind n' b $ tidyNames (S.insert n' used) sc
756 tidyNames used (Bind n b sc)
757 = let n' = uniqueNameSet n used in
758 Bind n' b $ tidyNames (S.insert n' used) sc
761solveDeferred :: FC -> Name -> Idris ()
764 case lookup n (idris_metavars i) of
765 Just (_, _, _, _, False) ->
766 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
767 _ -> putIState $ i { idris_metavars =
768 filter (\(n', _) -> n/=n')
771 filter (notMV n) (ibc_write i)
773 where notMV n (IBCMetavar n') = not (n == n')
776getUndefined :: Idris [Name]
777getUndefined = do i <- getIState
778 return (map fst (idris_metavars i) \\ primDefs)
780isMetavarName :: Name -> IState -> Bool
782 = case lookupNames n (tt_ctxt ist) of
783 (t:_) -> isJust $ lookup t (idris_metavars ist)
786getWidth :: Idris ConsoleWidth
787getWidth = fmap idris_consolewidth getIState
789setWidth :: ConsoleWidth -> Idris ()
790setWidth w = do ist <- getIState
791 put ist { idris_consolewidth = w }
793setDepth :: Maybe Int -> Idris ()
794setDepth d = do ist <- getIState
795 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
797typeDescription :: String
798typeDescription = "The type of types"
801type1Doc :: Doc OutputAnnotation
802type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
805isetPrompt :: String -> Idris ()
806isetPrompt p = do i <- getIState
807 case idris_outputmode i of
808 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
810-- | Tell clients how much was parsed and loaded
811isetLoadedRegion :: Idris ()
812isetLoadedRegion = do i <- getIState
813 let span = idris_parsedSpan i
816 case idris_outputmode i of
818 runIO . hPutStrLn h $
819 convSExp "set-loaded-region" fc n
822setLogLevel :: Int -> Idris ()
823setLogLevel l = do i <- getIState
824 let opts = idris_options i
825 let opt' = opts { opt_logLevel = l }
826 putIState $ i { idris_options = opt' }
828setLogCats :: [LogCat] -> Idris ()
831 let opts = idris_options i
832 let opt' = opts { opt_logcats = cs }
833 putIState $ i { idris_options = opt' }
835setCmdLine :: [Opt] -> Idris ()
836setCmdLine opts = do i <- getIState
837 let iopts = idris_options i
838 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
840getCmdLine :: Idris [Opt]
841getCmdLine = do i <- getIState
842 return (opt_cmdline (idris_options i))
844getDumpHighlighting :: Idris Bool
845getDumpHighlighting = do ist <- getIState
846 return (findC (opt_cmdline (idris_options ist)))
847 where findC = elem DumpHighlights
849getDumpDefun :: Idris (Maybe FilePath)
850getDumpDefun = do i <- getIState
851 return $ findC (opt_cmdline (idris_options i))
852 where findC [] = Nothing
853 findC (DumpDefun x : _) = Just x
854 findC (_ : xs) = findC xs
856getDumpCases :: Idris (Maybe FilePath)
857getDumpCases = do i <- getIState
858 return $ findC (opt_cmdline (idris_options i))
859 where findC [] = Nothing
860 findC (DumpCases x : _) = Just x
861 findC (_ : xs) = findC xs
864logLevel = do i <- getIState
865 return (opt_logLevel (idris_options i))
867setAutoImpls :: Bool -> Idris ()
868setAutoImpls b = do i <- getIState
869 let opts = idris_options i
870 let opt' = opts { opt_autoimpls = b }
871 putIState $ i { idris_options = opt' }
873getAutoImpls :: Idris Bool
874getAutoImpls = do i <- getIState
875 return (opt_autoimpls (idris_options i))
877setErrContext :: Bool -> Idris ()
878setErrContext t = do i <- getIState
879 let opts = idris_options i
880 let opts' = opts { opt_errContext = t }
881 putIState $ i { idris_options = opts' }
883errContext :: Idris Bool
884errContext = do i <- getIState
885 return (opt_errContext (idris_options i))
887getOptimise :: Idris [Optimisation]
888getOptimise = do i <- getIState
889 return (opt_optimise (idris_options i))
891setOptimise :: [Optimisation] -> Idris ()
892setOptimise newopts = do i <- getIState
893 let opts = idris_options i
894 let opts' = opts { opt_optimise = newopts }
895 putIState $ i { idris_options = opts' }
897addOptimise :: Optimisation -> Idris ()
898addOptimise opt = do opts <- getOptimise
899 setOptimise (nub (opt : opts))
901removeOptimise :: Optimisation -> Idris ()
902removeOptimise opt = do opts <- getOptimise
903 setOptimise ((nub opts) \\ [opt])
905-- | Set appropriate optimisation set for the given level. We only
906-- have one optimisation that is configurable at the moment, however!
907setOptLevel :: Int -> Idris ()
908setOptLevel n | n <= 0 = setOptimise []
909setOptLevel 1 = setOptimise []
910setOptLevel 2 = setOptimise [PETransform]
911setOptLevel n | n >= 3 = setOptimise [PETransform]
914useREPL = do i <- getIState
915 return (opt_repl (idris_options i))
917setREPL :: Bool -> Idris ()
918setREPL t = do i <- getIState
919 let opts = idris_options i
920 let opt' = opts { opt_repl = t }
921 putIState $ i { idris_options = opt' }
923showOrigErr :: Idris Bool
924showOrigErr = do i <- getIState
925 return (opt_origerr (idris_options i))
927setShowOrigErr :: Bool -> Idris ()
928setShowOrigErr b = do i <- getIState
929 let opts = idris_options i
930 let opt' = opts { opt_origerr = b }
931 putIState $ i { idris_options = opt' }
933setAutoSolve :: Bool -> Idris ()
934setAutoSolve b = do i <- getIState
935 let opts = idris_options i
936 let opt' = opts { opt_autoSolve = b }
937 putIState $ i { idris_options = opt' }
939setNoBanner :: Bool -> Idris ()
940setNoBanner n = do i <- getIState
941 let opts = idris_options i
942 let opt' = opts { opt_nobanner = n }
943 putIState $ i { idris_options = opt' }
945getNoBanner :: Idris Bool
946getNoBanner = do i <- getIState
947 let opts = idris_options i
948 return (opt_nobanner opts)
950setEvalTypes :: Bool -> Idris ()
951setEvalTypes n = do i <- getIState
952 let opts = idris_options i
953 let opt' = opts { opt_evaltypes = n }
954 putIState $ i { idris_options = opt' }
956getDesugarNats :: Idris Bool
957getDesugarNats = do i <- getIState
958 let opts = idris_options i
959 return (opt_desugarnats opts)
962setDesugarNats :: Bool -> Idris ()
963setDesugarNats n = do i <- getIState
964 let opts = idris_options i
965 let opt' = opts { opt_desugarnats = n }
966 putIState $ i { idris_options = opt' }
968setQuiet :: Bool -> Idris ()
969setQuiet q = do i <- getIState
970 let opts = idris_options i
971 let opt' = opts { opt_quiet = q }
972 putIState $ i { idris_options = opt' }
974getQuiet :: Idris Bool
975getQuiet = do i <- getIState
976 let opts = idris_options i
977 return (opt_quiet opts)
979setCodegen :: Codegen -> Idris ()
980setCodegen t = do i <- getIState
981 let opts = idris_options i
982 let opt' = opts { opt_codegen = t }
983 putIState $ i { idris_options = opt' }
985codegen :: Idris Codegen
986codegen = do i <- getIState
987 return (opt_codegen (idris_options i))
990setOutputTy :: OutputType -> Idris ()
991setOutputTy t = do i <- getIState
992 let opts = idris_options i
993 let opt' = opts { opt_outputTy = t }
994 putIState $ i { idris_options = opt' }
996outputTy :: Idris OutputType
997outputTy = do i <- getIState
998 return $ opt_outputTy $ idris_options i
1000setIdeMode :: Bool -> Handle -> Idris ()
1001setIdeMode True h = do i <- getIState
1002 putIState $ i { idris_outputmode = IdeMode 0 h
1003 , idris_colourRepl = False
1005setIdeMode False _ = return ()
1007setTargetTriple :: String -> Idris ()
1008setTargetTriple t = do i <- getIState
1009 let opts = idris_options i
1010 opt' = opts { opt_triple = t }
1011 putIState $ i { idris_options = opt' }
1013targetTriple :: Idris String
1014targetTriple = do i <- getIState
1015 return (opt_triple (idris_options i))
1017setTargetCPU :: String -> Idris ()
1018setTargetCPU t = do i <- getIState
1019 let opts = idris_options i
1020 opt' = opts { opt_cpu = t }
1021 putIState $ i { idris_options = opt' }
1023targetCPU :: Idris String
1024targetCPU = do i <- getIState
1025 return (opt_cpu (idris_options i))
1030 -- Quietness overrides verbosity
1031 let quiet = opt_quiet $ idris_options i
1034 else return $ (opt_verbose $ idris_options i)
1036setVerbose :: Int -> Idris ()
1039 let opts = idris_options i
1040 let opt' = opts { opt_verbose = t }
1041 putIState $ i { idris_options = opt' }
1043iReport :: Int -> String -> Idris ()
1044iReport level msg = do
1045 verbosity <- verbose
1047 when (level <= verbosity) $
1048 case idris_outputmode i of
1049 RawOutput h -> runIO $ hPutStrLn h msg
1050 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" msg n
1053typeInType :: Idris Bool
1054typeInType = do i <- getIState
1055 return (opt_typeintype (idris_options i))
1057setTypeInType :: Bool -> Idris ()
1058setTypeInType t = do i <- getIState
1059 let opts = idris_options i
1060 let opt' = opts { opt_typeintype = t }
1061 putIState $ i { idris_options = opt' }
1063coverage :: Idris Bool
1064coverage = do i <- getIState
1065 return (opt_coverage (idris_options i))
1067setCoverage :: Bool -> Idris ()
1068setCoverage t = do i <- getIState
1069 let opts = idris_options i
1070 let opt' = opts { opt_coverage = t }
1071 putIState $ i { idris_options = opt' }
1073setIBCSubDir :: FilePath -> Idris ()
1074setIBCSubDir fp = do i <- getIState
1075 let opts = idris_options i
1076 let opt' = opts { opt_ibcsubdir = fp }
1077 putIState $ i { idris_options = opt' }
1079valIBCSubDir :: IState -> Idris FilePath
1080valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1082addImportDir :: FilePath -> Idris ()
1083addImportDir fp = do i <- getIState
1084 let opts = idris_options i
1085 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1086 putIState $ i { idris_options = opt' }
1088setImportDirs :: [FilePath] -> Idris ()
1089setImportDirs fps = do i <- getIState
1090 let opts = idris_options i
1091 let opt' = opts { opt_importdirs = fps }
1092 putIState $ i { idris_options = opt' }
1094allImportDirs :: Idris [FilePath]
1095allImportDirs = do i <- getIState
1096 let optdirs = opt_importdirs (idris_options i)
1097 return ("." : reverse optdirs)
1099addSourceDir :: FilePath -> Idris ()
1100addSourceDir fp = do i <- getIState
1101 let opts = idris_options i
1102 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1103 putIState $ i { idris_options = opts' }
1105setSourceDirs :: [FilePath] -> Idris ()
1106setSourceDirs fps = do i <- getIState
1107 let opts = idris_options i
1108 let opts' = opts { opt_sourcedirs = nub $ fps }
1109 putIState $ i { idris_options = opts' }
1111allSourceDirs :: Idris [FilePath]
1112allSourceDirs = do i <- getIState
1113 let optdirs = opt_sourcedirs (idris_options i)
1114 return ("." : reverse optdirs)
1116colourise :: Idris Bool
1117colourise = do i <- getIState
1118 return $ idris_colourRepl i
1120setColourise :: Bool -> Idris ()
1121setColourise b = do i <- getIState
1122 putIState $ i { idris_colourRepl = b }
1124impShow :: Idris Bool
1125impShow = do i <- getIState
1126 return (opt_showimp (idris_options i))
1128setImpShow :: Bool -> Idris ()
1129setImpShow t = do i <- getIState
1130 let opts = idris_options i
1131 let opt' = opts { opt_showimp = t }
1132 putIState $ i { idris_options = opt' }
1134setColour :: ColourType -> IdrisColour -> Idris ()
1135setColour ct c = do i <- getIState
1136 let newTheme = setColour' ct c (idris_colourTheme i)
1137 putIState $ i { idris_colourTheme = newTheme }
1138 where setColour' KeywordColour c t = t { keywordColour = c }
1139 setColour' BoundVarColour c t = t { boundVarColour = c }
1140 setColour' ImplicitColour c t = t { implicitColour = c }
1141 setColour' FunctionColour c t = t { functionColour = c }
1142 setColour' TypeColour c t = t { typeColour = c }
1143 setColour' DataColour c t = t { dataColour = c }
1144 setColour' PromptColour c t = t { promptColour = c }
1145 setColour' PostulateColour c t = t { postulateColour = c }
1148logLvl :: Int -> String -> Idris ()
1149logLvl = logLvlCats []
1151logCoverage :: Int -> String -> Idris ()
1152logCoverage = logLvlCats [ICoverage]
1154logErasure :: Int -> String -> Idris ()
1155logErasure = logLvlCats [IErasure]
1157-- | Log an action of the parser
1158logParser :: Int -> String -> Idris ()
1159logParser = logLvlCats parserCats
1161-- | Log an action of the elaborator.
1162logElab :: Int -> String -> Idris ()
1163logElab = logLvlCats elabCats
1165-- | Log an action of the compiler.
1166logCodeGen :: Int -> String -> Idris ()
1167logCodeGen = logLvlCats codegenCats
1169logIBC :: Int -> String -> Idris ()
1170logIBC = logLvlCats [IIBC]
1172-- | Log aspect of Idris execution
1174-- An empty set of logging levels is used to denote all categories.
1176-- @TODO update IDE protocol
1177logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1178 -> Int -- ^ The Logging level the message should appear.
1179 -> String -- ^ The message to show the developer.
1181logLvlCats cs l str = do
1183 let lvl = opt_logLevel (idris_options i)
1184 let cats = opt_logcats (idris_options i)
1186 when (inCat cs cats || null cats) $
1187 case idris_outputmode i of
1189 runIO $ hPutStrLn h str
1191 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1192 runIO . hPutStrLn h $ convSExp "log" good n
1194 inCat :: [LogCat] -> [LogCat] -> Bool
1195 inCat cs cats = any (`elem` cats) cs
1197cmdOptType :: Opt -> Idris Bool
1198cmdOptType x = do i <- getIState
1199 return $ x `elem` opt_cmdline (idris_options i)
1201noErrors :: Idris Bool
1202noErrors = do i <- getIState
1204 Nothing -> return True
1207setTypeCase :: Bool -> Idris ()
1208setTypeCase t = do i <- getIState
1209 let opts = idris_options i
1210 let opt' = opts { opt_typecase = t }
1211 putIState $ i { idris_options = opt' }
1214-- Dealing with parameters
1216expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1217 [Name] -> -- all names
1218 [Name] -> -- names with no declaration
1220expandParams dec ps ns infs tm = en 0 tm
1222 -- if we shadow a name (say in a lambda binding) that is used in a call to
1223 -- a lifted function, we need access to both names - once in the scope of the
1224 -- binding and once to call the lifted functions. So we'll explicitly shadow
1225 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1226 -- but we didn't...)
1228 mkShadow (UN n) = MN 0 n
1229 mkShadow (MN i n) = MN (i+1) n
1230 mkShadow (NS x s) = NS (mkShadow x) s
1232 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1233 -- that are merely mentioned.
1235 en 0 (PLam fc n nfc t s)
1236 | n `elem` (map fst ps ++ ns)
1237 = let n' = mkShadow n in
1238 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1239 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1240 en 0 (PPi p n nfc t s)
1241 | n `elem` (map fst ps ++ ns)
1242 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1243 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1244 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1245 en 0 (PLet fc n nfc ty v s)
1246 | n `elem` (map fst ps ++ ns)
1247 = let n' = mkShadow n in
1248 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1249 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1250 -- FIXME: Should only do this in a type signature!
1251 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1252 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1253 = let n' = mkShadow n in
1254 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1255 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1256 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1257 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1258 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1259 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1260 en 0 (PHidden t) = PHidden (en 0 t)
1261 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1262 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1263 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1264 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1265 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1266 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1268 en 0 (PQuote (Var n))
1269 | n `nselem` ns = PQuote (Var (dec n))
1270 en 0 (PApp fc (PInferRef fc' hl n) as)
1271 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1272 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1273 en 0 (PApp fc (PRef fc' hl n) as)
1274 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1275 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1276 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1277 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1278 en 0 (PAppBind fc (PRef fc' hl n) as)
1279 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1280 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1281 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1282 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1284 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1285 (map ((pexp . (PRef fc hl)) . fst) ps)
1286 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1287 (map ((pexp . (PRef fc hl)) . fst) ps)
1288 en 0 (PInferRef fc hl n)
1289 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1290 (map ((pexp . (PRef fc hl)) . fst) ps)
1291 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1292 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1293 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1294 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1295 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1296 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1298 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1299 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1301 en ql t = descend (en ql) t
1304 nselem x (y : xs) | nseq x y = True
1305 | otherwise = nselem x xs
1307 nseq x y = nsroot x == nsroot y
1309 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1310 enTacImp ql other = other
1312expandParamsD :: Bool -> -- True = RHS only
1314 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1315expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1316 = if n `elem` ns && (not rhsonly)
1317 then -- trace (show (n, expandParams dec ps ns ty)) $
1318 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1319 else --trace (show (n, expandParams dec ps ns ty)) $
1320 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1321expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1322 = if n `elem` ns && (not rhsonly)
1323 then -- trace (show (n, expandParams dec ps ns ty)) $
1324 PPostulate e doc syn fc nfc o (dec n)
1325 (piBind ps (expandParams dec ps ns [] ty))
1326 else --trace (show (n, expandParams dec ps ns ty)) $
1327 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1328expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1329 = let n' = if n `elem` ns then dec n else n in
1330 PClauses fc opts n' (map expandParamsC cs)
1332 expandParamsC (PClause fc n lhs ws rhs ds)
1333 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1334 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1335 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1336 n' = if n `elem` ns then dec n else n
1337 -- names bound on the lhs should not be expanded on the rhs
1338 ns' = removeBound lhs ns in
1340 (map (expandParams dec ps'' ns' []) ws)
1341 (expandParams dec ps'' ns' [] rhs)
1342 (map (expandParamsD True ist dec ps'' ns') ds)
1343 expandParamsC (PWith fc n lhs ws wval pn ds)
1344 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1345 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1346 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1347 n' = if n `elem` ns then dec n else n
1348 ns' = removeBound lhs ns in
1350 (map (expandParams dec ps'' ns' []) ws)
1351 (expandParams dec ps'' ns' [] wval)
1353 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1354 updateps yn nm [] = []
1355 updateps yn nm (((a, t), i):as)
1356 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1357 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1359 removeBound lhs ns = ns \\ nub (bnames lhs)
1361 bnames (PRef _ _ n) = [n]
1362 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1363 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1364 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1367-- | Expands parameters defined in parameter and where blocks inside of declarations
1368expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1369 = PData doc argDocs syn fc co (expandPData pd)
1371 -- just do the type decl, leave constructors alone (parameters will be
1372 -- added implicitly)
1373 expandPData (PDatadecl n nfc ty cons)
1375 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1377 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1378 econ (doc, argDocs, n, nfc, t, fc, fs)
1379 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1380expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1382expandParamsD rhs ist dec ps ns (PParams f params pds)
1383 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1384 (map (expandParamsD True ist dec ps ns) pds)
1385-- (map (expandParamsD ist dec ps ns) pds)
1386expandParamsD rhs ist dec ps ns (PMutual f pds)
1387 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1388expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1389 = PInterface doc info f
1390 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1392 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1395 (map (expandParamsD rhs ist dec ps ns) decls)
1398expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1399 = let cn' = case cn of
1400 Just n -> if n `elem` ns then Just (dec n) else Just n
1401 Nothing -> Nothing in
1402 PImplementation doc argDocs info f
1403 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1406 (map (expandParams dec ps ns []) params)
1407 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1408 (expandParams dec ps ns [] ty)
1410 (map (expandParamsD True ist dec ps ns) decls)
1411expandParamsD rhs ist dec ps ns d = d
1413mapsnd f (x, t) = (x, f t)
1415expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1416 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1418expandImplementationScope ist dec ps ns d = d
1420-- | Calculate a priority for a type, for deciding elaboration order
1421-- * if it's just a type variable or concrete type, do it early (0)
1422-- * if there's only type variables and injective constructors, do it next (1)
1423-- * if there's a function type, next (2)
1424-- * finally, everything else (3)
1425getPriority :: IState -> PTerm -> Int
1426getPriority i tm = 1 -- pri tm
1429 case lookupP n (tt_ctxt i) of
1430 ((P (DCon _ _ _) _ _):_) -> 1
1431 ((P (TCon _ _) _ _):_) -> 1
1432 ((P Ref _ _):_) -> 1
1433 [] -> 0 -- must be locally bound, if it's not an error...
1434 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1436 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1437 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1438 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1439 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1440 pri (PTyped l r) = pri l
1441 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1442 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1443 pri (PAlternative _ a as) = maximum (map pri as)
1444 pri (PConstant _ _) = 0
1449addStatics :: Name -> Term -> PTerm -> Idris ()
1450addStatics n tm ptm =
1451 do let (statics, dynamics) = initStatics tm ptm
1454 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1455 Just p -> getNamesFrom 0 (fn_params p) tm ++
1456 concatMap (getParamNames ist . snd) statics
1457 _ -> concatMap (getParamNames ist . snd) statics
1459 let stnames = nub $ concatMap (freeArgNames . snd) statics
1460 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1462 -- also get the arguments which are 'uniquely inferrable' from
1463 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1464 -- or parameters to the type of a static
1465 let statics' = nub $ map fst statics ++
1466 filter (\x -> not (elem x dnames)) stnames
1467 let stpos = staticList statics' tm
1469 unless (null statics) $
1470 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1471 ++ showTmImpls ptm ++ "\n"
1472 ++ show statics ++ "\n" ++ show dynamics
1473 ++ "\n" ++ show paramnames
1474 ++ "\n" ++ show stpos
1475 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1476 addIBC (IBCStatic n)
1478 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1479 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1480 (static, (n, ty) : dynamic)
1481 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1482 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1483 if pstatic p == Static then ((n, ty) : static, dynamic)
1484 else if (not (searchArg p))
1485 then (static, (n, ty) : dynamic)
1486 else (static, dynamic)
1487 initStatics t pt = ([], [])
1489 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1490 = case lookupCtxtExact n (idris_datatypes ist) of
1491 Just ti -> getNamePos 0 (param_pos ti) args
1493 where getNamePos i ps [] = []
1494 getNamePos i ps (P _ n _ : as)
1495 | i `elem` ps = n : getNamePos (i + 1) ps as
1496 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1497 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1498 = n : getParamNames ist sc
1499 getParamNames ist _ = []
1501 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1502 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1503 | otherwise = getNamesFrom (i + 1) ps sc
1504 getNamesFrom i ps sc = []
1506 freeArgNames (Bind n (Pi _ ty _) sc)
1507 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1508 freeArgNames tm = let (_, args) = unApply tm in
1509 concatMap freeNames args
1511 -- if a name appears in an interface or tactic implicit index, it doesn't
1512 -- affect its 'uniquely inferrable' from a static status since these are
1513 -- resolved by searching.
1514 searchArg (Constraint _ _) = True
1515 searchArg (TacImp _ _ _) = True
1518 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1521-- Dealing with implicit arguments
1523-- Add some bound implicits to the using block if they aren't there already
1525addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1526addToUsing us [] = us
1527addToUsing us ((n, t) : ns)
1528 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1529 | otherwise = addToUsing us ns
1530 where impName (UImplicit n _) = Just n
1533-- Add constraint bindings from using block
1535addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1536addUsingConstraints syn fc t
1538 let ns = namesIn [] ist t
1539 let cs = getConstraints t -- check declared constraints
1540 let addconsts = uconsts \\ cs
1541 return (doAdd addconsts ns t)
1542 where uconsts = filter uconst (using syn)
1543 uconst (UConstraint _ _) = True
1547 -- if all of args in ns, then add it
1548 doAdd (UConstraint c args : cs) ns t
1549 | all (\n -> elem n ns) args
1550 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1551 (mkConst c args) (doAdd cs ns t)
1552 | otherwise = doAdd cs ns t
1554 mkConst c args = PApp fc (PRef fc [] c)
1555 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1557 getConstraints (PPi (Constraint _ _) _ _ c sc)
1558 = getcapp c ++ getConstraints sc
1559 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1560 getConstraints _ = []
1562 getcapp (PApp _ (PRef _ _ c) args)
1563 = do ns <- mapM getName args
1564 return (UConstraint c ns)
1567 getName (PExp _ _ _ (PRef _ _ n)) = return n
1570-- | Add implicit bindings from using block, and bind any missing names
1571addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1572addUsingImpls syn n fc t
1573 = do ist <- getIState
1574 autoimpl <- getAutoImpls
1575 let ns_in = implicitNamesIn (map iname uimpls) ist t
1576 let ns = if autoimpl then ns_in
1577 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1579 let badnames = filter (\n -> not (implicitable n) &&
1580 n `notElem` (map iname uimpls)) ns
1581 unless (null badnames) $
1582 throwError (At fc (Elaborating "type of " n Nothing
1583 (NoSuchVariable (head badnames))))
1584 let cs = getArgnames t -- get already bound names
1585 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1586 -- if all names in the arguments of addconsts appear in ns,
1587 -- add the constraint implicitly
1588 return (bindFree ns (doAdd addimpls ns t))
1589 where uimpls = filter uimpl (using syn)
1590 uimpl (UImplicit _ _) = True
1593 iname (UImplicit n _) = n
1594 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1597 -- if all of args in ns, then add it
1598 doAdd (UImplicit n ty : cs) ns t
1600 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1601 | otherwise = doAdd cs ns t
1603 -- bind the free names which weren't in the using block
1606 | elem n (map iname uimpls) = bindFree ns tm
1608 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1610 getArgnames (PPi _ n _ c sc)
1611 = n : getArgnames sc
1614-- Given the original type and the elaborated type, return the implicitness
1615-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1617getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1618getUnboundImplicits i t tm = getImps t (collectImps tm)
1619 where collectImps (PPi p n _ t sc)
1620 = (n, (p, t)) : collectImps sc
1623 scopedimpl (Just i) = not (toplevel_imp i)
1624 scopedimpl _ = False
1626 getImps (Bind n (Pi i _ _) sc) imps
1627 | scopedimpl i = getImps sc imps
1628 getImps (Bind n (Pi _ t _) sc) imps
1629 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1631 argInfo n (Imp opt _ _ _ _) Placeholder
1632 = (True, PImp 0 True opt n Placeholder)
1633 argInfo n (Imp opt _ _ _ _) t'
1634 = (False, PImp (getPriority i t') True opt n t')
1635 argInfo n (Exp opt _ _) t'
1636 = (InaccessibleArg `elem` opt,
1637 PExp (getPriority i t') opt n t')
1638 argInfo n (Constraint opt _) t'
1639 = (InaccessibleArg `elem` opt,
1640 PConstraint 10 opt n t')
1641 argInfo n (TacImp opt _ scr) t'
1642 = (InaccessibleArg `elem` opt,
1643 PTacImplicit 10 opt n scr t')
1644 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1645 where impBind n t = (True, PImp 1 True [] n Placeholder)
1648-- Add implicit Pi bindings for any names in the term which appear in an
1649-- argument position.
1651-- This has become a right mess already. Better redo it some time...
1652-- TODO: This is obsoleted by the new way of elaborating types, (which
1653-- calls addUsingImpls) but there's still a couple of places which use
1654-- it. Clean them up!
1656-- Issue 1739 in the issue tracker
1657-- https://github.com/idris-lang/Idris-dev/issues/1739
1658implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1659implicit info syn n ptm = implicit' info syn [] n ptm
1661implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1662implicit' info syn ignore n ptm
1664 auto <- getAutoImpls
1665 let (tm', impdata) = implicitise auto syn ignore i ptm
1666 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1667-- let (tm'', spos) = findStatics i tm'
1668 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1670 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1672-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1675 -- Detect unknown names in default arguments and throw error if found.
1676 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1677 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1679 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1680 notFoundInDefault kns (PTacImplicit _ _ n script _)
1682 case notFound kns (namesIn [] i script) of
1683 Nothing -> return (n:kns)
1684 Just name -> throwError (NoSuchVariable name)
1685 notFoundInDefault kns p = return ((pname p):kns)
1687 notFound :: [Name] -> [Name] -> Maybe Name
1688 notFound kns [] = Nothing
1689 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1690 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1692-- | Even if auto_implicits is off, we need to call this so we record
1693-- which arguments are implicit
1694implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1695implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1696 let (declimps, ns') = execState (imps True [] tm) ([], [])
1697 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1698 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1699 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1701 then (tm, reverse declimps)
1702 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1704 uvars = map ipair (filter uimplicit (using syn))
1705 pvars = syn_params syn
1707 inUsing n = n `elem` map fst uvars
1709 ipair (UImplicit x y) = (x, y)
1710 uimplicit (UImplicit _ _) = True
1713 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1714 | otherwise = x : dropAll xs ys
1717 -- Find names in argument position in a type, suitable for implicit
1719 -- Not the function position, but do everything else...
1720 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1721 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1723 imps top env ty@(PApp _ f as)
1724 = do (decls, ns) <- get
1725 let isn = nub (implNamesIn uvars ty)
1726 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1727 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1728 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1730 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1731 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1732 imps True (n:env) sc
1733 imps top env (PPi (Exp l _ _) n _ ty sc)
1734 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1735 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1737 (decls, ns) <- get -- ignore decls in HO types
1738 put (PExp (getPriority ist ty) l n Placeholder : decls,
1739 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1740 imps True (n:env) sc
1741 imps top env (PPi (Constraint l _) n _ ty sc)
1742 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1743 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1745 (decls, ns) <- get -- ignore decls in HO types
1746 put (PConstraint 10 l n Placeholder : decls,
1747 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1748 imps True (n:env) sc
1749 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1750 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1751 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1753 (decls, ns) <- get -- ignore decls in HO types
1754 put (PTacImplicit 10 l n scr Placeholder : decls,
1755 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1756 imps True (n:env) sc
1757 imps top env (PRewrite _ _ l r _)
1758 = do (decls, ns) <- get
1759 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1760 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1761 imps top env (PTyped l r)
1763 imps top env (PPair _ _ _ l r)
1764 = do (decls, ns) <- get
1765 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1766 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1767 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1768 = do (decls, ns) <- get
1769 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1770 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1771 imps top env (PDPair _ _ _ l t r)
1772 = do (decls, ns) <- get
1773 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1775 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1776 imps top env (PAlternative ms a as)
1777 = do (decls, ns) <- get
1778 let isn = concatMap (namesIn uvars ist) as
1779 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1780 imps top env (PLam fc n _ ty sc)
1781 = do imps False env ty
1782 imps False (n:env) sc
1783 imps top env (PHidden tm) = imps False env tm
1784 imps top env (PUnifyLog tm) = imps False env tm
1785 imps top env (PNoImplicits tm) = imps False env tm
1786 imps top env (PRunElab fc tm ns) = imps False env tm
1787 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1788 imps top env _ = return ()
1790 pibind using [] sc = sc
1791 pibind using (n:ns) sc
1792 = case lookup n using of
1793 Just ty -> PPi impl_gen
1794 n NoFC ty (pibind using ns sc)
1795 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1796 n NoFC Placeholder (pibind using ns sc)
1798-- | Add implicit arguments in function calls
1799addImplPat :: IState -> PTerm -> PTerm
1800addImplPat = addImpl' True [] [] []
1802addImplBound :: IState -> [Name] -> PTerm -> PTerm
1803addImplBound ist ns = addImpl' False ns [] [] ist
1805addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1806addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1808-- | Add the implicit arguments to applications in the term [Name]
1809-- gives the names to always expend, even when under a binder of that
1810-- name (this is to expand methods with implicit arguments in
1811-- dependent interfaces).
1812addImpl :: [Name] -> IState -> PTerm -> PTerm
1813addImpl = addImpl' False [] []
1815-- TODO: in patterns, don't add implicits to function names guarded by constructors
1816-- and *not* inside a PHidden
1818addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1819addImpl' inpat env infns imp_meths ist ptm
1820 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1822 topname = case ptm of
1824 PApp _ (PRef _ _ n) _ -> n
1825 _ -> sUN "" -- doesn't matter then
1827 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1828 ai inpat qq env ds (PRef fc fcs f)
1829 | f `elem` infns = PInferRef fc fcs f
1830 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1831 ai inpat qq env ds (PHidden (PRef fc hl f))
1832 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1833 ai inpat qq env ds (PRewrite fc by l r g)
1834 = let l' = ai inpat qq env ds l
1835 r' = ai inpat qq env ds r
1836 g' = fmap (ai inpat qq env ds) g in
1837 PRewrite fc by l' r' g'
1838 ai inpat qq env ds (PTyped l r)
1839 = let l' = ai inpat qq env ds l
1840 r' = ai inpat qq env ds r in
1842 ai inpat qq env ds (PPair fc hls p l r)
1843 = let l' = ai inpat qq env ds l
1844 r' = ai inpat qq env ds r in
1845 PPair fc hls p l' r'
1846 ai inpat qq env ds (PDPair fc hls p l t r)
1847 = let l' = ai inpat qq env ds l
1848 t' = ai inpat qq env ds t
1849 r' = ai inpat qq env ds r in
1850 PDPair fc hls p l' t' r'
1851 ai inpat qq env ds (PAlternative ms a as)
1852 = let as' = map (ai inpat qq env ds) as in
1853 PAlternative ms a as'
1854 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1855 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1856 = let as' = map (fmap (ai inpat qq env ds)) as in
1857 PApp fc (PInferRef ffc hl f) as'
1858 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1859 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1860 | not (f `elem` map fst env)
1861 = let as' = map (fmap (ai inpat qq env ds)) as in
1862 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1863 | Just (Just ty) <- lookup f env =
1864 let as' = map (fmap (ai inpat qq env ds)) as
1865 arity = getPArity ty in
1866 mkPApp fc arity ftm as'
1867 ai inpat qq env ds (PApp fc f as)
1868 = let f' = ai inpat qq env ds f
1869 as' = map (fmap (ai inpat qq env ds)) as in
1871 ai inpat qq env ds (PWithApp fc f a)
1872 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1873 ai inpat qq env ds (PCase fc c os)
1874 = let c' = ai inpat qq env ds c in
1875 -- leave lhs alone, because they get lifted into a new pattern match
1876 -- definition which is passed through addImpl again
1877 PCase fc c' (map aiCase os)
1880 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1882 -- Anything beginning with a lower case letter, not applied,
1883 -- and no namespace is a pattern variable
1884 patnames (PApp _ (PRef _ _ f) [])
1885 | implicitable f = [(f, Nothing)]
1886 patnames (PRef _ _ f)
1887 | implicitable f = [(f, Nothing)]
1888 patnames (PApp _ (PRef _ _ _) args)
1889 = concatMap patnames (map getTm args)
1890 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1891 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1892 patnames (PAs _ _ t) = patnames t
1893 patnames (PAlternative _ _ ts) = concatMap patnames ts
1897 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1898 (ai inpat qq env ds t)
1899 (ai inpat qq env ds f)
1901 -- If the name in a lambda is an unapplied data constructor name, do this
1902 -- as a 'case' instead because we'll expect to match on it
1903 ai inpat qq env ds (PLam fc n nfc ty sc)
1904 = if canBeDConName n (tt_ctxt ist)
1905 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1906 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1907 [(PRef fc [] n, sc)]))
1908 else let ty' = ai inpat qq env ds ty
1909 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1910 PLam fc n nfc ty' sc'
1911 ai inpat qq env ds (PLet fc n nfc ty val sc)
1912 = if canBeDConName n (tt_ctxt ist)
1913 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1914 else let ty' = ai inpat qq env ds ty
1915 val' = ai inpat qq env ds val
1916 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1917 PLet fc n nfc ty' val' sc'
1918 ai inpat qq env ds (PPi p n nfc ty sc)
1919 = let ty' = ai inpat qq env ds ty
1920 env' = if n `elem` imp_meths then env
1921 else ((n, Just ty) : env)
1922 sc' = ai inpat qq env' ds sc in
1924 ai inpat qq env ds (PGoal fc r n sc)
1925 = let r' = ai inpat qq env ds r
1926 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1928 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1929 -- Don't do PProof or PTactics since implicits get added when scope is
1930 -- properly known in ElabTerm.runTac
1931 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1932 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1933 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1934 (fmap (ai inpat True env ds) g)
1935 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1936 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1937 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1938 ai inpat qq env ds tm = tm
1940 handleErr (Left err) = PElabError err
1941 handleErr (Right x) = x
1943-- if in a pattern, and there are no arguments, and there's no possible
1944-- names with zero explicit arguments, don't add implicits.
1946aiFn :: Name -> Bool -> Bool -> Bool
1949 -> Name -- ^ function being applied
1951 -> [PArg] -- ^ initial arguments (if in a pattern)
1953aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1954 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1956 = case lookupDef f (tt_ctxt ist) of
1957 [] -> Right $ PPatvar ffc f
1958 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1959 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1960 if (not (vname f) || tcname f
1961 || any (conCaf (tt_ctxt ist)) ialts)
1962-- any constructor alts || any allImp ialts))
1963 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1964 else Right $ PPatvar ffc f
1965 where imp (PExp _ _ _ _) = False
1968 allImp xs = all imp xs
1970 unqualified (NS _ _) = False
1971 unqualified _ = True
1973 constructor (TyDecl (DCon _ _ _) _) = True
1974 constructor _ = False
1976 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1978 vname (UN n) = True -- non qualified
1981aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1982 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1983aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1984 -- This is where namespaces get resolved by adding PAlternative
1985 = do let ns = lookupCtxtName f (idris_implicits ist)
1986 let nh = filter (\(n, _) -> notHidden n) ns
1987 let ns' = case trimAlts ds nh of
1991 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1993 [] -> case metaVar f (map fst (idris_metavars ist)) of
1994 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1995 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1997 PAlternative [] (ExactlyOne True) $
1998 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1999 (insertImpl ns as)) alts
2001 -- if the name is in imp_meths, we should actually refer to the bound
2002 -- name rather than the global one after expanding implicits
2003 isImpName f f' | f `elem` imp_meths = f
2006 -- If it's a metavariable name, try to qualify it from the list of
2007 -- unsolved metavariables
2008 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
2009 metaVar f (_ : ns) = metaVar f ns
2010 metaVar f [] = Nothing
2012 trimAlts [] alts = alts
2014 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
2019 notHidden n = case getAccessibility n of
2025 = case lookupDefAccExact n False (tt_ctxt ist) of
2029 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
2030 -> [PArg] -- ^ given arguments
2033 = let (as', badimpls) = partition (impIn ps) as in
2034 map addUnknownImp badimpls ++
2035 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
2037 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2038 -> [PArg] -- parameters
2039 -> [PArg] -- explicit arguments
2040 -> [PArg] -- implicits given
2042 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2043 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2044 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2045 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2046 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2047 let rtc = PResolveTC fc in
2048 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2049 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2050 case find n imps [] of
2052 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2054 PImp p True l n Placeholder :
2055 insImpAcc (M.insert n Placeholder pnas) ps given imps
2056 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2057 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2058 case find n imps [] of
2060 PTacImplicit p l n sc tm :
2061 insImpAcc (M.insert n tm pnas) ps given imps'
2064 then PTacImplicit p l n sc Placeholder :
2065 insImpAcc (M.insert n Placeholder pnas) ps given imps
2066 else PTacImplicit p l n sc sc :
2067 insImpAcc (M.insert n sc pnas) ps given imps
2068 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2069 insImpAcc _ _ given imps = given ++ imps
2071 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2073 find n [] acc = Nothing
2074 find n (PImp _ _ _ n' t : gs) acc
2075 | n == n' = Just (t, reverse acc ++ gs)
2076 find n (PTacImplicit _ _ n' _ t : gs) acc
2077 | n == n' = Just (t, reverse acc ++ gs)
2078 find n (g : gs) acc = find n gs (g : acc)
2080-- | return True if the second argument is an implicit argument which
2081-- is expected in the implicits, or if it's not an implicit
2082impIn :: [PArg] -> PArg -> Bool
2083impIn ps (PExp _ _ _ _) = True
2084impIn ps (PConstraint _ _ _ _) = True
2085impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2087expArg (PExp _ _ _ _) = True
2088expArg (PConstraint _ _ _ _) = True
2091-- replace non-linear occurrences with _
2093stripLinear :: IState -> PTerm -> PTerm
2094stripLinear i tm = evalState (sl tm) [] where
2095 sl :: PTerm -> State [Name] PTerm
2097 | (_:_) <- lookupTy f (tt_ctxt i)
2098 = return $ PRef fc hl f
2099 | otherwise = do ns <- get
2101 then return $ PHidden (PRef fc hl f) -- Placeholder
2102 else do put (f : ns)
2103 return (PRef fc hl f)
2107 then return $ PHidden (PPatvar fc f) -- Placeholder
2108 else do put (f : ns)
2109 return (PPatvar fc f)
2110 -- Assumption is that variables are all the same in each alternative
2111 sl t@(PAlternative ms b as) = do ns <- get
2113 return (PAlternative ms b as')
2114 where slAlts ns (a : as) = do put ns
2118 slAlts ns [] = return []
2119 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2120 sl (PDPair fc hls p l t r) = do l' <- sl l
2123 return (PDPair fc hls p l' t' r')
2124 sl (PApp fc fn args) = do fn' <- case fn of
2125 -- Just the args, fn isn't matchable as a var
2126 PRef _ _ _ -> return fn
2128 args' <- mapM slA args
2129 return $ PApp fc fn' args'
2130 where slA (PImp p m l n t) = do t' <- sl t
2131 return $ PImp p m l n t'
2132 slA (PExp p l n t) = do t' <- sl t
2133 return $ PExp p l n t'
2134 slA (PConstraint p l n t)
2136 return $ PConstraint p l n t'
2137 slA (PTacImplicit p l n sc t)
2139 return $ PTacImplicit p l n sc t'
2142-- | Remove functions which aren't applied to anything, which must then
2143-- be resolved by unification. Assume names resolved and alternatives
2144-- filled in (so no ambiguity).
2145stripUnmatchable :: IState -> PTerm -> PTerm
2146stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2147 su :: PTerm -> PTerm
2148 su tm@(PRef fc hl f)
2149 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2151 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2152 not (implicitable f)
2154 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2155 not (implicitable f)
2157 su (PApp fc f@(PRef _ _ fn) args)
2158 -- here we use canBeDConName because the impossible pattern
2159 -- check will not necessarily fully resolve constructor names,
2160 -- and these bare names will otherwise get in the way of
2161 -- impossbility checking.
2162 | canBeDConName fn ctxt
2163 = PApp fc f (fmap (fmap su) args)
2165 = PHidden (PApp fc f args)
2166 su (PAlternative ms b alts)
2167 = let alts' = filter (/= Placeholder) (map su alts) in
2168 if null alts' then Placeholder
2169 else PAlternative ms b alts'
2170 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2171 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2172 su t@(PLam fc _ _ _ _) = PHidden t
2173 su t@(PPi _ _ _ _ _) = PHidden t
2174 su t@(PConstant _ c) | isTypeConst c = PHidden t
2179stripUnmatchable i tm = tm
2182mkPApp fc a f as = let rest = drop a as in
2183 if a == 0 then appRest fc f rest
2184 else appRest fc (PApp fc f (take a as)) rest
2187 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2191-- | Find 'static' argument positions
2192-- (the declared ones, plus any names in argument position in the declared
2194-- FIXME: It's possible that this really has to happen after elaboration
2195findStatics :: IState -> PTerm -> (PTerm, [Bool])
2196findStatics ist tm = let (ns, ss) = fs tm
2197 in runState (pos ns ss tm) []
2198 where fs (PPi p n fc t sc)
2199 | Static <- pstatic p
2200 = let (ns, ss) = fs sc in
2201 (namesIn [] ist t : ns, n : ss)
2202 | otherwise = let (ns, ss) = fs sc in
2206 inOne n ns = length (filter id (map (elem n) ns)) == 1
2208 pos ns ss (PPi p n fc t sc)
2209 | elem n ss = do sc' <- pos ns ss sc
2212 return (PPi (p { pstatic = Static }) n fc t sc')
2213 | otherwise = do sc' <- pos ns ss sc
2216 return (PPi p n fc t sc')
2217 pos ns ss t = return t
2219-- for 6.12/7 compatibility
2220data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2222instance Applicative (EitherErr a) where
2226instance Monad (EitherErr a) where
2229 (LeftErr e) >>= k = LeftErr e
2230 RightOK v >>= k = k v
2232toEither (LeftErr e) = Left e
2233toEither (RightOK ho) = Right ho
2235-- | Syntactic match of a against b, returning pair of variables in a
2236-- and what they match. Returns the pair that failed if not a match.
2237matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2238matchClause = matchClause' False
2240matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2241matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2242 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2244 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2247 match' x y = match (fullApp x) (fullApp y)
2248 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2249 | fi == txt "fromInteger" && b == txt "builtins",
2250 PConstant _ (I _) <- getTm x = match (getTm x) x'
2251 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2252 | fi == txt "fromInteger" && b == txt "builtins",
2253 PConstant _ (I _) <- getTm x = match (getTm x) x'
2254 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2255 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2256 match (PApp _ f args) (PApp _ f' args')
2257 | length args == length args'
2258 = do mf <- match' f f'
2259 ms <- zipWithM matchArg args args'
2260 return (mf ++ concat ms)
2261 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2262 match (PPatvar f n) xr = match (PRef f [f] n) xr
2263 match xr (PPatvar f n) = match xr (PRef f [f] n)
2264 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2265 match (PRef _ _ n) tm@(PRef _ _ n')
2266 | n == n' && not names &&
2267 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2268 || tm == Placeholder)
2270 -- if one namespace is missing, drop the other
2271 | n == n' || n == dropNS n' || dropNS n == n' = return []
2272 where dropNS (NS n _) = n
2274 match (PRef _ _ n) tm
2275 | not names && (not (isConName n (tt_ctxt i) ||
2276 isFnName n (tt_ctxt i)) || tm == Placeholder)
2278 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2279 = do ml <- match' l l'
2282 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2285 match (PTyped l r) x = match l x
2286 match x (PTyped l r) = match x l
2287 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2290 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2293 return (ml ++ mt ++ mr)
2294 match (PAlternative _ a as) (PAlternative _ a' as')
2295 = do ms <- zipWithM match' as as'
2297 match a@(PAlternative _ _ as) b
2298 = do let ms = zipWith match' as (repeat b)
2299 case (rights (map toEither ms)) of
2302 match (PCase _ _ _) _ = return [] -- lifted out
2303 match (PMetavar _ _) _ = return [] -- modified
2304 match (PInferRef _ _ _) _ = return [] -- modified
2305 match (PQuote _) _ = return []
2306 match (PProof _) _ = return []
2307 match (PTactics _) _ = return []
2308 match (PResolveTC _) (PResolveTC _) = return []
2309 match (PTrue _ _) (PTrue _ _) = return []
2310 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2313 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2316 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2317 mty <- match' ty ty'
2319 return (mt ++ mty ++ ms)
2320 match (PHidden x) (PHidden y)
2321 | RightOK xs <- match x y = return xs -- to collect variables
2322 | otherwise = return [] -- Otherwise hidden things are unmatchable
2324 | RightOK xs <- match x y = return xs
2325 | otherwise = return []
2327 | RightOK xs <- match x y = return xs
2328 | otherwise = return []
2329 match (PUnifyLog x) y = match' x y
2330 match x (PUnifyLog y) = match' x y
2331 match (PNoImplicits x) y = match' x y
2332 match x (PNoImplicits y) = match' x y
2333 match Placeholder _ = return []
2334 match _ Placeholder = return []
2335 match (PResolveTC _) _ = return []
2336 match a b | a == b = return []
2337 | otherwise = LeftErr (a, b)
2339 checkRpts (RightOK ms) = check ms where
2341 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2344 check (_:xs) = check xs
2346 checkRpts (LeftErr x) = Left x
2348substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2349substMatches ms = substMatchesShadow ms []
2351-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2352-- substMatchesShadow [] shs t = t
2353-- substMatchesShadow ((n,tm):ns) shs t
2354-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2356substMatch :: Name -> PTerm -> PTerm -> PTerm
2357substMatch n = substMatchShadow n []
2359substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2360substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2362substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2363substMatchesShadow nmap shs t = sm shs t where
2364 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2365 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2366 sm xs (PPi p x fc t sc)
2368 = let x' = nextName x in
2369 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2370 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2371 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2372 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2373 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2374 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2375 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2377 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2378 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2379 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2380 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2381 sm xs (PHidden x) = PHidden (sm xs x)
2382 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2383 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2384 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2385 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2388 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2391shadow :: Name -> Name -> PTerm -> PTerm
2392shadow n n' t = sm 0 t where
2393 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2394 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2395 | otherwise = PLam fc x xfc (sm 0 t) sc
2396 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2397 | otherwise = PPi p x fc (sm 0 t) sc
2398 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2399 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2400 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2401 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2402 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2403 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2404 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2405 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2406 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2407 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2408 sm 0 (PAlternative ms a as)
2409 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2410 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2411 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2412 sm 0 (PHidden x) = PHidden (sm 0 x)
2413 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2414 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2415 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2416 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2417 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2418 sm ql x = descend (sm ql) x
2420 shadowAlt p@(x, oldn) = (update x, update oldn)
2421 update oldn | n == oldn = n'
2424-- | Rename any binders which are repeated (so that we don't have to
2425-- mess about with shadowing anywhere else).
2426mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2427mkUniqueNames env shadows tm
2428 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2430 initMap = M.fromList shadows
2432 inScope :: S.Set Name
2433 inScope = S.fromList $ boundNamesIn tm
2435 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2436 return (arg { getTm = t' })
2438 -- Initialise the unique name with the environment length (so we're not
2439 -- looking for too long...)
2440 initN (UN n) l = UN $ txt (str n ++ show l)
2441 initN (MN i s) l = MN (i+l) s
2444 -- FIXME: Probably ought to do this for completeness! It's fine as
2445 -- long as there are no bindings inside tactics though.
2446 mkUniqT _ nmap tac = return tac
2448 mkUniq :: Int -- ^ The number of quotations that we're under
2449 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2450 mkUniq 0 nmap (PLam fc n nfc ty sc)
2454 then do let n' = uniqueNameSet (initN n (S.size env))
2455 (S.union env inScope)
2456 return (n', sc) -- shadow n n' sc)
2458 put (S.insert n' env)
2459 let nmap' = M.insert n n' nmap
2460 ty' <- mkUniq 0 nmap ty
2461 sc'' <- mkUniq 0 nmap' sc'
2462 return $! PLam fc n' nfc ty' sc''
2463 mkUniq 0 nmap (PPi p n fc ty sc)
2467 then do let n' = uniqueNameSet (initN n (S.size env))
2468 (S.union env inScope)
2469 return (n', sc) -- shadow n n' sc)
2471 put (S.insert n' env)
2472 let nmap' = M.insert n n' nmap
2473 ty' <- mkUniq 0 nmap ty
2474 sc'' <- mkUniq 0 nmap' sc'
2475 return $! PPi p n' fc ty' sc''
2476 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2480 then do let n' = uniqueNameSet (initN n (S.size env))
2481 (S.union env inScope)
2482 return (n', sc) -- shadow n n' sc)
2484 put (S.insert n' env)
2485 let nmap' = M.insert n n' nmap
2486 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2487 sc'' <- mkUniq 0 nmap' sc'
2488 return $! PLet fc n' nfc ty' val' sc''
2489 mkUniq 0 nmap (PApp fc t args)
2490 = do t' <- mkUniq 0 nmap t
2491 args' <- mapM (mkUniqA 0 nmap) args
2492 return $! PApp fc t' args'
2493 mkUniq 0 nmap (PAppBind fc t args)
2494 = do t' <- mkUniq 0 nmap t
2495 args' <- mapM (mkUniqA 0 nmap) args
2496 return $! PAppBind fc t' args'
2497 mkUniq 0 nmap (PCase fc t alts)
2498 = do t' <- mkUniq 0 nmap t
2499 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2500 return (x', y')) alts
2501 return $! PCase fc t' alts'
2502 mkUniq 0 nmap (PIfThenElse fc c t f)
2503 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2504 mkUniq 0 nmap (PPair fc hls p l r)
2505 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2506 return $! PPair fc hls p l' r'
2507 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2510 (n', sc') <- if n `S.member` env
2511 then do let n' = uniqueNameSet n (S.union env inScope)
2512 return (n', sc) -- shadow n n' sc)
2514 put (S.insert n' env)
2515 let nmap' = M.insert n n' nmap
2516 t' <- mkUniq 0 nmap t
2517 sc'' <- mkUniq 0 nmap' sc'
2518 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2519 mkUniq 0 nmap (PDPair fc hls p l t r)
2520 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2521 return $! PDPair fc hls p l' t' r'
2522 mkUniq 0 nmap (PAlternative ns b as)
2523 -- store the nmap and defer the rest until we've pruned the set
2524 -- during elaboration
2525 = return $ PAlternative (ns ++ M.toList nmap) b as
2526 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2527 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2528 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2529 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2530 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2531 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2532 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2533 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2534 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2535 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2538 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2540 mkUniq ql nmap (PQuasiquote tm ty) =
2541 do tm' <- mkUniq (ql + 1) nmap tm
2543 Nothing -> return Nothing
2544 Just t -> fmap Just $ mkUniq ql nmap t
2545 return $! PQuasiquote tm' ty'
2546 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2548 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2551getFile :: Opt -> Maybe String
2552getFile (Filename str) = Just str
2555getBC :: Opt -> Maybe String
2556getBC (BCAsm str) = Just str
2559getOutput :: Opt -> Maybe String
2560getOutput (Output str) = Just str
2561getOutput _ = Nothing
2563getIBCSubDir :: Opt -> Maybe String
2564getIBCSubDir (IBCSubDir str) = Just str
2565getIBCSubDir _ = Nothing
2567getImportDir :: Opt -> Maybe String
2568getImportDir (ImportDir str) = Just str
2569getImportDir _ = Nothing
2571getSourceDir :: Opt -> Maybe String
2572getSourceDir (SourceDir str) = Just str
2573getSourceDir _ = Nothing
2575getPkgDir :: Opt -> Maybe String
2576getPkgDir (Pkg str) = Just str
2577getPkgDir _ = Nothing
2579getPkg :: Opt -> Maybe (Bool, String)
2580getPkg (PkgBuild str) = Just (False, str)
2581getPkg (PkgInstall str) = Just (True, str)
2584getPkgClean :: Opt -> Maybe String
2585getPkgClean (PkgClean str) = Just str
2586getPkgClean _ = Nothing
2588getPkgREPL :: Opt -> Maybe String
2589getPkgREPL (PkgREPL str) = Just str
2590getPkgREPL _ = Nothing
2592getPkgCheck :: Opt -> Maybe String
2593getPkgCheck (PkgCheck str) = Just str
2594getPkgCheck _ = Nothing
2596-- | Returns None if given an Opt which is not PkgMkDoc
2597-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2598getPkgMkDoc :: Opt -- ^ Opt to extract
2599 -> Maybe (Bool, String) -- ^ Result
2600getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2601getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2602getPkgMkDoc _ = Nothing
2604getPkgTest :: Opt -- ^ the option to extract
2605 -> Maybe String -- ^ the package file to test
2606getPkgTest (PkgTest f) = Just f
2607getPkgTest _ = Nothing
2609getCodegen :: Opt -> Maybe Codegen
2610getCodegen (UseCodegen x) = Just x
2611getCodegen _ = Nothing
2613getCodegenArgs :: Opt -> Maybe String
2614getCodegenArgs (CodegenArgs args) = Just args
2615getCodegenArgs _ = Nothing
2617getConsoleWidth :: Opt -> Maybe ConsoleWidth
2618getConsoleWidth (UseConsoleWidth x) = Just x
2619getConsoleWidth _ = Nothing
2622getExecScript :: Opt -> Maybe String
2623getExecScript (InterpretScript expr) = Just expr
2624getExecScript _ = Nothing
2626getPkgIndex :: Opt -> Maybe FilePath
2627getPkgIndex (PkgIndex file) = Just file
2628getPkgIndex _ = Nothing
2630getEvalExpr :: Opt -> Maybe String
2631getEvalExpr (EvalExpr expr) = Just expr
2632getEvalExpr _ = Nothing
2634getOutputTy :: Opt -> Maybe OutputType
2635getOutputTy (OutputTy t) = Just t
2636getOutputTy _ = Nothing
2638getLanguageExt :: Opt -> Maybe LanguageExt
2639getLanguageExt (Extension e) = Just e
2640getLanguageExt _ = Nothing
2642getTriple :: Opt -> Maybe String
2643getTriple (TargetTriple x) = Just x
2644getTriple _ = Nothing
2646getCPU :: Opt -> Maybe String
2647getCPU (TargetCPU x) = Just x
2650getOptLevel :: Opt -> Maybe Int
2651getOptLevel (OptLevel x) = Just x
2652getOptLevel _ = Nothing
2654getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2655getOptimisation (AddOpt p) = Just (True, p)
2656getOptimisation (RemoveOpt p) = Just (False, p)
2657getOptimisation _ = Nothing
2659getColour :: Opt -> Maybe Bool
2660getColour (ColourREPL b) = Just b
2661getColour _ = Nothing
2663getClient :: Opt -> Maybe String
2664getClient (Client x) = Just x
2665getClient _ = Nothing
2667-- Get the first valid port
2668getPort :: [Opt] -> Maybe REPLPort
2670getPort (Port p : xs) = Just p
2671getPort (_ : xs) = getPort xs
2673opt :: (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