git.iko.soy/Idris-dev
on 50878fa help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2278 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
349push_estack :: Name -> Bool -> Idris ()
350push_estack n inst
351 = do i <- getIState
352 putIState (i { elab_stack = (n, inst) : elab_stack i })
354pop_estack :: Idris ()
355pop_estack = do i <- getIState
356 putIState (i { elab_stack = ptail (elab_stack i) })
357 where ptail [] = []
358 ptail (x : xs) = xs
360-- | Add a class instance function.
361--
362-- Precondition: the instance should have the correct type.
363--
364-- Dodgy hack 1: Put integer instances first in the list so they are
365-- resolved by default.
366--
367-- Dodgy hack 2: put constraint chasers (@@) last
368addInstance :: Bool -- ^ whether the name is an Integer instance
369 -> Bool -- ^ whether to include the instance in instance search
370 -> Name -- ^ the name of the class
371 -> Name -- ^ the name of the instance
372 -> Idris ()
373addInstance int res n i
374 = do ist <- getIState
375 case lookupCtxt n (idris_classes ist) of
376 [CI a b c d e ins fds] ->
377 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
378 putIState $ ist { idris_classes = cs }
379 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)
380 putIState $ ist { idris_classes = cs }
381 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
382 addI i ins | int = (i, res) : ins
383 | chaser n = ins ++ [(i, res)]
384 | otherwise = insI i ins
385 insI i [] = [(i, res)]
386 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
387 | otherwise = n : insI i ns
389 chaser (UN nm)
390 | ('@':'@':_) <- str nm = True
391 chaser (NS n _) = chaser n
392 chaser _ = False
394addClass :: Name -> ClassInfo -> Idris ()
395addClass n i
396 = do ist <- getIState
397 let i' = case lookupCtxt n (idris_classes ist) of
398 [c] -> c { class_instances = class_instances i }
399 _ -> i
400 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
402addRecord :: Name -> RecordInfo -> Idris ()
403addRecord n ri = do ist <- getIState
404 putIState $ ist { idris_records = addDef n ri (idris_records ist) }
406addAutoHint :: Name -> Name -> Idris ()
407addAutoHint n hint =
408 do ist <- getIState
409 case lookupCtxtExact n (idris_autohints ist) of
410 Nothing ->
411 do let hs = addDef n [hint] (idris_autohints ist)
412 putIState $ ist { idris_autohints = hs }
413 Just nhints ->
414 do let hs = addDef n (hint : nhints) (idris_autohints ist)
415 putIState $ ist { idris_autohints = hs }
417getAutoHints :: Name -> Idris [Name]
418getAutoHints n = do ist <- getIState
419 case lookupCtxtExact n (idris_autohints ist) of
420 Nothing -> return []
421 Just ns -> return ns
423addIBC :: IBCWrite -> Idris ()
424addIBC ibc@(IBCDef n)
425 = do i <- getIState
426 when (notDef (ibc_write i)) $
427 putIState $ i { ibc_write = ibc : ibc_write i }
428 where notDef [] = True
429 notDef (IBCDef n': is) | n == n' = False
430 notDef (_ : is) = notDef is
431addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
433clearIBC :: Idris ()
434clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
436resetNameIdx :: Idris ()
437resetNameIdx = do i <- getIState
438 put (i { idris_nameIdx = (0, emptyContext) })
440-- Used to preserve sharing of names
441addNameIdx :: Name -> Idris (Int, Name)
442addNameIdx n = do i <- getIState
443 let (i', x) = addNameIdx' i n
444 putIState i'
445 return x
447addNameIdx' :: IState -> Name -> (IState, (Int, Name))
448addNameIdx' i n
449 = let idxs = snd (idris_nameIdx i) in
450 case lookupCtxt n idxs of
451 [x] -> (i, x)
452 _ -> let i' = fst (idris_nameIdx i) + 1 in
453 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
455getSymbol :: Name -> Idris Name
456getSymbol n = do i <- getIState
457 case M.lookup n (idris_symbols i) of
458 Just n' -> return n'
459 Nothing -> do let sym' = M.insert n n (idris_symbols i)
460 put (i { idris_symbols = sym' })
461 return n
463getHdrs :: Codegen -> Idris [String]
464getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
466getImported :: Idris [(FilePath, Bool)]
467getImported = do i <- getIState; return (idris_imported i)
469setErrSpan :: FC -> Idris ()
470setErrSpan x = do i <- getIState;
471 case (errSpan i) of
472 Nothing -> putIState $ i { errSpan = Just x }
473 Just _ -> return ()
475clearErr :: Idris ()
476clearErr = do i <- getIState
477 putIState $ i { errSpan = Nothing }
479getSO :: Idris (Maybe String)
480getSO = do i <- getIState
481 return (compiled_so i)
483setSO :: Maybe String -> Idris ()
484setSO s = do i <- getIState
485 putIState $ (i { compiled_so = s })
487getIState :: Idris IState
488getIState = get
490putIState :: IState -> Idris ()
491putIState = put
493updateIState :: (IState -> IState) -> Idris ()
494updateIState f = do i <- getIState
495 putIState $ f i
497withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
498withContext ctx name dflt action = do
499 ist <- getIState
500 case lookupCtxt name (ctx ist) of
501 [x] -> action x
502 _ -> return dflt
504withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
505withContext_ ctx name action = withContext ctx name () action
507-- | A version of liftIO that puts errors into the exception type of the Idris monad
508runIO :: IO a -> Idris a
509runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
510-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
511--
512-- Issue #1738 on the issue tracker.
513-- https://github.com/idris-lang/Idris-dev/issues/1738
515getName :: Idris Int
516getName = do i <- getIState;
517 let idx = idris_name i;
518 putIState $ (i { idris_name = idx + 1 })
519 return idx
521-- InternalApp keeps track of the real function application for making case splits from, not the application the
522-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
523addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
524addInternalApp fp l t
525 = do i <- getIState
526 -- We canonicalise the path to make "./Test/Module.idr" equal
527 -- to "Test/Module.idr"
528 exists <- runIO $ doesFileExist fp
529 when exists $
530 do fp' <- runIO $ canonicalizePath fp
531 putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
533getInternalApp :: FilePath -> Int -> Idris PTerm
534getInternalApp fp l = do i <- getIState
535 -- We canonicalise the path to make
536 -- "./Test/Module.idr" equal to
537 -- "Test/Module.idr"
538 exists <- runIO $ doesFileExist fp
539 if exists
540 then do fp' <- runIO $ canonicalizePath fp
541 case lookup (fp', l) (idris_lineapps i) of
542 Just n' -> return n'
543 Nothing -> return Placeholder
544 -- TODO: What if it's not there?
545 else return Placeholder
547-- Pattern definitions are only used for coverage checking, so erase them
548-- when we're done
549clearOrigPats :: Idris ()
550clearOrigPats = do i <- get
551 let ps = idris_patdefs i
552 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
553 put (i { idris_patdefs = ps' })
555-- Erase types from Ps in the context (basically ending up with what's in
556-- the .ibc, which is all we need after all the analysis is done)
557clearPTypes :: Idris ()
558clearPTypes = do i <- get
559 let ctxt = tt_ctxt i
560 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
561 where pErase (CaseOp c t tys orig tot cds)
562 = CaseOp c t tys orig [] (pErase' cds)
563 pErase x = x
564 pErase' (CaseDefs _ (cs, c) _ rs)
565 = let c' = (cs, fmap pEraseType c) in
566 CaseDefs c' c' c' rs
568checkUndefined :: FC -> Name -> Idris ()
569checkUndefined fc n
570 = do i <- getContext
571 case lookupTy n i of
572 (_:_) -> throwError . Msg $ show fc ++ ":" ++
573 show n ++ " already defined"
574 _ -> return ()
576isUndefined :: FC -> Name -> Idris Bool
577isUndefined fc n
578 = do i <- getContext
579 case lookupTyExact n i of
580 Just _ -> return False
581 _ -> return True
583setContext :: Context -> Idris ()
584setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
586updateContext :: (Context -> Context) -> Idris ()
587updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
589addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
590addConstraints fc (v, cs)
591 = do i <- getIState
592 let ctxt = tt_ctxt i
593 let ctxt' = ctxt { next_tvar = v }
594 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
595 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
596 where
597 insertAll [] c = c
598 insertAll ((c, fc) : cs) ics
599 = insertAll cs $ S.insert (ConstraintFC c fc) ics
601addDeferred = addDeferred' Ref
602addDeferredTyCon = addDeferred' (TCon 0 0)
604-- | Save information about a name that is not yet defined
605addDeferred' :: NameType
606 -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]
607 -- ^ The Name is the name being made into a metavar,
608 -- the Int is the number of vars that are part of a
609 -- putative proof context, the Maybe Name is the
610 -- top-level function containing the new metavariable,
611 -- the Type is its type, and the Bool is whether :p is
612 -- allowed
613 -> Idris ()
614addDeferred' nt ns
615 = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
616 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
617 i <- getIState
618 putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++
619 idris_metavars i }
620 where
621 -- 'tidyNames' is to generate user accessible names in case they are
622 -- needed in tactic scripts
623 tidyNames used (Bind (MN i x) b sc)
624 = let n' = uniqueNameSet (UN x) used in
625 Bind n' b $ tidyNames (S.insert n' used) sc
626 tidyNames used (Bind n b sc)
627 = let n' = uniqueNameSet n used in
628 Bind n' b $ tidyNames (S.insert n' used) sc
629 tidyNames used b = b
631solveDeferred :: Name -> Idris ()
632solveDeferred n = do i <- getIState
633 putIState $ i { idris_metavars =
634 filter (\(n', _) -> n/=n')
635 (idris_metavars i),
636 ibc_write =
637 filter (notMV n) (ibc_write i)
638 }
639 where notMV n (IBCMetavar n') = not (n == n')
640 notMV n _ = True
642getUndefined :: Idris [Name]
643getUndefined = do i <- getIState
644 return (map fst (idris_metavars i) \\ primDefs)
646isMetavarName :: Name -> IState -> Bool
647isMetavarName n ist
648 = case lookupNames n (tt_ctxt ist) of
649 (t:_) -> isJust $ lookup t (idris_metavars ist)
650 _ -> False
652getWidth :: Idris ConsoleWidth
653getWidth = fmap idris_consolewidth getIState
655setWidth :: ConsoleWidth -> Idris ()
656setWidth w = do ist <- getIState
657 put ist { idris_consolewidth = w }
659setDepth :: Maybe Int -> Idris ()
660setDepth d = do ist <- getIState
661 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
663typeDescription :: String
664typeDescription = "The type of types"
667type1Doc :: Doc OutputAnnotation
668type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
671isetPrompt :: String -> Idris ()
672isetPrompt p = do i <- getIState
673 case idris_outputmode i of
674 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
676-- | Tell clients how much was parsed and loaded
677isetLoadedRegion :: Idris ()
678isetLoadedRegion = do i <- getIState
679 let span = idris_parsedSpan i
680 case span of
681 Just fc ->
682 case idris_outputmode i of
683 IdeMode n h ->
684 runIO . hPutStrLn h $
685 convSExp "set-loaded-region" fc n
686 Nothing -> return ()
688setLogLevel :: Int -> Idris ()
689setLogLevel l = do i <- getIState
690 let opts = idris_options i
691 let opt' = opts { opt_logLevel = l }
692 putIState $ i { idris_options = opt' }
694setCmdLine :: [Opt] -> Idris ()
695setCmdLine opts = do i <- getIState
696 let iopts = idris_options i
697 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
699getCmdLine :: Idris [Opt]
700getCmdLine = do i <- getIState
701 return (opt_cmdline (idris_options i))
703getDumpHighlighting :: Idris Bool
704getDumpHighlighting = do ist <- getIState
705 return (findC (opt_cmdline (idris_options ist)))
706 where findC = elem DumpHighlights
708getDumpDefun :: Idris (Maybe FilePath)
709getDumpDefun = do i <- getIState
710 return $ findC (opt_cmdline (idris_options i))
711 where findC [] = Nothing
712 findC (DumpDefun x : _) = Just x
713 findC (_ : xs) = findC xs
715getDumpCases :: Idris (Maybe FilePath)
716getDumpCases = do i <- getIState
717 return $ findC (opt_cmdline (idris_options i))
718 where findC [] = Nothing
719 findC (DumpCases x : _) = Just x
720 findC (_ : xs) = findC xs
722logLevel :: Idris Int
723logLevel = do i <- getIState
724 return (opt_logLevel (idris_options i))
726setErrContext :: Bool -> Idris ()
727setErrContext t = do i <- getIState
728 let opts = idris_options i
729 let opts' = opts { opt_errContext = t }
730 putIState $ i { idris_options = opts' }
732errContext :: Idris Bool
733errContext = do i <- getIState
734 return (opt_errContext (idris_options i))
736getOptimise :: Idris [Optimisation]
737getOptimise = do i <- getIState
738 return (opt_optimise (idris_options i))
740setOptimise :: [Optimisation] -> Idris ()
741setOptimise newopts = do i <- getIState
742 let opts = idris_options i
743 let opts' = opts { opt_optimise = newopts }
744 putIState $ i { idris_options = opts' }
746addOptimise :: Optimisation -> Idris ()
747addOptimise opt = do opts <- getOptimise
748 setOptimise (nub (opt : opts))
750removeOptimise :: Optimisation -> Idris ()
751removeOptimise opt = do opts <- getOptimise
752 setOptimise ((nub opts) \\ [opt])
754-- Set appropriate optimisation set for the given level. We only have
755-- one optimisation that is configurable at the moment, however!
756setOptLevel :: Int -> Idris ()
757setOptLevel n | n <= 0 = setOptimise []
758setOptLevel 1 = setOptimise []
759setOptLevel 2 = setOptimise [PETransform]
760setOptLevel n | n >= 3 = setOptimise [PETransform]
762useREPL :: Idris Bool
763useREPL = do i <- getIState
764 return (opt_repl (idris_options i))
766setREPL :: Bool -> Idris ()
767setREPL t = do i <- getIState
768 let opts = idris_options i
769 let opt' = opts { opt_repl = t }
770 putIState $ i { idris_options = opt' }
772showOrigErr :: Idris Bool
773showOrigErr = do i <- getIState
774 return (opt_origerr (idris_options i))
776setShowOrigErr :: Bool -> Idris ()
777setShowOrigErr b = do i <- getIState
778 let opts = idris_options i
779 let opt' = opts { opt_origerr = b }
780 putIState $ i { idris_options = opt' }
782setAutoSolve :: Bool -> Idris ()
783setAutoSolve b = do i <- getIState
784 let opts = idris_options i
785 let opt' = opts { opt_autoSolve = b }
786 putIState $ i { idris_options = opt' }
788setNoBanner :: Bool -> Idris ()
789setNoBanner n = do i <- getIState
790 let opts = idris_options i
791 let opt' = opts { opt_nobanner = n }
792 putIState $ i { idris_options = opt' }
794getNoBanner :: Idris Bool
795getNoBanner = do i <- getIState
796 let opts = idris_options i
797 return (opt_nobanner opts)
799setEvalTypes :: Bool -> Idris ()
800setEvalTypes n = do i <- getIState
801 let opts = idris_options i
802 let opt' = opts { opt_evaltypes = n }
803 putIState $ i { idris_options = opt' }
805getDesugarNats :: Idris Bool
806getDesugarNats = do i <- getIState
807 let opts = idris_options i
808 return (opt_desugarnats opts)
811setDesugarNats :: Bool -> Idris ()
812setDesugarNats n = do i <- getIState
813 let opts = idris_options i
814 let opt' = opts { opt_desugarnats = n }
815 putIState $ i { idris_options = opt' }
817setQuiet :: Bool -> Idris ()
818setQuiet q = do i <- getIState
819 let opts = idris_options i
820 let opt' = opts { opt_quiet = q }
821 putIState $ i { idris_options = opt' }
823getQuiet :: Idris Bool
824getQuiet = do i <- getIState
825 let opts = idris_options i
826 return (opt_quiet opts)
828setCodegen :: Codegen -> Idris ()
829setCodegen t = do i <- getIState
830 let opts = idris_options i
831 let opt' = opts { opt_codegen = t }
832 putIState $ i { idris_options = opt' }
834codegen :: Idris Codegen
835codegen = do i <- getIState
836 return (opt_codegen (idris_options i))
838setOutputTy :: OutputType -> Idris ()
839setOutputTy t = do i <- getIState
840 let opts = idris_options i
841 let opt' = opts { opt_outputTy = t }
842 putIState $ i { idris_options = opt' }
844outputTy :: Idris OutputType
845outputTy = do i <- getIState
846 return $ opt_outputTy $ idris_options i
848setIdeMode :: Bool -> Handle -> Idris ()
849setIdeMode True h = do i <- getIState
850 putIState $ i { idris_outputmode = IdeMode 0 h
851 , idris_colourRepl = False
852 }
853setIdeMode False _ = return ()
855setTargetTriple :: String -> Idris ()
856setTargetTriple t = do i <- getIState
857 let opts = idris_options i
858 opt' = opts { opt_triple = t }
859 putIState $ i { idris_options = opt' }
861targetTriple :: Idris String
862targetTriple = do i <- getIState
863 return (opt_triple (idris_options i))
865setTargetCPU :: String -> Idris ()
866setTargetCPU t = do i <- getIState
867 let opts = idris_options i
868 opt' = opts { opt_cpu = t }
869 putIState $ i { idris_options = opt' }
871targetCPU :: Idris String
872targetCPU = do i <- getIState
873 return (opt_cpu (idris_options i))
875verbose :: Idris Bool
876verbose = do i <- getIState
877 -- Quietness overrides verbosity
878 return (not (opt_quiet (idris_options i)) &&
879 opt_verbose (idris_options i))
881setVerbose :: Bool -> Idris ()
882setVerbose t = do i <- getIState
883 let opts = idris_options i
884 let opt' = opts { opt_verbose = t }
885 putIState $ i { idris_options = opt' }
887typeInType :: Idris Bool
888typeInType = do i <- getIState
889 return (opt_typeintype (idris_options i))
891setTypeInType :: Bool -> Idris ()
892setTypeInType t = do i <- getIState
893 let opts = idris_options i
894 let opt' = opts { opt_typeintype = t }
895 putIState $ i { idris_options = opt' }
897coverage :: Idris Bool
898coverage = do i <- getIState
899 return (opt_coverage (idris_options i))
901setCoverage :: Bool -> Idris ()
902setCoverage t = do i <- getIState
903 let opts = idris_options i
904 let opt' = opts { opt_coverage = t }
905 putIState $ i { idris_options = opt' }
907setIBCSubDir :: FilePath -> Idris ()
908setIBCSubDir fp = do i <- getIState
909 let opts = idris_options i
910 let opt' = opts { opt_ibcsubdir = fp }
911 putIState $ i { idris_options = opt' }
913valIBCSubDir :: IState -> Idris FilePath
914valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
916addImportDir :: FilePath -> Idris ()
917addImportDir fp = do i <- getIState
918 let opts = idris_options i
919 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
920 putIState $ i { idris_options = opt' }
922setImportDirs :: [FilePath] -> Idris ()
923setImportDirs fps = do i <- getIState
924 let opts = idris_options i
925 let opt' = opts { opt_importdirs = fps }
926 putIState $ i { idris_options = opt' }
928allImportDirs :: Idris [FilePath]
929allImportDirs = do i <- getIState
930 let optdirs = opt_importdirs (idris_options i)
931 return ("." : reverse optdirs)
933colourise :: Idris Bool
934colourise = do i <- getIState
935 return $ idris_colourRepl i
937setColourise :: Bool -> Idris ()
938setColourise b = do i <- getIState
939 putIState $ i { idris_colourRepl = b }
941impShow :: Idris Bool
942impShow = do i <- getIState
943 return (opt_showimp (idris_options i))
945setImpShow :: Bool -> Idris ()
946setImpShow t = do i <- getIState
947 let opts = idris_options i
948 let opt' = opts { opt_showimp = t }
949 putIState $ i { idris_options = opt' }
951setColour :: ColourType -> IdrisColour -> Idris ()
952setColour ct c = do i <- getIState
953 let newTheme = setColour' ct c (idris_colourTheme i)
954 putIState $ i { idris_colourTheme = newTheme }
955 where setColour' KeywordColour c t = t { keywordColour = c }
956 setColour' BoundVarColour c t = t { boundVarColour = c }
957 setColour' ImplicitColour c t = t { implicitColour = c }
958 setColour' FunctionColour c t = t { functionColour = c }
959 setColour' TypeColour c t = t { typeColour = c }
960 setColour' DataColour c t = t { dataColour = c }
961 setColour' PromptColour c t = t { promptColour = c }
962 setColour' PostulateColour c t = t { postulateColour = c }
964logLvl :: Int -> String -> Idris ()
965logLvl l str = do i <- getIState
966 let lvl = opt_logLevel (idris_options i)
967 when (lvl >= l) $
968 case idris_outputmode i of
969 RawOutput h -> do runIO $ hPutStrLn h str
970 IdeMode n h ->
971 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
972 runIO . hPutStrLn h $ convSExp "log" good n
974cmdOptType :: Opt -> Idris Bool
975cmdOptType x = do i <- getIState
976 return $ x `elem` opt_cmdline (idris_options i)
978noErrors :: Idris Bool
979noErrors = do i <- getIState
980 case errSpan i of
981 Nothing -> return True
982 _ -> return False
984setTypeCase :: Bool -> Idris ()
985setTypeCase t = do i <- getIState
986 let opts = idris_options i
987 let opt' = opts { opt_typecase = t }
988 putIState $ i { idris_options = opt' }
991-- Dealing with parameters
993expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
994 [Name] -> -- all names
995 [Name] -> -- names with no declaration
996 PTerm -> PTerm
997expandParams dec ps ns infs tm = en 0 tm
998 where
999 -- if we shadow a name (say in a lambda binding) that is used in a call to
1000 -- a lifted function, we need access to both names - once in the scope of the
1001 -- binding and once to call the lifted functions. So we'll explicitly shadow
1002 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1003 -- but we didn't...)
1005 mkShadow (UN n) = MN 0 n
1006 mkShadow (MN i n) = MN (i+1) n
1007 mkShadow (NS x s) = NS (mkShadow x) s
1009 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1010 -- that are merely mentioned.
1011 -> PTerm -> PTerm
1012 en 0 (PLam fc n nfc t s)
1013 | n `elem` (map fst ps ++ ns)
1014 = let n' = mkShadow n in
1015 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1016 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1017 en 0 (PPi p n nfc t s)
1018 | n `elem` (map fst ps ++ ns)
1019 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1020 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1021 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1022 en 0 (PLet fc n nfc ty v s)
1023 | n `elem` (map fst ps ++ ns)
1024 = let n' = mkShadow n in
1025 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1026 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1027 -- FIXME: Should only do this in a type signature!
1028 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1029 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1030 = let n' = mkShadow n in
1031 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1032 en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1033 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1034 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1035 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1036 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1037 en 0 (PHidden t) = PHidden (en 0 t)
1038 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1039 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1040 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1041 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1042 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1043 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1045 en 0 (PQuote (Var n))
1046 | n `nselem` ns = PQuote (Var (dec n))
1047 en 0 (PApp fc (PInferRef fc' hl n) as)
1048 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1049 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1050 en 0 (PApp fc (PRef fc' hl n) as)
1051 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1052 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1053 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1054 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1055 en 0 (PAppBind fc (PRef fc' hl n) as)
1056 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1057 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1058 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1059 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1060 en 0 (PRef fc hl n)
1061 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1062 (map (pexp . (PRef fc hl)) (map fst ps))
1063 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1064 (map (pexp . (PRef fc hl)) (map fst ps))
1065 en 0 (PInferRef fc hl n)
1066 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1067 (map (pexp . (PRef fc hl)) (map fst ps))
1068 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1069 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1070 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1071 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1072 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1073 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1075 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1076 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1078 en ql t = descend (en ql) t
1080 nselem x [] = False
1081 nselem x (y : xs) | nseq x y = True
1082 | otherwise = nselem x xs
1084 nseq x y = nsroot x == nsroot y
1086 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1087 enTacImp ql other = other
1089expandParamsD :: Bool -> -- True = RHS only
1090 IState ->
1091 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1092expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1093 = if n `elem` ns && (not rhsonly)
1094 then -- trace (show (n, expandParams dec ps ns ty)) $
1095 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1096 else --trace (show (n, expandParams dec ps ns ty)) $
1097 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1098expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1099 = if n `elem` ns && (not rhsonly)
1100 then -- trace (show (n, expandParams dec ps ns ty)) $
1101 PPostulate e doc syn fc nfc o (dec n)
1102 (piBind ps (expandParams dec ps ns [] ty))
1103 else --trace (show (n, expandParams dec ps ns ty)) $
1104 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1105expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1106 = let n' = if n `elem` ns then dec n else n in
1107 PClauses fc opts n' (map expandParamsC cs)
1108 where
1109 expandParamsC (PClause fc n lhs ws rhs ds)
1110 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1111 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1112 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1113 n' = if n `elem` ns then dec n else n
1114 -- names bound on the lhs should not be expanded on the rhs
1115 ns' = removeBound lhs ns in
1116 PClause fc n' lhs'
1117 (map (expandParams dec ps'' ns' []) ws)
1118 (expandParams dec ps'' ns' [] rhs)
1119 (map (expandParamsD True ist dec ps'' ns') ds)
1120 expandParamsC (PWith fc n lhs ws wval pn ds)
1121 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1122 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1123 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1124 n' = if n `elem` ns then dec n else n
1125 ns' = removeBound lhs ns in
1126 PWith fc n' lhs'
1127 (map (expandParams dec ps'' ns' []) ws)
1128 (expandParams dec ps'' ns' [] wval)
1129 pn
1130 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1131 updateps yn nm [] = []
1132 updateps yn nm (((a, t), i):as)
1133 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1134 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1136 removeBound lhs ns = ns \\ nub (bnames lhs)
1138 bnames (PRef _ _ n) = [n]
1139 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1140 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1141 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1142 bnames _ = []
1144-- | Expands parameters defined in parameter and where blocks inside of declarations
1145expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1146 = PData doc argDocs syn fc co (expandPData pd)
1147 where
1148 -- just do the type decl, leave constructors alone (parameters will be
1149 -- added implicitly)
1150 expandPData (PDatadecl n nfc ty cons)
1151 = if n `elem` ns
1152 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1153 (map econ cons)
1154 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1155 econ (doc, argDocs, n, nfc, t, fc, fs)
1156 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1157expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1158 = d
1159expandParamsD rhs ist dec ps ns (PParams f params pds)
1160 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1161 (map (expandParamsD True ist dec ps ns) pds)
1162-- (map (expandParamsD ist dec ps ns) pds)
1163expandParamsD rhs ist dec ps ns (PMutual f pds)
1164 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1165expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1166 = PClass doc info f
1167 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1168 n nfc
1169 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1170 pDocs
1171 fds
1172 (map (expandParamsD rhs ist dec ps ns) decls)
1173 cn
1174 cd
1175expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)
1176 = PInstance doc argDocs info f
1177 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1179 nfc
1180 (map (expandParams dec ps ns []) params)
1181 (expandParams dec ps ns [] ty)
1182 cn
1183 (map (expandParamsD rhs ist dec ps ns) decls)
1184expandParamsD rhs ist dec ps ns d = d
1186mapsnd f (x, t) = (x, f t)
1188-- Calculate a priority for a type, for deciding elaboration order
1189-- * if it's just a type variable or concrete type, do it early (0)
1190-- * if there's only type variables and injective constructors, do it next (1)
1191-- * if there's a function type, next (2)
1192-- * finally, everything else (3)
1194getPriority :: IState -> PTerm -> Int
1195getPriority i tm = 1 -- pri tm
1196 where
1197 pri (PRef _ _ n) =
1198 case lookupP n (tt_ctxt i) of
1199 ((P (DCon _ _ _) _ _):_) -> 1
1200 ((P (TCon _ _) _ _):_) -> 1
1201 ((P Ref _ _):_) -> 1
1202 [] -> 0 -- must be locally bound, if it's not an error...
1203 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1204 pri (PTrue _ _) = 0
1205 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1206 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1207 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1208 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1209 pri (PTyped l r) = pri l
1210 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1211 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1212 pri (PAlternative _ a as) = maximum (map pri as)
1213 pri (PConstant _ _) = 0
1214 pri Placeholder = 1
1215 pri _ = 3
1218addStatics :: Name -> Term -> PTerm -> Idris ()
1219addStatics n tm ptm =
1220 do let (statics, dynamics) = initStatics tm ptm
1221 ist <- getIState
1222 let paramnames
1223 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1224 Just p -> getNamesFrom 0 (fn_params p) tm ++
1225 concatMap (getParamNames ist) (map snd statics)
1226 _ -> concatMap (getParamNames ist) (map snd statics)
1228 let stnames = nub $ concatMap freeArgNames (map snd statics)
1229 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1230 \\ paramnames
1231 -- also get the arguments which are 'uniquely inferrable' from
1232 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1233 -- or parameters to the type of a static
1234 let statics' = nub $ map fst statics ++
1235 filter (\x -> not (elem x dnames)) stnames
1236 let stpos = staticList statics' tm
1237 i <- getIState
1238 when (not (null statics)) $
1239 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1240 ++ showTmImpls ptm ++ "\n"
1241 ++ show statics ++ "\n" ++ show dynamics
1242 ++ "\n" ++ show paramnames
1243 ++ "\n" ++ show stpos
1244 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1245 addIBC (IBCStatic n)
1246 where
1247 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1248 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1249 (static, (n, ty) : dynamic)
1250 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1251 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1252 if pstatic p == Static then ((n, ty) : static, dynamic)
1253 else if (not (searchArg p))
1254 then (static, (n, ty) : dynamic)
1255 else (static, dynamic)
1256 initStatics t pt = ([], [])
1258 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1259 = case lookupCtxtExact n (idris_datatypes ist) of
1260 Just ti -> getNamePos 0 (param_pos ti) args
1261 Nothing -> []
1262 where getNamePos i ps [] = []
1263 getNamePos i ps (P _ n _ : as)
1264 | i `elem` ps = n : getNamePos (i + 1) ps as
1265 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1266 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1267 = n : getParamNames ist sc
1268 getParamNames ist _ = []
1270 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1271 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1272 | otherwise = getNamesFrom (i + 1) ps sc
1273 getNamesFrom i ps sc = []
1275 freeArgNames (Bind n (Pi _ ty _) sc)
1276 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1277 freeArgNames tm = let (_, args) = unApply tm in
1278 concatMap freeNames args
1280 -- if a name appears in a type class or tactic implicit index, it doesn't
1281 -- affect its 'uniquely inferrable' from a static status since these are
1282 -- resolved by searching.
1283 searchArg (Constraint _ _) = True
1284 searchArg (TacImp _ _ _) = True
1285 searchArg _ = False
1287 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1288 staticList _ _ = []
1290-- Dealing with implicit arguments
1292-- Add some bound implicits to the using block if they aren't there already
1294addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1295addToUsing us [] = us
1296addToUsing us ((n, t) : ns)
1297 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1298 | otherwise = addToUsing us ns
1299 where impName (UImplicit n _) = Just n
1300 impName _ = Nothing
1302-- Add constraint bindings from using block
1304addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1305addUsingConstraints syn fc t
1306 = do ist <- get
1307 let ns = namesIn [] ist t
1308 let cs = getConstraints t -- check declared constraints
1309 let addconsts = uconsts \\ cs
1310 return (doAdd addconsts ns t)
1311 where uconsts = filter uconst (using syn)
1312 uconst (UConstraint _ _) = True
1313 uconst _ = False
1315 doAdd [] _ t = t
1316 -- if all of args in ns, then add it
1317 doAdd (UConstraint c args : cs) ns t
1318 | all (\n -> elem n ns) args
1319 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1320 (mkConst c args) (doAdd cs ns t)
1321 | otherwise = doAdd cs ns t
1323 mkConst c args = PApp fc (PRef fc [] c)
1324 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc [] n)) args)
1326 getConstraints (PPi (Constraint _ _) _ _ c sc)
1327 = getcapp c ++ getConstraints sc
1328 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1329 getConstraints _ = []
1331 getcapp (PApp _ (PRef _ _ c) args)
1332 = do ns <- mapM getName args
1333 return (UConstraint c ns)
1334 getcapp _ = []
1336 getName (PExp _ _ _ (PRef _ _ n)) = return n
1337 getName _ = []
1339-- Add implicit bindings from using block, and bind any missing names
1340addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1341addUsingImpls syn n fc t
1342 = do ist <- getIState
1343 let ns = implicitNamesIn (map iname uimpls) ist t
1344 let badnames = filter (\n -> not (implicitable n) &&
1345 n `notElem` (map iname uimpls)) ns
1346 when (not (null badnames)) $
1347 throwError (At fc (Elaborating "type of " n
1348 (NoSuchVariable (head badnames))))
1349 let cs = getArgnames t -- get already bound names
1350 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1351 -- if all names in the arguments of addconsts appear in ns,
1352 -- add the constraint implicitly
1353 return (bindFree ns (doAdd addimpls ns t))
1354 where uimpls = filter uimpl (using syn)
1355 uimpl (UImplicit _ _) = True
1356 uimpl _ = False
1358 iname (UImplicit n _) = n
1359 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1361 doAdd [] _ t = t
1362 -- if all of args in ns, then add it
1363 doAdd (UImplicit n ty : cs) ns t
1364 | elem n ns
1365 = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)
1366 | otherwise = doAdd cs ns t
1368 -- bind the free names which weren't in the using block
1369 bindFree [] tm = tm
1370 bindFree (n:ns) tm
1371 | elem n (map iname uimpls) = bindFree ns tm
1372 | otherwise
1373 = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1375 getArgnames (PPi _ n _ c sc)
1376 = n : getArgnames sc
1377 getArgnames _ = []
1379-- Given the original type and the elaborated type, return the implicitness
1380-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1382getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1383getUnboundImplicits i t tm = getImps t (collectImps tm)
1384 where collectImps (PPi p n _ t sc)
1385 = (n, (p, t)) : collectImps sc
1386 collectImps _ = []
1388 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1389 getImps (Bind n (Pi _ t _) sc) imps
1390 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1391 where
1392 argInfo n (Imp opt _ _ _) Placeholder
1393 = (True, PImp 0 True opt n Placeholder)
1394 argInfo n (Imp opt _ _ _) t'
1395 = (False, PImp (getPriority i t') True opt n t')
1396 argInfo n (Exp opt _ _) t'
1397 = (InaccessibleArg `elem` opt,
1398 PExp (getPriority i t') opt n t')
1399 argInfo n (Constraint opt _) t'
1400 = (InaccessibleArg `elem` opt,
1401 PConstraint 10 opt n t')
1402 argInfo n (TacImp opt _ scr) t'
1403 = (InaccessibleArg `elem` opt,
1404 PTacImplicit 10 opt n scr t')
1405 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1406 where impBind n t = (True, PImp 1 True [] n Placeholder)
1407 getImps sc tm = []
1409-- Add implicit Pi bindings for any names in the term which appear in an
1410-- argument position.
1412-- This has become a right mess already. Better redo it some time...
1413-- TODO: This is obsoleted by the new way of elaborating types, (which
1414-- calls addUsingImpls) but there's still a couple of places which use
1415-- it. Clean them up!
1417-- Issue 1739 in the issue tracker
1418-- https://github.com/idris-lang/Idris-dev/issues/1739
1419implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1420implicit info syn n ptm = implicit' info syn [] n ptm
1422implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1423implicit' info syn ignore n ptm
1424 = do i <- getIState
1425 let (tm', impdata) = implicitise syn ignore i ptm
1426 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1427-- let (tm'', spos) = findStatics i tm'
1428 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1429 addIBC (IBCImp n)
1430 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1431-- i <- get
1432-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1433 return tm'
1434 where
1435 -- Detect unknown names in default arguments and throw error if found.
1436 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1437 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1439 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1440 notFoundInDefault kns (PTacImplicit _ _ n script _)
1441 = do i <- getIState
1442 case notFound kns (namesIn [] i script) of
1443 Nothing -> return (n:kns)
1444 Just name -> throwError (NoSuchVariable name)
1445 notFoundInDefault kns p = return ((pname p):kns)
1447 notFound :: [Name] -> [Name] -> Maybe Name
1448 notFound kns [] = Nothing
1449 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1450 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1452implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1453implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1454 let (declimps, ns') = execState (imps True [] tm) ([], [])
1455 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1456 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1457 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1458 if null ns
1459 then (tm, reverse declimps)
1460 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1461 where
1462 uvars = map ipair (filter uimplicit (using syn))
1463 pvars = syn_params syn
1465 inUsing n = n `elem` map fst uvars
1467 ipair (UImplicit x y) = (x, y)
1468 uimplicit (UImplicit _ _) = True
1469 uimplicit _ = False
1471 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1472 | otherwise = x : dropAll xs ys
1473 dropAll [] ys = []
1475 -- Find names in argument position in a type, suitable for implicit
1476 -- binding
1477 -- Not the function position, but do everything else...
1478 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1479 implNamesIn uv t = namesIn uv ist t
1481 imps top env (PApp _ f as)
1482 = do (decls, ns) <- get
1483 let isn = concatMap (namesIn uvars ist) (map getTm as)
1484 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1485 imps top env (PPi (Imp l _ _ _) n _ ty sc)
1486 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1487 (decls , ns) <- get
1488 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1489 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1490 imps True (n:env) sc
1491 imps top env (PPi (Exp l _ _) n _ ty sc)
1492 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1493 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1494 _ -> [])
1495 (decls, ns) <- get -- ignore decls in HO types
1496 put (PExp (getPriority ist ty) l n Placeholder : decls,
1497 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1498 imps True (n:env) sc
1499 imps top env (PPi (Constraint l _) n _ ty sc)
1500 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1501 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1502 _ -> [])
1503 (decls, ns) <- get -- ignore decls in HO types
1504 put (PConstraint 10 l n Placeholder : decls,
1505 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1506 imps True (n:env) sc
1507 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1508 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1509 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1510 _ -> [])
1511 (decls, ns) <- get -- ignore decls in HO types
1512 put (PTacImplicit 10 l n scr Placeholder : decls,
1513 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1514 imps True (n:env) sc
1515 imps top env (PRewrite _ l r _)
1516 = do (decls, ns) <- get
1517 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1518 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1519 imps top env (PTyped l r)
1520 = imps top env l
1521 imps top env (PPair _ _ _ l r)
1522 = do (decls, ns) <- get
1523 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1524 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1525 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1526 = do (decls, ns) <- get
1527 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1528 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1529 imps top env (PDPair _ _ _ l t r)
1530 = do (decls, ns) <- get
1531 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1532 namesIn uvars ist r
1533 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1534 imps top env (PAlternative ms a as)
1535 = do (decls, ns) <- get
1536 let isn = concatMap (namesIn uvars ist) as
1537 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1538 imps top env (PLam fc n _ ty sc)
1539 = do imps False env ty
1540 imps False (n:env) sc
1541 imps top env (PHidden tm) = imps False env tm
1542 imps top env (PUnifyLog tm) = imps False env tm
1543 imps top env (PNoImplicits tm) = imps False env tm
1544 imps top env (PRunElab fc tm ns) = imps False env tm
1545 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1546 imps top env _ = return ()
1548 pibind using [] sc = sc
1549 pibind using (n:ns) sc
1550 = case lookup n using of
1551 Just ty -> PPi (Imp [] Dynamic False Nothing)
1552 n NoFC ty (pibind using ns sc)
1553 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)
1554 n NoFC Placeholder (pibind using ns sc)
1556-- Add implicit arguments in function calls
1557addImplPat :: IState -> PTerm -> PTerm
1558addImplPat = addImpl' True [] [] []
1560addImplBound :: IState -> [Name] -> PTerm -> PTerm
1561addImplBound ist ns = addImpl' False ns [] [] ist
1563addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1564addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1566-- | Add the implicit arguments to applications in the term
1567-- [Name] gives the names to always expend, even when under a binder of
1568-- that name (this is to expand methods with implicit arguments in dependent
1569-- type classes).
1570addImpl :: [Name] -> IState -> PTerm -> PTerm
1571addImpl = addImpl' False [] []
1573-- TODO: in patterns, don't add implicits to function names guarded by constructors
1574-- and *not* inside a PHidden
1576addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1577addImpl' inpat env infns imp_meths ist ptm
1578 = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1579 where
1580 topname = case ptm of
1581 PRef _ _ n -> n
1582 PApp _ (PRef _ _ n) _ -> n
1583 _ -> sUN "" -- doesn't matter then
1585 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1586 ai inpat qq env ds (PRef fc fcs f)
1587 | f `elem` infns = PInferRef fc fcs f
1588 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] []
1589 ai inpat qq env ds (PHidden (PRef fc hl f))
1590 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] [])
1591 ai inpat qq env ds (PRewrite fc l r g)
1592 = let l' = ai inpat qq env ds l
1593 r' = ai inpat qq env ds r
1594 g' = fmap (ai inpat qq env ds) g in
1595 PRewrite fc l' r' g'
1596 ai inpat qq env ds (PTyped l r)
1597 = let l' = ai inpat qq env ds l
1598 r' = ai inpat qq env ds r in
1599 PTyped l' r'
1600 ai inpat qq env ds (PPair fc hls p l r)
1601 = let l' = ai inpat qq env ds l
1602 r' = ai inpat qq env ds r in
1603 PPair fc hls p l' r'
1604 ai inpat qq env ds (PDPair fc hls p l t r)
1605 = let l' = ai inpat qq env ds l
1606 t' = ai inpat qq env ds t
1607 r' = ai inpat qq env ds r in
1608 PDPair fc hls p l' t' r'
1609 ai inpat qq env ds (PAlternative ms a as)
1610 = let as' = map (ai inpat qq env ds) as in
1611 PAlternative ms a as'
1612 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1613 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1614 = let as' = map (fmap (ai inpat qq env ds)) as in
1615 PApp fc (PInferRef ffc hl f) as'
1616 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1617 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1618 | not (f `elem` map fst env)
1619 = let as' = map (fmap (ai inpat qq env ds)) as
1620 asdotted' = map (fmap (ai False qq env ds)) as in
1621 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'
1622 | Just (Just ty) <- lookup f env =
1623 let as' = map (fmap (ai inpat qq env ds)) as
1624 arity = getPArity ty in
1625 mkPApp fc arity ftm as'
1626 ai inpat qq env ds (PApp fc f as)
1627 = let f' = ai inpat qq env ds f
1628 as' = map (fmap (ai inpat qq env ds)) as in
1629 mkPApp fc 1 f' as'
1630 ai inpat qq env ds (PCase fc c os)
1631 = let c' = ai inpat qq env ds c in
1632 -- leave os alone, because they get lifted into a new pattern match
1633 -- definition which is passed through addImpl agai inpatn with more scope
1634 -- information
1635 PCase fc c' os
1637 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1638 (ai inpat qq env ds t)
1639 (ai inpat qq env ds f)
1641 -- If the name in a lambda is a constructor name, do this as a 'case'
1642 -- instead (it is harmless to do so, especially since the lambda will
1643 -- be lifted anyway!)
1644 ai inpat qq env ds (PLam fc n nfc ty sc)
1645 = case lookupDef n (tt_ctxt ist) of
1646 [] -> let ty' = ai inpat qq env ds ty
1647 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1648 PLam fc n nfc ty' sc'
1649 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1650 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1651 [(PRef fc [] n, sc)]))
1652 ai inpat qq env ds (PLet fc n nfc ty val sc)
1653 = case lookupDef n (tt_ctxt ist) of
1654 [] -> let ty' = ai inpat qq env ds ty
1655 val' = ai inpat qq env ds val
1656 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1657 PLet fc n nfc ty' val' sc'
1658 defs ->
1659 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1660 ai inpat qq env ds (PPi p n nfc ty sc)
1661 = let ty' = ai inpat qq env ds ty
1662 env' = if n `elem` imp_meths then env
1663 else ((n, Just ty) : env)
1664 sc' = ai inpat qq env' ds sc in
1665 PPi p n nfc ty' sc'
1666 ai inpat qq env ds (PGoal fc r n sc)
1667 = let r' = ai inpat qq env ds r
1668 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1669 PGoal fc r' n sc'
1670 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1671 -- Don't do PProof or PTactics since implicits get added when scope is
1672 -- properly known in ElabTerm.runTac
1673 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1674 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1675 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1676 (fmap (ai inpat True env ds) g)
1677 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1678 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1679 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1680 ai inpat qq env ds tm = tm
1682 handleErr (Left err) = PElabError err
1683 handleErr (Right x) = x
1685-- if in a pattern, and there are no arguments, and there's no possible
1686-- names with zero explicit arguments, don't add implicits.
1688aiFn :: Name -> Bool -> Bool -> Bool
1689 -> [Name]
1690 -> IState -> FC
1691 -> Name -- ^ function being applied
1692 -> FC -> [[T.Text]]
1693 -> [PArg] -- ^ initial arguments (if in a pattern)
1694 -> [PArg] -- ^ initial arguments (if in an expression)
1695 -> Either Err PTerm
1696aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _
1697 = case lookupDef f (tt_ctxt ist) of
1698 [] -> Right $ PPatvar ffc f
1699 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1700 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1701 if (not (vname f) || tcname f
1702 || any (conCaf (tt_ctxt ist)) ialts)
1703-- any constructor alts || any allImp ialts))
1704 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor
1705 else Right $ PPatvar ffc f
1706 where imp (PExp _ _ _ _) = False
1707 imp _ = True
1708-- allImp [] = False
1709 allImp xs = all imp xs
1710 constructor (TyDecl (DCon _ _ _) _) = True
1711 constructor _ = False
1713 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1715 vname (UN n) = True -- non qualified
1716 vname _ = False
1718aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1719 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1720aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1721 -- This is where namespaces get resolved by adding PAlternative
1722 = do let ns = lookupCtxtName f (idris_implicits ist)
1723 let nh = filter (\(n, _) -> notHidden n) ns
1724 let ns' = case trimAlts ds nh of
1725 [] -> nh
1726 x -> x
1727 case ns' of
1728 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1729 (insertImpl ns (chooseArgs f' as asexp))
1730 [] -> if f `elem` (map fst (idris_metavars ist))
1731 then Right $ PApp fc (PRef ffc [ffc] f) as
1732 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1733 alts -> Right $
1734 PAlternative [] (ExactlyOne True) $
1735 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1736 (insertImpl ns (chooseArgs f' as asexp))) alts
1737 where
1738 -- choose whether to treat the arguments as patterns or expressions
1739 -- if 'f' is a defined function, treat as expression, otherwise do the default.
1740 -- This is so any names which later go under a PHidden are treated
1741 -- as function names rather than bound pattern variables
1742 chooseArgs f as asexp | isConName f (tt_ctxt ist) = as
1743 | f == topname = as
1744 | Nothing <- lookupDefExact f (tt_ctxt ist) = as
1745 | otherwise = asexp
1747 -- if the name is in imp_meths, we should actually refer to the bound
1748 -- name rather than the global one after expanding implicits
1749 isImpName f f' | f `elem` imp_meths = f
1750 | otherwise = f'
1752 trimAlts [] alts = alts
1753 trimAlts ns alts
1754 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1756 nspace (NS _ s) = s
1757 nspace _ = []
1759 notHidden n = case getAccessibility n of
1760 Hidden -> False
1761 _ -> True
1763 getAccessibility n
1764 = case lookupDefAccExact n False (tt_ctxt ist) of
1765 Just (n,t) -> t
1766 _ -> Public
1768 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1769 -> [PArg] -- ^ given arguments
1770 -> [PArg]
1771 insertImpl ps as
1772 = let (as', badimpls) = partition (impIn ps) as in
1773 map addUnknownImp badimpls ++
1774 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1776 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1777 -> [PArg] -- parameters
1778 -> [PArg] -- explicit arguments
1779 -> [PArg] -- implicits given
1780 -> [PArg]
1781 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1782 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1783 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1784 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1785 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1786 let rtc = PResolveTC fc in
1787 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1788 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1789 case find n imps [] of
1790 Just (tm, imps') ->
1791 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1792 Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in
1793 PImp p True l n ph :
1794 insImpAcc (M.insert n ph pnas) ps given imps
1795 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1796 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1797 case find n imps [] of
1798 Just (tm, imps') ->
1799 PTacImplicit p l n sc tm :
1800 insImpAcc (M.insert n tm pnas) ps given imps'
1801 Nothing ->
1802 if inpat
1803 then PTacImplicit p l n sc Placeholder :
1804 insImpAcc (M.insert n Placeholder pnas) ps given imps
1805 else PTacImplicit p l n sc sc :
1806 insImpAcc (M.insert n sc pnas) ps given imps
1807 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1808 insImpAcc _ _ given imps = given ++ imps
1810 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1812 find n [] acc = Nothing
1813 find n (PImp _ _ _ n' t : gs) acc
1814 | n == n' = Just (t, reverse acc ++ gs)
1815 find n (PTacImplicit _ _ n' _ t : gs) acc
1816 | n == n' = Just (t, reverse acc ++ gs)
1817 find n (g : gs) acc = find n gs (g : acc)
1819-- return True if the second argument is an implicit argument which is
1820-- expected in the implicits, or if it's not an implicit
1821impIn :: [PArg] -> PArg -> Bool
1822impIn ps (PExp _ _ _ _) = True
1823impIn ps (PConstraint _ _ _ _) = True
1824impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1826expArg (PExp _ _ _ _) = True
1827expArg (PConstraint _ _ _ _) = True
1828expArg _ = False
1830-- replace non-linear occurrences with _
1832stripLinear :: IState -> PTerm -> PTerm
1833stripLinear i tm = evalState (sl tm) [] where
1834 sl :: PTerm -> State [Name] PTerm
1835 sl (PRef fc hl f)
1836 | (_:_) <- lookupTy f (tt_ctxt i)
1837 = return $ PRef fc hl f
1838 | otherwise = do ns <- get
1839 if (f `elem` ns)
1840 then return $ PHidden (PRef fc hl f) -- Placeholder
1841 else do put (f : ns)
1842 return (PRef fc hl f)
1843 sl (PPatvar fc f)
1844 = do ns <- get
1845 if (f `elem` ns)
1846 then return $ PHidden (PPatvar fc f) -- Placeholder
1847 else do put (f : ns)
1848 return (PPatvar fc f)
1849 -- Assumption is that variables are all the same in each alternative
1850 sl t@(PAlternative ms b as) = do ns <- get
1851 as' <- slAlts ns as
1852 return (PAlternative ms b as')
1853 where slAlts ns (a : as) = do put ns
1854 a' <- sl a
1855 as' <- slAlts ns as
1856 return (a' : as')
1857 slAlts ns [] = return []
1858 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1859 sl (PDPair fc hls p l t r) = do l' <- sl l
1860 t' <- sl t
1861 r' <- sl r
1862 return (PDPair fc hls p l' t' r')
1863 sl (PApp fc fn args) = do fn' <- case fn of
1864 -- Just the args, fn isn't matchable as a var
1865 PRef _ _ _ -> return fn
1866 t -> sl t
1867 args' <- mapM slA args
1868 return $ PApp fc fn' args'
1869 where slA (PImp p m l n t) = do t' <- sl t
1870 return $ PImp p m l n t'
1871 slA (PExp p l n t) = do t' <- sl t
1872 return $ PExp p l n t'
1873 slA (PConstraint p l n t)
1874 = do t' <- sl t
1875 return $ PConstraint p l n t'
1876 slA (PTacImplicit p l n sc t)
1877 = do t' <- sl t
1878 return $ PTacImplicit p l n sc t'
1879 sl x = return x
1881-- | Remove functions which aren't applied to anything, which must then
1882-- be resolved by unification. Assume names resolved and alternatives
1883-- filled in (so no ambiguity).
1884stripUnmatchable :: IState -> PTerm -> PTerm
1885stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1886 su :: PTerm -> PTerm
1887 su tm@(PRef fc hl f)
1888 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1889 = Placeholder
1890 | (TType _ : _) <- lookupTy f (tt_ctxt i)
1891 = PHidden tm
1892 | (UType _ : _) <- lookupTy f (tt_ctxt i)
1893 = PHidden tm
1894 su (PApp fc f@(PRef _ _ fn) args)
1895 -- here we use canBeDConName because the impossible pattern
1896 -- check will not necessarily fully resolve constructor names,
1897 -- and these bare names will otherwise get in the way of
1898 -- impossbility checking.
1899 | canBeDConName fn ctxt
1900 = PApp fc f (fmap (fmap su) args)
1901 su (PApp fc f args)
1902 = PHidden (PApp fc f args)
1903 su (PAlternative ms b alts)
1904 = let alts' = filter (/= Placeholder) (map su alts) in
1905 if null alts' then Placeholder
1906 else PAlternative ms b alts'
1907 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
1908 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
1909 su t@(PLam fc _ _ _ _) = PHidden t
1910 su t@(PPi _ _ _ _ _) = PHidden t
1911 su t@(PConstant _ c) | isTypeConst c = PHidden t
1912 su t = t
1914 ctxt = tt_ctxt i
1916stripUnmatchable i tm = tm
1918mkPApp fc a f [] = f
1919mkPApp fc a f as = let rest = drop a as in
1920 if a == 0 then appRest fc f rest
1921 else appRest fc (PApp fc f (take a as)) rest
1922 where
1923 appRest fc f [] = f
1924 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1926-- Find 'static' argument positions
1927-- (the declared ones, plus any names in argument position in the declared
1928-- statics)
1929-- FIXME: It's possible that this really has to happen after elaboration
1931findStatics :: IState -> PTerm -> (PTerm, [Bool])
1932findStatics ist tm = let (ns, ss) = fs tm
1933 in runState (pos ns ss tm) []
1934 where fs (PPi p n fc t sc)
1935 | Static <- pstatic p
1936 = let (ns, ss) = fs sc in
1937 (namesIn [] ist t : ns, n : ss)
1938 | otherwise = let (ns, ss) = fs sc in
1939 (ns, ss)
1940 fs _ = ([], [])
1942 inOne n ns = length (filter id (map (elem n) ns)) == 1
1944 pos ns ss (PPi p n fc t sc)
1945 | elem n ss = do sc' <- pos ns ss sc
1946 spos <- get
1947 put (True : spos)
1948 return (PPi (p { pstatic = Static }) n fc t sc')
1949 | otherwise = do sc' <- pos ns ss sc
1950 spos <- get
1951 put (False : spos)
1952 return (PPi p n fc t sc')
1953 pos ns ss t = return t
1955-- for 6.12/7 compatibility
1956data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1958instance Applicative (EitherErr a) where
1959 pure = return
1960 (<*>) = ap
1962instance Monad (EitherErr a) where
1963 return = RightOK
1965 (LeftErr e) >>= k = LeftErr e
1966 RightOK v >>= k = k v
1968toEither (LeftErr e) = Left e
1969toEither (RightOK ho) = Right ho
1971-- | Syntactic match of a against b, returning pair of variables in a
1972-- and what they match. Returns the pair that failed if not a match.
1973matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1974matchClause = matchClause' False
1976matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1977matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1978 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1980 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1981 fullApp x = x
1983 match' x y = match (fullApp x) (fullApp y)
1984 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
1985 | fi == txt "fromInteger" && b == txt "builtins",
1986 PConstant _ (I _) <- getTm x = match (getTm x) x'
1987 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
1988 | fi == txt "fromInteger" && b == txt "builtins",
1989 PConstant _ (I _) <- getTm x = match (getTm x) x'
1990 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1991 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1992 match (PApp _ f args) (PApp _ f' args')
1993 | length args == length args'
1994 = do mf <- match' f f'
1995 ms <- zipWithM matchArg args args'
1996 return (mf ++ concat ms)
1997 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
1998 match (PPatvar f n) xr = match (PRef f [f] n) xr
1999 match xr (PPatvar f n) = match xr (PRef f [f] n)
2000 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2001 match (PRef _ _ n) tm@(PRef _ _ n')
2002 | n == n' && not names &&
2003 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2004 || tm == Placeholder)
2005 = return [(n, tm)]
2006 -- if one namespace is missing, drop the other
2007 | n == n' || n == dropNS n' || dropNS n == n' = return []
2008 where dropNS (NS n _) = n
2009 dropNS n = n
2010 match (PRef _ _ n) tm
2011 | not names && (not (isConName n (tt_ctxt i) ||
2012 isFnName n (tt_ctxt i)) || tm == Placeholder)
2013 = return [(n, tm)]
2014 match (PRewrite _ l r _) (PRewrite _ l' r' _)
2015 = do ml <- match' l l'
2016 mr <- match' r r'
2017 return (ml ++ mr)
2018 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2019 mr <- match r r'
2020 return (ml ++ mr)
2021 match (PTyped l r) x = match l x
2022 match x (PTyped l r) = match x l
2023 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2024 mr <- match' r r'
2025 return (ml ++ mr)
2026 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2027 mt <- match' t t'
2028 mr <- match' r r'
2029 return (ml ++ mt ++ mr)
2030 match (PAlternative _ a as) (PAlternative _ a' as')
2031 = do ms <- zipWithM match' as as'
2032 return (concat ms)
2033 match a@(PAlternative _ _ as) b
2034 = do let ms = zipWith match' as (repeat b)
2035 case (rights (map toEither ms)) of
2036 (x: _) -> return x
2037 _ -> LeftErr (a, b)
2038 match (PCase _ _ _) _ = return [] -- lifted out
2039 match (PMetavar _ _) _ = return [] -- modified
2040 match (PInferRef _ _ _) _ = return [] -- modified
2041 match (PQuote _) _ = return []
2042 match (PProof _) _ = return []
2043 match (PTactics _) _ = return []
2044 match (PResolveTC _) (PResolveTC _) = return []
2045 match (PTrue _ _) (PTrue _ _) = return []
2046 match (PReturn _) (PReturn _) = return []
2047 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2048 ms <- match' s s'
2049 return (mt ++ ms)
2050 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2051 ms <- match' s s'
2052 return (mt ++ ms)
2053 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2054 mty <- match' ty ty'
2055 ms <- match' s s'
2056 return (mt ++ mty ++ ms)
2057 match (PHidden x) (PHidden y)
2058 | RightOK xs <- match x y = return xs -- to collect variables
2059 | otherwise = return [] -- Otherwise hidden things are unmatchable
2060 match (PHidden x) y
2061 | RightOK xs <- match x y = return xs
2062 | otherwise = return []
2063 match x (PHidden y)
2064 | RightOK xs <- match x y = return xs
2065 | otherwise = return []
2066 match (PUnifyLog x) y = match' x y
2067 match x (PUnifyLog y) = match' x y
2068 match (PNoImplicits x) y = match' x y
2069 match x (PNoImplicits y) = match' x y
2070 match Placeholder _ = return []
2071 match _ Placeholder = return []
2072 match (PResolveTC _) _ = return []
2073 match a b | a == b = return []
2074 | otherwise = LeftErr (a, b)
2076 checkRpts (RightOK ms) = check ms where
2077 check ((n,t):xs)
2078 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2079 then Left (t, t')
2080 else check xs
2081 check (_:xs) = check xs
2082 check [] = Right ms
2083 checkRpts (LeftErr x) = Left x
2085substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2086substMatches ms = substMatchesShadow ms []
2088substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2089substMatchesShadow [] shs t = t
2090substMatchesShadow ((n,tm):ns) shs t
2091 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2093substMatch :: Name -> PTerm -> PTerm -> PTerm
2094substMatch n = substMatchShadow n []
2096substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2097substMatchShadow n shs tm t = sm shs t where
2098 sm xs (PRef _ _ n') | n == n' = tm
2099 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2100 sm xs (PPi p x fc t sc)
2101 | x `elem` xs
2102 = let x' = nextName x in
2103 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2104 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2105 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2106 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2107 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2108 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2109 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2110 (fmap (sm xs) tm)
2111 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2112 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2113 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2114 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2115 sm xs (PHidden x) = PHidden (sm xs x)
2116 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2117 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2118 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2119 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2120 sm xs x = x
2122 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2123 fullApp x = x
2125shadow :: Name -> Name -> PTerm -> PTerm
2126shadow n n' t = sm 0 t where
2127 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2128 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2129 | otherwise = PLam fc x xfc (sm 0 t) sc
2130 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2131 | otherwise = PPi p x fc (sm 0 t) sc
2132 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2133 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2134 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2135 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2136 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2137 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2138 sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2139 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2140 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2141 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2142 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2143 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2144 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2145 sm 0 (PHidden x) = PHidden (sm 0 x)
2146 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2147 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2148 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2149 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2150 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2151 sm ql x = descend (sm ql) x
2153-- | Rename any binders which are repeated (so that we don't have to mess
2154-- about with shadowing anywhere else).
2155mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2156mkUniqueNames env shadows tm
2157 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2159 initMap = M.fromList shadows
2161 inScope :: S.Set Name
2162 inScope = S.fromList $ boundNamesIn tm
2164 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2165 return (arg { getTm = t' })
2167 -- Initialise the unique name with the environment length (so we're not
2168 -- looking for too long...)
2169 initN (UN n) l = UN $ txt (str n ++ show l)
2170 initN (MN i s) l = MN (i+l) s
2171 initN n l = n
2173 -- FIXME: Probably ought to do this for completeness! It's fine as
2174 -- long as there are no bindings inside tactics though.
2175 mkUniqT _ nmap tac = return tac
2177 mkUniq :: Int -- ^ The number of quotations that we're under
2178 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2179 mkUniq 0 nmap (PLam fc n nfc ty sc)
2180 = do env <- get
2181 (n', sc') <-
2182 if n `S.member` env
2183 then do let n' = uniqueNameSet (initN n (S.size env))
2184 (S.union env inScope)
2185 return (n', sc) -- shadow n n' sc)
2186 else return (n, sc)
2187 put (S.insert n' env)
2188 let nmap' = M.insert n n' nmap
2189 ty' <- mkUniq 0 nmap ty
2190 sc'' <- mkUniq 0 nmap' sc'
2191 return $! PLam fc n' nfc ty' sc''
2192 mkUniq 0 nmap (PPi p n fc ty sc)
2193 = do env <- get
2194 (n', sc') <-
2195 if n `S.member` env
2196 then do let n' = uniqueNameSet (initN n (S.size env))
2197 (S.union env inScope)
2198 return (n', sc) -- shadow n n' sc)
2199 else return (n, sc)
2200 put (S.insert n' env)
2201 let nmap' = M.insert n n' nmap
2202 ty' <- mkUniq 0 nmap ty
2203 sc'' <- mkUniq 0 nmap' sc'
2204 return $! PPi p n' fc ty' sc''
2205 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2206 = do env <- get
2207 (n', sc') <-
2208 if n `S.member` env
2209 then do let n' = uniqueNameSet (initN n (S.size env))
2210 (S.union env inScope)
2211 return (n', sc) -- shadow n n' sc)
2212 else return (n, sc)
2213 put (S.insert n' env)
2214 let nmap' = M.insert n n' nmap
2215 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2216 sc'' <- mkUniq 0 nmap' sc'
2217 return $! PLet fc n' nfc ty' val' sc''
2218 mkUniq 0 nmap (PApp fc t args)
2219 = do t' <- mkUniq 0 nmap t
2220 args' <- mapM (mkUniqA 0 nmap) args
2221 return $! PApp fc t' args'
2222 mkUniq 0 nmap (PAppBind fc t args)
2223 = do t' <- mkUniq 0 nmap t
2224 args' <- mapM (mkUniqA 0 nmap) args
2225 return $! PAppBind fc t' args'
2226 mkUniq 0 nmap (PCase fc t alts)
2227 = do t' <- mkUniq 0 nmap t
2228 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2229 return (x', y')) alts
2230 return $! PCase fc t' alts'
2231 mkUniq 0 nmap (PIfThenElse fc c t f)
2232 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2233 mkUniq 0 nmap (PPair fc hls p l r)
2234 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2235 return $! PPair fc hls p l' r'
2236 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2237 | t /= Placeholder
2238 = do env <- get
2239 (n', sc') <- if n `S.member` env
2240 then do let n' = uniqueNameSet n (S.union env inScope)
2241 return (n', sc) -- shadow n n' sc)
2242 else return (n, sc)
2243 put (S.insert n' env)
2244 let nmap' = M.insert n n' nmap
2245 t' <- mkUniq 0 nmap t
2246 sc'' <- mkUniq 0 nmap' sc'
2247 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2248 mkUniq 0 nmap (PDPair fc hls p l t r)
2249 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2250 return $! PDPair fc hls p l' t' r'
2251 mkUniq 0 nmap (PAlternative ns b as)
2252 -- store the nmap and defer the rest until we've pruned the set
2253 -- during elaboration
2254 = return $ PAlternative (M.toList nmap ++ ns) b as
2255 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2256 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2257 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2258 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2259 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2260 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2261 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2262 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2263 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2264 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2265 where
2266 shadowAll [] t = t
2267 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2269 mkUniq ql nmap (PQuasiquote tm ty) =
2270 do tm' <- mkUniq (ql + 1) nmap tm
2271 ty' <- case ty of
2272 Nothing -> return Nothing
2273 Just t -> fmap Just $ mkUniq ql nmap t
2274 return $! PQuasiquote tm' ty'
2275 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2277 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm