2Module : Idris.AbsSyntax
3Description : Provides Idris' core data definitions and utility code.
6Maintainer : The Idris Community.
8{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
9 PatternGuards, TypeSynonymInstances #-}
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
13 , module Idris.AbsSyntaxTree
16import Idris.AbsSyntaxTree
18import Idris.Core.Elaborate hiding (Tactic(..))
19import Idris.Core.Evaluate
21import Idris.Core.Typecheck
22import Idris.Docstrings
23import Idris.IdeMode hiding (Opt(..))
24import IRTS.CodegenCommon
26import Util.DynamicLinker
31import Control.Applicative
32import Control.Monad (liftM3)
33import Control.Monad.State
36import Data.Generics.Uniplate.Data (descend, descendM)
37import Data.List hiding (insert, union)
38import qualified Data.Map as M
40import qualified Data.Set as S
41import qualified Data.Text as T
42import Data.Word (Word)
44import Network (PortID(PortNumber))
45import System.Console.Haskeline
46import System.Directory (canonicalizePath, doesFileExist)
48import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)
50getContext :: Idris Context
51getContext = do i <- getIState; return (tt_ctxt i)
53forCodegen :: Codegen -> [(Codegen, a)] -> [a]
54forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
56 eqLang (Via _ x) (Via _ y) = x == y
57 eqLang Bytecode Bytecode = True
60getObjectFiles :: Codegen -> Idris [FilePath]
61getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
63addObjectFile :: Codegen -> FilePath -> Idris ()
64addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
66getLibs :: Codegen -> Idris [String]
67getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
69addLib :: Codegen -> String -> Idris ()
70addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
72getFlags :: Codegen -> Idris [String]
73getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
75addFlag :: Codegen -> String -> Idris ()
76addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
78addDyLib :: [String] -> Idris (Either DynamicLib String)
79addDyLib libs = do i <- getIState
80 let ls = idris_dynamic_libs i
81 let importdirs = opt_importdirs (idris_options i)
82 case mapMaybe (findDyLib ls) libs of
83 x:_ -> return (Left x)
85 handle <- lift . lift .
86 mapM (\l -> catchIO (tryLoadLib importdirs l)
87 (\_ -> return Nothing)) $ libs
89 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
90 intercalate "," libs ++ "\"")
91 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
93 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
94 findDyLib [] l = Nothing
95 findDyLib (lib:libs) l | l == lib_name lib = Just lib
96 | otherwise = findDyLib libs l
98getAutoImports :: Idris [FilePath]
99getAutoImports = do i <- getIState
100 return (opt_autoImport (idris_options i))
102addAutoImport :: FilePath -> Idris ()
103addAutoImport fp = do i <- getIState
104 let opts = idris_options i
105 let autoimps = opt_autoImport opts
106 put (i { idris_options = opts { opt_autoImport =
107 fp : opt_autoImport opts } } )
109addDefinedName :: Name -> Idris ()
110addDefinedName n = do ist <- getIState
111 putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }
113getDefinedNames :: Idris [Name]
114getDefinedNames = do ist <- getIState
115 return (S.toList (idris_inmodule ist))
117addTT :: Term -> Idris (Maybe Term)
118addTT t = do ist <- getIState
119 case M.lookup t (idris_ttstats ist) of
120 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
121 putIState $ ist { idris_ttstats = tt' }
123 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
124 putIState $ ist { idris_ttstats = tt' }
128dumpTT = do ist <- get
129 let sts = sortBy count (M.toList (idris_ttstats ist))
133 count (_,x) (_,y) = compare y x
134 dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)
136addHdr :: Codegen -> String -> Idris ()
137addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
139addImported :: Bool -> FilePath -> Idris ()
142 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
144addLangExt :: LanguageExt -> Idris ()
145addLangExt TypeProviders = do i <- getIState
147 idris_language_extensions = TypeProviders : idris_language_extensions i
149addLangExt ErrorReflection = do i <- getIState
151 idris_language_extensions = ErrorReflection : idris_language_extensions i
154-- | Transforms are organised by the function being applied on the lhs
155-- of the transform, to make looking up appropriate transforms quicker
156addTrans :: Name -> (Term, Term) -> Idris ()
159 let t' = case lookupCtxtExact basefn (idris_transforms i) of
160 Just def -> (t : def)
162 putIState $ i { idris_transforms = addDef basefn t'
163 (idris_transforms i) }
165addErrRev :: (Term, Term) -> Idris ()
166addErrRev t = do i <- getIState
167 putIState $ i { idris_errRev = t : idris_errRev i }
169addErasureUsage :: Name -> Int -> Idris ()
170addErasureUsage n i = do ist <- getIState
171 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
173addExport :: Name -> Idris ()
174addExport n = do ist <- getIState
175 putIState $ ist { idris_exports = n : idris_exports ist }
177addUsedName :: FC -> Name -> Name -> Idris ()
179 = do ist <- getIState
180 case lookupTyName n (tt_ctxt ist) of
181 [(n', ty)] -> addUsage n' 0 ty
182 [] -> throwError (At fc (NoSuchVariable n))
183 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
184 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
186 | otherwise = addUsage n (i + 1) sc
187 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
189getErasureUsage :: Idris [(Name, Int)]
190getErasureUsage = do ist <- getIState;
191 return (idris_erasureUsed ist)
193getExports :: Idris [Name]
194getExports = do ist <- getIState
195 return (idris_exports ist)
197totcheck :: (FC, Name) -> Idris ()
198totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
200defer_totcheck :: (FC, Name) -> Idris ()
203 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
205clear_totcheck :: Idris ()
206clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
208setFlags :: Name -> [FnOpt] -> Idris ()
209setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
211addFnOpt :: Name -> FnOpt -> Idris ()
212addFnOpt n f = do i <- getIState
213 let fls = case lookupCtxtExact n (idris_flags i) of
218setFnInfo :: Name -> FnInfo -> Idris ()
219setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
221setAccessibility :: Name -> Accessibility -> Idris ()
224 let ctxt = setAccess n a (tt_ctxt i)
225 putIState $ i { tt_ctxt = ctxt }
227-- | get the accessibility of a name outside this module
228getFromHideList :: Name -> Idris (Maybe Accessibility)
229getFromHideList n = do i <- getIState
230 return $ lookupCtxtExact n (hide_list i)
232setTotality :: Name -> Totality -> Idris ()
235 let ctxt = setTotal n a (tt_ctxt i)
236 putIState $ i { tt_ctxt = ctxt }
238setInjectivity :: Name -> Injectivity -> Idris ()
241 let ctxt = setInjective n a (tt_ctxt i)
242 putIState $ i { tt_ctxt = ctxt }
244getTotality :: Name -> Idris Totality
247 case lookupTotal n (tt_ctxt i) of
249 _ -> return (Total [])
251-- Get coercions which might return the required type
252getCoercionsTo :: IState -> Type -> [Name]
254 let cs = idris_coercions i
255 (fn,_) = unApply (getRetTy ty) in
257 where findCoercions t [] = []
258 findCoercions t (n : ns) =
259 let ps = case lookupTy n (tt_ctxt i) of
260 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
261 (t', _) -> [n | t == t']
263 ps ++ findCoercions t ns
265addToCG :: Name -> CGInfo -> Idris ()
268 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
270addCalls :: Name -> [Name] -> Idris ()
273 case lookupCtxtExact n (idris_callgraph i) of
274 Nothing -> addToCG n (CGInfo calls Nothing [] [])
275 Just (CGInfo cs ans scg used) ->
276 addToCG n (CGInfo (nub (calls ++ cs)) ans scg used)
278addTyInferred :: Name -> Idris ()
281 putIState $ i { idris_tyinfodata =
282 addDef n TIPartial (idris_tyinfodata i) }
284addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
285addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
286 mapM_ addConstraint ts
288 where addConstraint (x, y) = findMVApps x y
291 = do let (fx, argsx) = unApply x
292 let (fy, argsy) = unApply y
297 else mapM_ addConstraint (zip argsx argsy)
299 tryAddMV (P _ mv _) y =
301 case lookup mv (idris_metavars ist) of
302 Just _ -> addConstraintRule mv y
304 tryAddMV _ _ = return ()
306 addConstraintRule :: Name -> Term -> Idris ()
307 addConstraintRule n t
309 logLvl 1 $ "TI constraint: " ++ show (n, t)
310 case lookupCtxt n (idris_tyinfodata ist) of
312 do mapM_ (checkConsistent t) ts
313 let ti' = addDef n (TISolution (t : ts))
314 (idris_tyinfodata ist)
315 put $ ist { idris_tyinfodata = ti' }
317 do let ti' = addDef n (TISolution [t])
318 (idris_tyinfodata ist)
319 put $ ist { idris_tyinfodata = ti' }
321 -- Check a solution is consistent with previous solutions
322 -- Meaning: If heads are both data types, they had better be the
324 checkConsistent :: Term -> Term -> Idris ()
325 checkConsistent x y =
326 do let (fx, _) = unApply x
327 let (fy, _) = unApply y
329 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
330 (P (TCon _ _) n _, Constant _) -> errWhen True
331 (Constant _, P (TCon _ _) n' _) -> errWhen True
332 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
337 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
338 errWhen False = return ()
340isTyInferred :: Name -> Idris Bool
343 case lookupCtxt n (idris_tyinfodata i) of
344 [TIPartial] -> return True
347-- | Adds error handlers for a particular function and argument. If
348-- names are ambiguous, all matching handlers are updated.
349addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
350addFunctionErrorHandlers f arg hs =
352 let oldHandlers = idris_function_errorhandlers i
353 let newHandlers = flip (addDef f) oldHandlers $
354 case lookupCtxtExact f oldHandlers of
355 Nothing -> M.singleton arg (S.fromList hs)
356 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
357 -- will always be one of those two, thus no extra case
358 putIState $ i { idris_function_errorhandlers = newHandlers }
360getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
361getFunctionErrorHandlers f arg = do i <- getIState
362 return . maybe [] S.toList $
363 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
366-- | Trace all the names in a call graph starting at the given name
367getAllNames :: Name -> Idris [Name]
368getAllNames n = do i <- getIState
369 case getCGAllNames i n of
371 Nothing -> do ns <- allNames [] n
375getCGAllNames :: IState -> Name -> Maybe [Name]
376getCGAllNames i n = case lookupCtxtExact n (idris_callgraph i) of
377 Just ci -> allCalls ci
380addCGAllNames :: IState -> Name -> [Name] -> Idris ()
382 = case lookupCtxtExact n (idris_callgraph i) of
383 Just ci -> addToCG n (ci { allCalls = Just ns })
384 _ -> addToCG n (CGInfo [] (Just ns) [] [])
386allNames :: [Name] -> Name -> Idris [Name]
387allNames ns n | n `elem` ns = return []
388allNames ns n = do i <- getIState
389 case getCGAllNames i n of
391 Nothing -> case lookupCtxtExact n (idris_callgraph i) of
393 do more <- mapM (allNames (n:ns)) (calls ci)
394 let ns' = nub (n : concat more)
395 addCGAllNames i n ns'
399addCoercion :: Name -> Idris ()
400addCoercion n = do i <- getIState
401 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
403addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
406 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
408addNameHint :: Name -> Name -> Idris ()
411 ty' <- case lookupCtxtName ty (idris_implicits i) of
412 [(tyn, _)] -> return tyn
413 [] -> throwError (NoSuchVariable ty)
414 tyns -> throwError (CantResolveAlts (map fst tyns))
415 let ns' = case lookupCtxt ty' (idris_namehints i) of
418 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
420getNameHints :: IState -> Name -> [Name]
421getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
423 case lookupCtxt n (idris_namehints i) of
427addDeprecated :: Name -> String -> Idris ()
428addDeprecated n reason = do
430 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
432getDeprecated :: Name -> Idris (Maybe String)
435 return $ lookupCtxtExact n (idris_deprecated i)
438addFragile :: Name -> String -> Idris ()
439addFragile n reason = do
441 putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }
443getFragile :: Name -> Idris (Maybe String)
446 return $ lookupCtxtExact n (idris_fragile i)
448push_estack :: Name -> Bool -> Idris ()
451 putIState (i { elab_stack = (n, impl) : elab_stack i })
453pop_estack :: Idris ()
454pop_estack = do i <- getIState
455 putIState (i { elab_stack = ptail (elab_stack i) })
459-- | Add an interface implementation function.
461-- Precondition: the implementation should have the correct type.
463-- Dodgy hack 1: Put integer implementations first in the list so they are
464-- resolved by default.
466-- Dodgy hack 2: put constraint chasers (ParentN) last
467addImplementation :: Bool -- ^ whether the name is an Integer implementation
468 -> Bool -- ^ whether to include the implementation in implementation search
469 -> Name -- ^ the name of the interface
470 -> Name -- ^ the name of the implementation
472addImplementation int res n i
473 = do ist <- getIState
474 case lookupCtxt n (idris_interfaces ist) of
475 [CI a b c d e f g ins fds] ->
476 do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
477 putIState $ ist { idris_interfaces = cs }
478 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
479 putIState $ ist { idris_interfaces = cs }
480 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
481 addI i ins | int = (i, res) : ins
482 | chaser n = ins ++ [(i, res)]
483 | otherwise = insI i ins
484 insI i [] = [(i, res)]
485 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
486 | otherwise = n : insI i ns
488 chaser (SN (ParentN _ _)) = True
489 chaser (NS n _) = chaser n
492-- | Add a privileged implementation - one which implementation search will
493-- happily resolve immediately if it is type correct This is used for
494-- naming parent implementations when defining an implementation with
495-- constraints. Returns the old list, so we can revert easily at the
497addOpenImpl :: [Name] -> Idris [Name]
498addOpenImpl ns = do ist <- getIState
499 ns' <- mapM (checkValid ist) ns
500 let open = idris_openimpls ist
501 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
505 = case lookupCtxtName n (idris_implicits ist) of
506 [(n', _)] -> return n'
507 [] -> throwError (NoSuchVariable n)
508 more -> throwError (CantResolveAlts (map fst more))
510setOpenImpl :: [Name] -> Idris ()
511setOpenImpl ns = do ist <- getIState
512 putIState $ ist { idris_openimpls = ns }
514getOpenImpl :: Idris [Name]
515getOpenImpl = do ist <- getIState
516 return (idris_openimpls ist)
518addInterface :: Name -> InterfaceInfo -> Idris ()
520 = do ist <- getIState
521 let i' = case lookupCtxt n (idris_interfaces ist) of
522 [c] -> c { interface_implementations = interface_implementations i }
524 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
526addRecord :: Name -> RecordInfo -> Idris ()
527addRecord n ri = do ist <- getIState
528 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
530addAutoHint :: Name -> Name -> Idris ()
533 case lookupCtxtExact n (idris_autohints ist) of
535 do let hs = addDef n [hint] (idris_autohints ist)
536 putIState $ ist { idris_autohints = hs }
538 do let hs = addDef n (hint : nhints) (idris_autohints ist)
539 putIState $ ist { idris_autohints = hs }
541getAutoHints :: Name -> Idris [Name]
542getAutoHints n = do ist <- getIState
543 case lookupCtxtExact n (idris_autohints ist) of
547addIBC :: IBCWrite -> Idris ()
550 when (notDef (ibc_write i)) $
551 putIState $ i { ibc_write = ibc : ibc_write i }
552 where notDef [] = True
553 notDef (IBCDef n': is) | n == n' = False
554 notDef (_ : is) = notDef is
555addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
558clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
559 idris_inmodule = S.empty }
561resetNameIdx :: Idris ()
562resetNameIdx = do i <- getIState
563 put (i { idris_nameIdx = (0, emptyContext) })
565-- | Used to preserve sharing of names
566addNameIdx :: Name -> Idris (Int, Name)
567addNameIdx n = do i <- getIState
568 let (i', x) = addNameIdx' i n
572addNameIdx' :: IState -> Name -> (IState, (Int, Name))
574 = let idxs = snd (idris_nameIdx i) in
575 case lookupCtxt n idxs of
577 _ -> let i' = fst (idris_nameIdx i) + 1 in
578 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
580getSymbol :: Name -> Idris Name
581getSymbol n = do i <- getIState
582 case M.lookup n (idris_symbols i) of
584 Nothing -> do let sym' = M.insert n n (idris_symbols i)
585 put (i { idris_symbols = sym' })
588getHdrs :: Codegen -> Idris [String]
589getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
591getImported :: Idris [(FilePath, Bool)]
592getImported = do i <- getIState; return (idris_imported i)
594setErrSpan :: FC -> Idris ()
595setErrSpan x = do i <- getIState;
597 Nothing -> putIState $ i { errSpan = Just x }
601clearErr = do i <- getIState
602 putIState $ i { errSpan = Nothing }
604getSO :: Idris (Maybe String)
605getSO = do i <- getIState
606 return (compiled_so i)
608setSO :: Maybe String -> Idris ()
609setSO s = do i <- getIState
610 putIState (i { compiled_so = s })
612getIState :: Idris IState
615putIState :: IState -> Idris ()
618updateIState :: (IState -> IState) -> Idris ()
619updateIState f = do i <- getIState
622withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
623withContext ctx name dflt action = do
625 case lookupCtxt name (ctx ist) of
629withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
630withContext_ ctx name action = withContext ctx name () action
632-- | A version of liftIO that puts errors into the exception type of
634runIO :: IO a -> Idris a
635runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
636-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
638-- Issue #1738 on the issue tracker.
639-- https://github.com/idris-lang/Idris-dev/issues/1738
642getName = do i <- getIState;
643 let idx = idris_name i;
644 putIState (i { idris_name = idx + 1 })
647-- | InternalApp keeps track of the real function application for
648-- making case splits from, not the application the programmer wrote,
649-- which doesn't have the whole context in any case other than top
651addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
654 -- We canonicalise the path to make "./Test/Module.idr" equal
655 -- to "Test/Module.idr"
656 exists <- runIO $ doesFileExist fp
658 do fp' <- runIO $ canonicalizePath fp
659 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
661getInternalApp :: FilePath -> Int -> Idris PTerm
662getInternalApp fp l = do i <- getIState
663 -- We canonicalise the path to make
664 -- "./Test/Module.idr" equal to
666 exists <- runIO $ doesFileExist fp
668 then do fp' <- runIO $ canonicalizePath fp
669 case lookup (fp', l) (idris_lineapps i) of
671 Nothing -> return Placeholder
672 -- TODO: What if it's not there?
673 else return Placeholder
675-- | Pattern definitions are only used for coverage checking, so erase
676-- them when we're done
677clearOrigPats :: Idris ()
678clearOrigPats = do i <- get
679 let ps = idris_patdefs i
680 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
681 put (i { idris_patdefs = ps' })
683-- | Erase types from Ps in the context (basically ending up with
684-- what's in the .ibc, which is all we need after all the analysis is
686clearPTypes :: Idris ()
687clearPTypes = do i <- get
689 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
690 where pErase (CaseOp c t tys orig tot cds)
691 = CaseOp c t tys orig [] (pErase' cds)
693 pErase' (CaseDefs (cs, c) rs)
694 = let c' = (cs, fmap pEraseType c) in
697checkUndefined :: FC -> Name -> Idris ()
701 (_:_) -> throwError . Msg $ show fc ++ ":" ++
702 show n ++ " already defined"
705isUndefined :: FC -> Name -> Idris Bool
708 case lookupTyExact n i of
709 Just _ -> return False
712setContext :: Context -> Idris ()
713setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )
715updateContext :: (Context -> Context) -> Idris ()
716updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )
718addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
719addConstraints fc (v, cs)
720 = do tit <- typeInType
724 let ctxt' = ctxt { next_tvar = v }
725 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
726 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
729 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
730 insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
731 insertAll ((c, fc) : cs) ics
732 = insertAll cs $ S.insert (ConstraintFC c fc) ics
734addDeferred = addDeferred' Ref
735addDeferredTyCon = addDeferred' (TCon 0 0)
737-- | Save information about a name that is not yet defined
738addDeferred' :: NameType
739 -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
740 -- ^ The Name is the name being made into a metavar,
741 -- the Int is the number of vars that are part of a
742 -- putative proof context, the Maybe Name is the
743 -- top-level function containing the new metavariable,
744 -- the Type is its type, and the Bool is whether :p is
748 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
749 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
751 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
752 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
755 -- 'tidyNames' is to generate user accessible names in case they are
756 -- needed in tactic scripts
757 tidyNames used (Bind (MN i x) b sc)
758 = let n' = uniqueNameSet (UN x) used in
759 Bind n' b $ tidyNames (S.insert n' used) sc
760 tidyNames used (Bind n b sc)
761 = let n' = uniqueNameSet n used in
762 Bind n' b $ tidyNames (S.insert n' used) sc
765solveDeferred :: FC -> Name -> Idris ()
768 case lookup n (idris_metavars i) of
769 Just (_, _, _, _, False) ->
770 throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
771 _ -> putIState $ i { idris_metavars =
772 filter (\(n', _) -> n/=n')
775 filter (notMV n) (ibc_write i)
777 where notMV n (IBCMetavar n') = not (n == n')
780getUndefined :: Idris [Name]
781getUndefined = do i <- getIState
782 return (map fst (idris_metavars i) \\ primDefs)
784isMetavarName :: Name -> IState -> Bool
786 = case lookupNames n (tt_ctxt ist) of
787 (t:_) -> isJust $ lookup t (idris_metavars ist)
790getWidth :: Idris ConsoleWidth
791getWidth = fmap idris_consolewidth getIState
793setWidth :: ConsoleWidth -> Idris ()
794setWidth w = do ist <- getIState
795 put ist { idris_consolewidth = w }
797setDepth :: Maybe Int -> Idris ()
798setDepth d = do ist <- getIState
799 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
801typeDescription :: String
802typeDescription = "The type of types"
805type1Doc :: Doc OutputAnnotation
806type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
809isetPrompt :: String -> Idris ()
810isetPrompt p = do i <- getIState
811 case idris_outputmode i of
812 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
814-- | Tell clients how much was parsed and loaded
815isetLoadedRegion :: Idris ()
816isetLoadedRegion = do i <- getIState
817 let span = idris_parsedSpan i
820 case idris_outputmode i of
822 runIO . hPutStrLn h $
823 convSExp "set-loaded-region" fc n
826setLogLevel :: Int -> Idris ()
827setLogLevel l = do i <- getIState
828 let opts = idris_options i
829 let opt' = opts { opt_logLevel = l }
830 putIState $ i { idris_options = opt' }
832setLogCats :: [LogCat] -> Idris ()
835 let opts = idris_options i
836 let opt' = opts { opt_logcats = cs }
837 putIState $ i { idris_options = opt' }
839setCmdLine :: [Opt] -> Idris ()
840setCmdLine opts = do i <- getIState
841 let iopts = idris_options i
842 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
844getCmdLine :: Idris [Opt]
845getCmdLine = do i <- getIState
846 return (opt_cmdline (idris_options i))
848getDumpHighlighting :: Idris Bool
849getDumpHighlighting = do ist <- getIState
850 return (findC (opt_cmdline (idris_options ist)))
851 where findC = elem DumpHighlights
853getDumpDefun :: Idris (Maybe FilePath)
854getDumpDefun = do i <- getIState
855 return $ findC (opt_cmdline (idris_options i))
856 where findC [] = Nothing
857 findC (DumpDefun x : _) = Just x
858 findC (_ : xs) = findC xs
860getDumpCases :: Idris (Maybe FilePath)
861getDumpCases = do i <- getIState
862 return $ findC (opt_cmdline (idris_options i))
863 where findC [] = Nothing
864 findC (DumpCases x : _) = Just x
865 findC (_ : xs) = findC xs
868logLevel = do i <- getIState
869 return (opt_logLevel (idris_options i))
871setAutoImpls :: Bool -> Idris ()
872setAutoImpls b = do i <- getIState
873 let opts = idris_options i
874 let opt' = opts { opt_autoimpls = b }
875 putIState $ i { idris_options = opt' }
877getAutoImpls :: Idris Bool
878getAutoImpls = do i <- getIState
879 return (opt_autoimpls (idris_options i))
881setErrContext :: Bool -> Idris ()
882setErrContext t = do i <- getIState
883 let opts = idris_options i
884 let opts' = opts { opt_errContext = t }
885 putIState $ i { idris_options = opts' }
887errContext :: Idris Bool
888errContext = do i <- getIState
889 return (opt_errContext (idris_options i))
891getOptimise :: Idris [Optimisation]
892getOptimise = do i <- getIState
893 return (opt_optimise (idris_options i))
895setOptimise :: [Optimisation] -> Idris ()
896setOptimise newopts = do i <- getIState
897 let opts = idris_options i
898 let opts' = opts { opt_optimise = newopts }
899 putIState $ i { idris_options = opts' }
901addOptimise :: Optimisation -> Idris ()
902addOptimise opt = do opts <- getOptimise
903 setOptimise (nub (opt : opts))
905removeOptimise :: Optimisation -> Idris ()
906removeOptimise opt = do opts <- getOptimise
907 setOptimise ((nub opts) \\ [opt])
909-- | Set appropriate optimisation set for the given level. We only
910-- have one optimisation that is configurable at the moment, however!
911setOptLevel :: Int -> Idris ()
912setOptLevel n | n <= 0 = setOptimise []
913setOptLevel 1 = setOptimise []
914setOptLevel 2 = setOptimise [PETransform]
915setOptLevel n | n >= 3 = setOptimise [PETransform]
918useREPL = do i <- getIState
919 return (opt_repl (idris_options i))
921setREPL :: Bool -> Idris ()
922setREPL t = do i <- getIState
923 let opts = idris_options i
924 let opt' = opts { opt_repl = t }
925 putIState $ i { idris_options = opt' }
927showOrigErr :: Idris Bool
928showOrigErr = do i <- getIState
929 return (opt_origerr (idris_options i))
931setShowOrigErr :: Bool -> Idris ()
932setShowOrigErr b = do i <- getIState
933 let opts = idris_options i
934 let opt' = opts { opt_origerr = b }
935 putIState $ i { idris_options = opt' }
937setAutoSolve :: Bool -> Idris ()
938setAutoSolve b = do i <- getIState
939 let opts = idris_options i
940 let opt' = opts { opt_autoSolve = b }
941 putIState $ i { idris_options = opt' }
943setNoBanner :: Bool -> Idris ()
944setNoBanner n = do i <- getIState
945 let opts = idris_options i
946 let opt' = opts { opt_nobanner = n }
947 putIState $ i { idris_options = opt' }
949getNoBanner :: Idris Bool
950getNoBanner = do i <- getIState
951 let opts = idris_options i
952 return (opt_nobanner opts)
954setEvalTypes :: Bool -> Idris ()
955setEvalTypes n = do i <- getIState
956 let opts = idris_options i
957 let opt' = opts { opt_evaltypes = n }
958 putIState $ i { idris_options = opt' }
960getDesugarNats :: Idris Bool
961getDesugarNats = do i <- getIState
962 let opts = idris_options i
963 return (opt_desugarnats opts)
966setDesugarNats :: Bool -> Idris ()
967setDesugarNats n = do i <- getIState
968 let opts = idris_options i
969 let opt' = opts { opt_desugarnats = n }
970 putIState $ i { idris_options = opt' }
972setQuiet :: Bool -> Idris ()
973setQuiet q = do i <- getIState
974 let opts = idris_options i
975 let opt' = opts { opt_quiet = q }
976 putIState $ i { idris_options = opt' }
978getQuiet :: Idris Bool
979getQuiet = do i <- getIState
980 let opts = idris_options i
981 return (opt_quiet opts)
983setCodegen :: Codegen -> Idris ()
984setCodegen t = do i <- getIState
985 let opts = idris_options i
986 let opt' = opts { opt_codegen = t }
987 putIState $ i { idris_options = opt' }
989codegen :: Idris Codegen
990codegen = do i <- getIState
991 return (opt_codegen (idris_options i))
994setOutputTy :: OutputType -> Idris ()
995setOutputTy t = do i <- getIState
996 let opts = idris_options i
997 let opt' = opts { opt_outputTy = t }
998 putIState $ i { idris_options = opt' }
1000outputTy :: Idris OutputType
1001outputTy = do i <- getIState
1002 return $ opt_outputTy $ idris_options i
1004setIdeMode :: Bool -> Handle -> Idris ()
1005setIdeMode True h = do i <- getIState
1006 putIState $ i { idris_outputmode = IdeMode 0 h
1007 , idris_colourRepl = False
1009setIdeMode False _ = return ()
1011setTargetTriple :: String -> Idris ()
1012setTargetTriple t = do i <- getIState
1013 let opts = idris_options i
1014 opt' = opts { opt_triple = t }
1015 putIState $ i { idris_options = opt' }
1017targetTriple :: Idris String
1018targetTriple = do i <- getIState
1019 return (opt_triple (idris_options i))
1021setTargetCPU :: String -> Idris ()
1022setTargetCPU t = do i <- getIState
1023 let opts = idris_options i
1024 opt' = opts { opt_cpu = t }
1025 putIState $ i { idris_options = opt' }
1027targetCPU :: Idris String
1028targetCPU = do i <- getIState
1029 return (opt_cpu (idris_options i))
1031verbose :: Idris Bool
1032verbose = do i <- getIState
1033 -- Quietness overrides verbosity
1034 return (not (opt_quiet (idris_options i)) &&
1035 opt_verbose (idris_options i))
1037setVerbose :: Bool -> Idris ()
1038setVerbose t = do i <- getIState
1039 let opts = idris_options i
1040 let opt' = opts { opt_verbose = t }
1041 putIState $ i { idris_options = opt' }
1043typeInType :: Idris Bool
1044typeInType = do i <- getIState
1045 return (opt_typeintype (idris_options i))
1047setTypeInType :: Bool -> Idris ()
1048setTypeInType t = do i <- getIState
1049 let opts = idris_options i
1050 let opt' = opts { opt_typeintype = t }
1051 putIState $ i { idris_options = opt' }
1053coverage :: Idris Bool
1054coverage = do i <- getIState
1055 return (opt_coverage (idris_options i))
1057setCoverage :: Bool -> Idris ()
1058setCoverage t = do i <- getIState
1059 let opts = idris_options i
1060 let opt' = opts { opt_coverage = t }
1061 putIState $ i { idris_options = opt' }
1063setIBCSubDir :: FilePath -> Idris ()
1064setIBCSubDir fp = do i <- getIState
1065 let opts = idris_options i
1066 let opt' = opts { opt_ibcsubdir = fp }
1067 putIState $ i { idris_options = opt' }
1069valIBCSubDir :: IState -> Idris FilePath
1070valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
1072addImportDir :: FilePath -> Idris ()
1073addImportDir fp = do i <- getIState
1074 let opts = idris_options i
1075 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
1076 putIState $ i { idris_options = opt' }
1078setImportDirs :: [FilePath] -> Idris ()
1079setImportDirs fps = do i <- getIState
1080 let opts = idris_options i
1081 let opt' = opts { opt_importdirs = fps }
1082 putIState $ i { idris_options = opt' }
1084allImportDirs :: Idris [FilePath]
1085allImportDirs = do i <- getIState
1086 let optdirs = opt_importdirs (idris_options i)
1087 return ("." : reverse optdirs)
1089addSourceDir :: FilePath -> Idris ()
1090addSourceDir fp = do i <- getIState
1091 let opts = idris_options i
1092 let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts }
1093 putIState $ i { idris_options = opts' }
1095setSourceDirs :: [FilePath] -> Idris ()
1096setSourceDirs fps = do i <- getIState
1097 let opts = idris_options i
1098 let opts' = opts { opt_sourcedirs = nub $ fps }
1099 putIState $ i { idris_options = opts' }
1101allSourceDirs :: Idris [FilePath]
1102allSourceDirs = do i <- getIState
1103 let optdirs = opt_sourcedirs (idris_options i)
1104 return ("." : reverse optdirs)
1106colourise :: Idris Bool
1107colourise = do i <- getIState
1108 return $ idris_colourRepl i
1110setColourise :: Bool -> Idris ()
1111setColourise b = do i <- getIState
1112 putIState $ i { idris_colourRepl = b }
1114impShow :: Idris Bool
1115impShow = do i <- getIState
1116 return (opt_showimp (idris_options i))
1118setImpShow :: Bool -> Idris ()
1119setImpShow t = do i <- getIState
1120 let opts = idris_options i
1121 let opt' = opts { opt_showimp = t }
1122 putIState $ i { idris_options = opt' }
1124setColour :: ColourType -> IdrisColour -> Idris ()
1125setColour ct c = do i <- getIState
1126 let newTheme = setColour' ct c (idris_colourTheme i)
1127 putIState $ i { idris_colourTheme = newTheme }
1128 where setColour' KeywordColour c t = t { keywordColour = c }
1129 setColour' BoundVarColour c t = t { boundVarColour = c }
1130 setColour' ImplicitColour c t = t { implicitColour = c }
1131 setColour' FunctionColour c t = t { functionColour = c }
1132 setColour' TypeColour c t = t { typeColour = c }
1133 setColour' DataColour c t = t { dataColour = c }
1134 setColour' PromptColour c t = t { promptColour = c }
1135 setColour' PostulateColour c t = t { postulateColour = c }
1138logLvl :: Int -> String -> Idris ()
1139logLvl = logLvlCats []
1141logCoverage :: Int -> String -> Idris ()
1142logCoverage = logLvlCats [ICoverage]
1144logErasure :: Int -> String -> Idris ()
1145logErasure = logLvlCats [IErasure]
1147-- | Log an action of the parser
1148logParser :: Int -> String -> Idris ()
1149logParser = logLvlCats parserCats
1151-- | Log an action of the elaborator.
1152logElab :: Int -> String -> Idris ()
1153logElab = logLvlCats elabCats
1155-- | Log an action of the compiler.
1156logCodeGen :: Int -> String -> Idris ()
1157logCodeGen = logLvlCats codegenCats
1159logIBC :: Int -> String -> Idris ()
1160logIBC = logLvlCats [IIBC]
1162-- | Log aspect of Idris execution
1164-- An empty set of logging levels is used to denote all categories.
1166-- @TODO update IDE protocol
1167logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1168 -> Int -- ^ The Logging level the message should appear.
1169 -> String -- ^ The message to show the developer.
1171logLvlCats cs l str = do
1173 let lvl = opt_logLevel (idris_options i)
1174 let cats = opt_logcats (idris_options i)
1176 when (inCat cs cats || null cats) $
1177 case idris_outputmode i of
1179 runIO $ hPutStrLn h str
1181 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1182 runIO . hPutStrLn h $ convSExp "log" good n
1184 inCat :: [LogCat] -> [LogCat] -> Bool
1185 inCat cs cats = any (`elem` cats) cs
1187cmdOptType :: Opt -> Idris Bool
1188cmdOptType x = do i <- getIState
1189 return $ x `elem` opt_cmdline (idris_options i)
1191noErrors :: Idris Bool
1192noErrors = do i <- getIState
1194 Nothing -> return True
1197setTypeCase :: Bool -> Idris ()
1198setTypeCase t = do i <- getIState
1199 let opts = idris_options i
1200 let opt' = opts { opt_typecase = t }
1201 putIState $ i { idris_options = opt' }
1204-- Dealing with parameters
1206expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1207 [Name] -> -- all names
1208 [Name] -> -- names with no declaration
1210expandParams dec ps ns infs tm = en 0 tm
1212 -- if we shadow a name (say in a lambda binding) that is used in a call to
1213 -- a lifted function, we need access to both names - once in the scope of the
1214 -- binding and once to call the lifted functions. So we'll explicitly shadow
1215 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1216 -- but we didn't...)
1218 mkShadow (UN n) = MN 0 n
1219 mkShadow (MN i n) = MN (i+1) n
1220 mkShadow (NS x s) = NS (mkShadow x) s
1222 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1223 -- that are merely mentioned.
1225 en 0 (PLam fc n nfc t s)
1226 | n `elem` (map fst ps ++ ns)
1227 = let n' = mkShadow n in
1228 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1229 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1230 en 0 (PPi p n nfc t s)
1231 | n `elem` (map fst ps ++ ns)
1232 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1233 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1234 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1235 en 0 (PLet fc n nfc ty v s)
1236 | n `elem` (map fst ps ++ ns)
1237 = let n' = mkShadow n in
1238 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1239 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1240 -- FIXME: Should only do this in a type signature!
1241 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1242 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1243 = let n' = mkShadow n in
1244 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1245 en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
1246 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1247 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1248 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1249 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1250 en 0 (PHidden t) = PHidden (en 0 t)
1251 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1252 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1253 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1254 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1255 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1256 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1258 en 0 (PQuote (Var n))
1259 | n `nselem` ns = PQuote (Var (dec n))
1260 en 0 (PApp fc (PInferRef fc' hl n) as)
1261 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1262 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1263 en 0 (PApp fc (PRef fc' hl n) as)
1264 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1265 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1266 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1267 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1268 en 0 (PAppBind fc (PRef fc' hl n) as)
1269 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1270 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1271 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1272 (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
1274 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1275 (map ((pexp . (PRef fc hl)) . fst) ps)
1276 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1277 (map ((pexp . (PRef fc hl)) . fst) ps)
1278 en 0 (PInferRef fc hl n)
1279 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1280 (map ((pexp . (PRef fc hl)) . fst) ps)
1281 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1282 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1283 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1284 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1285 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1286 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1288 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1289 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1291 en ql t = descend (en ql) t
1294 nselem x (y : xs) | nseq x y = True
1295 | otherwise = nselem x xs
1297 nseq x y = nsroot x == nsroot y
1299 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1300 enTacImp ql other = other
1302expandParamsD :: Bool -> -- True = RHS only
1304 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1305expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1306 = if n `elem` ns && (not rhsonly)
1307 then -- trace (show (n, expandParams dec ps ns ty)) $
1308 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1309 else --trace (show (n, expandParams dec ps ns ty)) $
1310 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1311expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1312 = if n `elem` ns && (not rhsonly)
1313 then -- trace (show (n, expandParams dec ps ns ty)) $
1314 PPostulate e doc syn fc nfc o (dec n)
1315 (piBind ps (expandParams dec ps ns [] ty))
1316 else --trace (show (n, expandParams dec ps ns ty)) $
1317 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1318expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1319 = let n' = if n `elem` ns then dec n else n in
1320 PClauses fc opts n' (map expandParamsC cs)
1322 expandParamsC (PClause fc n lhs ws rhs ds)
1323 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1324 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1325 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1326 n' = if n `elem` ns then dec n else n
1327 -- names bound on the lhs should not be expanded on the rhs
1328 ns' = removeBound lhs ns in
1330 (map (expandParams dec ps'' ns' []) ws)
1331 (expandParams dec ps'' ns' [] rhs)
1332 (map (expandParamsD True ist dec ps'' ns') ds)
1333 expandParamsC (PWith fc n lhs ws wval pn ds)
1334 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1335 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1336 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1337 n' = if n `elem` ns then dec n else n
1338 ns' = removeBound lhs ns in
1340 (map (expandParams dec ps'' ns' []) ws)
1341 (expandParams dec ps'' ns' [] wval)
1343 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1344 updateps yn nm [] = []
1345 updateps yn nm (((a, t), i):as)
1346 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1347 | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
1349 removeBound lhs ns = ns \\ nub (bnames lhs)
1351 bnames (PRef _ _ n) = [n]
1352 bnames (PApp _ _ args) = concatMap (bnames . getTm) args
1353 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1354 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1357-- | Expands parameters defined in parameter and where blocks inside of declarations
1358expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1359 = PData doc argDocs syn fc co (expandPData pd)
1361 -- just do the type decl, leave constructors alone (parameters will be
1362 -- added implicitly)
1363 expandPData (PDatadecl n nfc ty cons)
1365 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1367 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1368 econ (doc, argDocs, n, nfc, t, fc, fs)
1369 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1370expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1372expandParamsD rhs ist dec ps ns (PParams f params pds)
1373 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1374 (map (expandParamsD True ist dec ps ns) pds)
1375-- (map (expandParamsD ist dec ps ns) pds)
1376expandParamsD rhs ist dec ps ns (PMutual f pds)
1377 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1378expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
1379 = PInterface doc info f
1380 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1382 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1385 (map (expandParamsD rhs ist dec ps ns) decls)
1388expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1389 = let cn' = case cn of
1390 Just n -> if n `elem` ns then Just (dec n) else Just n
1391 Nothing -> Nothing in
1392 PImplementation doc argDocs info f
1393 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1396 (map (expandParams dec ps ns []) params)
1397 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
1398 (expandParams dec ps ns [] ty)
1400 (map (expandParamsD True ist dec ps ns) decls)
1401expandParamsD rhs ist dec ps ns d = d
1403mapsnd f (x, t) = (x, f t)
1405expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
1406 = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
1408expandImplementationScope ist dec ps ns d = d
1410-- | Calculate a priority for a type, for deciding elaboration order
1411-- * if it's just a type variable or concrete type, do it early (0)
1412-- * if there's only type variables and injective constructors, do it next (1)
1413-- * if there's a function type, next (2)
1414-- * finally, everything else (3)
1415getPriority :: IState -> PTerm -> Int
1416getPriority i tm = 1 -- pri tm
1419 case lookupP n (tt_ctxt i) of
1420 ((P (DCon _ _ _) _ _):_) -> 1
1421 ((P (TCon _ _) _ _):_) -> 1
1422 ((P Ref _ _):_) -> 1
1423 [] -> 0 -- must be locally bound, if it's not an error...
1424 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1426 pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
1427 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1428 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
1429 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
1430 pri (PTyped l r) = pri l
1431 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1432 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1433 pri (PAlternative _ a as) = maximum (map pri as)
1434 pri (PConstant _ _) = 0
1439addStatics :: Name -> Term -> PTerm -> Idris ()
1440addStatics n tm ptm =
1441 do let (statics, dynamics) = initStatics tm ptm
1444 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1445 Just p -> getNamesFrom 0 (fn_params p) tm ++
1446 concatMap (getParamNames ist . snd) statics
1447 _ -> concatMap (getParamNames ist . snd) statics
1449 let stnames = nub $ concatMap (freeArgNames . snd) statics
1450 let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
1452 -- also get the arguments which are 'uniquely inferrable' from
1453 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1454 -- or parameters to the type of a static
1455 let statics' = nub $ map fst statics ++
1456 filter (\x -> not (elem x dnames)) stnames
1457 let stpos = staticList statics' tm
1459 unless (null statics) $
1460 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1461 ++ showTmImpls ptm ++ "\n"
1462 ++ show statics ++ "\n" ++ show dynamics
1463 ++ "\n" ++ show paramnames
1464 ++ "\n" ++ show stpos
1465 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1466 addIBC (IBCStatic n)
1468 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1469 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1470 (static, (n, ty) : dynamic)
1471 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1472 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1473 if pstatic p == Static then ((n, ty) : static, dynamic)
1474 else if (not (searchArg p))
1475 then (static, (n, ty) : dynamic)
1476 else (static, dynamic)
1477 initStatics t pt = ([], [])
1479 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1480 = case lookupCtxtExact n (idris_datatypes ist) of
1481 Just ti -> getNamePos 0 (param_pos ti) args
1483 where getNamePos i ps [] = []
1484 getNamePos i ps (P _ n _ : as)
1485 | i `elem` ps = n : getNamePos (i + 1) ps as
1486 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1487 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1488 = n : getParamNames ist sc
1489 getParamNames ist _ = []
1491 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1492 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1493 | otherwise = getNamesFrom (i + 1) ps sc
1494 getNamesFrom i ps sc = []
1496 freeArgNames (Bind n (Pi _ ty _) sc)
1497 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1498 freeArgNames tm = let (_, args) = unApply tm in
1499 concatMap freeNames args
1501 -- if a name appears in an interface or tactic implicit index, it doesn't
1502 -- affect its 'uniquely inferrable' from a static status since these are
1503 -- resolved by searching.
1504 searchArg (Constraint _ _) = True
1505 searchArg (TacImp _ _ _) = True
1508 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1511-- Dealing with implicit arguments
1513-- Add some bound implicits to the using block if they aren't there already
1515addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1516addToUsing us [] = us
1517addToUsing us ((n, t) : ns)
1518 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1519 | otherwise = addToUsing us ns
1520 where impName (UImplicit n _) = Just n
1523-- Add constraint bindings from using block
1525addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1526addUsingConstraints syn fc t
1528 let ns = namesIn [] ist t
1529 let cs = getConstraints t -- check declared constraints
1530 let addconsts = uconsts \\ cs
1531 return (doAdd addconsts ns t)
1532 where uconsts = filter uconst (using syn)
1533 uconst (UConstraint _ _) = True
1537 -- if all of args in ns, then add it
1538 doAdd (UConstraint c args : cs) ns t
1539 | all (\n -> elem n ns) args
1540 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1541 (mkConst c args) (doAdd cs ns t)
1542 | otherwise = doAdd cs ns t
1544 mkConst c args = PApp fc (PRef fc [] c)
1545 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1547 getConstraints (PPi (Constraint _ _) _ _ c sc)
1548 = getcapp c ++ getConstraints sc
1549 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1550 getConstraints _ = []
1552 getcapp (PApp _ (PRef _ _ c) args)
1553 = do ns <- mapM getName args
1554 return (UConstraint c ns)
1557 getName (PExp _ _ _ (PRef _ _ n)) = return n
1560-- | Add implicit bindings from using block, and bind any missing names
1561addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1562addUsingImpls syn n fc t
1563 = do ist <- getIState
1564 autoimpl <- getAutoImpls
1565 let ns_in = implicitNamesIn (map iname uimpls) ist t
1566 let ns = if autoimpl then ns_in
1567 else filter (\n -> n `elem` (map iname uimpls)) ns_in
1569 let badnames = filter (\n -> not (implicitable n) &&
1570 n `notElem` (map iname uimpls)) ns
1571 unless (null badnames) $
1572 throwError (At fc (Elaborating "type of " n Nothing
1573 (NoSuchVariable (head badnames))))
1574 let cs = getArgnames t -- get already bound names
1575 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1576 -- if all names in the arguments of addconsts appear in ns,
1577 -- add the constraint implicitly
1578 return (bindFree ns (doAdd addimpls ns t))
1579 where uimpls = filter uimpl (using syn)
1580 uimpl (UImplicit _ _) = True
1583 iname (UImplicit n _) = n
1584 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1587 -- if all of args in ns, then add it
1588 doAdd (UImplicit n ty : cs) ns t
1590 = PPi impl_gen n NoFC ty (doAdd cs ns t)
1591 | otherwise = doAdd cs ns t
1593 -- bind the free names which weren't in the using block
1596 | elem n (map iname uimpls) = bindFree ns tm
1598 = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)
1600 getArgnames (PPi _ n _ c sc)
1601 = n : getArgnames sc
1604-- Given the original type and the elaborated type, return the implicitness
1605-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1607getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1608getUnboundImplicits i t tm = getImps t (collectImps tm)
1609 where collectImps (PPi p n _ t sc)
1610 = (n, (p, t)) : collectImps sc
1613 scopedimpl (Just i) = not (toplevel_imp i)
1614 scopedimpl _ = False
1616 getImps (Bind n (Pi i _ _) sc) imps
1617 | scopedimpl i = getImps sc imps
1618 getImps (Bind n (Pi _ t _) sc) imps
1619 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1621 argInfo n (Imp opt _ _ _ _) Placeholder
1622 = (True, PImp 0 True opt n Placeholder)
1623 argInfo n (Imp opt _ _ _ _) t'
1624 = (False, PImp (getPriority i t') True opt n t')
1625 argInfo n (Exp opt _ _) t'
1626 = (InaccessibleArg `elem` opt,
1627 PExp (getPriority i t') opt n t')
1628 argInfo n (Constraint opt _) t'
1629 = (InaccessibleArg `elem` opt,
1630 PConstraint 10 opt n t')
1631 argInfo n (TacImp opt _ scr) t'
1632 = (InaccessibleArg `elem` opt,
1633 PTacImplicit 10 opt n scr t')
1634 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1635 where impBind n t = (True, PImp 1 True [] n Placeholder)
1638-- Add implicit Pi bindings for any names in the term which appear in an
1639-- argument position.
1641-- This has become a right mess already. Better redo it some time...
1642-- TODO: This is obsoleted by the new way of elaborating types, (which
1643-- calls addUsingImpls) but there's still a couple of places which use
1644-- it. Clean them up!
1646-- Issue 1739 in the issue tracker
1647-- https://github.com/idris-lang/Idris-dev/issues/1739
1648implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1649implicit info syn n ptm = implicit' info syn [] n ptm
1651implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1652implicit' info syn ignore n ptm
1654 auto <- getAutoImpls
1655 let (tm', impdata) = implicitise auto syn ignore i ptm
1656 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1657-- let (tm'', spos) = findStatics i tm'
1658 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1660 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1662-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1665 -- Detect unknown names in default arguments and throw error if found.
1666 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1667 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1669 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1670 notFoundInDefault kns (PTacImplicit _ _ n script _)
1672 case notFound kns (namesIn [] i script) of
1673 Nothing -> return (n:kns)
1674 Just name -> throwError (NoSuchVariable name)
1675 notFoundInDefault kns p = return ((pname p):kns)
1677 notFound :: [Name] -> [Name] -> Maybe Name
1678 notFound kns [] = Nothing
1679 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1680 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1682-- | Even if auto_implicits is off, we need to call this so we record
1683-- which arguments are implicit
1684implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1685implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1686 let (declimps, ns') = execState (imps True [] tm) ([], [])
1687 ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
1688 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1689 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1691 then (tm, reverse declimps)
1692 else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
1694 uvars = map ipair (filter uimplicit (using syn))
1695 pvars = syn_params syn
1697 inUsing n = n `elem` map fst uvars
1699 ipair (UImplicit x y) = (x, y)
1700 uimplicit (UImplicit _ _) = True
1703 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1704 | otherwise = x : dropAll xs ys
1707 -- Find names in argument position in a type, suitable for implicit
1709 -- Not the function position, but do everything else...
1710 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
1711 implNamesIn uv t = implicitNamesIn (map fst uv) ist t
1713 imps top env ty@(PApp _ f as)
1714 = do (decls, ns) <- get
1715 let isn = nub (implNamesIn uvars ty)
1716 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1717 imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
1718 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1720 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1721 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1722 imps True (n:env) sc
1723 imps top env (PPi (Exp l _ _) n _ ty sc)
1724 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1725 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1727 (decls, ns) <- get -- ignore decls in HO types
1728 put (PExp (getPriority ist ty) l n Placeholder : decls,
1729 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1730 imps True (n:env) sc
1731 imps top env (PPi (Constraint l _) n _ ty sc)
1732 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1733 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1735 (decls, ns) <- get -- ignore decls in HO types
1736 put (PConstraint 10 l n Placeholder : decls,
1737 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1738 imps True (n:env) sc
1739 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1740 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1741 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1743 (decls, ns) <- get -- ignore decls in HO types
1744 put (PTacImplicit 10 l n scr Placeholder : decls,
1745 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1746 imps True (n:env) sc
1747 imps top env (PRewrite _ _ l r _)
1748 = do (decls, ns) <- get
1749 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1750 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1751 imps top env (PTyped l r)
1753 imps top env (PPair _ _ _ l r)
1754 = do (decls, ns) <- get
1755 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1756 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1757 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1758 = do (decls, ns) <- get
1759 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1760 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1761 imps top env (PDPair _ _ _ l t r)
1762 = do (decls, ns) <- get
1763 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1765 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1766 imps top env (PAlternative ms a as)
1767 = do (decls, ns) <- get
1768 let isn = concatMap (namesIn uvars ist) as
1769 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1770 imps top env (PLam fc n _ ty sc)
1771 = do imps False env ty
1772 imps False (n:env) sc
1773 imps top env (PHidden tm) = imps False env tm
1774 imps top env (PUnifyLog tm) = imps False env tm
1775 imps top env (PNoImplicits tm) = imps False env tm
1776 imps top env (PRunElab fc tm ns) = imps False env tm
1777 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1778 imps top env _ = return ()
1780 pibind using [] sc = sc
1781 pibind using (n:ns) sc
1782 = case lookup n using of
1783 Just ty -> PPi impl_gen
1784 n NoFC ty (pibind using ns sc)
1785 Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
1786 n NoFC Placeholder (pibind using ns sc)
1788-- | Add implicit arguments in function calls
1789addImplPat :: IState -> PTerm -> PTerm
1790addImplPat = addImpl' True [] [] []
1792addImplBound :: IState -> [Name] -> PTerm -> PTerm
1793addImplBound ist ns = addImpl' False ns [] [] ist
1795addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1796addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1798-- | Add the implicit arguments to applications in the term [Name]
1799-- gives the names to always expend, even when under a binder of that
1800-- name (this is to expand methods with implicit arguments in
1801-- dependent interfaces).
1802addImpl :: [Name] -> IState -> PTerm -> PTerm
1803addImpl = addImpl' False [] []
1805-- TODO: in patterns, don't add implicits to function names guarded by constructors
1806-- and *not* inside a PHidden
1808addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1809addImpl' inpat env infns imp_meths ist ptm
1810 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
1812 topname = case ptm of
1814 PApp _ (PRef _ _ n) _ -> n
1815 _ -> sUN "" -- doesn't matter then
1817 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1818 ai inpat qq env ds (PRef fc fcs f)
1819 | f `elem` infns = PInferRef fc fcs f
1820 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1821 ai inpat qq env ds (PHidden (PRef fc hl f))
1822 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1823 ai inpat qq env ds (PRewrite fc by l r g)
1824 = let l' = ai inpat qq env ds l
1825 r' = ai inpat qq env ds r
1826 g' = fmap (ai inpat qq env ds) g in
1827 PRewrite fc by l' r' g'
1828 ai inpat qq env ds (PTyped l r)
1829 = let l' = ai inpat qq env ds l
1830 r' = ai inpat qq env ds r in
1832 ai inpat qq env ds (PPair fc hls p l r)
1833 = let l' = ai inpat qq env ds l
1834 r' = ai inpat qq env ds r in
1835 PPair fc hls p l' r'
1836 ai inpat qq env ds (PDPair fc hls p l t r)
1837 = let l' = ai inpat qq env ds l
1838 t' = ai inpat qq env ds t
1839 r' = ai inpat qq env ds r in
1840 PDPair fc hls p l' t' r'
1841 ai inpat qq env ds (PAlternative ms a as)
1842 = let as' = map (ai inpat qq env ds) as in
1843 PAlternative ms a as'
1844 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1845 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1846 = let as' = map (fmap (ai inpat qq env ds)) as in
1847 PApp fc (PInferRef ffc hl f) as'
1848 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1849 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1850 | not (f `elem` map fst env)
1851 = let as' = map (fmap (ai inpat qq env ds)) as in
1852 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1853 | Just (Just ty) <- lookup f env =
1854 let as' = map (fmap (ai inpat qq env ds)) as
1855 arity = getPArity ty in
1856 mkPApp fc arity ftm as'
1857 ai inpat qq env ds (PApp fc f as)
1858 = let f' = ai inpat qq env ds f
1859 as' = map (fmap (ai inpat qq env ds)) as in
1861 ai inpat qq env ds (PWithApp fc f a)
1862 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1863 ai inpat qq env ds (PCase fc c os)
1864 = let c' = ai inpat qq env ds c in
1865 -- leave lhs alone, because they get lifted into a new pattern match
1866 -- definition which is passed through addImpl again
1867 PCase fc c' (map aiCase os)
1870 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1872 -- Anything beginning with a lower case letter, not applied,
1873 -- and no namespace is a pattern variable
1874 patnames (PApp _ (PRef _ _ f) [])
1875 | implicitable f = [(f, Nothing)]
1876 patnames (PRef _ _ f)
1877 | implicitable f = [(f, Nothing)]
1878 patnames (PApp _ (PRef _ _ _) args)
1879 = concatMap patnames (map getTm args)
1880 patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1881 patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1882 patnames (PAs _ _ t) = patnames t
1883 patnames (PAlternative _ _ ts) = concatMap patnames ts
1887 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1888 (ai inpat qq env ds t)
1889 (ai inpat qq env ds f)
1891 -- If the name in a lambda is an unapplied data constructor name, do this
1892 -- as a 'case' instead because we'll expect to match on it
1893 ai inpat qq env ds (PLam fc n nfc ty sc)
1894 = if canBeDConName n (tt_ctxt ist)
1895 then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1896 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1897 [(PRef fc [] n, sc)]))
1898 else let ty' = ai inpat qq env ds ty
1899 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1900 PLam fc n nfc ty' sc'
1901 ai inpat qq env ds (PLet fc n nfc ty val sc)
1902 = if canBeDConName n (tt_ctxt ist)
1903 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1904 else let ty' = ai inpat qq env ds ty
1905 val' = ai inpat qq env ds val
1906 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1907 PLet fc n nfc ty' val' sc'
1908 ai inpat qq env ds (PPi p n nfc ty sc)
1909 = let ty' = ai inpat qq env ds ty
1910 env' = if n `elem` imp_meths then env
1911 else ((n, Just ty) : env)
1912 sc' = ai inpat qq env' ds sc in
1914 ai inpat qq env ds (PGoal fc r n sc)
1915 = let r' = ai inpat qq env ds r
1916 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1918 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1919 -- Don't do PProof or PTactics since implicits get added when scope is
1920 -- properly known in ElabTerm.runTac
1921 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1922 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1923 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1924 (fmap (ai inpat True env ds) g)
1925 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1926 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1927 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1928 ai inpat qq env ds tm = tm
1930 handleErr (Left err) = PElabError err
1931 handleErr (Right x) = x
1933-- if in a pattern, and there are no arguments, and there's no possible
1934-- names with zero explicit arguments, don't add implicits.
1936aiFn :: Name -> Bool -> Bool -> Bool
1939 -> Name -- ^ function being applied
1941 -> [PArg] -- ^ initial arguments (if in a pattern)
1943aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1944 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1946 = case lookupDef f (tt_ctxt ist) of
1947 [] -> Right $ PPatvar ffc f
1948 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1949 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1950 if (not (vname f) || tcname f
1951 || any (conCaf (tt_ctxt ist)) ialts)
1952-- any constructor alts || any allImp ialts))
1953 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1954 else Right $ PPatvar ffc f
1955 where imp (PExp _ _ _ _) = False
1958 allImp xs = all imp xs
1960 unqualified (NS _ _) = False
1961 unqualified _ = True
1963 constructor (TyDecl (DCon _ _ _) _) = True
1964 constructor _ = False
1966 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1968 vname (UN n) = True -- non qualified
1971aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1972 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1973aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1974 -- This is where namespaces get resolved by adding PAlternative
1975 = do let ns = lookupCtxtName f (idris_implicits ist)
1976 let nh = filter (\(n, _) -> notHidden n) ns
1977 let ns' = case trimAlts ds nh of
1981 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1983 [] -> case metaVar f (map fst (idris_metavars ist)) of
1984 Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1985 Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1987 PAlternative [] (ExactlyOne True) $
1988 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1989 (insertImpl ns as)) alts
1991 -- if the name is in imp_meths, we should actually refer to the bound
1992 -- name rather than the global one after expanding implicits
1993 isImpName f f' | f `elem` imp_meths = f
1996 -- If it's a metavariable name, try to qualify it from the list of
1997 -- unsolved metavariables
1998 metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1999 metaVar f (_ : ns) = metaVar f ns
2000 metaVar f [] = Nothing
2002 trimAlts [] alts = alts
2004 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
2009 notHidden n = case getAccessibility n of
2015 = case lookupDefAccExact n False (tt_ctxt ist) of
2019 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
2020 -> [PArg] -- ^ given arguments
2023 = let (as', badimpls) = partition (impIn ps) as in
2024 map addUnknownImp badimpls ++
2025 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
2027 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
2028 -> [PArg] -- parameters
2029 -> [PArg] -- explicit arguments
2030 -> [PArg] -- implicits given
2032 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
2033 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2034 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
2035 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
2036 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
2037 let rtc = PResolveTC fc in
2038 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
2039 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
2040 case find n imps [] of
2042 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
2044 PImp p True l n Placeholder :
2045 insImpAcc (M.insert n Placeholder pnas) ps given imps
2046 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
2047 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
2048 case find n imps [] of
2050 PTacImplicit p l n sc tm :
2051 insImpAcc (M.insert n tm pnas) ps given imps'
2054 then PTacImplicit p l n sc Placeholder :
2055 insImpAcc (M.insert n Placeholder pnas) ps given imps
2056 else PTacImplicit p l n sc sc :
2057 insImpAcc (M.insert n sc pnas) ps given imps
2058 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
2059 insImpAcc _ _ given imps = given ++ imps
2061 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
2063 find n [] acc = Nothing
2064 find n (PImp _ _ _ n' t : gs) acc
2065 | n == n' = Just (t, reverse acc ++ gs)
2066 find n (PTacImplicit _ _ n' _ t : gs) acc
2067 | n == n' = Just (t, reverse acc ++ gs)
2068 find n (g : gs) acc = find n gs (g : acc)
2070-- | return True if the second argument is an implicit argument which
2071-- is expected in the implicits, or if it's not an implicit
2072impIn :: [PArg] -> PArg -> Bool
2073impIn ps (PExp _ _ _ _) = True
2074impIn ps (PConstraint _ _ _ _) = True
2075impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
2077expArg (PExp _ _ _ _) = True
2078expArg (PConstraint _ _ _ _) = True
2081-- replace non-linear occurrences with _
2083stripLinear :: IState -> PTerm -> PTerm
2084stripLinear i tm = evalState (sl tm) [] where
2085 sl :: PTerm -> State [Name] PTerm
2087 | (_:_) <- lookupTy f (tt_ctxt i)
2088 = return $ PRef fc hl f
2089 | otherwise = do ns <- get
2091 then return $ PHidden (PRef fc hl f) -- Placeholder
2092 else do put (f : ns)
2093 return (PRef fc hl f)
2097 then return $ PHidden (PPatvar fc f) -- Placeholder
2098 else do put (f : ns)
2099 return (PPatvar fc f)
2100 -- Assumption is that variables are all the same in each alternative
2101 sl t@(PAlternative ms b as) = do ns <- get
2103 return (PAlternative ms b as')
2104 where slAlts ns (a : as) = do put ns
2108 slAlts ns [] = return []
2109 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
2110 sl (PDPair fc hls p l t r) = do l' <- sl l
2113 return (PDPair fc hls p l' t' r')
2114 sl (PApp fc fn args) = do fn' <- case fn of
2115 -- Just the args, fn isn't matchable as a var
2116 PRef _ _ _ -> return fn
2118 args' <- mapM slA args
2119 return $ PApp fc fn' args'
2120 where slA (PImp p m l n t) = do t' <- sl t
2121 return $ PImp p m l n t'
2122 slA (PExp p l n t) = do t' <- sl t
2123 return $ PExp p l n t'
2124 slA (PConstraint p l n t)
2126 return $ PConstraint p l n t'
2127 slA (PTacImplicit p l n sc t)
2129 return $ PTacImplicit p l n sc t'
2132-- | Remove functions which aren't applied to anything, which must then
2133-- be resolved by unification. Assume names resolved and alternatives
2134-- filled in (so no ambiguity).
2135stripUnmatchable :: IState -> PTerm -> PTerm
2136stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
2137 su :: PTerm -> PTerm
2138 su tm@(PRef fc hl f)
2139 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
2141 | (TType _ : _) <- lookupTy f (tt_ctxt i),
2142 not (implicitable f)
2144 | (UType _ : _) <- lookupTy f (tt_ctxt i),
2145 not (implicitable f)
2147 su (PApp fc f@(PRef _ _ fn) args)
2148 -- here we use canBeDConName because the impossible pattern
2149 -- check will not necessarily fully resolve constructor names,
2150 -- and these bare names will otherwise get in the way of
2151 -- impossbility checking.
2152 | canBeDConName fn ctxt
2153 = PApp fc f (fmap (fmap su) args)
2155 = PHidden (PApp fc f args)
2156 su (PAlternative ms b alts)
2157 = let alts' = filter (/= Placeholder) (map su alts) in
2158 if null alts' then Placeholder
2159 else PAlternative ms b alts'
2160 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
2161 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
2162 su t@(PLam fc _ _ _ _) = PHidden t
2163 su t@(PPi _ _ _ _ _) = PHidden t
2164 su t@(PConstant _ c) | isTypeConst c = PHidden t
2169stripUnmatchable i tm = tm
2172mkPApp fc a f as = let rest = drop a as in
2173 if a == 0 then appRest fc f rest
2174 else appRest fc (PApp fc f (take a as)) rest
2177 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
2181-- | Find 'static' argument positions
2182-- (the declared ones, plus any names in argument position in the declared
2184-- FIXME: It's possible that this really has to happen after elaboration
2185findStatics :: IState -> PTerm -> (PTerm, [Bool])
2186findStatics ist tm = let (ns, ss) = fs tm
2187 in runState (pos ns ss tm) []
2188 where fs (PPi p n fc t sc)
2189 | Static <- pstatic p
2190 = let (ns, ss) = fs sc in
2191 (namesIn [] ist t : ns, n : ss)
2192 | otherwise = let (ns, ss) = fs sc in
2196 inOne n ns = length (filter id (map (elem n) ns)) == 1
2198 pos ns ss (PPi p n fc t sc)
2199 | elem n ss = do sc' <- pos ns ss sc
2202 return (PPi (p { pstatic = Static }) n fc t sc')
2203 | otherwise = do sc' <- pos ns ss sc
2206 return (PPi p n fc t sc')
2207 pos ns ss t = return t
2209-- for 6.12/7 compatibility
2210data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2212instance Applicative (EitherErr a) where
2216instance Monad (EitherErr a) where
2219 (LeftErr e) >>= k = LeftErr e
2220 RightOK v >>= k = k v
2222toEither (LeftErr e) = Left e
2223toEither (RightOK ho) = Right ho
2225-- | Syntactic match of a against b, returning pair of variables in a
2226-- and what they match. Returns the pair that failed if not a match.
2227matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2228matchClause = matchClause' False
2230matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2231matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2232 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2234 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2237 match' x y = match (fullApp x) (fullApp y)
2238 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2239 | fi == txt "fromInteger" && b == txt "builtins",
2240 PConstant _ (I _) <- getTm x = match (getTm x) x'
2241 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2242 | fi == txt "fromInteger" && b == txt "builtins",
2243 PConstant _ (I _) <- getTm x = match (getTm x) x'
2244 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2245 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2246 match (PApp _ f args) (PApp _ f' args')
2247 | length args == length args'
2248 = do mf <- match' f f'
2249 ms <- zipWithM matchArg args args'
2250 return (mf ++ concat ms)
2251 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2252 match (PPatvar f n) xr = match (PRef f [f] n) xr
2253 match xr (PPatvar f n) = match xr (PRef f [f] n)
2254 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2255 match (PRef _ _ n) tm@(PRef _ _ n')
2256 | n == n' && not names &&
2257 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2258 || tm == Placeholder)
2260 -- if one namespace is missing, drop the other
2261 | n == n' || n == dropNS n' || dropNS n == n' = return []
2262 where dropNS (NS n _) = n
2264 match (PRef _ _ n) tm
2265 | not names && (not (isConName n (tt_ctxt i) ||
2266 isFnName n (tt_ctxt i)) || tm == Placeholder)
2268 match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'
2269 = do ml <- match' l l'
2272 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2275 match (PTyped l r) x = match l x
2276 match x (PTyped l r) = match x l
2277 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2280 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2283 return (ml ++ mt ++ mr)
2284 match (PAlternative _ a as) (PAlternative _ a' as')
2285 = do ms <- zipWithM match' as as'
2287 match a@(PAlternative _ _ as) b
2288 = do let ms = zipWith match' as (repeat b)
2289 case (rights (map toEither ms)) of
2292 match (PCase _ _ _) _ = return [] -- lifted out
2293 match (PMetavar _ _) _ = return [] -- modified
2294 match (PInferRef _ _ _) _ = return [] -- modified
2295 match (PQuote _) _ = return []
2296 match (PProof _) _ = return []
2297 match (PTactics _) _ = return []
2298 match (PResolveTC _) (PResolveTC _) = return []
2299 match (PTrue _ _) (PTrue _ _) = return []
2300 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2303 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2306 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2307 mty <- match' ty ty'
2309 return (mt ++ mty ++ ms)
2310 match (PHidden x) (PHidden y)
2311 | RightOK xs <- match x y = return xs -- to collect variables
2312 | otherwise = return [] -- Otherwise hidden things are unmatchable
2314 | RightOK xs <- match x y = return xs
2315 | otherwise = return []
2317 | RightOK xs <- match x y = return xs
2318 | otherwise = return []
2319 match (PUnifyLog x) y = match' x y
2320 match x (PUnifyLog y) = match' x y
2321 match (PNoImplicits x) y = match' x y
2322 match x (PNoImplicits y) = match' x y
2323 match Placeholder _ = return []
2324 match _ Placeholder = return []
2325 match (PResolveTC _) _ = return []
2326 match a b | a == b = return []
2327 | otherwise = LeftErr (a, b)
2329 checkRpts (RightOK ms) = check ms where
2331 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2334 check (_:xs) = check xs
2336 checkRpts (LeftErr x) = Left x
2338substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2339substMatches ms = substMatchesShadow ms []
2341-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2342-- substMatchesShadow [] shs t = t
2343-- substMatchesShadow ((n,tm):ns) shs t
2344-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2346substMatch :: Name -> PTerm -> PTerm -> PTerm
2347substMatch n = substMatchShadow n []
2349substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2350substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t
2352substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2353substMatchesShadow nmap shs t = sm shs t where
2354 sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm
2355 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2356 sm xs (PPi p x fc t sc)
2358 = let x' = nextName x in
2359 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2360 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2361 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2362 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2363 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2364 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2365 sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)
2367 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2368 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2369 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2370 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2371 sm xs (PHidden x) = PHidden (sm xs x)
2372 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2373 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2374 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2375 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2378 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2381shadow :: Name -> Name -> PTerm -> PTerm
2382shadow n n' t = sm 0 t where
2383 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2384 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2385 | otherwise = PLam fc x xfc (sm 0 t) sc
2386 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2387 | otherwise = PPi p x fc (sm 0 t) sc
2388 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2389 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2390 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2391 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2392 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2393 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2394 sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2395 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2396 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2397 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2398 sm 0 (PAlternative ms a as)
2399 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2400 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2401 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2402 sm 0 (PHidden x) = PHidden (sm 0 x)
2403 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2404 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2405 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2406 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2407 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2408 sm ql x = descend (sm ql) x
2410 shadowAlt p@(x, oldn) = (update x, update oldn)
2411 update oldn | n == oldn = n'
2414-- | Rename any binders which are repeated (so that we don't have to
2415-- mess about with shadowing anywhere else).
2416mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2417mkUniqueNames env shadows tm
2418 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2420 initMap = M.fromList shadows
2422 inScope :: S.Set Name
2423 inScope = S.fromList $ boundNamesIn tm
2425 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2426 return (arg { getTm = t' })
2428 -- Initialise the unique name with the environment length (so we're not
2429 -- looking for too long...)
2430 initN (UN n) l = UN $ txt (str n ++ show l)
2431 initN (MN i s) l = MN (i+l) s
2434 -- FIXME: Probably ought to do this for completeness! It's fine as
2435 -- long as there are no bindings inside tactics though.
2436 mkUniqT _ nmap tac = return tac
2438 mkUniq :: Int -- ^ The number of quotations that we're under
2439 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2440 mkUniq 0 nmap (PLam fc n nfc ty sc)
2444 then do let n' = uniqueNameSet (initN n (S.size env))
2445 (S.union env inScope)
2446 return (n', sc) -- shadow n n' sc)
2448 put (S.insert n' env)
2449 let nmap' = M.insert n n' nmap
2450 ty' <- mkUniq 0 nmap ty
2451 sc'' <- mkUniq 0 nmap' sc'
2452 return $! PLam fc n' nfc ty' sc''
2453 mkUniq 0 nmap (PPi p n fc ty sc)
2457 then do let n' = uniqueNameSet (initN n (S.size env))
2458 (S.union env inScope)
2459 return (n', sc) -- shadow n n' sc)
2461 put (S.insert n' env)
2462 let nmap' = M.insert n n' nmap
2463 ty' <- mkUniq 0 nmap ty
2464 sc'' <- mkUniq 0 nmap' sc'
2465 return $! PPi p n' fc ty' sc''
2466 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2470 then do let n' = uniqueNameSet (initN n (S.size env))
2471 (S.union env inScope)
2472 return (n', sc) -- shadow n n' sc)
2474 put (S.insert n' env)
2475 let nmap' = M.insert n n' nmap
2476 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2477 sc'' <- mkUniq 0 nmap' sc'
2478 return $! PLet fc n' nfc ty' val' sc''
2479 mkUniq 0 nmap (PApp fc t args)
2480 = do t' <- mkUniq 0 nmap t
2481 args' <- mapM (mkUniqA 0 nmap) args
2482 return $! PApp fc t' args'
2483 mkUniq 0 nmap (PAppBind fc t args)
2484 = do t' <- mkUniq 0 nmap t
2485 args' <- mapM (mkUniqA 0 nmap) args
2486 return $! PAppBind fc t' args'
2487 mkUniq 0 nmap (PCase fc t alts)
2488 = do t' <- mkUniq 0 nmap t
2489 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2490 return (x', y')) alts
2491 return $! PCase fc t' alts'
2492 mkUniq 0 nmap (PIfThenElse fc c t f)
2493 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2494 mkUniq 0 nmap (PPair fc hls p l r)
2495 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2496 return $! PPair fc hls p l' r'
2497 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2500 (n', sc') <- if n `S.member` env
2501 then do let n' = uniqueNameSet n (S.union env inScope)
2502 return (n', sc) -- shadow n n' sc)
2504 put (S.insert n' env)
2505 let nmap' = M.insert n n' nmap
2506 t' <- mkUniq 0 nmap t
2507 sc'' <- mkUniq 0 nmap' sc'
2508 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2509 mkUniq 0 nmap (PDPair fc hls p l t r)
2510 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2511 return $! PDPair fc hls p l' t' r'
2512 mkUniq 0 nmap (PAlternative ns b as)
2513 -- store the nmap and defer the rest until we've pruned the set
2514 -- during elaboration
2515 = return $ PAlternative (ns ++ M.toList nmap) b as
2516 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2517 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2518 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2519 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2520 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2521 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2522 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2523 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2524 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2525 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2528 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2530 mkUniq ql nmap (PQuasiquote tm ty) =
2531 do tm' <- mkUniq (ql + 1) nmap tm
2533 Nothing -> return Nothing
2534 Just t -> fmap Just $ mkUniq ql nmap t
2535 return $! PQuasiquote tm' ty'
2536 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2538 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2541getFile :: Opt -> Maybe String
2542getFile (Filename str) = Just str
2545getBC :: Opt -> Maybe String
2546getBC (BCAsm str) = Just str
2549getOutput :: Opt -> Maybe String
2550getOutput (Output str) = Just str
2551getOutput _ = Nothing
2553getIBCSubDir :: Opt -> Maybe String
2554getIBCSubDir (IBCSubDir str) = Just str
2555getIBCSubDir _ = Nothing
2557getImportDir :: Opt -> Maybe String
2558getImportDir (ImportDir str) = Just str
2559getImportDir _ = Nothing
2561getSourceDir :: Opt -> Maybe String
2562getSourceDir (SourceDir str) = Just str
2563getSourceDir _ = Nothing
2565getPkgDir :: Opt -> Maybe String
2566getPkgDir (Pkg str) = Just str
2567getPkgDir _ = Nothing
2569getPkg :: Opt -> Maybe (Bool, String)
2570getPkg (PkgBuild str) = Just (False, str)
2571getPkg (PkgInstall str) = Just (True, str)
2574getPkgClean :: Opt -> Maybe String
2575getPkgClean (PkgClean str) = Just str
2576getPkgClean _ = Nothing
2578getPkgREPL :: Opt -> Maybe String
2579getPkgREPL (PkgREPL str) = Just str
2580getPkgREPL _ = Nothing
2582getPkgCheck :: Opt -> Maybe String
2583getPkgCheck (PkgCheck str) = Just str
2584getPkgCheck _ = Nothing
2586-- | Returns None if given an Opt which is not PkgMkDoc
2587-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2588getPkgMkDoc :: Opt -- ^ Opt to extract
2589 -> Maybe (Bool, String) -- ^ Result
2590getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2591getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2592getPkgMkDoc _ = Nothing
2594getPkgTest :: Opt -- ^ the option to extract
2595 -> Maybe String -- ^ the package file to test
2596getPkgTest (PkgTest f) = Just f
2597getPkgTest _ = Nothing
2599getCodegen :: Opt -> Maybe Codegen
2600getCodegen (UseCodegen x) = Just x
2601getCodegen _ = Nothing
2603getCodegenArgs :: Opt -> Maybe String
2604getCodegenArgs (CodegenArgs args) = Just args
2605getCodegenArgs _ = Nothing
2607getConsoleWidth :: Opt -> Maybe ConsoleWidth
2608getConsoleWidth (UseConsoleWidth x) = Just x
2609getConsoleWidth _ = Nothing
2612getExecScript :: Opt -> Maybe String
2613getExecScript (InterpretScript expr) = Just expr
2614getExecScript _ = Nothing
2616getPkgIndex :: Opt -> Maybe FilePath
2617getPkgIndex (PkgIndex file) = Just file
2618getPkgIndex _ = Nothing
2620getEvalExpr :: Opt -> Maybe String
2621getEvalExpr (EvalExpr expr) = Just expr
2622getEvalExpr _ = Nothing
2624getOutputTy :: Opt -> Maybe OutputType
2625getOutputTy (OutputTy t) = Just t
2626getOutputTy _ = Nothing
2628getLanguageExt :: Opt -> Maybe LanguageExt
2629getLanguageExt (Extension e) = Just e
2630getLanguageExt _ = Nothing
2632getTriple :: Opt -> Maybe String
2633getTriple (TargetTriple x) = Just x
2634getTriple _ = Nothing
2636getCPU :: Opt -> Maybe String
2637getCPU (TargetCPU x) = Just x
2640getOptLevel :: Opt -> Maybe Int
2641getOptLevel (OptLevel x) = Just x
2642getOptLevel _ = Nothing
2644getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2645getOptimisation (AddOpt p) = Just (True, p)
2646getOptimisation (RemoveOpt p) = Just (False, p)
2647getOptimisation _ = Nothing
2649getColour :: Opt -> Maybe Bool
2650getColour (ColourREPL b) = Just b
2651getColour _ = Nothing
2653getClient :: Opt -> Maybe String
2654getClient (Client x) = Just x
2655getClient _ = Nothing
2657-- Get the first valid port
2658getPort :: [Opt] -> Maybe REPLPort
2660getPort (Port p : xs) = Just p
2661getPort (_ : xs) = getPort xs
2663opt :: (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