2Module : Idris.AbsSyntax
3Description : Provides Idris' core data definitions and utility code.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveFunctor, PatternGuards #-}
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
13 , module Idris.AbsSyntaxTree
16import Idris.AbsSyntaxTree
18import Idris.Core.Evaluate
20import Idris.Docstrings
21import Idris.IdeMode hiding (Opt(..))
22import IRTS.CodegenCommon
24import System.Directory (canonicalizePath, doesFileExist)
27import Control.Applicative
28import Control.Monad.State
29import Prelude hiding (Applicative, Foldable, Traversable, (<$>))
32import Data.List hiding (insert, union)
33import qualified Data.Map as M
35import qualified Data.Set as S
36import qualified Data.Text as T
37import System.IO.Error (tryIOError)
39import Data.Generics.Uniplate.Data (descend, descendM)
42import Util.DynamicLinker
46getContext :: Idris Context
47getContext = do i <- getIState; return (tt_ctxt i)
49forCodegen :: Codegen -> [(Codegen, a)] -> [a]
50forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
52 eqLang (Via _ x) (Via _ y) = x == y
53 eqLang Bytecode Bytecode = True
56getObjectFiles :: Codegen -> Idris [FilePath]
57getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
59addObjectFile :: Codegen -> FilePath -> Idris ()
60addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
62getLibs :: Codegen -> Idris [String]
63getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
65addLib :: Codegen -> String -> Idris ()
66addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
68getFlags :: Codegen -> Idris [String]
69getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
71addFlag :: Codegen -> String -> Idris ()
72addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
74addDyLib :: [String] -> Idris (Either DynamicLib String)
75addDyLib libs = do i <- getIState
76 let ls = idris_dynamic_libs i
77 let importdirs = opt_importdirs (idris_options i)
78 case mapMaybe (findDyLib ls) libs of
79 x:_ -> return (Left x)
81 handle <- lift . lift .
82 mapM (\l -> catchIO (tryLoadLib importdirs l)
83 (\_ -> return Nothing)) $ libs
85 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
86 intercalate "," libs ++ "\"")
87 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
89 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
90 findDyLib [] _ = Nothing
91 findDyLib (lib:libs') l | l == lib_name lib = Just lib
92 | otherwise = findDyLib libs' l
94getAutoImports :: Idris [FilePath]
95getAutoImports = do i <- getIState
96 return (opt_autoImport (idris_options i))
98addAutoImport :: FilePath -> Idris ()
99addAutoImport fp = do i <- getIState
100 let opts = idris_options i
101 put (i { idris_options = opts { opt_autoImport =
102 fp : opt_autoImport opts } } )
104addDefinedName :: Name -> Idris ()
105addDefinedName n = do ist <- getIState
106 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
108getDefinedNames :: Idris [Name]
109getDefinedNames = do ist <- getIState
110 return (S.toList (idris_inmodule ist))
112addTT :: Term -> Idris (Maybe Term)
113addTT t = do ist <- getIState
114 case M.lookup t (idris_ttstats ist) of
115 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
116 putIState $ ist { idris_ttstats = tt' }
118 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
119 putIState $ ist { idris_ttstats = tt' }
123dumpTT = do ist <- get
124 let sts = sortBy count (M.toList (idris_ttstats ist))
128 count (_,x) (_,y) = compare y x
129 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
131addHdr :: Codegen -> String -> Idris ()
132addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
134addImported :: Bool -> FilePath -> Idris ()
137 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
139addLangExt :: LanguageExt -> Idris ()
140addLangExt e = do i <- getIState
142 idris_language_extensions = e : idris_language_extensions i
145-- | Transforms are organised by the function being applied on the lhs
146-- of the transform, to make looking up appropriate transforms quicker
147addTrans :: Name -> (Term, Term) -> Idris ()
150 let t' = case lookupCtxtExact basefn (idris_transforms i) of
151 Just def -> (t : def)
153 putIState $ i { idris_transforms = addDef basefn t'
154 (idris_transforms i) }
156-- | Add transformation rules from a definition, which will reverse the
157-- definition for an error to make it more readable
158addErrRev :: (Term, Term) -> Idris ()
159addErrRev t = do i <- getIState
160 putIState $ i { idris_errRev = t : idris_errRev i }
162-- | Say that the name should always be reduced in error messages, to
163-- help readability/error reflection
164addErrReduce :: Name -> Idris ()
165addErrReduce t = do i <- getIState
166 putIState $ i { idris_errReduce = t : idris_errReduce i }
168addErasureUsage :: Name -> Int -> Idris ()
169addErasureUsage n i = do ist <- getIState
170 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
172addExport :: Name -> Idris ()
173addExport n = do ist <- getIState
174 putIState $ ist { idris_exports = n : idris_exports ist }
176addUsedName :: FC -> Name -> Name -> Idris ()
178 = do ist <- getIState
179 case lookupTyName n (tt_ctxt ist) of
180 [(n', ty)] -> addUsage n' 0 ty
181 [] -> throwError (At fc (NoSuchVariable n))
182 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
183 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
185 | otherwise = addUsage n (i + 1) sc
186 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
188getErasureUsage :: Idris [(Name, Int)]
189getErasureUsage = do ist <- getIState;
190 return (idris_erasureUsed ist)
192getExports :: Idris [Name]
193getExports = do ist <- getIState
194 return (idris_exports ist)
196totcheck :: (FC, Name) -> Idris ()
197totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
199defer_totcheck :: (FC, Name) -> Idris ()
202 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
204clear_totcheck :: Idris ()
205clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
207setFlags :: Name -> [FnOpt] -> Idris ()
208setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
210addFnOpt :: Name -> FnOpt -> Idris ()
211addFnOpt n f = do i <- getIState
212 let fls = case lookupCtxtExact n (idris_flags i) of
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 _ [] = []
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 Nothing [] [])
274 Just (CGInfo cs ans scg used) ->
275 addToCG n (CGInfo (nub (calls ++ cs)) ans 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 }
359-- | Trace all the names in a call graph starting at the given name
360getAllNames :: Name -> Idris [Name]
361getAllNames n = do i <- getIState
362 case getCGAllNames i n of
364 Nothing -> do ns <- allNames [] n
368getCGAllNames :: IState -> Name -> Maybe [Name]
369getCGAllNames i n = case lookupCtxtExact n (idris_callgraph i) of
370 Just ci -> allCalls ci
373addCGAllNames :: IState -> Name -> [Name] -> Idris ()
375 = case lookupCtxtExact n (idris_callgraph i) of
376 Just ci -> addToCG n (ci { allCalls = Just ns })
377 _ -> addToCG n (CGInfo [] (Just ns) [] [])
379allNames :: [Name] -> Name -> Idris [Name]
380allNames ns n | n `elem` ns = return []
381allNames ns n = do i <- getIState
382 case getCGAllNames i n of
384 Nothing -> case lookupCtxtExact n (idris_callgraph i) of
386 do more <- mapM (allNames (n:ns)) (calls ci)
387 let ns' = nub (n : concat more)
388 addCGAllNames i n ns'
392addCoercion :: Name -> Idris ()
393addCoercion n = do i <- getIState
394 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
396addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
399 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
401addNameHint :: Name -> Name -> Idris ()
404 ty' <- case lookupCtxtName ty (idris_implicits i) of
405 [(tyn, _)] -> return tyn
406 [] -> throwError (NoSuchVariable ty)
407 tyns -> throwError (CantResolveAlts (map fst tyns))
408 let ns' = case lookupCtxt ty' (idris_namehints i) of
411 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
413getNameHints :: IState -> Name -> [Name]
414getNameHints _ (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
416 case lookupCtxt n (idris_namehints i) of
420addDeprecated :: Name -> String -> Idris ()
421addDeprecated n reason = do
423 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
425getDeprecated :: Name -> Idris (Maybe String)
428 return $ lookupCtxtExact n (idris_deprecated i)
430addFragile :: Name -> String -> Idris ()
431addFragile n reason = do
433 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
435getFragile :: Name -> Idris (Maybe String)
438 return $ lookupCtxtExact n (idris_fragile i)
440push_estack :: Name -> Bool -> Idris ()
441push_estack n implementation
443 putIState (i { elab_stack = (n, implementation) : elab_stack i })
445pop_estack :: Idris ()
446pop_estack = do i <- getIState
447 putIState (i { elab_stack = ptail (elab_stack i) })
451-- | Add an interface implementation function.
453-- Precondition: the implementation should have the correct type.
455-- Dodgy hack 1: Put integer implementations first in the list so they are
456-- resolved by default.
458-- Dodgy hack 2: put constraint chasers (ParentN) last
459addImplementation :: Bool -- ^ whether the name is an Integer implementation
460 -> Bool -- ^ whether to include the implementation in implementation search
461 -> Name -- ^ the name of the interface
462 -> Name -- ^ the name of the implementation
464addImplementation int res n i
465 = do ist <- getIState
466 case lookupCtxt n (idris_interfaces ist) of
467 [CI a b c d e f g ins fds] ->
468 do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
469 putIState $ ist { idris_interfaces = cs }
470 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
471 putIState $ ist { idris_interfaces = cs }
472 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
473 addI i ins | int = (i, res) : ins
474 | chaser n = ins ++ [(i, res)]
475 | otherwise = insI i ins
476 insI i [] = [(i, res)]
477 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
478 | otherwise = n : insI i ns
480 chaser (SN (ParentN _ _)) = True
481 chaser (NS n _) = chaser n
484-- | Add a privileged implementation - one which implementation search will
485-- happily resolve immediately if it is type correct This is used for
486-- naming parent implementations when defining an implementation with
487-- constraints. Returns the old list, so we can revert easily at the
489addOpenImpl :: [Name] -> Idris [Name]
490addOpenImpl ns = do ist <- getIState
491 ns' <- mapM (checkValid ist) ns
492 let open = idris_openimpls ist
493 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
497 = case lookupCtxtName n (idris_implicits ist) of
498 [(n', _)] -> return n'
499 [] -> throwError (NoSuchVariable n)
500 more -> throwError (CantResolveAlts (map fst more))
502setOpenImpl :: [Name] -> Idris ()
503setOpenImpl ns = do ist <- getIState
504 putIState $ ist { idris_openimpls = ns }
506getOpenImpl :: Idris [Name]
507getOpenImpl = do ist <- getIState
508 return (idris_openimpls ist)
510addInterface :: Name -> InterfaceInfo -> Idris ()
512 = do ist <- getIState
513 let i' = case lookupCtxt n (idris_interfaces ist) of
514 [c] -> i { interface_implementations = interface_implementations c ++
515 interface_implementations i }
517 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
519updateIMethods :: Name -> [(Name, PTerm)] -> Idris ()
520updateIMethods n meths
521 = do ist <- getIState
522 let i = case lookupCtxtExact n (idris_interfaces ist) of
523 Just c -> c { interface_methods = update (interface_methods c) }
524 Nothing -> error "Can't happen updateIMethods"
525 putIState $ ist { idris_interfaces = addDef n i (idris_interfaces ist) }
528 update (m@(n, (b, opts, t)) : rest)
529 | Just ty <- lookup n meths
530 = (n, (b, opts, ty)) : update rest
531 | otherwise = m : update rest
533addRecord :: Name -> RecordInfo -> Idris ()
534addRecord n ri = do ist <- getIState
535 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
537addAutoHint :: Name -> Name -> Idris ()
540 case lookupCtxtExact n (idris_autohints ist) of
542 do let hs = addDef n [hint] (idris_autohints ist)
543 putIState $ ist { idris_autohints = hs }
545 do let hs = addDef n (hint : nhints) (idris_autohints ist)
546 putIState $ ist { idris_autohints = hs }
548getAutoHints :: Name -> Idris [Name]
549getAutoHints n = do ist <- getIState
550 case lookupCtxtExact n (idris_autohints ist) of
554addIBC :: IBCWrite -> Idris ()
557 when (notDef (ibc_write i)) $
558 putIState $ i { ibc_write = ibc : ibc_write i }
559 where notDef [] = True
560 notDef (IBCDef n': _) | n == n' = False
561 notDef (_ : is) = notDef is
562addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
565clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
566 idris_inmodule = S.empty }
568resetNameIdx :: Idris ()
569resetNameIdx = do i <- getIState
570 put (i { idris_nameIdx = (0, emptyContext) })
572-- | Used to preserve sharing of names
573addNameIdx :: Name -> Idris (Int, Name)
574addNameIdx n = do i <- getIState
575 let (i', x) = addNameIdx' i n
579addNameIdx' :: IState -> Name -> (IState, (Int, Name))
581 = let idxs = snd (idris_nameIdx i) in
582 case lookupCtxt n idxs of
584 _ -> let i' = fst (idris_nameIdx i) + 1 in
585 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
587getSymbol :: Name -> Idris Name
588getSymbol n = do i <- getIState
589 case M.lookup n (idris_symbols i) of
591 Nothing -> do let sym' = M.insert n n (idris_symbols i)
592 put (i { idris_symbols = sym' })
595getHdrs :: Codegen -> Idris [String]
596getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
598getImported :: Idris [(FilePath, Bool)]
599getImported = do i <- getIState; return (idris_imported i)
601setErrSpan :: FC -> Idris ()
602setErrSpan x = do i <- getIState;
604 Nothing -> putIState $ i { errSpan = Just x }
608clearErr = do i <- getIState
609 putIState $ i { errSpan = Nothing }
611getSO :: Idris (Maybe String)
612getSO = do i <- getIState
613 return (compiled_so i)
615setSO :: Maybe String -> Idris ()
616setSO s = do i <- getIState
617 putIState (i { compiled_so = s })
619getIState :: Idris IState
622putIState :: IState -> Idris ()
625updateIState :: (IState -> IState) -> Idris ()
626updateIState f = do i <- getIState
629withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
630withContext ctx name dflt action = do
632 case lookupCtxt name (ctx ist) of
636withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
637withContext_ ctx name action = withContext ctx name () action
639-- | A version of liftIO that puts errors into the exception type of
641runIO :: IO a -> Idris a
642runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
643-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
645-- Issue #1738 on the issue tracker.
646-- https://github.com/idris-lang/Idris-dev/issues/1738
649getName = do i <- getIState;
650 let idx = idris_name i;
651 putIState (i { idris_name = idx + 1 })
654-- | InternalApp keeps track of the real function application for
655-- making case splits from, not the application the programmer wrote,
656-- which doesn't have the whole context in any case other than top
658addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
661 -- We canonicalise the path to make "./Test/Module.idr" equal
662 -- to "Test/Module.idr"
663 exists <- runIO $ doesFileExist fp
665 do fp' <- runIO $ canonicalizePath fp
666 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
668getInternalApp :: FilePath -> Int -> Idris PTerm
669getInternalApp fp l = do i <- getIState
670 -- We canonicalise the path to make
671 -- "./Test/Module.idr" equal to
673 exists <- runIO $ doesFileExist fp
675 then do fp' <- runIO $ canonicalizePath fp
676 case lookup (fp', l) (idris_lineapps i) of
678 Nothing -> return Placeholder
679 -- TODO: What if it's not there?
680 else return Placeholder
682-- | Pattern definitions are only used for coverage checking, so erase
683-- them when we're done
684clearOrigPats :: Idris ()
685clearOrigPats = do i <- get
686 let ps = idris_patdefs i
687 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
688 put (i { idris_patdefs = ps' })
690-- | Erase types from Ps in the context (basically ending up with
691-- what's in the .ibc, which is all we need after all the analysis is
693clearPTypes :: Idris ()
694clearPTypes = do i <- get
696 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
697 where pErase (CaseOp c t tys orig _ cds)
698 = CaseOp c t tys orig [] (pErase' cds)
700 pErase' (CaseDefs (cs, c) rs)
701 = let c' = (cs, fmap pEraseType c) in
704checkUndefined :: FC -> Name -> Idris ()
708 (_:_) -> throwError . Msg $ show fc ++ ":" ++
709 show n ++ " already defined"
712isUndefined :: FC -> Name -> Idris Bool
715 case lookupTyExact n i of
716 Just _ -> return False
719setContext :: Context -> Idris ()
720setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
722updateContext :: (Context -> Context) -> Idris ()
723updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
725addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
726addConstraints fc (v, cs)
727 = do tit <- typeInType
731 let ctxt' = ctxt { next_tvar = v }
732 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
733 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
736 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
737 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
738 insertAll ((c, fc) : cs) ics
739 = insertAll cs $ S.insert (ConstraintFC c fc) ics
741addDeferred = addDeferred' Ref
742addDeferredTyCon = addDeferred' (TCon 0 0)
744-- | Save information about a name that is not yet defined
745addDeferred' :: NameType
746 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
747 -- ^ The Name is the name being made into a metavar,
748 -- the Int is the number of vars that are part of a
749 -- putative proof context, the Maybe Name is the
750 -- top-level function containing the new metavariable,
751 -- the Type is its type, and the Bool is whether :p is
755 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
756 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
758 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
759 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
762 -- 'tidyNames' is to generate user accessible names in case they are
763 -- needed in tactic scripts
764 tidyNames used (Bind (MN i x) b sc)
765 = let n' = uniqueNameSet (UN x) used in
766 Bind n' b $ tidyNames (S.insert n' used) sc
767 tidyNames used (Bind n b sc)
768 = let n' = uniqueNameSet n used in
769 Bind n' b $ tidyNames (S.insert n' used) sc
772solveDeferred :: FC -> Name -> Idris ()
775 case lookup n (idris_metavars i) of
776 Just (_, _, _, _, False) ->
777 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
778 _ -> putIState $ i { idris_metavars =
779 filter (\(n', _) -> n/=n')
782 filter (notMV n) (ibc_write i)
784 where notMV n (IBCMetavar n') = not (n == n')
787getUndefined :: Idris [Name]
788getUndefined = do i <- getIState
789 return (map fst (idris_metavars i) \\ primDefs)
791isMetavarName :: Name -> IState -> Bool
793 = case lookupNames n (tt_ctxt ist) of
794 (t:_) -> isJust $ lookup t (idris_metavars ist)
797getWidth :: Idris ConsoleWidth
798getWidth = fmap idris_consolewidth getIState
800setWidth :: ConsoleWidth -> Idris ()
801setWidth w = do ist <- getIState
802 put ist { idris_consolewidth = w }
804setDepth :: Maybe Int -> Idris ()
805setDepth d = do ist <- getIState
806 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
808typeDescription :: String
809typeDescription = "The type of types"
812type1Doc :: Doc OutputAnnotation
813type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
816isetPrompt :: String -> Idris ()
817isetPrompt p = do i <- getIState
818 case idris_outputmode i of
819 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
821-- | Tell clients how much was parsed and loaded
822isetLoadedRegion :: Idris ()
823isetLoadedRegion = do i <- getIState
824 let span = idris_parsedSpan i
827 case idris_outputmode i of
829 runIO . hPutStrLn h $
830 convSExp "set-loaded-region" fc n
833setLogLevel :: Int -> Idris ()
834setLogLevel l = do i <- getIState
835 let opts = idris_options i
836 let opt' = opts { opt_logLevel = l }
837 putIState $ i { idris_options = opt' }
839setLogCats :: [LogCat] -> Idris ()
842 let opts = idris_options i
843 let opt' = opts { opt_logcats = cs }
844 putIState $ i { idris_options = opt' }
846setCmdLine :: [Opt] -> Idris ()
847setCmdLine opts = do i <- getIState
848 let iopts = idris_options i
849 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
851getCmdLine :: Idris [Opt]
852getCmdLine = do i <- getIState
853 return (opt_cmdline (idris_options i))
855getDumpHighlighting :: Idris Bool
856getDumpHighlighting = do ist <- getIState
857 return (findC (opt_cmdline (idris_options ist)))
858 where findC = elem DumpHighlights
860getDumpDefun :: Idris (Maybe FilePath)
861getDumpDefun = do i <- getIState
862 return $ findC (opt_cmdline (idris_options i))
863 where findC [] = Nothing
864 findC (DumpDefun x : _) = Just x
865 findC (_ : xs) = findC xs
867getDumpCases :: Idris (Maybe FilePath)
868getDumpCases = do i <- getIState
869 return $ findC (opt_cmdline (idris_options i))
870 where findC [] = Nothing
871 findC (DumpCases x : _) = Just x
872 findC (_ : xs) = findC xs
875logLevel = do i <- getIState
876 return (opt_logLevel (idris_options i))
878setAutoImpls :: Bool -> Idris ()
879setAutoImpls b = do i <- getIState
880 let opts = idris_options i
881 let opt' = opts { opt_autoimpls = b }
882 putIState $ i { idris_options = opt' }
884getAutoImpls :: Idris Bool
885getAutoImpls = do i <- getIState
886 return (opt_autoimpls (idris_options i))
888setErrContext :: Bool -> Idris ()
889setErrContext t = do i <- getIState
890 let opts = idris_options i
891 let opts' = opts { opt_errContext = t }
892 putIState $ i { idris_options = opts' }
894errContext :: Idris Bool
895errContext = do i <- getIState
896 return (opt_errContext (idris_options i))
898getOptimise :: Idris [Optimisation]
899getOptimise = do i <- getIState
900 return (opt_optimise (idris_options i))
902setOptimise :: [Optimisation] -> Idris ()
903setOptimise newopts = do i <- getIState
904 let opts = idris_options i
905 let opts' = opts { opt_optimise = newopts }
906 putIState $ i { idris_options = opts' }
908addOptimise :: Optimisation -> Idris ()
909addOptimise opt = do opts <- getOptimise
910 setOptimise (nub (opt : opts))
912removeOptimise :: Optimisation -> Idris ()
913removeOptimise opt = do opts <- getOptimise
914 setOptimise ((nub opts) \\ [opt])
916-- | Set appropriate optimisation set for the given level. We only
917-- have one optimisation that is configurable at the moment, however!
918setOptLevel :: Int -> Idris ()
919setOptLevel n | n <= 0 = setOptimise []
920setOptLevel 1 = setOptimise []
921setOptLevel 2 = setOptimise [PETransform]
922setOptLevel n | n >= 3 = setOptimise [PETransform]
925useREPL = do i <- getIState
926 return (opt_repl (idris_options i))
928setREPL :: Bool -> Idris ()
929setREPL t = do i <- getIState
930 let opts = idris_options i
931 let opt' = opts { opt_repl = t }
932 putIState $ i { idris_options = opt' }
934showOrigErr :: Idris Bool
935showOrigErr = do i <- getIState
936 return (opt_origerr (idris_options i))
938setShowOrigErr :: Bool -> Idris ()
939setShowOrigErr b = do i <- getIState
940 let opts = idris_options i
941 let opt' = opts { opt_origerr = b }
942 putIState $ i { idris_options = opt' }
944setAutoSolve :: Bool -> Idris ()
945setAutoSolve b = do i <- getIState
946 let opts = idris_options i
947 let opt' = opts { opt_autoSolve = b }
948 putIState $ i { idris_options = opt' }
950setNoBanner :: Bool -> Idris ()
951setNoBanner n = do i <- getIState
952 let opts = idris_options i
953 let opt' = opts { opt_nobanner = n }
954 putIState $ i { idris_options = opt' }
956getNoBanner :: Idris Bool
957getNoBanner = do i <- getIState
958 let opts = idris_options i
959 return (opt_nobanner opts)
961setEvalTypes :: Bool -> Idris ()
962setEvalTypes n = do i <- getIState
963 let opts = idris_options i
964 let opt' = opts { opt_evaltypes = n }
965 putIState $ i { idris_options = opt' }
967getDesugarNats :: Idris Bool
968getDesugarNats = do i <- getIState
969 let opts = idris_options i
970 return (opt_desugarnats opts)
973setDesugarNats :: Bool -> Idris ()
974setDesugarNats n = do i <- getIState
975 let opts = idris_options i
976 let opt' = opts { opt_desugarnats = n }
977 putIState $ i { idris_options = opt' }
979setQuiet :: Bool -> Idris ()
980setQuiet q = do i <- getIState
981 let opts = idris_options i
982 let opt' = opts { opt_quiet = q }
983 putIState $ i { idris_options = opt' }
985getQuiet :: Idris Bool
986getQuiet = do i <- getIState
987 let opts = idris_options i
988 return (opt_quiet opts)
990setCodegen :: Codegen -> Idris ()
991setCodegen t = do i <- getIState
992 let opts = idris_options i
993 let opt' = opts { opt_codegen = t }
994 putIState $ i { idris_options = opt' }
996codegen :: Idris Codegen
997codegen = do i <- getIState
998 return (opt_codegen (idris_options i))
1001setOutputTy :: OutputType -> Idris ()
1002setOutputTy t = do i <- getIState
1003 let opts = idris_options i
1004 let opt' = opts { opt_outputTy = t }
1005 putIState $ i { idris_options = opt' }
1007outputTy :: Idris OutputType
1008outputTy = do i <- getIState
1009 return $ opt_outputTy $ idris_options i
1011setIdeMode :: Bool -> Handle -> Idris ()
1012setIdeMode True h = do i <- getIState
1013 putIState $ i { idris_outputmode = IdeMode 0 h
1014 , idris_colourRepl = False
1016setIdeMode False _ = return ()
1018setTargetTriple :: String -> Idris ()
1019setTargetTriple t = do i <- getIState
1020 let opts = idris_options i
1021 opt' = opts { opt_triple = t }
1022 putIState $ i { idris_options = opt' }
1024targetTriple :: Idris String
1025targetTriple = do i <- getIState
1026 return (opt_triple (idris_options i))
1028setTargetCPU :: String -> Idris ()
1029setTargetCPU t = do i <- getIState
1030 let opts = idris_options i
1031 opt' = opts { opt_cpu = t }
1032 putIState $ i { idris_options = opt' }
1034targetCPU :: Idris String
1035targetCPU = do i <- getIState
1036 return (opt_cpu (idris_options i))
1041 -- Quietness overrides verbosity
1042 let quiet = opt_quiet $ idris_options i
1045 else return $ (opt_verbose $ idris_options i)
1047setVerbose :: Int -> Idris ()
1050 let opts = idris_options i
1051 let opt' = opts { opt_verbose = t }
1052 putIState $ i { idris_options = opt' }
1054iReport :: Int -> String -> Idris ()
1055iReport level msg = do
1056 verbosity <- verbose
1058 when (level <= verbosity) $
1059 case idris_outputmode i of
1060 RawOutput h -> runIO $ hPutStrLn h msg
1061 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" msg n
1064typeInType :: Idris Bool
1065typeInType = do i <- getIState
1066 return (opt_typeintype (idris_options i))
1068setTypeInType :: Bool -> Idris ()
1069setTypeInType t = do i <- getIState
1070 let opts = idris_options i
1071 let opt' = opts { opt_typeintype = t }
1072 putIState $ i { idris_options = opt' }
1074coverage :: Idris Bool
1075coverage = do i <- getIState
1076 return (opt_coverage (idris_options i))
1078setCoverage :: Bool -> Idris ()
1079setCoverage t = do i <- getIState
1080 let opts = idris_options i
1081 let opt' = opts { opt_coverage = t }
1082 putIState $ i { idris_options = opt' }
1084setIBCSubDir :: FilePath -> Idris ()
1085setIBCSubDir fp = do i <- getIState
1086 let opts = idris_options i
1087 let opt' = opts { opt_ibcsubdir = fp }
1088 putIState $ i { idris_options = opt' }
1090valIBCSubDir :: IState -> Idris FilePath
1091valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1093addImportDir :: FilePath -> Idris ()
1094addImportDir fp = do i <- getIState
1095 let opts = idris_options i
1096 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1097 putIState $ i { idris_options = opt' }
1099setImportDirs :: [FilePath] -> Idris ()
1100setImportDirs fps = do i <- getIState
1101 let opts = idris_options i
1102 let opt' = opts { opt_importdirs = fps }
1103 putIState $ i { idris_options = opt' }
1105allImportDirs :: Idris [FilePath]
1106allImportDirs = do i <- getIState
1107 let optdirs = opt_importdirs (idris_options i)
1108 return ("." : reverse optdirs)
1110addSourceDir :: FilePath -> Idris ()
1111addSourceDir fp = do i <- getIState
1112 let opts = idris_options i
1113 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1114 putIState $ i { idris_options = opts' }
1116setSourceDirs :: [FilePath] -> Idris ()
1117setSourceDirs fps = do i <- getIState
1118 let opts = idris_options i
1119 let opts' = opts { opt_sourcedirs = nub $ fps }
1120 putIState $ i { idris_options = opts' }
1122allSourceDirs :: Idris [FilePath]
1123allSourceDirs = do i <- getIState
1124 let optdirs = opt_sourcedirs (idris_options i)
1125 return ("." : reverse optdirs)
1127colourise :: Idris Bool
1128colourise = do i <- getIState
1129 return $ idris_colourRepl i
1131setColourise :: Bool -> Idris ()
1132setColourise b = do i <- getIState
1133 putIState $ i { idris_colourRepl = b }
1135impShow :: Idris Bool
1136impShow = do i <- getIState
1137 return (opt_showimp (idris_options i))
1139setImpShow :: Bool -> Idris ()
1140setImpShow t = do i <- getIState
1141 let opts = idris_options i
1142 let opt' = opts { opt_showimp = t }
1143 putIState $ i { idris_options = opt' }
1145setColour :: ColourType -> IdrisColour -> Idris ()
1146setColour ct c = do i <- getIState
1147 let newTheme = setColour' ct c (idris_colourTheme i)
1148 putIState $ i { idris_colourTheme = newTheme }
1149 where setColour' KeywordColour c t = t { keywordColour = c }
1150 setColour' BoundVarColour c t = t { boundVarColour = c }
1151 setColour' ImplicitColour c t = t { implicitColour = c }
1152 setColour' FunctionColour c t = t { functionColour = c }
1153 setColour' TypeColour c t = t { typeColour = c }
1154 setColour' DataColour c t = t { dataColour = c }
1155 setColour' PromptColour c t = t { promptColour = c }
1156 setColour' PostulateColour c t = t { postulateColour = c }
1158logLvl :: Int -> String -> Idris ()
1159logLvl = logLvlCats []
1161logCoverage :: Int -> String -> Idris ()
1162logCoverage = logLvlCats [ICoverage]
1164logErasure :: Int -> String -> Idris ()
1165logErasure = logLvlCats [IErasure]
1167-- | Log an action of the parser
1168logParser :: Int -> String -> Idris ()
1169logParser = logLvlCats parserCats
1171-- | Log an action of the elaborator.
1172logElab :: Int -> String -> Idris ()
1173logElab = logLvlCats elabCats
1175-- | Log an action of the compiler.
1176logCodeGen :: Int -> String -> Idris ()
1177logCodeGen = logLvlCats codegenCats
1179logIBC :: Int -> String -> Idris ()
1180logIBC = logLvlCats [IIBC]
1182-- | Log aspect of Idris execution
1184-- An empty set of logging levels is used to denote all categories.
1186-- @TODO update IDE protocol
1187logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1188 -> Int -- ^ The Logging level the message should appear.
1189 -> String -- ^ The message to show the developer.
1191logLvlCats cs l msg = do
1193 let lvl = opt_logLevel (idris_options i)
1194 let cats = opt_logcats (idris_options i)
1196 when (inCat cs cats || null cats) $
1197 case idris_outputmode i of
1199 runIO $ hPutStrLn h msg
1201 let good = SexpList [IntegerAtom (toInteger l), toSExp msg]
1202 runIO . hPutStrLn h $ convSExp "log" good n
1204 inCat :: [LogCat] -> [LogCat] -> Bool
1205 inCat cs cats = any (`elem` cats) cs
1207cmdOptType :: Opt -> Idris Bool
1208cmdOptType x = do i <- getIState
1209 return $ x `elem` opt_cmdline (idris_options i)
1211noErrors :: Idris Bool
1212noErrors = do i <- getIState
1214 Nothing -> return True
1217setTypeCase :: Bool -> Idris ()
1218setTypeCase t = do i <- getIState
1219 let opts = idris_options i
1220 let opt' = opts { opt_typecase = t }
1221 putIState $ i { idris_options = opt' }
1223getIndentWith :: Idris Int
1226 return $ interactiveOpts_indentWith (idris_interactiveOpts i)
1228setIndentWith :: Int -> Idris ()
1229setIndentWith indentWith = do
1231 let opts = idris_interactiveOpts i
1232 let opts' = opts { interactiveOpts_indentWith = indentWith }
1233 putIState $ i { idris_interactiveOpts = opts' }
1235getIndentClause :: Idris Int
1238 return $ interactiveOpts_indentClause (idris_interactiveOpts i)
1240setIndentClause :: Int -> Idris ()
1241setIndentClause indentClause = do
1243 let opts = idris_interactiveOpts i
1244 let opts' = opts { interactiveOpts_indentClause = indentClause }
1245 putIState $ i { idris_interactiveOpts = opts' }
1247-- Dealing with parameters
1249expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1250 [Name] -> -- all names
1251 [Name] -> -- names with no declaration
1253expandParams dec ps ns infs tm = en 0 tm
1255 -- if we shadow a name (say in a lambda binding) that is used in a call to
1256 -- a lifted function, we need access to both names - once in the scope of the
1257 -- binding and once to call the lifted functions. So we'll explicitly shadow
1258 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1259 -- but we didn't...)
1261 mkShadow (UN n) = MN 0 n
1262 mkShadow (MN i n) = MN (i+1) n
1263 mkShadow (NS x s) = NS (mkShadow x) s
1265 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1266 -- that are merely mentioned.
1268 en 0 (PLam fc n nfc t s)
1269 | n `elem` (map fst ps ++ ns)
1270 = let n' = mkShadow n in
1271 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1272 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1273 en 0 (PPi p n nfc t s)
1274 | n `elem` (map fst ps ++ ns)
1275 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1276 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1277 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1278 en 0 (PLet fc n nfc ty v s)
1279 | n `elem` (map fst ps ++ ns)
1280 = let n' = mkShadow n in
1281 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1282 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1283 -- FIXME: Should only do this in a type signature!
1284 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1285 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1286 = let n' = mkShadow n in
1287 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1288 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1289 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1290 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1291 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1292 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1293 en 0 (PHidden t) = PHidden (en 0 t)
1294 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1295 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1296 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1297 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1298 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1299 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1301 en 0 (PQuote (Var n))
1302 | n `nselem` ns = PQuote (Var (dec n))
1303 en 0 (PApp fc (PInferRef fc' hl n) as)
1304 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1305 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1306 en 0 (PApp fc (PRef fc' hl n) as)
1307 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1308 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1309 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1310 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1311 en 0 (PAppBind fc (PRef fc' hl n) as)
1312 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1313 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1314 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1315 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1317 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1318 (map ((pexp . (PRef fc hl)) . fst) ps)
1319 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1320 (map ((pexp . (PRef fc hl)) . fst) ps)
1321 en 0 (PInferRef fc hl n)
1322 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1323 (map ((pexp . (PRef fc hl)) . fst) ps)
1324 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1325 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1326 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1327 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1328 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1329 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1331 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1332 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1334 en ql t = descend (en ql) t
1337 nselem x (y : xs) | nseq x y = True
1338 | otherwise = nselem x xs
1340 nseq x y = nsroot x == nsroot y
1342 enTacImp ql (TacImp aos st scr rig) = TacImp aos st (en ql scr) rig
1343 enTacImp ql other = other
1345expandParamsD :: Bool -> -- True = RHS only
1347 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1348expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1349 = if n `elem` ns && (not rhsonly)
1350 then -- trace (show (n, expandParams dec ps ns ty)) $
1351 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1352 else --trace (show (n, expandParams dec ps ns ty)) $
1353 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1354expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1355 = if n `elem` ns && (not rhsonly)
1356 then -- trace (show (n, expandParams dec ps ns ty)) $
1357 PPostulate e doc syn fc nfc o (dec n)
1358 (piBind ps (expandParams dec ps ns [] ty))
1359 else --trace (show (n, expandParams dec ps ns ty)) $
1360 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1361expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1362 = let n' = if n `elem` ns then dec n else n in
1363 PClauses fc opts n' (map expandParamsC cs)
1365 expandParamsC (PClause fc n lhs ws rhs ds)
1366 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1367 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1368 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1369 n' = if n `elem` ns then dec n else n
1370 -- names bound on the lhs should not be expanded on the rhs
1371 ns' = removeBound lhs ns in
1373 (map (expandParams dec ps'' ns' []) ws)
1374 (expandParams dec ps'' ns' [] rhs)
1375 (map (expandParamsD True ist dec ps'' ns') ds)
1376 expandParamsC (PWith fc n lhs ws wval pn ds)
1377 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1378 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1379 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1380 n' = if n `elem` ns then dec n else n
1381 ns' = removeBound lhs ns in
1383 (map (expandParams dec ps'' ns' []) ws)
1384 (expandParams dec ps'' ns' [] wval)
1386 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1387 updateps yn nm [] = []
1388 updateps yn nm (((a, t), i):as)
1389 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1390 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1392 removeBound lhs ns = ns \\ nub (bnames lhs)
1394 bnames (PRef _ _ n) = [n]
1395 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1396 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1397 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1400-- | Expands parameters defined in parameter and where blocks inside of declarations
1401expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1402 = PData doc argDocs syn fc co (expandPData pd)
1404 -- just do the type decl, leave constructors alone (parameters will be
1405 -- added implicitly)
1406 expandPData (PDatadecl n nfc ty cons)
1408 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1410 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1411 econ (doc, argDocs, n, nfc, t, fc, fs)
1412 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1413expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1415expandParamsD rhs ist dec ps ns (PParams f params pds)
1416 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1417 (map (expandParamsD True ist dec ps ns) pds)
1418-- (map (expandParamsD ist dec ps ns) pds)
1419expandParamsD rhs ist dec ps ns (PMutual f pds)
1420 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1421expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1422 = PInterface doc info f
1423 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1425 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1428 (map (expandParamsD rhs ist dec ps ns) decls)
1431expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1432 = let cn' = case cn of
1433 Just n -> if n `elem` ns then Just (dec n) else Just n
1434 Nothing -> Nothing in
1435 PImplementation doc argDocs info f
1436 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1439 (map (expandParams dec ps ns []) params)
1440 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1441 (expandParams dec ps ns [] ty)
1443 (map (expandParamsD True ist dec ps ns) decls)
1444expandParamsD rhs ist dec ps ns d = d
1446mapsnd f (x, t) = (x, f t)
1448expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1449 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1451expandImplementationScope ist dec ps ns d = d
1453-- | Calculate a priority for a type, for deciding elaboration order
1454-- * if it's just a type variable or concrete type, do it early (0)
1455-- * if there's only type variables and injective constructors, do it next (1)
1456-- * if there's a function type, next (2)
1457-- * finally, everything else (3)
1458getPriority :: IState -> PTerm -> Int
1459getPriority i tm = 1 -- pri tm
1462 case lookupP n (tt_ctxt i) of
1463 ((P (DCon _ _ _) _ _):_) -> 1
1464 ((P (TCon _ _) _ _):_) -> 1
1465 ((P Ref _ _):_) -> 1
1466 [] -> 0 -- must be locally bound, if it's not an error...
1467 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1469 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1470 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1471 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1472 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1473 pri (PTyped l r) = pri l
1474 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1475 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1476 pri (PAlternative _ a as) = maximum (map pri as)
1477 pri (PConstant _ _) = 0
1482addStatics :: Name -> Term -> PTerm -> Idris ()
1483addStatics n tm ptm =
1484 do let (statics, dynamics) = initStatics tm ptm
1487 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1488 Just p -> getNamesFrom 0 (fn_params p) tm ++
1489 concatMap (getParamNames ist . snd) statics
1490 _ -> concatMap (getParamNames ist . snd) statics
1492 let stnames = nub $ concatMap (freeArgNames . snd) statics
1493 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1495 -- also get the arguments which are 'uniquely inferrable' from
1496 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1497 -- or parameters to the type of a static
1498 let statics' = nub $ map fst statics ++
1499 filter (\x -> not (elem x dnames)) stnames
1500 let stpos = staticList statics' tm
1502 unless (null statics) $
1503 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1504 ++ showTmImpls ptm ++ "\n"
1505 ++ show statics ++ "\n" ++ show dynamics
1506 ++ "\n" ++ show paramnames
1507 ++ "\n" ++ show stpos
1508 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1509 addIBC (IBCStatic n)
1511 initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc t s)
1512 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1513 (static, (n, ty) : dynamic)
1514 initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc _ s)
1515 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1516 if pstatic p == Static then ((n, ty) : static, dynamic)
1517 else if (not (searchArg p))
1518 then (static, (n, ty) : dynamic)
1519 else (static, dynamic)
1520 initStatics t pt = ([], [])
1522 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1523 = case lookupCtxtExact n (idris_datatypes ist) of
1524 Just ti -> getNamePos 0 (param_pos ti) args
1526 where getNamePos i ps [] = []
1527 getNamePos i ps (P _ n _ : as)
1528 | i `elem` ps = n : getNamePos (i + 1) ps as
1529 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1530 getParamNames ist (Bind t (Pi _ _ (P _ n _) _) sc)
1531 = n : getParamNames ist sc
1532 getParamNames ist _ = []
1534 getNamesFrom i ps (Bind n (Pi _ _ _ _) sc)
1535 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1536 | otherwise = getNamesFrom (i + 1) ps sc
1537 getNamesFrom i ps sc = []
1539 freeArgNames (Bind n (Pi _ _ ty _) sc)
1540 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1541 freeArgNames tm = let (_, args) = unApply tm in
1542 concatMap freeNames args
1544 -- if a name appears in an interface or tactic implicit index, it doesn't
1545 -- affect its 'uniquely inferrable' from a static status since these are
1546 -- resolved by searching.
1547 searchArg (Constraint _ _ _) = True
1548 searchArg (TacImp _ _ _ _) = True
1551 staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc
1554-- Dealing with implicit arguments
1556-- Add some bound implicits to the using block if they aren't there already
1558addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1559addToUsing us [] = us
1560addToUsing us ((n, t) : ns)
1561 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1562 | otherwise = addToUsing us ns
1563 where impName (UImplicit n _) = Just n
1566-- Add constraint bindings from using block
1568addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1569addUsingConstraints syn fc t
1571 let ns = namesIn [] ist t
1572 let cs = getConstraints t -- check declared constraints
1573 let addconsts = uconsts \\ cs
1574 return (doAdd addconsts ns t)
1575 where uconsts = filter uconst (using syn)
1576 uconst (UConstraint _ _) = True
1580 -- if all of args in ns, then add it
1581 doAdd (UConstraint c args : cs) ns t
1582 | all (\n -> elem n ns) args
1583 = PPi (Constraint [] Dynamic RigW) (sMN 0 "cu") NoFC
1584 (mkConst c args) (doAdd cs ns t)
1585 | otherwise = doAdd cs ns t
1587 mkConst c args = PApp fc (PRef fc [] c)
1588 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1590 getConstraints (PPi (Constraint _ _ _) _ _ c sc)
1591 = getcapp c ++ getConstraints sc
1592 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1593 getConstraints _ = []
1595 getcapp (PApp _ (PRef _ _ c) args)
1596 = do ns <- mapM getName args
1597 return (UConstraint c ns)
1600 getName (PExp _ _ _ (PRef _ _ n)) = return n
1603-- | Add implicit bindings from using block, and bind any missing names
1604addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1605addUsingImpls syn n fc t
1606 = do ist <- getIState
1607 autoimpl <- getAutoImpls
1608 let ns_in = implicitNamesIn (map iname uimpls) ist t
1609 let ns = if autoimpl then ns_in
1610 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1612 let badnames = filter (\n -> not (implicitable n) &&
1613 n `notElem` (map iname uimpls)) ns
1614 unless (null badnames) $
1615 throwError (At fc (Elaborating "type of " n Nothing
1616 (NoSuchVariable (head badnames))))
1617 let cs = getArgnames t -- get already bound names
1618 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1619 -- if all names in the arguments of addconsts appear in ns,
1620 -- add the constraint implicitly
1621 return (bindFree ns (doAdd addimpls ns t))
1622 where uimpls = filter uimpl (using syn)
1623 uimpl (UImplicit _ _) = True
1626 iname (UImplicit n _) = n
1627 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1630 -- if all of args in ns, then add it
1631 doAdd (UImplicit n ty : cs) ns t
1633 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1634 | otherwise = doAdd cs ns t
1636 -- bind the free names which weren't in the using block
1639 | elem n (map iname uimpls) = bindFree ns tm
1641 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1643 getArgnames (PPi _ n _ c sc)
1644 = n : getArgnames sc
1647-- Given the original type and the elaborated type, return the implicitness
1648-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1650getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1651getUnboundImplicits i t tm = getImps t (collectImps tm)
1652 where collectImps (PPi p n _ t sc)
1653 = (n, (p, t)) : collectImps sc
1656 scopedimpl (Just i) = not (toplevel_imp i)
1657 scopedimpl _ = False
1659 getImps (Bind n (Pi _ i _ _) sc) imps
1660 | scopedimpl i = getImps sc imps
1661 getImps (Bind n (Pi _ _ t _) sc) imps
1662 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1664 argInfo n (Imp opt _ _ _ _ _) Placeholder
1665 = (True, PImp 0 True opt n Placeholder)
1666 argInfo n (Imp opt _ _ _ _ _) t'
1667 = (False, PImp (getPriority i t') True opt n t')
1668 argInfo n (Exp opt _ _ _) t'
1669 = (InaccessibleArg `elem` opt,
1670 PExp (getPriority i t') opt n t')
1671 argInfo n (Constraint opt _ _) t'
1672 = (InaccessibleArg `elem` opt,
1673 PConstraint 10 opt n t')
1674 argInfo n (TacImp opt _ scr _) t'
1675 = (InaccessibleArg `elem` opt,
1676 PTacImplicit 10 opt n scr t')
1677 getImps (Bind n (Pi _ _ t _) sc) imps = impBind n t : getImps sc imps
1678 where impBind n t = (True, PImp 1 True [] n Placeholder)
1681-- Add implicit Pi bindings for any names in the term which appear in an
1682-- argument position.
1684-- This has become a right mess already. Better redo it some time...
1685-- TODO: This is obsoleted by the new way of elaborating types, (which
1686-- calls addUsingImpls) but there's still a couple of places which use
1687-- it. Clean them up!
1689-- Issue 1739 in the issue tracker
1690-- https://github.com/idris-lang/Idris-dev/issues/1739
1691implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1692implicit info syn n ptm = implicit' info syn [] n ptm
1694implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1695implicit' info syn ignore n ptm
1697 auto <- getAutoImpls
1698 let (tm', impdata) = implicitise auto syn ignore i ptm
1699 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1700-- let (tm'', spos) = findStatics i tm'
1701 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1703 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1705-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1708 -- Detect unknown names in default arguments and throw error if found.
1709 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1710 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1712 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1713 notFoundInDefault kns (PTacImplicit _ _ n script _)
1715 case notFound kns (namesIn [] i script) of
1716 Nothing -> return (n:kns)
1717 Just name -> throwError (NoSuchVariable name)
1718 notFoundInDefault kns p = return ((pname p):kns)
1720 notFound :: [Name] -> [Name] -> Maybe Name
1721 notFound kns [] = Nothing
1722 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1723 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1725-- | Even if auto_implicits is off, we need to call this so we record
1726-- which arguments are implicit
1727implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1728implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1729 let (declimps, ns') = execState (imps True [] tm) ([], [])
1730 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1731 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1732 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1734 then (tm, reverse declimps)
1735 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1737 uvars = map ipair (filter uimplicit (using syn))
1738 pvars = syn_params syn
1740 inUsing n = n `elem` map fst uvars
1742 ipair (UImplicit x y) = (x, y)
1743 uimplicit (UImplicit _ _) = True
1746 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1747 | otherwise = x : dropAll xs ys
1750 -- Find names in argument position in a type, suitable for implicit
1752 -- Not the function position, but do everything else...
1753 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1754 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1756 imps top env ty@(PApp _ f as)
1757 = do (decls, ns) <- get
1758 let isn = nub (implNamesIn uvars ty)
1759 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1760 imps top env (PPi (Imp l _ _ _ _ _) n _ ty sc)
1761 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1763 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1764 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1765 imps True (n:env) sc
1766 imps top env (PPi (Exp l _ _ _) n _ ty sc)
1767 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1768 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1770 (decls, ns) <- get -- ignore decls in HO types
1771 put (PExp (getPriority ist ty) l n Placeholder : decls,
1772 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1773 imps True (n:env) sc
1774 imps top env (PPi (Constraint l _ _) n _ ty sc)
1775 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1776 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1778 (decls, ns) <- get -- ignore decls in HO types
1779 put (PConstraint 10 l n Placeholder : decls,
1780 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1781 imps True (n:env) sc
1782 imps top env (PPi (TacImp l _ scr _) n _ ty sc)
1783 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1784 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1786 (decls, ns) <- get -- ignore decls in HO types
1787 put (PTacImplicit 10 l n scr Placeholder : decls,
1788 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1789 imps True (n:env) sc
1790 imps top env (PRewrite _ _ l r _)
1791 = do (decls, ns) <- get
1792 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1793 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1794 imps top env (PTyped l r)
1796 imps top env (PPair _ _ _ l r)
1797 = do (decls, ns) <- get
1798 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1799 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1800 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1801 = do (decls, ns) <- get
1802 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1803 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1804 imps top env (PDPair _ _ _ l t r)
1805 = do (decls, ns) <- get
1806 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1808 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1809 imps top env (PAlternative ms a as)
1810 = do (decls, ns) <- get
1811 let isn = concatMap (namesIn uvars ist) as
1812 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1813 imps top env (PLam fc n _ ty sc)
1814 = do imps False env ty
1815 imps False (n:env) sc
1816 imps top env (PHidden tm) = imps False env tm
1817 imps top env (PUnifyLog tm) = imps False env tm
1818 imps top env (PNoImplicits tm) = imps False env tm
1819 imps top env (PRunElab fc tm ns) = imps False env tm
1820 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1821 imps top env _ = return ()
1823 pibind using [] sc = sc
1824 pibind using (n:ns) sc
1825 = case lookup n using of
1826 Just ty -> PPi impl_gen
1827 n NoFC ty (pibind using ns sc)
1828 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1829 n NoFC Placeholder (pibind using ns sc)
1831-- | Add implicit arguments in function calls
1832addImplPat :: IState -> PTerm -> PTerm
1833addImplPat = addImpl' True [] [] []
1835addImplBound :: IState -> [Name] -> PTerm -> PTerm
1836addImplBound ist ns = addImpl' False ns [] [] ist
1838addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1839addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1841-- | Add the implicit arguments to applications in the term [Name]
1842-- gives the names to always expend, even when under a binder of that
1843-- name (this is to expand methods with implicit arguments in
1844-- dependent interfaces).
1845addImpl :: [Name] -> IState -> PTerm -> PTerm
1846addImpl = addImpl' False [] []
1848-- TODO: in patterns, don't add implicits to function names guarded by constructors
1849-- and *not* inside a PHidden
1851addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1852addImpl' inpat env infns imp_meths ist ptm
1853 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1855 topname = case ptm of
1857 PApp _ (PRef _ _ n) _ -> n
1858 _ -> sUN "" -- doesn't matter then
1860 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1861 ai inpat qq env ds (PRef fc fcs f)
1862 | f `elem` infns = PInferRef fc fcs f
1863 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1864 ai inpat qq env ds (PHidden (PRef fc hl f))
1865 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1866 ai inpat qq env ds (PRewrite fc by l r g)
1867 = let l' = ai inpat qq env ds l
1868 r' = ai inpat qq env ds r
1869 g' = fmap (ai inpat qq env ds) g in
1870 PRewrite fc by l' r' g'
1871 ai inpat qq env ds (PTyped l r)
1872 = let l' = ai inpat qq env ds l
1873 r' = ai inpat qq env ds r in
1875 ai inpat qq env ds (PPair fc hls p l r)
1876 = let l' = ai inpat qq env ds l
1877 r' = ai inpat qq env ds r in
1878 PPair fc hls p l' r'
1879 ai inpat qq env ds (PDPair fc hls p l t r)
1880 = let l' = ai inpat qq env ds l
1881 t' = ai inpat qq env ds t
1882 r' = ai inpat qq env ds r in
1883 PDPair fc hls p l' t' r'
1884 ai inpat qq env ds (PAlternative ms a as)
1885 = let as' = map (ai inpat qq env ds) as in
1886 PAlternative ms a as'
1887 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1888 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1889 = let as' = map (fmap (ai inpat qq env ds)) as in
1890 PApp fc (PInferRef ffc hl f) as'
1891 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1892 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1893 | not (f `elem` map fst env)
1894 = let as' = map (fmap (ai inpat qq env ds)) as in
1895 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1896 | Just (Just ty) <- lookup f env =
1897 let as' = map (fmap (ai inpat qq env ds)) as
1898 arity = getPArity ty in
1899 mkPApp fc arity ftm as'
1900 ai inpat qq env ds (PApp fc f as)
1901 = let f' = ai inpat qq env ds f
1902 as' = map (fmap (ai inpat qq env ds)) as in
1904 ai inpat qq env ds (PWithApp fc f a)
1905 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1906 ai inpat qq env ds (PCase fc c os)
1907 = let c' = ai inpat qq env ds c in
1908 -- leave lhs alone, because they get lifted into a new pattern match
1909 -- definition which is passed through addImpl again
1910 PCase fc c' (map aiCase os)
1913 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1915 -- Anything beginning with a lower case letter, not applied,
1916 -- and no namespace is a pattern variable
1917 patnames (PApp _ (PRef _ _ f) [])
1918 | implicitable f = [(f, Nothing)]
1919 patnames (PRef _ _ f)
1920 | implicitable f = [(f, Nothing)]
1921 patnames (PApp _ (PRef _ _ _) args)
1922 = concatMap patnames (map getTm args)
1923 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1924 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1925 patnames (PAs _ _ t) = patnames t
1926 patnames (PAlternative _ _ ts) = concatMap patnames ts
1930 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1931 (ai inpat qq env ds t)
1932 (ai inpat qq env ds f)
1934 -- If the name in a lambda is an unapplied data constructor name, do this
1935 -- as a 'case' instead because we'll expect to match on it
1936 ai inpat qq env ds (PLam fc n nfc ty sc)
1937 = if canBeDConName n (tt_ctxt ist)
1938 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1939 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1940 [(PRef fc [] n, sc)]))
1941 else let ty' = ai inpat qq env ds ty
1942 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1943 PLam fc n nfc ty' sc'
1944 ai inpat qq env ds (PLet fc n nfc ty val sc)
1945 = if canBeDConName n (tt_ctxt ist)
1946 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1947 else let ty' = ai inpat qq env ds ty
1948 val' = ai inpat qq env ds val
1949 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1950 PLet fc n nfc ty' val' sc'
1951 ai inpat qq env ds (PPi p n nfc ty sc)
1952 = let ty' = ai inpat qq env ds ty
1953 env' = if n `elem` imp_meths then env
1955 ((n, Just ty) : env)
1956 sc' = ai inpat qq env' ds sc in
1958 ai inpat qq env ds (PGoal fc r n sc)
1959 = let r' = ai inpat qq env ds r
1960 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1962 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1963 -- Don't do PProof or PTactics since implicits get added when scope is
1964 -- properly known in ElabTerm.runTac
1965 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1966 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1967 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1968 (fmap (ai inpat True env ds) g)
1969 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1970 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1971 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1972 ai inpat qq env ds tm = tm
1974 handleErr (Left err) = PElabError err
1975 handleErr (Right x) = x
1977-- if in a pattern, and there are no arguments, and there's no possible
1978-- names with zero explicit arguments, don't add implicits.
1980aiFn :: Name -> Bool -> Bool -> Bool
1983 -> Name -- ^ function being applied
1985 -> [PArg] -- ^ initial arguments (if in a pattern)
1987aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1988 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1990 = case lookupDef f (tt_ctxt ist) of
1991 [] -> Right $ PPatvar ffc f
1992 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1993 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1994 if (not (vname f) || tcname f
1995 || any (conCaf (tt_ctxt ist)) ialts)
1996-- any constructor alts || any allImp ialts))
1997 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1998 else Right $ PPatvar ffc f
1999 where imp (PExp _ _ _ _) = False
2002 allImp xs = all imp xs
2004 unqualified (NS _ _) = False
2005 unqualified _ = True
2007 constructor (TyDecl (DCon _ _ _) _) = True
2008 constructor _ = False
2010 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
2012 vname (UN n) = True -- non qualified
2015aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
2016 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
2017aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
2018 -- This is where namespaces get resolved by adding PAlternative
2019 = do let ns = lookupCtxtName f (idris_implicits ist)
2020 let nh = filter (\(n, _) -> notHidden n) ns
2021 let ns' = case trimAlts ds nh of
2025 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
2027 [] -> case metaVar f (map fst (idris_metavars ist)) of
2028 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
2029 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
2031 PAlternative [] (ExactlyOne True) $
2032 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
2033 (insertImpl ns as)) alts
2035 -- if the name is in imp_meths, we should actually refer to the bound
2036 -- name rather than the global one after expanding implicits
2037 isImpName f f' | f `elem` imp_meths = f
2040 -- If it's a metavariable name, try to qualify it from the list of
2041 -- unsolved metavariables
2042 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
2043 metaVar f (_ : ns) = metaVar f ns
2044 metaVar f [] = Nothing
2046 trimAlts [] alts = alts
2048 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
2053 notHidden n = case getAccessibility n of
2059 = case lookupDefAccExact n False (tt_ctxt ist) of
2063 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
2064 -> [PArg] -- ^ given arguments
2067 = let (as', badimpls) = partition (impIn ps) as in
2068 map addUnknownImp badimpls ++
2069 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
2071 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2072 -> [PArg] -- parameters
2073 -> [PArg] -- explicit arguments
2074 -> [PArg] -- implicits given
2076 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2077 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2078 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2079 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2080 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2081 let rtc = PResolveTC fc in
2082 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2083 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2084 case find n imps [] of
2086 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2088 PImp p True l n Placeholder :
2089 insImpAcc (M.insert n Placeholder pnas) ps given imps
2090 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2091 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2092 case find n imps [] of
2094 PTacImplicit p l n sc tm :
2095 insImpAcc (M.insert n tm pnas) ps given imps'
2098 then PTacImplicit p l n sc Placeholder :
2099 insImpAcc (M.insert n Placeholder pnas) ps given imps
2100 else PTacImplicit p l n sc sc :
2101 insImpAcc (M.insert n sc pnas) ps given imps
2102 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2103 insImpAcc _ _ given imps = given ++ imps
2105 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2107 find n [] acc = Nothing
2108 find n (PImp _ _ _ n' t : gs) acc
2109 | n == n' = Just (t, reverse acc ++ gs)
2110 find n (PTacImplicit _ _ n' _ t : gs) acc
2111 | n == n' = Just (t, reverse acc ++ gs)
2112 find n (g : gs) acc = find n gs (g : acc)
2114-- | return True if the second argument is an implicit argument which
2115-- is expected in the implicits, or if it's not an implicit
2116impIn :: [PArg] -> PArg -> Bool
2117impIn ps (PExp _ _ _ _) = True
2118impIn ps (PConstraint _ _ _ _) = True
2119impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2121expArg (PExp _ _ _ _) = True
2122expArg (PConstraint _ _ _ _) = True
2125-- replace non-linear occurrences with _
2127stripLinear :: IState -> PTerm -> PTerm
2128stripLinear i tm = evalState (sl tm) [] where
2129 sl :: PTerm -> State [Name] PTerm
2131 | (_:_) <- lookupTy f (tt_ctxt i)
2132 = return $ PRef fc hl f
2133 | otherwise = do ns <- get
2135 then return $ PHidden (PRef fc hl f) -- Placeholder
2136 else do put (f : ns)
2137 return (PRef fc hl f)
2141 then return $ PHidden (PPatvar fc f) -- Placeholder
2142 else do put (f : ns)
2143 return (PPatvar fc f)
2144 -- Assumption is that variables are all the same in each alternative
2145 sl t@(PAlternative ms b as) = do ns <- get
2147 return (PAlternative ms b as')
2148 where slAlts ns (a : as) = do put ns
2152 slAlts ns [] = return []
2153 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2154 sl (PDPair fc hls p l t r) = do l' <- sl l
2157 return (PDPair fc hls p l' t' r')
2158 sl (PApp fc fn args) = do fn' <- case fn of
2159 -- Just the args, fn isn't matchable as a var
2160 PRef _ _ _ -> return fn
2162 args' <- mapM slA args
2163 return $ PApp fc fn' args'
2164 where slA (PImp p m l n t) = do t' <- sl t
2165 return $ PImp p m l n t'
2166 slA (PExp p l n t) = do t' <- sl t
2167 return $ PExp p l n t'
2168 slA (PConstraint p l n t)
2170 return $ PConstraint p l n t'
2171 slA (PTacImplicit p l n sc t)
2173 return $ PTacImplicit p l n sc t'
2176-- | Remove functions which aren't applied to anything, which must then
2177-- be resolved by unification. Assume names resolved and alternatives
2178-- filled in (so no ambiguity).
2179stripUnmatchable :: IState -> PTerm -> PTerm
2180stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2181 su :: PTerm -> PTerm
2182 su tm@(PRef fc hl f)
2183 | (Bind n (Pi _ _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2185 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2186 not (implicitable f)
2188 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2189 not (implicitable f)
2191 su (PApp fc f@(PRef _ _ fn) args)
2192 -- here we use canBeDConName because the impossible pattern
2193 -- check will not necessarily fully resolve constructor names,
2194 -- and these bare names will otherwise get in the way of
2195 -- impossbility checking.
2196 | -- Just fn <- getFn f,
2197 canBeDConName fn ctxt
2198 = PApp fc f (fmap (fmap su) args)
2199 where getFn (PRef _ _ fn) = Just fn
2200 getFn (PApp _ f args) = getFn f
2203 = PHidden (PApp fc f args)
2204 su (PAlternative ms b alts)
2205 = let alts' = filter (/= Placeholder) (map su alts) in
2206 if null alts' then Placeholder
2207 else PAlternative ms b alts'
2208 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2209 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2210 su t@(PLam fc _ _ _ _) = PHidden t
2211 su t@(PPi _ _ _ _ _) = PHidden t
2212 su t@(PConstant _ c) | isTypeConst c = PHidden t
2217stripUnmatchable i tm = tm
2220mkPApp fc a f as = let rest = drop a as in
2221 if a == 0 then appRest fc f rest
2222 else appRest fc (PApp fc f (take a as)) rest
2225 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2229-- | Find 'static' argument positions
2230-- (the declared ones, plus any names in argument position in the declared
2232-- FIXME: It's possible that this really has to happen after elaboration
2233findStatics :: IState -> PTerm -> (PTerm, [Bool])
2234findStatics ist tm = let (ns, ss) = fs tm
2235 in runState (pos ns ss tm) []
2236 where fs (PPi p n fc t sc)
2237 | Static <- pstatic p
2238 = let (ns, ss) = fs sc in
2239 (namesIn [] ist t : ns, n : ss)
2240 | otherwise = let (ns, ss) = fs sc in
2244 inOne n ns = length (filter id (map (elem n) ns)) == 1
2246 pos ns ss (PPi p n fc t sc)
2247 | elem n ss = do sc' <- pos ns ss sc
2250 return (PPi (p { pstatic = Static }) n fc t sc')
2251 | otherwise = do sc' <- pos ns ss sc
2254 return (PPi p n fc t sc')
2255 pos ns ss t = return t
2257-- for 6.12/7 compatibility
2258data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2260instance Applicative (EitherErr a) where
2264instance Monad (EitherErr a) where
2267 (LeftErr e) >>= _ = LeftErr e
2268 RightOK v >>= k = k v
2270toEither :: EitherErr a b -> Either a b
2271toEither (LeftErr e) = Left e
2272toEither (RightOK ho) = Right ho
2274-- | Syntactic match of a against b, returning pair of variables in a
2275-- and what they match. Returns the pair that failed if not a match.
2276matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2277matchClause = matchClause' False
2279matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2280matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2281 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2283 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2286 match' x y = match (fullApp x) (fullApp y)
2287 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2288 | fi == txt "fromInteger" && b == txt "builtins",
2289 PConstant _ (I _) <- getTm x = match (getTm x) x'
2290 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2291 | fi == txt "fromInteger" && b == txt "builtins",
2292 PConstant _ (I _) <- getTm x = match (getTm x) x'
2293 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2294 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2295 match (PApp _ f args) (PApp _ f' args')
2296 | length args == length args'
2297 = do mf <- match' f f'
2298 ms <- zipWithM matchArg args args'
2299 return (mf ++ concat ms)
2300 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2301 match (PPatvar f n) xr = match (PRef f [f] n) xr
2302 match xr (PPatvar f n) = match xr (PRef f [f] n)
2303 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2304 match (PRef _ _ n) tm@(PRef _ _ n')
2305 | n == n' && not names &&
2306 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2307 || tm == Placeholder)
2309 -- if one namespace is missing, drop the other
2310 | n == n' || n == dropNS n' || dropNS n == n' = return []
2311 where dropNS (NS n _) = n
2313 match (PRef _ _ n) tm
2314 | not names && (not (isConName n (tt_ctxt i) ||
2315 isFnName n (tt_ctxt i)) || tm == Placeholder)
2317 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2318 = do ml <- match' l l'
2321 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2324 match (PTyped l r) x = match l x
2325 match x (PTyped l r) = match x l
2326 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2329 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2332 return (ml ++ mt ++ mr)
2333 match (PAlternative _ a as) (PAlternative _ a' as')
2334 = do ms <- zipWithM match' as as'
2336 match a@(PAlternative _ _ as) b
2337 = do let ms = zipWith match' as (repeat b)
2338 case (rights (map toEither ms)) of
2341 match (PCase _ _ _) _ = return [] -- lifted out
2342 match (PMetavar _ _) _ = return [] -- modified
2343 match (PInferRef _ _ _) _ = return [] -- modified
2344 match (PQuote _) _ = return []
2345 match (PProof _) _ = return []
2346 match (PTactics _) _ = return []
2347 match (PResolveTC _) (PResolveTC _) = return []
2348 match (PTrue _ _) (PTrue _ _) = return []
2349 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2352 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2355 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2356 mty <- match' ty ty'
2358 return (mt ++ mty ++ ms)
2359 match (PHidden x) (PHidden y)
2360 | RightOK xs <- match x y = return xs -- to collect variables
2361 | otherwise = return [] -- Otherwise hidden things are unmatchable
2363 | RightOK xs <- match x y = return xs
2364 | otherwise = return []
2366 | RightOK xs <- match x y = return xs
2367 | otherwise = return []
2368 match (PUnifyLog x) y = match' x y
2369 match x (PUnifyLog y) = match' x y
2370 match (PNoImplicits x) y = match' x y
2371 match x (PNoImplicits y) = match' x y
2372 match Placeholder _ = return []
2373 match _ Placeholder = return []
2374 match (PResolveTC _) _ = return []
2375 match a b | a == b = return []
2376 | otherwise = LeftErr (a, b)
2378 checkRpts (RightOK ms) = check ms where
2380 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2383 check (_:xs) = check xs
2385 checkRpts (LeftErr x) = Left x
2387substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2388substMatches ms = substMatchesShadow ms []
2390-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2391-- substMatchesShadow [] shs t = t
2392-- substMatchesShadow ((n,tm):ns) shs t
2393-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2395substMatch :: Name -> PTerm -> PTerm -> PTerm
2396substMatch n = substMatchShadow n []
2398substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2399substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2401substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2402substMatchesShadow nmap shs t = sm shs t where
2403 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2404 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2405 sm xs (PPi p x fc t sc)
2407 = let x' = nextName x in
2408 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2409 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2410 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2411 sm xs (PLet fc x xfc val t sc)
2412 = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)
2413 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2414 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2415 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2416 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2418 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2419 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2420 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2421 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2422 sm xs (PHidden x) = PHidden (sm xs x)
2423 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2424 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2425 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2426 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2429 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2432shadow :: Name -> Name -> PTerm -> PTerm
2433shadow n n' t = sm 0 t where
2434 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2435 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2436 | otherwise = PLam fc x xfc (sm 0 t) sc
2437 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2438 | otherwise = PPi p x fc (sm 0 t) sc
2439 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2440 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2441 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2442 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2443 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2444 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2445 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2446 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2447 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2448 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2449 sm 0 (PAlternative ms a as)
2450 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2451 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2452 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2453 sm 0 (PHidden x) = PHidden (sm 0 x)
2454 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2455 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2456 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2457 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2458 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2459 sm ql x = descend (sm ql) x
2461 shadowAlt p@(x, oldn) = (update x, update oldn)
2462 update oldn | n == oldn = n'
2465-- | Rename any binders which are repeated (so that we don't have to
2466-- mess about with shadowing anywhere else).
2467mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2468mkUniqueNames env shadows tm
2469 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2471 initMap = M.fromList shadows
2473 inScope :: S.Set Name
2474 inScope = S.fromList $ boundNamesIn tm
2476 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2477 return (arg { getTm = t' })
2479 -- Initialise the unique name with the environment length (so we're not
2480 -- looking for too long...)
2481 initN (UN n) l = UN $ txt (str n ++ show l)
2482 initN (MN i s) l = MN (i+l) s
2485 -- FIXME: Probably ought to do this for completeness! It's fine as
2486 -- long as there are no bindings inside tactics though.
2487 mkUniqT _ nmap tac = return tac
2489 mkUniq :: Int -- ^ The number of quotations that we're under
2490 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2491 mkUniq 0 nmap (PLam fc n nfc ty sc)
2495 then do let n' = uniqueNameSet (initN n (S.size env))
2496 (S.union env inScope)
2497 return (n', sc) -- shadow n n' sc)
2499 put (S.insert n' env)
2500 let nmap' = M.insert n n' nmap
2501 ty' <- mkUniq 0 nmap ty
2502 sc'' <- mkUniq 0 nmap' sc'
2503 return $! PLam fc n' nfc ty' sc''
2504 mkUniq 0 nmap (PPi p n fc ty sc)
2508 then do let n' = uniqueNameSet (initN n (S.size env))
2509 (S.union env inScope)
2510 return (n', sc) -- shadow n n' sc)
2512 put (S.insert n' env)
2513 let nmap' = M.insert n n' nmap
2514 ty' <- mkUniq 0 nmap ty
2515 sc'' <- mkUniq 0 nmap' sc'
2516 return $! PPi p n' fc ty' sc''
2517 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2521 then do let n' = uniqueNameSet (initN n (S.size env))
2522 (S.union env inScope)
2523 return (n', sc) -- shadow n n' sc)
2525 put (S.insert n' env)
2526 let nmap' = M.insert n n' nmap
2527 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2528 sc'' <- mkUniq 0 nmap' sc'
2529 return $! PLet fc n' nfc ty' val' sc''
2530 mkUniq 0 nmap (PApp fc t args)
2531 = do t' <- mkUniq 0 nmap t
2532 args' <- mapM (mkUniqA 0 nmap) args
2533 return $! PApp fc t' args'
2534 mkUniq 0 nmap (PAppBind fc t args)
2535 = do t' <- mkUniq 0 nmap t
2536 args' <- mapM (mkUniqA 0 nmap) args
2537 return $! PAppBind fc t' args'
2538 mkUniq 0 nmap (PCase fc t alts)
2539 = do t' <- mkUniq 0 nmap t
2540 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2541 return (x', y')) alts
2542 return $! PCase fc t' alts'
2543 mkUniq 0 nmap (PIfThenElse fc c t f)
2544 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2545 mkUniq 0 nmap (PPair fc hls p l r)
2546 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2547 return $! PPair fc hls p l' r'
2548 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2551 (n', sc') <- if n `S.member` env
2552 then do let n' = uniqueNameSet n (S.union env inScope)
2553 return (n', sc) -- shadow n n' sc)
2555 put (S.insert n' env)
2556 let nmap' = M.insert n n' nmap
2557 t' <- mkUniq 0 nmap t
2558 sc'' <- mkUniq 0 nmap' sc'
2559 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2560 mkUniq 0 nmap (PDPair fc hls p l t r)
2561 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2562 return $! PDPair fc hls p l' t' r'
2563 mkUniq 0 nmap (PAlternative ns b as)
2564 -- store the nmap and defer the rest until we've pruned the set
2565 -- during elaboration
2566 = return $ PAlternative (ns ++ M.toList nmap) b as
2567 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2568 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2569 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2570 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2571 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2572 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2573 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2574 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2575 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2576 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2579 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2581 mkUniq ql nmap (PQuasiquote tm ty) =
2582 do tm' <- mkUniq (ql + 1) nmap tm
2584 Nothing -> return Nothing
2585 Just t -> fmap Just $ mkUniq ql nmap t
2586 return $! PQuasiquote tm' ty'
2587 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2589 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2591getFile :: Opt -> Maybe String
2592getFile (Filename s) = Just s
2595getBC :: Opt -> Maybe String
2596getBC (BCAsm s) = Just s
2599getOutput :: Opt -> Maybe String
2600getOutput (Output s) = Just s
2601getOutput _ = Nothing
2603getIBCSubDir :: Opt -> Maybe String
2604getIBCSubDir (IBCSubDir s) = Just s
2605getIBCSubDir _ = Nothing
2607getImportDir :: Opt -> Maybe String
2608getImportDir (ImportDir s) = Just s
2609getImportDir _ = Nothing
2611getSourceDir :: Opt -> Maybe String
2612getSourceDir (SourceDir s) = Just s
2613getSourceDir _ = Nothing
2615getPkgDir :: Opt -> Maybe String
2616getPkgDir (Pkg s) = Just s
2617getPkgDir _ = Nothing
2619getPkg :: Opt -> Maybe (Bool, String)
2620getPkg (PkgBuild s) = Just (False, s)
2621getPkg (PkgInstall s) = Just (True, s)
2624getPkgClean :: Opt -> Maybe String
2625getPkgClean (PkgClean s) = Just s
2626getPkgClean _ = Nothing
2628getPkgREPL :: Opt -> Maybe String
2629getPkgREPL (PkgREPL s) = Just s
2630getPkgREPL _ = Nothing
2632getPkgCheck :: Opt -> Maybe String
2633getPkgCheck (PkgCheck s) = Just s
2634getPkgCheck _ = Nothing
2636-- | Returns None if given an Opt which is not PkgMkDoc
2637-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2638getPkgMkDoc :: Opt -- ^ Opt to extract
2639 -> Maybe (Bool, String) -- ^ Result
2640getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2641getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2642getPkgMkDoc _ = Nothing
2644getPkgTest :: Opt -- ^ the option to extract
2645 -> Maybe String -- ^ the package file to test
2646getPkgTest (PkgTest f) = Just f
2647getPkgTest _ = Nothing
2649getCodegen :: Opt -> Maybe Codegen
2650getCodegen (UseCodegen x) = Just x
2651getCodegen _ = Nothing
2653getCodegenArgs :: Opt -> Maybe String
2654getCodegenArgs (CodegenArgs args) = Just args
2655getCodegenArgs _ = Nothing
2657getConsoleWidth :: Opt -> Maybe ConsoleWidth
2658getConsoleWidth (UseConsoleWidth x) = Just x
2659getConsoleWidth _ = Nothing
2661getExecScript :: Opt -> Maybe String
2662getExecScript (InterpretScript expr) = Just expr
2663getExecScript _ = Nothing
2665getPkgIndex :: Opt -> Maybe FilePath
2666getPkgIndex (PkgIndex file) = Just file
2667getPkgIndex _ = Nothing
2669getEvalExpr :: Opt -> Maybe String
2670getEvalExpr (EvalExpr expr) = Just expr
2671getEvalExpr _ = Nothing
2673getOutputTy :: Opt -> Maybe OutputType
2674getOutputTy (OutputTy t) = Just t
2675getOutputTy _ = Nothing
2677getLanguageExt :: Opt -> Maybe LanguageExt
2678getLanguageExt (Extension e) = Just e
2679getLanguageExt _ = Nothing
2681getTriple :: Opt -> Maybe String
2682getTriple (TargetTriple x) = Just x
2683getTriple _ = Nothing
2685getCPU :: Opt -> Maybe String
2686getCPU (TargetCPU x) = Just x
2689getOptLevel :: Opt -> Maybe Int
2690getOptLevel (OptLevel x) = Just x
2691getOptLevel _ = Nothing
2693getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2694getOptimisation (AddOpt p) = Just (True, p)
2695getOptimisation (RemoveOpt p) = Just (False, p)
2696getOptimisation _ = Nothing
2698getColour :: Opt -> Maybe Bool
2699getColour (ColourREPL b) = Just b
2700getColour _ = Nothing
2702getClient :: Opt -> Maybe String
2703getClient (Client x) = Just x
2704getClient _ = Nothing
2706-- Get the first valid port
2707getPort :: [Opt] -> Maybe REPLPort
2709getPort (Port p : _ ) = Just p
2710getPort (_ : xs) = getPort xs
2712opt :: (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