git.iko.soy/Idris-dev
on ebbae35 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2298 lines 99 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.Docstrings
13import Idris.IdeMode hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import System.Console.Haskeline
18import System.IO
19import System.Directory (canonicalizePath, doesFileExist)
21import Control.Applicative
22import Control.Monad (liftM3)
23import Control.Monad.State
25import Data.List hiding (insert,union)
26import Data.Char
27import qualified Data.Text as T
28import Data.Either
29import qualified Data.Map as M
30import Data.Maybe
31import qualified Data.Set as S
32import Data.Word (Word)
34import Data.Generics.Uniplate.Data (descend, descendM)
36import Debug.Trace
38import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
40import Util.Pretty
41import Util.ScreenSize
42import Util.System
44getContext :: Idris Context
45getContext = do i <- getIState; return (tt_ctxt i)
47forCodegen :: Codegen -> [(Codegen, a)] -> [a]
48forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
50getObjectFiles :: Codegen -> Idris [FilePath]
51getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
53addObjectFile :: Codegen -> FilePath -> Idris ()
54addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
56getLibs :: Codegen -> Idris [String]
57getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
59addLib :: Codegen -> String -> Idris ()
60addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
62getFlags :: Codegen -> Idris [String]
63getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
65addFlag :: Codegen -> String -> Idris ()
66addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
68addDyLib :: [String] -> Idris (Either DynamicLib String)
69addDyLib libs = do i <- getIState
70 let ls = idris_dynamic_libs i
71 let importdirs = opt_importdirs (idris_options i)
72 case mapMaybe (findDyLib ls) libs of
73 x:_ -> return (Left x)
74 [] -> do
75 handle <- lift . lift .
76 mapM (\l -> catchIO (tryLoadLib importdirs l)
77 (\_ -> return Nothing)) $ libs
78 case msum handle of
79 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
80 concat (intersperse "," libs) ++ "\"")
81 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
82 return (Left x)
83 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
84 findDyLib [] l = Nothing
85 findDyLib (lib:libs) l | l == lib_name lib = Just lib
86 | otherwise = findDyLib libs l
88getAutoImports :: Idris [FilePath]
89getAutoImports = do i <- getIState
90 return (opt_autoImport (idris_options i))
92addAutoImport :: FilePath -> Idris ()
93addAutoImport fp = do i <- getIState
94 let opts = idris_options i
95 let autoimps = opt_autoImport opts
96 put (i { idris_options = opts { opt_autoImport =
97 fp : opt_autoImport opts } } )
99addHdr :: Codegen -> String -> Idris ()
100addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
102addImported :: Bool -> FilePath -> Idris ()
103addImported pub f
104 = do i <- getIState
105 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
107addLangExt :: LanguageExt -> Idris ()
108addLangExt TypeProviders = do i <- getIState
109 putIState $ i {
110 idris_language_extensions = TypeProviders : idris_language_extensions i
111 }
112addLangExt ErrorReflection = do i <- getIState
113 putIState $ i {
114 idris_language_extensions = ErrorReflection : idris_language_extensions i
115 }
117-- Transforms are organised by the function being applied on the lhs of the
118-- transform, to make looking up appropriate transforms quicker
119addTrans :: Name -> (Term, Term) -> Idris ()
120addTrans basefn t
121 = do i <- getIState
122 let t' = case lookupCtxtExact basefn (idris_transforms i) of
123 Just def -> (t : def)
124 Nothing -> [t]
125 putIState $ i { idris_transforms = addDef basefn t'
126 (idris_transforms i) }
128addErrRev :: (Term, Term) -> Idris ()
129addErrRev t = do i <- getIState
130 putIState $ i { idris_errRev = t : idris_errRev i }
132addErasureUsage :: Name -> Int -> Idris ()
133addErasureUsage n i = do ist <- getIState
134 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
136addExport :: Name -> Idris ()
137addExport n = do ist <- getIState
138 putIState $ ist { idris_exports = n : idris_exports ist }
140addUsedName :: FC -> Name -> Name -> Idris ()
141addUsedName fc n arg
142 = do ist <- getIState
143 case lookupTyName n (tt_ctxt ist) of
144 [(n', ty)] -> addUsage n' 0 ty
145 [] -> throwError (At fc (NoSuchVariable n))
146 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
147 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
148 addErasureUsage n i
149 | otherwise = addUsage n (i + 1) sc
150 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
152getErasureUsage :: Idris [(Name, Int)]
153getErasureUsage = do ist <- getIState;
154 return (idris_erasureUsed ist)
156getExports :: Idris [Name]
157getExports = do ist <- getIState
158 return (idris_exports ist)
160totcheck :: (FC, Name) -> Idris ()
161totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
163defer_totcheck :: (FC, Name) -> Idris ()
164defer_totcheck n
165 = do i <- getIState;
166 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
168clear_totcheck :: Idris ()
169clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
171setFlags :: Name -> [FnOpt] -> Idris ()
172setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
174setFnInfo :: Name -> FnInfo -> Idris ()
175setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
177setAccessibility :: Name -> Accessibility -> Idris ()
178setAccessibility n a
179 = do i <- getIState
180 let ctxt = setAccess n a (tt_ctxt i)
181 putIState $ i { tt_ctxt = ctxt }
183setTotality :: Name -> Totality -> Idris ()
184setTotality n a
185 = do i <- getIState
186 let ctxt = setTotal n a (tt_ctxt i)
187 putIState $ i { tt_ctxt = ctxt }
189getTotality :: Name -> Idris Totality
190getTotality n
191 = do i <- getIState
192 case lookupTotal n (tt_ctxt i) of
193 [t] -> return t
194 _ -> return (Total [])
196-- Get coercions which might return the required type
197getCoercionsTo :: IState -> Type -> [Name]
198getCoercionsTo i ty =
199 let cs = idris_coercions i
200 (fn,_) = unApply (getRetTy ty) in
201 findCoercions fn cs
202 where findCoercions t [] = []
203 findCoercions t (n : ns) =
204 let ps = case lookupTy n (tt_ctxt i) of
205 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
206 (t', _) ->
207 if t == t' then [n] else []
208 _ -> [] in
209 ps ++ findCoercions t ns
211addToCG :: Name -> CGInfo -> Idris ()
212addToCG n cg
213 = do i <- getIState
214 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
216addTyInferred :: Name -> Idris ()
217addTyInferred n
218 = do i <- getIState
219 putIState $ i { idris_tyinfodata =
220 addDef n TIPartial (idris_tyinfodata i) }
222addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
223addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
224 mapM_ addConstraint ts
225 return ()
226 where addConstraint (x, y) = findMVApps x y
228 findMVApps x y
229 = do let (fx, argsx) = unApply x
230 let (fy, argsy) = unApply y
231 if (not (fx == fy))
232 then do
233 tryAddMV fx y
234 tryAddMV fy x
235 else mapM_ addConstraint (zip argsx argsy)
237 tryAddMV (P _ mv _) y =
238 do ist <- get
239 case lookup mv (idris_metavars ist) of
240 Just _ -> addConstraintRule mv y
241 _ -> return ()
242 tryAddMV _ _ = return ()
244 addConstraintRule :: Name -> Term -> Idris ()
245 addConstraintRule n t
246 = do ist <- get
247 logLvl 1 $ "TI constraint: " ++ show (n, t)
248 case lookupCtxt n (idris_tyinfodata ist) of
249 [TISolution ts] ->
250 do mapM_ (checkConsistent t) ts
251 let ti' = addDef n (TISolution (t : ts))
252 (idris_tyinfodata ist)
253 put $ ist { idris_tyinfodata = ti' }
254 _ ->
255 do let ti' = addDef n (TISolution [t])
256 (idris_tyinfodata ist)
257 put $ ist { idris_tyinfodata = ti' }
259 -- Check a solution is consistent with previous solutions
260 -- Meaning: If heads are both data types, they had better be the
261 -- same.
262 checkConsistent :: Term -> Term -> Idris ()
263 checkConsistent x y =
264 do let (fx, _) = unApply x
265 let (fy, _) = unApply y
266 case (fx, fy) of
267 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
268 (P (TCon _ _) n _, Constant _) -> errWhen True
269 (Constant _, P (TCon _ _) n' _) -> errWhen True
270 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
271 _ -> return ()
273 where errWhen True
274 = throwError (At fc
275 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
276 errWhen False = return ()
278isTyInferred :: Name -> Idris Bool
279isTyInferred n
280 = do i <- getIState
281 case lookupCtxt n (idris_tyinfodata i) of
282 [TIPartial] -> return True
283 _ -> return False
285-- | Adds error handlers for a particular function and argument. If names are
286-- ambiguous, all matching handlers are updated.
287addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
288addFunctionErrorHandlers f arg hs =
289 do i <- getIState
290 let oldHandlers = idris_function_errorhandlers i
291 let newHandlers = flip (addDef f) oldHandlers $
292 case lookupCtxtExact f oldHandlers of
293 Nothing -> M.singleton arg (S.fromList hs)
294 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
295 -- will always be one of those two, thus no extra case
296 putIState $ i { idris_function_errorhandlers = newHandlers }
298getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
299getFunctionErrorHandlers f arg = do i <- getIState
300 return . maybe [] S.toList $
301 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
304-- Trace all the names in a call graph starting at the given name
305getAllNames :: Name -> Idris [Name]
306getAllNames n = allNames [] n
308allNames :: [Name] -> Name -> Idris [Name]
309allNames ns n | n `elem` ns = return []
310allNames ns n = do i <- getIState
311 case lookupCtxtExact n (idris_callgraph i) of
312 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
313 return (nub (n : concat more))
314 _ -> return [n]
316addCoercion :: Name -> Idris ()
317addCoercion n = do i <- getIState
318 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
320addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
321addDocStr n doc args
322 = do i <- getIState
323 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
325addNameHint :: Name -> Name -> Idris ()
326addNameHint ty n
327 = do i <- getIState
328 ty' <- case lookupCtxtName ty (idris_implicits i) of
329 [(tyn, _)] -> return tyn
330 [] -> throwError (NoSuchVariable ty)
331 tyns -> throwError (CantResolveAlts (map fst tyns))
332 let ns' = case lookupCtxt ty' (idris_namehints i) of
333 [ns] -> ns ++ [n]
334 _ -> [n]
335 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
337getNameHints :: IState -> Name -> [Name]
338getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
339getNameHints i n =
340 case lookupCtxt n (idris_namehints i) of
341 [ns] -> ns
342 _ -> []
344-- Issue #1737 in the Issue Tracker.
345-- https://github.com/idris-lang/Idris-dev/issues/1737
346addToCalledG :: Name -> [Name] -> Idris ()
347addToCalledG n ns = return () -- TODO
349addDeprecated :: Name -> String -> Idris ()
350addDeprecated n reason = do i <- getIState
351 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }
353getDeprecated :: Name -> Idris (Maybe String)
354getDeprecated n = do i <- getIState
355 return $ lookupCtxtExact n (idris_deprecated i)
357push_estack :: Name -> Bool -> Idris ()
358push_estack n inst
359 = do i <- getIState
360 putIState (i { elab_stack = (n, inst) : elab_stack i })
362pop_estack :: Idris ()
363pop_estack = do i <- getIState
364 putIState (i { elab_stack = ptail (elab_stack i) })
365 where ptail [] = []
366 ptail (x : xs) = xs
368-- | Add a class instance function.
369--
370-- Precondition: the instance should have the correct type.
371--
372-- Dodgy hack 1: Put integer instances first in the list so they are
373-- resolved by default.
374--
375-- Dodgy hack 2: put constraint chasers (@@) last
376addInstance :: Bool -- ^ whether the name is an Integer instance
377 -> Bool -- ^ whether to include the instance in instance search
378 -> Name -- ^ the name of the class
379 -> Name -- ^ the name of the instance
380 -> Idris ()
381addInstance int res n i
382 = do ist <- getIState
383 case lookupCtxt n (idris_classes ist) of
384 [CI a b c d e ins fds] ->
385 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
386 putIState $ ist { idris_classes = cs }
387 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)
388 putIState $ ist { idris_classes = cs }
389 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
390 addI i ins | int = (i, res) : ins
391 | chaser n = ins ++ [(i, res)]
392 | otherwise = insI i ins
393 insI i [] = [(i, res)]
394 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
395 | otherwise = n : insI i ns
397 chaser (UN nm)
398 | ('@':'@':_) <- str nm = True
399 chaser (NS n _) = chaser n
400 chaser _ = False
402addClass :: Name -> ClassInfo -> Idris ()
403addClass n i
404 = do ist <- getIState
405 let i' = case lookupCtxt n (idris_classes ist) of
406 [c] -> c { class_instances = class_instances i }
407 _ -> i
408 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
410addRecord :: Name -> RecordInfo -> Idris ()
411addRecord n ri = do ist <- getIState
412 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
414addAutoHint :: Name -> Name -> Idris ()
415addAutoHint n hint =
416 do ist <- getIState
417 case lookupCtxtExact n (idris_autohints ist) of
418 Nothing ->
419 do let hs = addDef n [hint] (idris_autohints ist)
420 putIState $ ist { idris_autohints = hs }
421 Just nhints ->
422 do let hs = addDef n (hint : nhints) (idris_autohints ist)
423 putIState $ ist { idris_autohints = hs }
425getAutoHints :: Name -> Idris [Name]
426getAutoHints n = do ist <- getIState
427 case lookupCtxtExact n (idris_autohints ist) of
428 Nothing -> return []
429 Just ns -> return ns
431addIBC :: IBCWrite -> Idris ()
432addIBC ibc@(IBCDef n)
433 = do i <- getIState
434 when (notDef (ibc_write i)) $
435 putIState $ i { ibc_write = ibc : ibc_write i }
436 where notDef [] = True
437 notDef (IBCDef n': is) | n == n' = False
438 notDef (_ : is) = notDef is
439addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
441clearIBC :: Idris ()
442clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
444resetNameIdx :: Idris ()
445resetNameIdx = do i <- getIState
446 put (i { idris_nameIdx = (0, emptyContext) })
448-- Used to preserve sharing of names
449addNameIdx :: Name -> Idris (Int, Name)
450addNameIdx n = do i <- getIState
451 let (i', x) = addNameIdx' i n
452 putIState i'
453 return x
455addNameIdx' :: IState -> Name -> (IState, (Int, Name))
456addNameIdx' i n
457 = let idxs = snd (idris_nameIdx i) in
458 case lookupCtxt n idxs of
459 [x] -> (i, x)
460 _ -> let i' = fst (idris_nameIdx i) + 1 in
461 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
463getSymbol :: Name -> Idris Name
464getSymbol n = do i <- getIState
465 case M.lookup n (idris_symbols i) of
466 Just n' -> return n'
467 Nothing -> do let sym' = M.insert n n (idris_symbols i)
468 put (i { idris_symbols = sym' })
469 return n
471getHdrs :: Codegen -> Idris [String]
472getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
474getImported :: Idris [(FilePath, Bool)]
475getImported = do i <- getIState; return (idris_imported i)
477setErrSpan :: FC -> Idris ()
478setErrSpan x = do i <- getIState;
479 case (errSpan i) of
480 Nothing -> putIState $ i { errSpan = Just x }
481 Just _ -> return ()
483clearErr :: Idris ()
484clearErr = do i <- getIState
485 putIState $ i { errSpan = Nothing }
487getSO :: Idris (Maybe String)
488getSO = do i <- getIState
489 return (compiled_so i)
491setSO :: Maybe String -> Idris ()
492setSO s = do i <- getIState
493 putIState $ (i { compiled_so = s })
495getIState :: Idris IState
496getIState = get
498putIState :: IState -> Idris ()
499putIState = put
501updateIState :: (IState -> IState) -> Idris ()
502updateIState f = do i <- getIState
503 putIState $ f i
505withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
506withContext ctx name dflt action = do
507 ist <- getIState
508 case lookupCtxt name (ctx ist) of
509 [x] -> action x
510 _ -> return dflt
512withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
513withContext_ ctx name action = withContext ctx name () action
515-- | A version of liftIO that puts errors into the exception type of the Idris monad
516runIO :: IO a -> Idris a
517runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
518-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
519--
520-- Issue #1738 on the issue tracker.
521-- https://github.com/idris-lang/Idris-dev/issues/1738
523getName :: Idris Int
524getName = do i <- getIState;
525 let idx = idris_name i;
526 putIState $ (i { idris_name = idx + 1 })
527 return idx
529-- InternalApp keeps track of the real function application for making case splits from, not the application the
530-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
531addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
532addInternalApp fp l t
533 = do i <- getIState
534 -- We canonicalise the path to make "./Test/Module.idr" equal
535 -- to "Test/Module.idr"
536 exists <- runIO $ doesFileExist fp
537 when exists $
538 do fp' <- runIO $ canonicalizePath fp
539 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
541getInternalApp :: FilePath -> Int -> Idris PTerm
542getInternalApp fp l = do i <- getIState
543 -- We canonicalise the path to make
544 -- "./Test/Module.idr" equal to
545 -- "Test/Module.idr"
546 exists <- runIO $ doesFileExist fp
547 if exists
548 then do fp' <- runIO $ canonicalizePath fp
549 case lookup (fp', l) (idris_lineapps i) of
550 Just n' -> return n'
551 Nothing -> return Placeholder
552 -- TODO: What if it's not there?
553 else return Placeholder
555-- Pattern definitions are only used for coverage checking, so erase them
556-- when we're done
557clearOrigPats :: Idris ()
558clearOrigPats = do i <- get
559 let ps = idris_patdefs i
560 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
561 put (i { idris_patdefs = ps' })
563-- Erase types from Ps in the context (basically ending up with what's in
564-- the .ibc, which is all we need after all the analysis is done)
565clearPTypes :: Idris ()
566clearPTypes = do i <- get
567 let ctxt = tt_ctxt i
568 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
569 where pErase (CaseOp c t tys orig tot cds)
570 = CaseOp c t tys orig [] (pErase' cds)
571 pErase x = x
572 pErase' (CaseDefs _ (cs, c) _ rs)
573 = let c' = (cs, fmap pEraseType c) in
574 CaseDefs c' c' c' rs
576checkUndefined :: FC -> Name -> Idris ()
577checkUndefined fc n
578 = do i <- getContext
579 case lookupTy n i of
580 (_:_) -> throwError . Msg $ show fc ++ ":" ++
581 show n ++ " already defined"
582 _ -> return ()
584isUndefined :: FC -> Name -> Idris Bool
585isUndefined fc n
586 = do i <- getContext
587 case lookupTyExact n i of
588 Just _ -> return False
589 _ -> return True
591setContext :: Context -> Idris ()
592setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
594updateContext :: (Context -> Context) -> Idris ()
595updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
597addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
598addConstraints fc (v, cs)
599 = do i <- getIState
600 let ctxt = tt_ctxt i
601 let ctxt' = ctxt { next_tvar = v }
602 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
603 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
604 where
605 insertAll [] c = c
606 insertAll ((c, fc) : cs) ics
607 = insertAll cs $ S.insert (ConstraintFC c fc) ics
609addDeferred = addDeferred' Ref
610addDeferredTyCon = addDeferred' (TCon 0 0)
612-- | Save information about a name that is not yet defined
613addDeferred' :: NameType
614 -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]
615 -- ^ The Name is the name being made into a metavar,
616 -- the Int is the number of vars that are part of a
617 -- putative proof context, the Maybe Name is the
618 -- top-level function containing the new metavariable,
619 -- the Type is its type, and the Bool is whether :p is
620 -- allowed
621 -> Idris ()
622addDeferred' nt ns
623 = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
624 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
625 i <- getIState
626 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++
627 idris_metavars i }
628 where
629 -- 'tidyNames' is to generate user accessible names in case they are
630 -- needed in tactic scripts
631 tidyNames used (Bind (MN i x) b sc)
632 = let n' = uniqueNameSet (UN x) used in
633 Bind n' b $ tidyNames (S.insert n' used) sc
634 tidyNames used (Bind n b sc)
635 = let n' = uniqueNameSet n used in
636 Bind n' b $ tidyNames (S.insert n' used) sc
637 tidyNames used b = b
639solveDeferred :: Name -> Idris ()
640solveDeferred n = do i <- getIState
641 putIState $ i { idris_metavars =
642 filter (\(n', _) -> n/=n')
643 (idris_metavars i),
644 ibc_write =
645 filter (notMV n) (ibc_write i)
646 }
647 where notMV n (IBCMetavar n') = not (n == n')
648 notMV n _ = True
650getUndefined :: Idris [Name]
651getUndefined = do i <- getIState
652 return (map fst (idris_metavars i) \\ primDefs)
654isMetavarName :: Name -> IState -> Bool
655isMetavarName n ist
656 = case lookupNames n (tt_ctxt ist) of
657 (t:_) -> isJust $ lookup t (idris_metavars ist)
658 _ -> False
660getWidth :: Idris ConsoleWidth
661getWidth = fmap idris_consolewidth getIState
663setWidth :: ConsoleWidth -> Idris ()
664setWidth w = do ist <- getIState
665 put ist { idris_consolewidth = w }
667setDepth :: Maybe Int -> Idris ()
668setDepth d = do ist <- getIState
669 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
671typeDescription :: String
672typeDescription = "The type of types"
675type1Doc :: Doc OutputAnnotation
676type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
679isetPrompt :: String -> Idris ()
680isetPrompt p = do i <- getIState
681 case idris_outputmode i of
682 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
684-- | Tell clients how much was parsed and loaded
685isetLoadedRegion :: Idris ()
686isetLoadedRegion = do i <- getIState
687 let span = idris_parsedSpan i
688 case span of
689 Just fc ->
690 case idris_outputmode i of
691 IdeMode n h ->
692 runIO . hPutStrLn h $
693 convSExp "set-loaded-region" fc n
694 Nothing -> return ()
696setLogLevel :: Int -> Idris ()
697setLogLevel l = do i <- getIState
698 let opts = idris_options i
699 let opt' = opts { opt_logLevel = l }
700 putIState $ i { idris_options = opt' }
702setCmdLine :: [Opt] -> Idris ()
703setCmdLine opts = do i <- getIState
704 let iopts = idris_options i
705 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
707getCmdLine :: Idris [Opt]
708getCmdLine = do i <- getIState
709 return (opt_cmdline (idris_options i))
711getDumpHighlighting :: Idris Bool
712getDumpHighlighting = do ist <- getIState
713 return (findC (opt_cmdline (idris_options ist)))
714 where findC = elem DumpHighlights
716getDumpDefun :: Idris (Maybe FilePath)
717getDumpDefun = do i <- getIState
718 return $ findC (opt_cmdline (idris_options i))
719 where findC [] = Nothing
720 findC (DumpDefun x : _) = Just x
721 findC (_ : xs) = findC xs
723getDumpCases :: Idris (Maybe FilePath)
724getDumpCases = do i <- getIState
725 return $ findC (opt_cmdline (idris_options i))
726 where findC [] = Nothing
727 findC (DumpCases x : _) = Just x
728 findC (_ : xs) = findC xs
730logLevel :: Idris Int
731logLevel = do i <- getIState
732 return (opt_logLevel (idris_options i))
734setErrContext :: Bool -> Idris ()
735setErrContext t = do i <- getIState
736 let opts = idris_options i
737 let opts' = opts { opt_errContext = t }
738 putIState $ i { idris_options = opts' }
740errContext :: Idris Bool
741errContext = do i <- getIState
742 return (opt_errContext (idris_options i))
744getOptimise :: Idris [Optimisation]
745getOptimise = do i <- getIState
746 return (opt_optimise (idris_options i))
748setOptimise :: [Optimisation] -> Idris ()
749setOptimise newopts = do i <- getIState
750 let opts = idris_options i
751 let opts' = opts { opt_optimise = newopts }
752 putIState $ i { idris_options = opts' }
754addOptimise :: Optimisation -> Idris ()
755addOptimise opt = do opts <- getOptimise
756 setOptimise (nub (opt : opts))
758removeOptimise :: Optimisation -> Idris ()
759removeOptimise opt = do opts <- getOptimise
760 setOptimise ((nub opts) \\ [opt])
762-- Set appropriate optimisation set for the given level. We only have
763-- one optimisation that is configurable at the moment, however!
764setOptLevel :: Int -> Idris ()
765setOptLevel n | n <= 0 = setOptimise []
766setOptLevel 1 = setOptimise []
767setOptLevel 2 = setOptimise [PETransform]
768setOptLevel n | n >= 3 = setOptimise [PETransform]
770useREPL :: Idris Bool
771useREPL = do i <- getIState
772 return (opt_repl (idris_options i))
774setREPL :: Bool -> Idris ()
775setREPL t = do i <- getIState
776 let opts = idris_options i
777 let opt' = opts { opt_repl = t }
778 putIState $ i { idris_options = opt' }
780showOrigErr :: Idris Bool
781showOrigErr = do i <- getIState
782 return (opt_origerr (idris_options i))
784setShowOrigErr :: Bool -> Idris ()
785setShowOrigErr b = do i <- getIState
786 let opts = idris_options i
787 let opt' = opts { opt_origerr = b }
788 putIState $ i { idris_options = opt' }
790setAutoSolve :: Bool -> Idris ()
791setAutoSolve b = do i <- getIState
792 let opts = idris_options i
793 let opt' = opts { opt_autoSolve = b }
794 putIState $ i { idris_options = opt' }
796setNoBanner :: Bool -> Idris ()
797setNoBanner n = do i <- getIState
798 let opts = idris_options i
799 let opt' = opts { opt_nobanner = n }
800 putIState $ i { idris_options = opt' }
802getNoBanner :: Idris Bool
803getNoBanner = do i <- getIState
804 let opts = idris_options i
805 return (opt_nobanner opts)
807setEvalTypes :: Bool -> Idris ()
808setEvalTypes n = do i <- getIState
809 let opts = idris_options i
810 let opt' = opts { opt_evaltypes = n }
811 putIState $ i { idris_options = opt' }
813getDesugarNats :: Idris Bool
814getDesugarNats = do i <- getIState
815 let opts = idris_options i
816 return (opt_desugarnats opts)
819setDesugarNats :: Bool -> Idris ()
820setDesugarNats n = do i <- getIState
821 let opts = idris_options i
822 let opt' = opts { opt_desugarnats = n }
823 putIState $ i { idris_options = opt' }
825setQuiet :: Bool -> Idris ()
826setQuiet q = do i <- getIState
827 let opts = idris_options i
828 let opt' = opts { opt_quiet = q }
829 putIState $ i { idris_options = opt' }
831getQuiet :: Idris Bool
832getQuiet = do i <- getIState
833 let opts = idris_options i
834 return (opt_quiet opts)
836setCodegen :: Codegen -> Idris ()
837setCodegen t = do i <- getIState
838 let opts = idris_options i
839 let opt' = opts { opt_codegen = t }
840 putIState $ i { idris_options = opt' }
842codegen :: Idris Codegen
843codegen = do i <- getIState
844 return (opt_codegen (idris_options i))
846setOutputTy :: OutputType -> Idris ()
847setOutputTy t = do i <- getIState
848 let opts = idris_options i
849 let opt' = opts { opt_outputTy = t }
850 putIState $ i { idris_options = opt' }
852outputTy :: Idris OutputType
853outputTy = do i <- getIState
854 return $ opt_outputTy $ idris_options i
856setIdeMode :: Bool -> Handle -> Idris ()
857setIdeMode True h = do i <- getIState
858 putIState $ i { idris_outputmode = IdeMode 0 h
859 , idris_colourRepl = False
860 }
861setIdeMode False _ = return ()
863setTargetTriple :: String -> Idris ()
864setTargetTriple t = do i <- getIState
865 let opts = idris_options i
866 opt' = opts { opt_triple = t }
867 putIState $ i { idris_options = opt' }
869targetTriple :: Idris String
870targetTriple = do i <- getIState
871 return (opt_triple (idris_options i))
873setTargetCPU :: String -> Idris ()
874setTargetCPU t = do i <- getIState
875 let opts = idris_options i
876 opt' = opts { opt_cpu = t }
877 putIState $ i { idris_options = opt' }
879targetCPU :: Idris String
880targetCPU = do i <- getIState
881 return (opt_cpu (idris_options i))
883verbose :: Idris Bool
884verbose = do i <- getIState
885 -- Quietness overrides verbosity
886 return (not (opt_quiet (idris_options i)) &&
887 opt_verbose (idris_options i))
889setVerbose :: Bool -> Idris ()
890setVerbose t = do i <- getIState
891 let opts = idris_options i
892 let opt' = opts { opt_verbose = t }
893 putIState $ i { idris_options = opt' }
895typeInType :: Idris Bool
896typeInType = do i <- getIState
897 return (opt_typeintype (idris_options i))
899setTypeInType :: Bool -> Idris ()
900setTypeInType t = do i <- getIState
901 let opts = idris_options i
902 let opt' = opts { opt_typeintype = t }
903 putIState $ i { idris_options = opt' }
905coverage :: Idris Bool
906coverage = do i <- getIState
907 return (opt_coverage (idris_options i))
909setCoverage :: Bool -> Idris ()
910setCoverage t = do i <- getIState
911 let opts = idris_options i
912 let opt' = opts { opt_coverage = t }
913 putIState $ i { idris_options = opt' }
915setIBCSubDir :: FilePath -> Idris ()
916setIBCSubDir fp = do i <- getIState
917 let opts = idris_options i
918 let opt' = opts { opt_ibcsubdir = fp }
919 putIState $ i { idris_options = opt' }
921valIBCSubDir :: IState -> Idris FilePath
922valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
924addImportDir :: FilePath -> Idris ()
925addImportDir fp = do i <- getIState
926 let opts = idris_options i
927 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
928 putIState $ i { idris_options = opt' }
930setImportDirs :: [FilePath] -> Idris ()
931setImportDirs fps = do i <- getIState
932 let opts = idris_options i
933 let opt' = opts { opt_importdirs = fps }
934 putIState $ i { idris_options = opt' }
936allImportDirs :: Idris [FilePath]
937allImportDirs = do i <- getIState
938 let optdirs = opt_importdirs (idris_options i)
939 return ("." : reverse optdirs)
941colourise :: Idris Bool
942colourise = do i <- getIState
943 return $ idris_colourRepl i
945setColourise :: Bool -> Idris ()
946setColourise b = do i <- getIState
947 putIState $ i { idris_colourRepl = b }
949impShow :: Idris Bool
950impShow = do i <- getIState
951 return (opt_showimp (idris_options i))
953setImpShow :: Bool -> Idris ()
954setImpShow t = do i <- getIState
955 let opts = idris_options i
956 let opt' = opts { opt_showimp = t }
957 putIState $ i { idris_options = opt' }
959setColour :: ColourType -> IdrisColour -> Idris ()
960setColour ct c = do i <- getIState
961 let newTheme = setColour' ct c (idris_colourTheme i)
962 putIState $ i { idris_colourTheme = newTheme }
963 where setColour' KeywordColour c t = t { keywordColour = c }
964 setColour' BoundVarColour c t = t { boundVarColour = c }
965 setColour' ImplicitColour c t = t { implicitColour = c }
966 setColour' FunctionColour c t = t { functionColour = c }
967 setColour' TypeColour c t = t { typeColour = c }
968 setColour' DataColour c t = t { dataColour = c }
969 setColour' PromptColour c t = t { promptColour = c }
970 setColour' PostulateColour c t = t { postulateColour = c }
972logLvl :: Int -> String -> Idris ()
973logLvl l str = do i <- getIState
974 let lvl = opt_logLevel (idris_options i)
975 when (lvl >= l) $
976 case idris_outputmode i of
977 RawOutput h -> do runIO $ hPutStrLn h str
978 IdeMode n h ->
979 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
980 runIO . hPutStrLn h $ convSExp "log" good n
982cmdOptType :: Opt -> Idris Bool
983cmdOptType x = do i <- getIState
984 return $ x `elem` opt_cmdline (idris_options i)
986noErrors :: Idris Bool
987noErrors = do i <- getIState
988 case errSpan i of
989 Nothing -> return True
990 _ -> return False
992setTypeCase :: Bool -> Idris ()
993setTypeCase t = do i <- getIState
994 let opts = idris_options i
995 let opt' = opts { opt_typecase = t }
996 putIState $ i { idris_options = opt' }
999-- Dealing with parameters
1001expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1002 [Name] -> -- all names
1003 [Name] -> -- names with no declaration
1004 PTerm -> PTerm
1005expandParams dec ps ns infs tm = en 0 tm
1006 where
1007 -- if we shadow a name (say in a lambda binding) that is used in a call to
1008 -- a lifted function, we need access to both names - once in the scope of the
1009 -- binding and once to call the lifted functions. So we'll explicitly shadow
1010 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1011 -- but we didn't...)
1013 mkShadow (UN n) = MN 0 n
1014 mkShadow (MN i n) = MN (i+1) n
1015 mkShadow (NS x s) = NS (mkShadow x) s
1017 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1018 -- that are merely mentioned.
1019 -> PTerm -> PTerm
1020 en 0 (PLam fc n nfc t s)
1021 | n `elem` (map fst ps ++ ns)
1022 = let n' = mkShadow n in
1023 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1024 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1025 en 0 (PPi p n nfc t s)
1026 | n `elem` (map fst ps ++ ns)
1027 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1028 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1029 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1030 en 0 (PLet fc n nfc ty v s)
1031 | n `elem` (map fst ps ++ ns)
1032 = let n' = mkShadow n in
1033 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1034 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1035 -- FIXME: Should only do this in a type signature!
1036 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1037 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1038 = let n' = mkShadow n in
1039 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1040 en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1041 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1042 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1043 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1044 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1045 en 0 (PHidden t) = PHidden (en 0 t)
1046 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1047 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1048 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1049 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1050 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1051 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1053 en 0 (PQuote (Var n))
1054 | n `nselem` ns = PQuote (Var (dec n))
1055 en 0 (PApp fc (PInferRef fc' hl n) as)
1056 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1057 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1058 en 0 (PApp fc (PRef fc' hl n) as)
1059 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1060 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1061 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1062 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1063 en 0 (PAppBind fc (PRef fc' hl n) as)
1064 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1065 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1066 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1067 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1068 en 0 (PRef fc hl n)
1069 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1070 (map (pexp . (PRef fc hl)) (map fst ps))
1071 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1072 (map (pexp . (PRef fc hl)) (map fst ps))
1073 en 0 (PInferRef fc hl n)
1074 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1075 (map (pexp . (PRef fc hl)) (map fst ps))
1076 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1077 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1078 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1079 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1080 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1081 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1083 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1084 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1086 en ql t = descend (en ql) t
1088 nselem x [] = False
1089 nselem x (y : xs) | nseq x y = True
1090 | otherwise = nselem x xs
1092 nseq x y = nsroot x == nsroot y
1094 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1095 enTacImp ql other = other
1097expandParamsD :: Bool -> -- True = RHS only
1098 IState ->
1099 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1100expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1101 = if n `elem` ns && (not rhsonly)
1102 then -- trace (show (n, expandParams dec ps ns ty)) $
1103 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1104 else --trace (show (n, expandParams dec ps ns ty)) $
1105 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1106expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1107 = if n `elem` ns && (not rhsonly)
1108 then -- trace (show (n, expandParams dec ps ns ty)) $
1109 PPostulate e doc syn fc nfc o (dec n)
1110 (piBind ps (expandParams dec ps ns [] ty))
1111 else --trace (show (n, expandParams dec ps ns ty)) $
1112 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1113expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1114 = let n' = if n `elem` ns then dec n else n in
1115 PClauses fc opts n' (map expandParamsC cs)
1116 where
1117 expandParamsC (PClause fc n lhs ws rhs ds)
1118 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1119 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1120 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1121 n' = if n `elem` ns then dec n else n
1122 -- names bound on the lhs should not be expanded on the rhs
1123 ns' = removeBound lhs ns in
1124 PClause fc n' lhs'
1125 (map (expandParams dec ps'' ns' []) ws)
1126 (expandParams dec ps'' ns' [] rhs)
1127 (map (expandParamsD True ist dec ps'' ns') ds)
1128 expandParamsC (PWith fc n lhs ws wval pn ds)
1129 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1130 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1131 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1132 n' = if n `elem` ns then dec n else n
1133 ns' = removeBound lhs ns in
1134 PWith fc n' lhs'
1135 (map (expandParams dec ps'' ns' []) ws)
1136 (expandParams dec ps'' ns' [] wval)
1137 pn
1138 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1139 updateps yn nm [] = []
1140 updateps yn nm (((a, t), i):as)
1141 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1142 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1144 removeBound lhs ns = ns \\ nub (bnames lhs)
1146 bnames (PRef _ _ n) = [n]
1147 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1148 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1149 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1150 bnames _ = []
1152-- | Expands parameters defined in parameter and where blocks inside of declarations
1153expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1154 = PData doc argDocs syn fc co (expandPData pd)
1155 where
1156 -- just do the type decl, leave constructors alone (parameters will be
1157 -- added implicitly)
1158 expandPData (PDatadecl n nfc ty cons)
1159 = if n `elem` ns
1160 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1161 (map econ cons)
1162 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1163 econ (doc, argDocs, n, nfc, t, fc, fs)
1164 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1165expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1166 = d
1167expandParamsD rhs ist dec ps ns (PParams f params pds)
1168 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1169 (map (expandParamsD True ist dec ps ns) pds)
1170-- (map (expandParamsD ist dec ps ns) pds)
1171expandParamsD rhs ist dec ps ns (PMutual f pds)
1172 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1173expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1174 = PClass doc info f
1175 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1176 n nfc
1177 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1178 pDocs
1179 fds
1180 (map (expandParamsD rhs ist dec ps ns) decls)
1181 cn
1182 cd
1183expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)
1184 = PInstance doc argDocs info f
1185 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1187 nfc
1188 (map (expandParams dec ps ns []) params)
1189 (expandParams dec ps ns [] ty)
1190 cn
1191 (map (expandParamsD rhs ist dec ps ns) decls)
1192expandParamsD rhs ist dec ps ns d = d
1194mapsnd f (x, t) = (x, f t)
1196-- Calculate a priority for a type, for deciding elaboration order
1197-- * if it's just a type variable or concrete type, do it early (0)
1198-- * if there's only type variables and injective constructors, do it next (1)
1199-- * if there's a function type, next (2)
1200-- * finally, everything else (3)
1202getPriority :: IState -> PTerm -> Int
1203getPriority i tm = 1 -- pri tm
1204 where
1205 pri (PRef _ _ n) =
1206 case lookupP n (tt_ctxt i) of
1207 ((P (DCon _ _ _) _ _):_) -> 1
1208 ((P (TCon _ _) _ _):_) -> 1
1209 ((P Ref _ _):_) -> 1
1210 [] -> 0 -- must be locally bound, if it's not an error...
1211 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1212 pri (PTrue _ _) = 0
1213 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1214 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1215 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1216 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1217 pri (PTyped l r) = pri l
1218 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1219 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1220 pri (PAlternative _ a as) = maximum (map pri as)
1221 pri (PConstant _ _) = 0
1222 pri Placeholder = 1
1223 pri _ = 3
1226addStatics :: Name -> Term -> PTerm -> Idris ()
1227addStatics n tm ptm =
1228 do let (statics, dynamics) = initStatics tm ptm
1229 ist <- getIState
1230 let paramnames
1231 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1232 Just p -> getNamesFrom 0 (fn_params p) tm ++
1233 concatMap (getParamNames ist) (map snd statics)
1234 _ -> concatMap (getParamNames ist) (map snd statics)
1236 let stnames = nub $ concatMap freeArgNames (map snd statics)
1237 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1238 \\ paramnames
1239 -- also get the arguments which are 'uniquely inferrable' from
1240 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1241 -- or parameters to the type of a static
1242 let statics' = nub $ map fst statics ++
1243 filter (\x -> not (elem x dnames)) stnames
1244 let stpos = staticList statics' tm
1245 i <- getIState
1246 when (not (null statics)) $
1247 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1248 ++ showTmImpls ptm ++ "\n"
1249 ++ show statics ++ "\n" ++ show dynamics
1250 ++ "\n" ++ show paramnames
1251 ++ "\n" ++ show stpos
1252 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1253 addIBC (IBCStatic n)
1254 where
1255 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1256 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1257 (static, (n, ty) : dynamic)
1258 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1259 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1260 if pstatic p == Static then ((n, ty) : static, dynamic)
1261 else if (not (searchArg p))
1262 then (static, (n, ty) : dynamic)
1263 else (static, dynamic)
1264 initStatics t pt = ([], [])
1266 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1267 = case lookupCtxtExact n (idris_datatypes ist) of
1268 Just ti -> getNamePos 0 (param_pos ti) args
1269 Nothing -> []
1270 where getNamePos i ps [] = []
1271 getNamePos i ps (P _ n _ : as)
1272 | i `elem` ps = n : getNamePos (i + 1) ps as
1273 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1274 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1275 = n : getParamNames ist sc
1276 getParamNames ist _ = []
1278 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1279 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1280 | otherwise = getNamesFrom (i + 1) ps sc
1281 getNamesFrom i ps sc = []
1283 freeArgNames (Bind n (Pi _ ty _) sc)
1284 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1285 freeArgNames tm = let (_, args) = unApply tm in
1286 concatMap freeNames args
1288 -- if a name appears in a type class or tactic implicit index, it doesn't
1289 -- affect its 'uniquely inferrable' from a static status since these are
1290 -- resolved by searching.
1291 searchArg (Constraint _ _) = True
1292 searchArg (TacImp _ _ _) = True
1293 searchArg _ = False
1295 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1296 staticList _ _ = []
1298-- Dealing with implicit arguments
1300-- Add some bound implicits to the using block if they aren't there already
1302addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1303addToUsing us [] = us
1304addToUsing us ((n, t) : ns)
1305 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1306 | otherwise = addToUsing us ns
1307 where impName (UImplicit n _) = Just n
1308 impName _ = Nothing
1310-- Add constraint bindings from using block
1312addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1313addUsingConstraints syn fc t
1314 = do ist <- get
1315 let ns = namesIn [] ist t
1316 let cs = getConstraints t -- check declared constraints
1317 let addconsts = uconsts \\ cs
1318 return (doAdd addconsts ns t)
1319 where uconsts = filter uconst (using syn)
1320 uconst (UConstraint _ _) = True
1321 uconst _ = False
1323 doAdd [] _ t = t
1324 -- if all of args in ns, then add it
1325 doAdd (UConstraint c args : cs) ns t
1326 | all (\n -> elem n ns) args
1327 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1328 (mkConst c args) (doAdd cs ns t)
1329 | otherwise = doAdd cs ns t
1331 mkConst c args = PApp fc (PRef fc [] c)
1332 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc [] n)) args)
1334 getConstraints (PPi (Constraint _ _) _ _ c sc)
1335 = getcapp c ++ getConstraints sc
1336 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1337 getConstraints _ = []
1339 getcapp (PApp _ (PRef _ _ c) args)
1340 = do ns <- mapM getName args
1341 return (UConstraint c ns)
1342 getcapp _ = []
1344 getName (PExp _ _ _ (PRef _ _ n)) = return n
1345 getName _ = []
1347-- Add implicit bindings from using block, and bind any missing names
1348addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1349addUsingImpls syn n fc t
1350 = do ist <- getIState
1351 let ns = implicitNamesIn (map iname uimpls) ist t
1352 let badnames = filter (\n -> not (implicitable n) &&
1353 n `notElem` (map iname uimpls)) ns
1354 when (not (null badnames)) $
1355 throwError (At fc (Elaborating "type of " n Nothing
1356 (NoSuchVariable (head badnames))))
1357 let cs = getArgnames t -- get already bound names
1358 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1359 -- if all names in the arguments of addconsts appear in ns,
1360 -- add the constraint implicitly
1361 return (bindFree ns (doAdd addimpls ns t))
1362 where uimpls = filter uimpl (using syn)
1363 uimpl (UImplicit _ _) = True
1364 uimpl _ = False
1366 iname (UImplicit n _) = n
1367 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1369 doAdd [] _ t = t
1370 -- if all of args in ns, then add it
1371 doAdd (UImplicit n ty : cs) ns t
1372 | elem n ns
1373 = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)
1374 | otherwise = doAdd cs ns t
1376 -- bind the free names which weren't in the using block
1377 bindFree [] tm = tm
1378 bindFree (n:ns) tm
1379 | elem n (map iname uimpls) = bindFree ns tm
1380 | otherwise
1381 = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1383 getArgnames (PPi _ n _ c sc)
1384 = n : getArgnames sc
1385 getArgnames _ = []
1387-- Given the original type and the elaborated type, return the implicitness
1388-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1390getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1391getUnboundImplicits i t tm = getImps t (collectImps tm)
1392 where collectImps (PPi p n _ t sc)
1393 = (n, (p, t)) : collectImps sc
1394 collectImps _ = []
1396 scopedimpl (Just i) = not (toplevel_imp i)
1397 scopedimpl _ = False
1399 getImps (Bind n (Pi i _ _) sc) imps
1400 | scopedimpl i = getImps sc imps
1401 getImps (Bind n (Pi _ t _) sc) imps
1402 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1403 where
1404 argInfo n (Imp opt _ _ _) Placeholder
1405 = (True, PImp 0 True opt n Placeholder)
1406 argInfo n (Imp opt _ _ _) t'
1407 = (False, PImp (getPriority i t') True opt n t')
1408 argInfo n (Exp opt _ _) t'
1409 = (InaccessibleArg `elem` opt,
1410 PExp (getPriority i t') opt n t')
1411 argInfo n (Constraint opt _) t'
1412 = (InaccessibleArg `elem` opt,
1413 PConstraint 10 opt n t')
1414 argInfo n (TacImp opt _ scr) t'
1415 = (InaccessibleArg `elem` opt,
1416 PTacImplicit 10 opt n scr t')
1417 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1418 where impBind n t = (True, PImp 1 True [] n Placeholder)
1419 getImps sc tm = []
1421-- Add implicit Pi bindings for any names in the term which appear in an
1422-- argument position.
1424-- This has become a right mess already. Better redo it some time...
1425-- TODO: This is obsoleted by the new way of elaborating types, (which
1426-- calls addUsingImpls) but there's still a couple of places which use
1427-- it. Clean them up!
1429-- Issue 1739 in the issue tracker
1430-- https://github.com/idris-lang/Idris-dev/issues/1739
1431implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1432implicit info syn n ptm = implicit' info syn [] n ptm
1434implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1435implicit' info syn ignore n ptm
1436 = do i <- getIState
1437 let (tm', impdata) = implicitise syn ignore i ptm
1438 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1439-- let (tm'', spos) = findStatics i tm'
1440 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1441 addIBC (IBCImp n)
1442 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1443-- i <- get
1444-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1445 return tm'
1446 where
1447 -- Detect unknown names in default arguments and throw error if found.
1448 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1449 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1451 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1452 notFoundInDefault kns (PTacImplicit _ _ n script _)
1453 = do i <- getIState
1454 case notFound kns (namesIn [] i script) of
1455 Nothing -> return (n:kns)
1456 Just name -> throwError (NoSuchVariable name)
1457 notFoundInDefault kns p = return ((pname p):kns)
1459 notFound :: [Name] -> [Name] -> Maybe Name
1460 notFound kns [] = Nothing
1461 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1462 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1464implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1465implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1466 let (declimps, ns') = execState (imps True [] tm) ([], [])
1467 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1468 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1469 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1470 if null ns
1471 then (tm, reverse declimps)
1472 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1473 where
1474 uvars = map ipair (filter uimplicit (using syn))
1475 pvars = syn_params syn
1477 inUsing n = n `elem` map fst uvars
1479 ipair (UImplicit x y) = (x, y)
1480 uimplicit (UImplicit _ _) = True
1481 uimplicit _ = False
1483 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1484 | otherwise = x : dropAll xs ys
1485 dropAll [] ys = []
1487 -- Find names in argument position in a type, suitable for implicit
1488 -- binding
1489 -- Not the function position, but do everything else...
1490 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1491 implNamesIn uv t = namesIn uv ist t
1493 imps top env (PApp _ f as)
1494 = do (decls, ns) <- get
1495 let isn = concatMap (namesIn uvars ist) (map getTm as)
1496 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1497 imps top env (PPi (Imp l _ _ _) n _ ty sc)
1498 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1499 (decls , ns) <- get
1500 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1501 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1502 imps True (n:env) sc
1503 imps top env (PPi (Exp l _ _) n _ ty sc)
1504 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1505 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1506 _ -> [])
1507 (decls, ns) <- get -- ignore decls in HO types
1508 put (PExp (getPriority ist ty) l n Placeholder : decls,
1509 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1510 imps True (n:env) sc
1511 imps top env (PPi (Constraint l _) n _ ty sc)
1512 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1513 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1514 _ -> [])
1515 (decls, ns) <- get -- ignore decls in HO types
1516 put (PConstraint 10 l n Placeholder : decls,
1517 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1518 imps True (n:env) sc
1519 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1520 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1521 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1522 _ -> [])
1523 (decls, ns) <- get -- ignore decls in HO types
1524 put (PTacImplicit 10 l n scr Placeholder : decls,
1525 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1526 imps True (n:env) sc
1527 imps top env (PRewrite _ l r _)
1528 = do (decls, ns) <- get
1529 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1530 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1531 imps top env (PTyped l r)
1532 = imps top env l
1533 imps top env (PPair _ _ _ l r)
1534 = do (decls, ns) <- get
1535 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1536 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1537 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1538 = do (decls, ns) <- get
1539 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1540 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1541 imps top env (PDPair _ _ _ l t r)
1542 = do (decls, ns) <- get
1543 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1544 namesIn uvars ist r
1545 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1546 imps top env (PAlternative ms a as)
1547 = do (decls, ns) <- get
1548 let isn = concatMap (namesIn uvars ist) as
1549 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1550 imps top env (PLam fc n _ ty sc)
1551 = do imps False env ty
1552 imps False (n:env) sc
1553 imps top env (PHidden tm) = imps False env tm
1554 imps top env (PUnifyLog tm) = imps False env tm
1555 imps top env (PNoImplicits tm) = imps False env tm
1556 imps top env (PRunElab fc tm ns) = imps False env tm
1557 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1558 imps top env _ = return ()
1560 pibind using [] sc = sc
1561 pibind using (n:ns) sc
1562 = case lookup n using of
1563 Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))
1564 n NoFC ty (pibind using ns sc)
1565 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))
1566 n NoFC Placeholder (pibind using ns sc)
1568-- Add implicit arguments in function calls
1569addImplPat :: IState -> PTerm -> PTerm
1570addImplPat = addImpl' True [] [] []
1572addImplBound :: IState -> [Name] -> PTerm -> PTerm
1573addImplBound ist ns = addImpl' False ns [] [] ist
1575addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1576addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1578-- | Add the implicit arguments to applications in the term
1579-- [Name] gives the names to always expend, even when under a binder of
1580-- that name (this is to expand methods with implicit arguments in dependent
1581-- type classes).
1582addImpl :: [Name] -> IState -> PTerm -> PTerm
1583addImpl = addImpl' False [] []
1585-- TODO: in patterns, don't add implicits to function names guarded by constructors
1586-- and *not* inside a PHidden
1588addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1589addImpl' inpat env infns imp_meths ist ptm
1590 = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1591 where
1592 topname = case ptm of
1593 PRef _ _ n -> n
1594 PApp _ (PRef _ _ n) _ -> n
1595 _ -> sUN "" -- doesn't matter then
1597 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1598 ai inpat qq env ds (PRef fc fcs f)
1599 | f `elem` infns = PInferRef fc fcs f
1600 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] []
1601 ai inpat qq env ds (PHidden (PRef fc hl f))
1602 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] [])
1603 ai inpat qq env ds (PRewrite fc l r g)
1604 = let l' = ai inpat qq env ds l
1605 r' = ai inpat qq env ds r
1606 g' = fmap (ai inpat qq env ds) g in
1607 PRewrite fc l' r' g'
1608 ai inpat qq env ds (PTyped l r)
1609 = let l' = ai inpat qq env ds l
1610 r' = ai inpat qq env ds r in
1611 PTyped l' r'
1612 ai inpat qq env ds (PPair fc hls p l r)
1613 = let l' = ai inpat qq env ds l
1614 r' = ai inpat qq env ds r in
1615 PPair fc hls p l' r'
1616 ai inpat qq env ds (PDPair fc hls p l t r)
1617 = let l' = ai inpat qq env ds l
1618 t' = ai inpat qq env ds t
1619 r' = ai inpat qq env ds r in
1620 PDPair fc hls p l' t' r'
1621 ai inpat qq env ds (PAlternative ms a as)
1622 = let as' = map (ai inpat qq env ds) as in
1623 PAlternative ms a as'
1624 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1625 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1626 = let as' = map (fmap (ai inpat qq env ds)) as in
1627 PApp fc (PInferRef ffc hl f) as'
1628 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1629 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1630 | not (f `elem` map fst env)
1631 = let as' = map (fmap (ai inpat qq env ds)) as
1632 asdotted' = map (fmap (ai False qq env ds)) as in
1633 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'
1634 | Just (Just ty) <- lookup f env =
1635 let as' = map (fmap (ai inpat qq env ds)) as
1636 arity = getPArity ty in
1637 mkPApp fc arity ftm as'
1638 ai inpat qq env ds (PApp fc f as)
1639 = let f' = ai inpat qq env ds f
1640 as' = map (fmap (ai inpat qq env ds)) as in
1641 mkPApp fc 1 f' as'
1642 ai inpat qq env ds (PCase fc c os)
1643 = let c' = ai inpat qq env ds c in
1644 -- leave os alone, because they get lifted into a new pattern match
1645 -- definition which is passed through addImpl agai inpatn with more scope
1646 -- information
1647 PCase fc c' os
1649 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1650 (ai inpat qq env ds t)
1651 (ai inpat qq env ds f)
1653 -- If the name in a lambda is a constructor name, do this as a 'case'
1654 -- instead (it is harmless to do so, especially since the lambda will
1655 -- be lifted anyway!)
1656 ai inpat qq env ds (PLam fc n nfc ty sc)
1657 = case lookupDef n (tt_ctxt ist) of
1658 [] -> let ty' = ai inpat qq env ds ty
1659 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1660 PLam fc n nfc ty' sc'
1661 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1662 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1663 [(PRef fc [] n, sc)]))
1664 ai inpat qq env ds (PLet fc n nfc ty val sc)
1665 = case lookupDef n (tt_ctxt ist) of
1666 [] -> let ty' = ai inpat qq env ds ty
1667 val' = ai inpat qq env ds val
1668 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1669 PLet fc n nfc ty' val' sc'
1670 defs ->
1671 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1672 ai inpat qq env ds (PPi p n nfc ty sc)
1673 = let ty' = ai inpat qq env ds ty
1674 env' = if n `elem` imp_meths then env
1675 else ((n, Just ty) : env)
1676 sc' = ai inpat qq env' ds sc in
1677 PPi p n nfc ty' sc'
1678 ai inpat qq env ds (PGoal fc r n sc)
1679 = let r' = ai inpat qq env ds r
1680 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1681 PGoal fc r' n sc'
1682 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1683 -- Don't do PProof or PTactics since implicits get added when scope is
1684 -- properly known in ElabTerm.runTac
1685 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1686 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1687 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1688 (fmap (ai inpat True env ds) g)
1689 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1690 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1691 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1692 ai inpat qq env ds tm = tm
1694 handleErr (Left err) = PElabError err
1695 handleErr (Right x) = x
1697-- if in a pattern, and there are no arguments, and there's no possible
1698-- names with zero explicit arguments, don't add implicits.
1700aiFn :: Name -> Bool -> Bool -> Bool
1701 -> [Name]
1702 -> IState -> FC
1703 -> Name -- ^ function being applied
1704 -> FC -> [[T.Text]]
1705 -> [PArg] -- ^ initial arguments (if in a pattern)
1706 -> [PArg] -- ^ initial arguments (if in an expression)
1707 -> Either Err PTerm
1708aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _
1709 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1710 | otherwise
1711 = case lookupDef f (tt_ctxt ist) of
1712 [] -> Right $ PPatvar ffc f
1713 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1714 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1715 if (not (vname f) || tcname f
1716 || any (conCaf (tt_ctxt ist)) ialts)
1717-- any constructor alts || any allImp ialts))
1718 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor
1719 else Right $ PPatvar ffc f
1720 where imp (PExp _ _ _ _) = False
1721 imp _ = True
1722-- allImp [] = False
1723 allImp xs = all imp xs
1725 unqualified (NS _ _) = False
1726 unqualified _ = True
1728 constructor (TyDecl (DCon _ _ _) _) = True
1729 constructor _ = False
1731 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1733 vname (UN n) = True -- non qualified
1734 vname _ = False
1736aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1737 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1738aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1739 -- This is where namespaces get resolved by adding PAlternative
1740 = do let ns = lookupCtxtName f (idris_implicits ist)
1741 let nh = filter (\(n, _) -> notHidden n) ns
1742 let ns' = case trimAlts ds nh of
1743 [] -> nh
1744 x -> x
1745 case ns' of
1746 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1747 (insertImpl ns (chooseArgs f' as asexp))
1748 [] -> if f `elem` (map fst (idris_metavars ist))
1749 then Right $ PApp fc (PRef ffc [ffc] f) as
1750 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1751 alts -> Right $
1752 PAlternative [] (ExactlyOne True) $
1753 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1754 (insertImpl ns (chooseArgs f' as asexp))) alts
1755 where
1756 -- choose whether to treat the arguments as patterns or expressions
1757 -- if 'f' is a defined function, treat as expression, otherwise do the default.
1758 -- This is so any names which later go under a PHidden are treated
1759 -- as function names rather than bound pattern variables
1760 chooseArgs f as asexp | isConName f (tt_ctxt ist) = as
1761 | f == topname = as
1762 | Nothing <- lookupDefExact f (tt_ctxt ist) = as
1763 | otherwise = asexp
1765 -- if the name is in imp_meths, we should actually refer to the bound
1766 -- name rather than the global one after expanding implicits
1767 isImpName f f' | f `elem` imp_meths = f
1768 | otherwise = f'
1770 trimAlts [] alts = alts
1771 trimAlts ns alts
1772 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1774 nspace (NS _ s) = s
1775 nspace _ = []
1777 notHidden n = case getAccessibility n of
1778 Hidden -> False
1779 _ -> True
1781 getAccessibility n
1782 = case lookupDefAccExact n False (tt_ctxt ist) of
1783 Just (n,t) -> t
1784 _ -> Public
1786 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1787 -> [PArg] -- ^ given arguments
1788 -> [PArg]
1789 insertImpl ps as
1790 = let (as', badimpls) = partition (impIn ps) as in
1791 map addUnknownImp badimpls ++
1792 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1794 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1795 -> [PArg] -- parameters
1796 -> [PArg] -- explicit arguments
1797 -> [PArg] -- implicits given
1798 -> [PArg]
1799 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1800 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1801 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1802 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1803 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1804 let rtc = PResolveTC fc in
1805 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1806 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1807 case find n imps [] of
1808 Just (tm, imps') ->
1809 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1810 Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in
1811 PImp p True l n ph :
1812 insImpAcc (M.insert n ph pnas) ps given imps
1813 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1814 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1815 case find n imps [] of
1816 Just (tm, imps') ->
1817 PTacImplicit p l n sc tm :
1818 insImpAcc (M.insert n tm pnas) ps given imps'
1819 Nothing ->
1820 if inpat
1821 then PTacImplicit p l n sc Placeholder :
1822 insImpAcc (M.insert n Placeholder pnas) ps given imps
1823 else PTacImplicit p l n sc sc :
1824 insImpAcc (M.insert n sc pnas) ps given imps
1825 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1826 insImpAcc _ _ given imps = given ++ imps
1828 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1830 find n [] acc = Nothing
1831 find n (PImp _ _ _ n' t : gs) acc
1832 | n == n' = Just (t, reverse acc ++ gs)
1833 find n (PTacImplicit _ _ n' _ t : gs) acc
1834 | n == n' = Just (t, reverse acc ++ gs)
1835 find n (g : gs) acc = find n gs (g : acc)
1837-- return True if the second argument is an implicit argument which is
1838-- expected in the implicits, or if it's not an implicit
1839impIn :: [PArg] -> PArg -> Bool
1840impIn ps (PExp _ _ _ _) = True
1841impIn ps (PConstraint _ _ _ _) = True
1842impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1844expArg (PExp _ _ _ _) = True
1845expArg (PConstraint _ _ _ _) = True
1846expArg _ = False
1848-- replace non-linear occurrences with _
1850stripLinear :: IState -> PTerm -> PTerm
1851stripLinear i tm = evalState (sl tm) [] where
1852 sl :: PTerm -> State [Name] PTerm
1853 sl (PRef fc hl f)
1854 | (_:_) <- lookupTy f (tt_ctxt i)
1855 = return $ PRef fc hl f
1856 | otherwise = do ns <- get
1857 if (f `elem` ns)
1858 then return $ PHidden (PRef fc hl f) -- Placeholder
1859 else do put (f : ns)
1860 return (PRef fc hl f)
1861 sl (PPatvar fc f)
1862 = do ns <- get
1863 if (f `elem` ns)
1864 then return $ PHidden (PPatvar fc f) -- Placeholder
1865 else do put (f : ns)
1866 return (PPatvar fc f)
1867 -- Assumption is that variables are all the same in each alternative
1868 sl t@(PAlternative ms b as) = do ns <- get
1869 as' <- slAlts ns as
1870 return (PAlternative ms b as')
1871 where slAlts ns (a : as) = do put ns
1872 a' <- sl a
1873 as' <- slAlts ns as
1874 return (a' : as')
1875 slAlts ns [] = return []
1876 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1877 sl (PDPair fc hls p l t r) = do l' <- sl l
1878 t' <- sl t
1879 r' <- sl r
1880 return (PDPair fc hls p l' t' r')
1881 sl (PApp fc fn args) = do fn' <- case fn of
1882 -- Just the args, fn isn't matchable as a var
1883 PRef _ _ _ -> return fn
1884 t -> sl t
1885 args' <- mapM slA args
1886 return $ PApp fc fn' args'
1887 where slA (PImp p m l n t) = do t' <- sl t
1888 return $ PImp p m l n t'
1889 slA (PExp p l n t) = do t' <- sl t
1890 return $ PExp p l n t'
1891 slA (PConstraint p l n t)
1892 = do t' <- sl t
1893 return $ PConstraint p l n t'
1894 slA (PTacImplicit p l n sc t)
1895 = do t' <- sl t
1896 return $ PTacImplicit p l n sc t'
1897 sl x = return x
1899-- | Remove functions which aren't applied to anything, which must then
1900-- be resolved by unification. Assume names resolved and alternatives
1901-- filled in (so no ambiguity).
1902stripUnmatchable :: IState -> PTerm -> PTerm
1903stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1904 su :: PTerm -> PTerm
1905 su tm@(PRef fc hl f)
1906 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1907 = Placeholder
1908 | (TType _ : _) <- lookupTy f (tt_ctxt i),
1909 not (implicitable f)
1910 = PHidden tm
1911 | (UType _ : _) <- lookupTy f (tt_ctxt i),
1912 not (implicitable f)
1913 = PHidden tm
1914 su (PApp fc f@(PRef _ _ fn) args)
1915 -- here we use canBeDConName because the impossible pattern
1916 -- check will not necessarily fully resolve constructor names,
1917 -- and these bare names will otherwise get in the way of
1918 -- impossbility checking.
1919 | canBeDConName fn ctxt
1920 = PApp fc f (fmap (fmap su) args)
1921 su (PApp fc f args)
1922 = PHidden (PApp fc f args)
1923 su (PAlternative ms b alts)
1924 = let alts' = filter (/= Placeholder) (map su alts) in
1925 if null alts' then Placeholder
1926 else PAlternative ms b alts'
1927 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
1928 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
1929 su t@(PLam fc _ _ _ _) = PHidden t
1930 su t@(PPi _ _ _ _ _) = PHidden t
1931 su t@(PConstant _ c) | isTypeConst c = PHidden t
1932 su t = t
1934 ctxt = tt_ctxt i
1936stripUnmatchable i tm = tm
1938mkPApp fc a f [] = f
1939mkPApp fc a f as = let rest = drop a as in
1940 if a == 0 then appRest fc f rest
1941 else appRest fc (PApp fc f (take a as)) rest
1942 where
1943 appRest fc f [] = f
1944 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1946-- Find 'static' argument positions
1947-- (the declared ones, plus any names in argument position in the declared
1948-- statics)
1949-- FIXME: It's possible that this really has to happen after elaboration
1951findStatics :: IState -> PTerm -> (PTerm, [Bool])
1952findStatics ist tm = let (ns, ss) = fs tm
1953 in runState (pos ns ss tm) []
1954 where fs (PPi p n fc t sc)
1955 | Static <- pstatic p
1956 = let (ns, ss) = fs sc in
1957 (namesIn [] ist t : ns, n : ss)
1958 | otherwise = let (ns, ss) = fs sc in
1959 (ns, ss)
1960 fs _ = ([], [])
1962 inOne n ns = length (filter id (map (elem n) ns)) == 1
1964 pos ns ss (PPi p n fc t sc)
1965 | elem n ss = do sc' <- pos ns ss sc
1966 spos <- get
1967 put (True : spos)
1968 return (PPi (p { pstatic = Static }) n fc t sc')
1969 | otherwise = do sc' <- pos ns ss sc
1970 spos <- get
1971 put (False : spos)
1972 return (PPi p n fc t sc')
1973 pos ns ss t = return t
1975-- for 6.12/7 compatibility
1976data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1978instance Applicative (EitherErr a) where
1979 pure = return
1980 (<*>) = ap
1982instance Monad (EitherErr a) where
1983 return = RightOK
1985 (LeftErr e) >>= k = LeftErr e
1986 RightOK v >>= k = k v
1988toEither (LeftErr e) = Left e
1989toEither (RightOK ho) = Right ho
1991-- | Syntactic match of a against b, returning pair of variables in a
1992-- and what they match. Returns the pair that failed if not a match.
1993matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1994matchClause = matchClause' False
1996matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1997matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1998 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2000 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2001 fullApp x = x
2003 match' x y = match (fullApp x) (fullApp y)
2004 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2005 | fi == txt "fromInteger" && b == txt "builtins",
2006 PConstant _ (I _) <- getTm x = match (getTm x) x'
2007 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2008 | fi == txt "fromInteger" && b == txt "builtins",
2009 PConstant _ (I _) <- getTm x = match (getTm x) x'
2010 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2011 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2012 match (PApp _ f args) (PApp _ f' args')
2013 | length args == length args'
2014 = do mf <- match' f f'
2015 ms <- zipWithM matchArg args args'
2016 return (mf ++ concat ms)
2017 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2018 match (PPatvar f n) xr = match (PRef f [f] n) xr
2019 match xr (PPatvar f n) = match xr (PRef f [f] n)
2020 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2021 match (PRef _ _ n) tm@(PRef _ _ n')
2022 | n == n' && not names &&
2023 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2024 || tm == Placeholder)
2025 = return [(n, tm)]
2026 -- if one namespace is missing, drop the other
2027 | n == n' || n == dropNS n' || dropNS n == n' = return []
2028 where dropNS (NS n _) = n
2029 dropNS n = n
2030 match (PRef _ _ n) tm
2031 | not names && (not (isConName n (tt_ctxt i) ||
2032 isFnName n (tt_ctxt i)) || tm == Placeholder)
2033 = return [(n, tm)]
2034 match (PRewrite _ l r _) (PRewrite _ l' r' _)
2035 = do ml <- match' l l'
2036 mr <- match' r r'
2037 return (ml ++ mr)
2038 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2039 mr <- match r r'
2040 return (ml ++ mr)
2041 match (PTyped l r) x = match l x
2042 match x (PTyped l r) = match x l
2043 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2044 mr <- match' r r'
2045 return (ml ++ mr)
2046 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2047 mt <- match' t t'
2048 mr <- match' r r'
2049 return (ml ++ mt ++ mr)
2050 match (PAlternative _ a as) (PAlternative _ a' as')
2051 = do ms <- zipWithM match' as as'
2052 return (concat ms)
2053 match a@(PAlternative _ _ as) b
2054 = do let ms = zipWith match' as (repeat b)
2055 case (rights (map toEither ms)) of
2056 (x: _) -> return x
2057 _ -> LeftErr (a, b)
2058 match (PCase _ _ _) _ = return [] -- lifted out
2059 match (PMetavar _ _) _ = return [] -- modified
2060 match (PInferRef _ _ _) _ = return [] -- modified
2061 match (PQuote _) _ = return []
2062 match (PProof _) _ = return []
2063 match (PTactics _) _ = return []
2064 match (PResolveTC _) (PResolveTC _) = return []
2065 match (PTrue _ _) (PTrue _ _) = return []
2066 match (PReturn _) (PReturn _) = return []
2067 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2068 ms <- match' s s'
2069 return (mt ++ ms)
2070 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2071 ms <- match' s s'
2072 return (mt ++ ms)
2073 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2074 mty <- match' ty ty'
2075 ms <- match' s s'
2076 return (mt ++ mty ++ ms)
2077 match (PHidden x) (PHidden y)
2078 | RightOK xs <- match x y = return xs -- to collect variables
2079 | otherwise = return [] -- Otherwise hidden things are unmatchable
2080 match (PHidden x) y
2081 | RightOK xs <- match x y = return xs
2082 | otherwise = return []
2083 match x (PHidden y)
2084 | RightOK xs <- match x y = return xs
2085 | otherwise = return []
2086 match (PUnifyLog x) y = match' x y
2087 match x (PUnifyLog y) = match' x y
2088 match (PNoImplicits x) y = match' x y
2089 match x (PNoImplicits y) = match' x y
2090 match Placeholder _ = return []
2091 match _ Placeholder = return []
2092 match (PResolveTC _) _ = return []
2093 match a b | a == b = return []
2094 | otherwise = LeftErr (a, b)
2096 checkRpts (RightOK ms) = check ms where
2097 check ((n,t):xs)
2098 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2099 then Left (t, t')
2100 else check xs
2101 check (_:xs) = check xs
2102 check [] = Right ms
2103 checkRpts (LeftErr x) = Left x
2105substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2106substMatches ms = substMatchesShadow ms []
2108substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2109substMatchesShadow [] shs t = t
2110substMatchesShadow ((n,tm):ns) shs t
2111 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2113substMatch :: Name -> PTerm -> PTerm -> PTerm
2114substMatch n = substMatchShadow n []
2116substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2117substMatchShadow n shs tm t = sm shs t where
2118 sm xs (PRef _ _ n') | n == n' = tm
2119 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2120 sm xs (PPi p x fc t sc)
2121 | x `elem` xs
2122 = let x' = nextName x in
2123 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2124 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2125 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2126 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2127 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2128 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2129 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2130 (fmap (sm xs) tm)
2131 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2132 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2133 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2134 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2135 sm xs (PHidden x) = PHidden (sm xs x)
2136 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2137 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2138 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2139 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2140 sm xs x = x
2142 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2143 fullApp x = x
2145shadow :: Name -> Name -> PTerm -> PTerm
2146shadow n n' t = sm 0 t where
2147 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2148 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2149 | otherwise = PLam fc x xfc (sm 0 t) sc
2150 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2151 | otherwise = PPi p x fc (sm 0 t) sc
2152 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2153 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2154 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2155 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2156 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2157 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2158 sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2159 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2160 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2161 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2162 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2163 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2164 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2165 sm 0 (PHidden x) = PHidden (sm 0 x)
2166 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2167 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2168 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2169 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2170 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2171 sm ql x = descend (sm ql) x
2173-- | Rename any binders which are repeated (so that we don't have to mess
2174-- about with shadowing anywhere else).
2175mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2176mkUniqueNames env shadows tm
2177 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2179 initMap = M.fromList shadows
2181 inScope :: S.Set Name
2182 inScope = S.fromList $ boundNamesIn tm
2184 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2185 return (arg { getTm = t' })
2187 -- Initialise the unique name with the environment length (so we're not
2188 -- looking for too long...)
2189 initN (UN n) l = UN $ txt (str n ++ show l)
2190 initN (MN i s) l = MN (i+l) s
2191 initN n l = n
2193 -- FIXME: Probably ought to do this for completeness! It's fine as
2194 -- long as there are no bindings inside tactics though.
2195 mkUniqT _ nmap tac = return tac
2197 mkUniq :: Int -- ^ The number of quotations that we're under
2198 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2199 mkUniq 0 nmap (PLam fc n nfc ty sc)
2200 = do env <- get
2201 (n', sc') <-
2202 if n `S.member` env
2203 then do let n' = uniqueNameSet (initN n (S.size env))
2204 (S.union env inScope)
2205 return (n', sc) -- shadow n n' sc)
2206 else return (n, sc)
2207 put (S.insert n' env)
2208 let nmap' = M.insert n n' nmap
2209 ty' <- mkUniq 0 nmap ty
2210 sc'' <- mkUniq 0 nmap' sc'
2211 return $! PLam fc n' nfc ty' sc''
2212 mkUniq 0 nmap (PPi p n fc ty sc)
2213 = do env <- get
2214 (n', sc') <-
2215 if n `S.member` env
2216 then do let n' = uniqueNameSet (initN n (S.size env))
2217 (S.union env inScope)
2218 return (n', sc) -- shadow n n' sc)
2219 else return (n, sc)
2220 put (S.insert n' env)
2221 let nmap' = M.insert n n' nmap
2222 ty' <- mkUniq 0 nmap ty
2223 sc'' <- mkUniq 0 nmap' sc'
2224 return $! PPi p n' fc ty' sc''
2225 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2226 = do env <- get
2227 (n', sc') <-
2228 if n `S.member` env
2229 then do let n' = uniqueNameSet (initN n (S.size env))
2230 (S.union env inScope)
2231 return (n', sc) -- shadow n n' sc)
2232 else return (n, sc)
2233 put (S.insert n' env)
2234 let nmap' = M.insert n n' nmap
2235 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2236 sc'' <- mkUniq 0 nmap' sc'
2237 return $! PLet fc n' nfc ty' val' sc''
2238 mkUniq 0 nmap (PApp fc t args)
2239 = do t' <- mkUniq 0 nmap t
2240 args' <- mapM (mkUniqA 0 nmap) args
2241 return $! PApp fc t' args'
2242 mkUniq 0 nmap (PAppBind fc t args)
2243 = do t' <- mkUniq 0 nmap t
2244 args' <- mapM (mkUniqA 0 nmap) args
2245 return $! PAppBind fc t' args'
2246 mkUniq 0 nmap (PCase fc t alts)
2247 = do t' <- mkUniq 0 nmap t
2248 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2249 return (x', y')) alts
2250 return $! PCase fc t' alts'
2251 mkUniq 0 nmap (PIfThenElse fc c t f)
2252 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2253 mkUniq 0 nmap (PPair fc hls p l r)
2254 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2255 return $! PPair fc hls p l' r'
2256 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2257 | t /= Placeholder
2258 = do env <- get
2259 (n', sc') <- if n `S.member` env
2260 then do let n' = uniqueNameSet n (S.union env inScope)
2261 return (n', sc) -- shadow n n' sc)
2262 else return (n, sc)
2263 put (S.insert n' env)
2264 let nmap' = M.insert n n' nmap
2265 t' <- mkUniq 0 nmap t
2266 sc'' <- mkUniq 0 nmap' sc'
2267 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2268 mkUniq 0 nmap (PDPair fc hls p l t r)
2269 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2270 return $! PDPair fc hls p l' t' r'
2271 mkUniq 0 nmap (PAlternative ns b as)
2272 -- store the nmap and defer the rest until we've pruned the set
2273 -- during elaboration
2274 = return $ PAlternative (M.toList nmap ++ ns) b as
2275 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2276 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2277 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2278 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2279 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2280 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2281 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2282 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2283 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2284 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2285 where
2286 shadowAll [] t = t
2287 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2289 mkUniq ql nmap (PQuasiquote tm ty) =
2290 do tm' <- mkUniq (ql + 1) nmap tm
2291 ty' <- case ty of
2292 Nothing -> return Nothing
2293 Just t -> fmap Just $ mkUniq ql nmap t
2294 return $! PQuasiquote tm' ty'
2295 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2297 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm