git.iko.soy/Idris-dev
on 21f0db3 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2344 lines 101 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' }
702setLogCats :: [LogCat] -> Idris ()
703setLogCats cs = do
704 i <- getIState
705 let opts = idris_options i
706 let opt' = opts { opt_logcats = cs }
707 putIState $ i { idris_options = opt' }
709setCmdLine :: [Opt] -> Idris ()
710setCmdLine opts = do i <- getIState
711 let iopts = idris_options i
712 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
714getCmdLine :: Idris [Opt]
715getCmdLine = do i <- getIState
716 return (opt_cmdline (idris_options i))
718getDumpHighlighting :: Idris Bool
719getDumpHighlighting = do ist <- getIState
720 return (findC (opt_cmdline (idris_options ist)))
721 where findC = elem DumpHighlights
723getDumpDefun :: Idris (Maybe FilePath)
724getDumpDefun = do i <- getIState
725 return $ findC (opt_cmdline (idris_options i))
726 where findC [] = Nothing
727 findC (DumpDefun x : _) = Just x
728 findC (_ : xs) = findC xs
730getDumpCases :: Idris (Maybe FilePath)
731getDumpCases = do i <- getIState
732 return $ findC (opt_cmdline (idris_options i))
733 where findC [] = Nothing
734 findC (DumpCases x : _) = Just x
735 findC (_ : xs) = findC xs
737logLevel :: Idris Int
738logLevel = do i <- getIState
739 return (opt_logLevel (idris_options i))
741setErrContext :: Bool -> Idris ()
742setErrContext t = do i <- getIState
743 let opts = idris_options i
744 let opts' = opts { opt_errContext = t }
745 putIState $ i { idris_options = opts' }
747errContext :: Idris Bool
748errContext = do i <- getIState
749 return (opt_errContext (idris_options i))
751getOptimise :: Idris [Optimisation]
752getOptimise = do i <- getIState
753 return (opt_optimise (idris_options i))
755setOptimise :: [Optimisation] -> Idris ()
756setOptimise newopts = do i <- getIState
757 let opts = idris_options i
758 let opts' = opts { opt_optimise = newopts }
759 putIState $ i { idris_options = opts' }
761addOptimise :: Optimisation -> Idris ()
762addOptimise opt = do opts <- getOptimise
763 setOptimise (nub (opt : opts))
765removeOptimise :: Optimisation -> Idris ()
766removeOptimise opt = do opts <- getOptimise
767 setOptimise ((nub opts) \\ [opt])
769-- Set appropriate optimisation set for the given level. We only have
770-- one optimisation that is configurable at the moment, however!
771setOptLevel :: Int -> Idris ()
772setOptLevel n | n <= 0 = setOptimise []
773setOptLevel 1 = setOptimise []
774setOptLevel 2 = setOptimise [PETransform]
775setOptLevel n | n >= 3 = setOptimise [PETransform]
777useREPL :: Idris Bool
778useREPL = do i <- getIState
779 return (opt_repl (idris_options i))
781setREPL :: Bool -> Idris ()
782setREPL t = do i <- getIState
783 let opts = idris_options i
784 let opt' = opts { opt_repl = t }
785 putIState $ i { idris_options = opt' }
787showOrigErr :: Idris Bool
788showOrigErr = do i <- getIState
789 return (opt_origerr (idris_options i))
791setShowOrigErr :: Bool -> Idris ()
792setShowOrigErr b = do i <- getIState
793 let opts = idris_options i
794 let opt' = opts { opt_origerr = b }
795 putIState $ i { idris_options = opt' }
797setAutoSolve :: Bool -> Idris ()
798setAutoSolve b = do i <- getIState
799 let opts = idris_options i
800 let opt' = opts { opt_autoSolve = b }
801 putIState $ i { idris_options = opt' }
803setNoBanner :: Bool -> Idris ()
804setNoBanner n = do i <- getIState
805 let opts = idris_options i
806 let opt' = opts { opt_nobanner = n }
807 putIState $ i { idris_options = opt' }
809getNoBanner :: Idris Bool
810getNoBanner = do i <- getIState
811 let opts = idris_options i
812 return (opt_nobanner opts)
814setEvalTypes :: Bool -> Idris ()
815setEvalTypes n = do i <- getIState
816 let opts = idris_options i
817 let opt' = opts { opt_evaltypes = n }
818 putIState $ i { idris_options = opt' }
820getDesugarNats :: Idris Bool
821getDesugarNats = do i <- getIState
822 let opts = idris_options i
823 return (opt_desugarnats opts)
826setDesugarNats :: Bool -> Idris ()
827setDesugarNats n = do i <- getIState
828 let opts = idris_options i
829 let opt' = opts { opt_desugarnats = n }
830 putIState $ i { idris_options = opt' }
832setQuiet :: Bool -> Idris ()
833setQuiet q = do i <- getIState
834 let opts = idris_options i
835 let opt' = opts { opt_quiet = q }
836 putIState $ i { idris_options = opt' }
838getQuiet :: Idris Bool
839getQuiet = do i <- getIState
840 let opts = idris_options i
841 return (opt_quiet opts)
843setCodegen :: Codegen -> Idris ()
844setCodegen t = do i <- getIState
845 let opts = idris_options i
846 let opt' = opts { opt_codegen = t }
847 putIState $ i { idris_options = opt' }
849codegen :: Idris Codegen
850codegen = do i <- getIState
851 return (opt_codegen (idris_options i))
853setOutputTy :: OutputType -> Idris ()
854setOutputTy t = do i <- getIState
855 let opts = idris_options i
856 let opt' = opts { opt_outputTy = t }
857 putIState $ i { idris_options = opt' }
859outputTy :: Idris OutputType
860outputTy = do i <- getIState
861 return $ opt_outputTy $ idris_options i
863setIdeMode :: Bool -> Handle -> Idris ()
864setIdeMode True h = do i <- getIState
865 putIState $ i { idris_outputmode = IdeMode 0 h
866 , idris_colourRepl = False
867 }
868setIdeMode False _ = return ()
870setTargetTriple :: String -> Idris ()
871setTargetTriple t = do i <- getIState
872 let opts = idris_options i
873 opt' = opts { opt_triple = t }
874 putIState $ i { idris_options = opt' }
876targetTriple :: Idris String
877targetTriple = do i <- getIState
878 return (opt_triple (idris_options i))
880setTargetCPU :: String -> Idris ()
881setTargetCPU t = do i <- getIState
882 let opts = idris_options i
883 opt' = opts { opt_cpu = t }
884 putIState $ i { idris_options = opt' }
886targetCPU :: Idris String
887targetCPU = do i <- getIState
888 return (opt_cpu (idris_options i))
890verbose :: Idris Bool
891verbose = do i <- getIState
892 -- Quietness overrides verbosity
893 return (not (opt_quiet (idris_options i)) &&
894 opt_verbose (idris_options i))
896setVerbose :: Bool -> Idris ()
897setVerbose t = do i <- getIState
898 let opts = idris_options i
899 let opt' = opts { opt_verbose = t }
900 putIState $ i { idris_options = opt' }
902typeInType :: Idris Bool
903typeInType = do i <- getIState
904 return (opt_typeintype (idris_options i))
906setTypeInType :: Bool -> Idris ()
907setTypeInType t = do i <- getIState
908 let opts = idris_options i
909 let opt' = opts { opt_typeintype = t }
910 putIState $ i { idris_options = opt' }
912coverage :: Idris Bool
913coverage = do i <- getIState
914 return (opt_coverage (idris_options i))
916setCoverage :: Bool -> Idris ()
917setCoverage t = do i <- getIState
918 let opts = idris_options i
919 let opt' = opts { opt_coverage = t }
920 putIState $ i { idris_options = opt' }
922setIBCSubDir :: FilePath -> Idris ()
923setIBCSubDir fp = do i <- getIState
924 let opts = idris_options i
925 let opt' = opts { opt_ibcsubdir = fp }
926 putIState $ i { idris_options = opt' }
928valIBCSubDir :: IState -> Idris FilePath
929valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
931addImportDir :: FilePath -> Idris ()
932addImportDir fp = do i <- getIState
933 let opts = idris_options i
934 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
935 putIState $ i { idris_options = opt' }
937setImportDirs :: [FilePath] -> Idris ()
938setImportDirs fps = do i <- getIState
939 let opts = idris_options i
940 let opt' = opts { opt_importdirs = fps }
941 putIState $ i { idris_options = opt' }
943allImportDirs :: Idris [FilePath]
944allImportDirs = do i <- getIState
945 let optdirs = opt_importdirs (idris_options i)
946 return ("." : reverse optdirs)
948colourise :: Idris Bool
949colourise = do i <- getIState
950 return $ idris_colourRepl i
952setColourise :: Bool -> Idris ()
953setColourise b = do i <- getIState
954 putIState $ i { idris_colourRepl = b }
956impShow :: Idris Bool
957impShow = do i <- getIState
958 return (opt_showimp (idris_options i))
960setImpShow :: Bool -> Idris ()
961setImpShow t = do i <- getIState
962 let opts = idris_options i
963 let opt' = opts { opt_showimp = t }
964 putIState $ i { idris_options = opt' }
966setColour :: ColourType -> IdrisColour -> Idris ()
967setColour ct c = do i <- getIState
968 let newTheme = setColour' ct c (idris_colourTheme i)
969 putIState $ i { idris_colourTheme = newTheme }
970 where setColour' KeywordColour c t = t { keywordColour = c }
971 setColour' BoundVarColour c t = t { boundVarColour = c }
972 setColour' ImplicitColour c t = t { implicitColour = c }
973 setColour' FunctionColour c t = t { functionColour = c }
974 setColour' TypeColour c t = t { typeColour = c }
975 setColour' DataColour c t = t { dataColour = c }
976 setColour' PromptColour c t = t { promptColour = c }
977 setColour' PostulateColour c t = t { postulateColour = c }
980logLvl :: Int -> String -> Idris ()
981logLvl = logLvlCats []
983logCoverage :: Int -> String -> Idris ()
984logCoverage = logLvlCats [ICoverage]
986logErasure :: Int -> String -> Idris ()
987logErasure = logLvlCats [IErasure]
989-- | Log an action of the parser
990logParser :: Int -> String -> Idris ()
991logParser = logLvlCats parserCats
993-- | Log an action of the elaborator.
994logElab :: Int -> String -> Idris ()
995logElab = logLvlCats elabCats
997-- | Log an action of the compiler.
998logCodeGen :: Int -> String -> Idris ()
999logCodeGen = logLvlCats codegenCats
1001logIBC :: Int -> String -> Idris ()
1002logIBC = logLvlCats [IIBC]
1004-- | Log aspect of Idris execution
1006-- An empty set of logging levels is used to denote all categories.
1008-- @TODO update IDE protocol
1009logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
1010 -> Int -- ^ The Logging level the message should appear.
1011 -> String -- ^ The message to show the developer.
1012 -> Idris ()
1013logLvlCats cs l str = do
1014 i <- getIState
1015 let lvl = opt_logLevel (idris_options i)
1016 let cats = opt_logcats (idris_options i)
1017 when (lvl >= l) $
1018 when (inCat cs cats || null cats) $
1019 case idris_outputmode i of
1020 RawOutput h -> do
1021 runIO $ hPutStrLn h str
1022 IdeMode n h -> do
1023 let good = SexpList [IntegerAtom (toInteger l), toSExp str]
1024 runIO . hPutStrLn h $ convSExp "log" good n
1025 where
1026 inCat :: [LogCat] -> [LogCat] -> Bool
1027 inCat cs cats = or $ map (\x -> elem x cats) cs
1029cmdOptType :: Opt -> Idris Bool
1030cmdOptType x = do i <- getIState
1031 return $ x `elem` opt_cmdline (idris_options i)
1033noErrors :: Idris Bool
1034noErrors = do i <- getIState
1035 case errSpan i of
1036 Nothing -> return True
1037 _ -> return False
1039setTypeCase :: Bool -> Idris ()
1040setTypeCase t = do i <- getIState
1041 let opts = idris_options i
1042 let opt' = opts { opt_typecase = t }
1043 putIState $ i { idris_options = opt' }
1046-- Dealing with parameters
1048expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
1049 [Name] -> -- all names
1050 [Name] -> -- names with no declaration
1051 PTerm -> PTerm
1052expandParams dec ps ns infs tm = en 0 tm
1053 where
1054 -- if we shadow a name (say in a lambda binding) that is used in a call to
1055 -- a lifted function, we need access to both names - once in the scope of the
1056 -- binding and once to call the lifted functions. So we'll explicitly shadow
1057 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1058 -- but we didn't...)
1060 mkShadow (UN n) = MN 0 n
1061 mkShadow (MN i n) = MN (i+1) n
1062 mkShadow (NS x s) = NS (mkShadow x) s
1064 en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1065 -- that are merely mentioned.
1066 -> PTerm -> PTerm
1067 en 0 (PLam fc n nfc t s)
1068 | n `elem` (map fst ps ++ ns)
1069 = let n' = mkShadow n in
1070 PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1071 | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1072 en 0 (PPi p n nfc t s)
1073 | n `elem` (map fst ps ++ ns)
1074 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1075 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1076 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1077 en 0 (PLet fc n nfc ty v s)
1078 | n `elem` (map fst ps ++ ns)
1079 = let n' = mkShadow n in
1080 PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1081 | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
1082 -- FIXME: Should only do this in a type signature!
1083 en 0 (PDPair f hls p (PRef f' fcs n) t r)
1084 | n `elem` (map fst ps ++ ns) && t /= Placeholder
1085 = let n' = mkShadow n in
1086 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1087 en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1088 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1089 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1090 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1091 en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1092 en 0 (PHidden t) = PHidden (en 0 t)
1093 en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1094 en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1095 en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1096 en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1097 en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1098 en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1100 en 0 (PQuote (Var n))
1101 | n `nselem` ns = PQuote (Var (dec n))
1102 en 0 (PApp fc (PInferRef fc' hl n) as)
1103 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1104 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1105 en 0 (PApp fc (PRef fc' hl n) as)
1106 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1107 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1108 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1109 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1110 en 0 (PAppBind fc (PRef fc' hl n) as)
1111 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1112 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1113 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1114 (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1115 en 0 (PRef fc hl n)
1116 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
1117 (map (pexp . (PRef fc hl)) (map fst ps))
1118 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
1119 (map (pexp . (PRef fc hl)) (map fst ps))
1120 en 0 (PInferRef fc hl n)
1121 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
1122 (map (pexp . (PRef fc hl)) (map fst ps))
1123 en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1124 en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1125 en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1126 en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1127 en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1128 en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1130 en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1131 en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1133 en ql t = descend (en ql) t
1135 nselem x [] = False
1136 nselem x (y : xs) | nseq x y = True
1137 | otherwise = nselem x xs
1139 nseq x y = nsroot x == nsroot y
1141 enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1142 enTacImp ql other = other
1144expandParamsD :: Bool -> -- True = RHS only
1145 IState ->
1146 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1147expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
1148 = if n `elem` ns && (not rhsonly)
1149 then -- trace (show (n, expandParams dec ps ns ty)) $
1150 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
1151 else --trace (show (n, expandParams dec ps ns ty)) $
1152 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
1153expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
1154 = if n `elem` ns && (not rhsonly)
1155 then -- trace (show (n, expandParams dec ps ns ty)) $
1156 PPostulate e doc syn fc nfc o (dec n)
1157 (piBind ps (expandParams dec ps ns [] ty))
1158 else --trace (show (n, expandParams dec ps ns ty)) $
1159 PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
1160expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1161 = let n' = if n `elem` ns then dec n else n in
1162 PClauses fc opts n' (map expandParamsC cs)
1163 where
1164 expandParamsC (PClause fc n lhs ws rhs ds)
1165 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1166 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1167 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1168 n' = if n `elem` ns then dec n else n
1169 -- names bound on the lhs should not be expanded on the rhs
1170 ns' = removeBound lhs ns in
1171 PClause fc n' lhs'
1172 (map (expandParams dec ps'' ns' []) ws)
1173 (expandParams dec ps'' ns' [] rhs)
1174 (map (expandParamsD True ist dec ps'' ns') ds)
1175 expandParamsC (PWith fc n lhs ws wval pn ds)
1176 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1177 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1178 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1179 n' = if n `elem` ns then dec n else n
1180 ns' = removeBound lhs ns in
1181 PWith fc n' lhs'
1182 (map (expandParams dec ps'' ns' []) ws)
1183 (expandParams dec ps'' ns' [] wval)
1184 pn
1185 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1186 updateps yn nm [] = []
1187 updateps yn nm (((a, t), i):as)
1188 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1189 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1191 removeBound lhs ns = ns \\ nub (bnames lhs)
1193 bnames (PRef _ _ n) = [n]
1194 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1195 bnames (PPair _ _ _ l r) = bnames l ++ bnames r
1196 bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
1197 bnames _ = []
1199-- | Expands parameters defined in parameter and where blocks inside of declarations
1200expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1201 = PData doc argDocs syn fc co (expandPData pd)
1202 where
1203 -- just do the type decl, leave constructors alone (parameters will be
1204 -- added implicitly)
1205 expandPData (PDatadecl n nfc ty cons)
1206 = if n `elem` ns
1207 then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
1208 (map econ cons)
1209 else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
1210 econ (doc, argDocs, n, nfc, t, fc, fs)
1211 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1212expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
1213 = d
1214expandParamsD rhs ist dec ps ns (PParams f params pds)
1215 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1216 (map (expandParamsD True ist dec ps ns) pds)
1217-- (map (expandParamsD ist dec ps ns) pds)
1218expandParamsD rhs ist dec ps ns (PMutual f pds)
1219 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1220expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)
1221 = PClass doc info f
1222 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1223 n nfc
1224 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
1225 pDocs
1226 fds
1227 (map (expandParamsD rhs ist dec ps ns) decls)
1228 cn
1229 cd
1230expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)
1231 = PInstance doc argDocs info f
1232 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1234 nfc
1235 (map (expandParams dec ps ns []) params)
1236 (expandParams dec ps ns [] ty)
1237 cn
1238 (map (expandParamsD rhs ist dec ps ns) decls)
1239expandParamsD rhs ist dec ps ns d = d
1241mapsnd f (x, t) = (x, f t)
1243-- Calculate a priority for a type, for deciding elaboration order
1244-- * if it's just a type variable or concrete type, do it early (0)
1245-- * if there's only type variables and injective constructors, do it next (1)
1246-- * if there's a function type, next (2)
1247-- * finally, everything else (3)
1249getPriority :: IState -> PTerm -> Int
1250getPriority i tm = 1 -- pri tm
1251 where
1252 pri (PRef _ _ n) =
1253 case lookupP n (tt_ctxt i) of
1254 ((P (DCon _ _ _) _ _):_) -> 1
1255 ((P (TCon _ _) _ _):_) -> 1
1256 ((P Ref _ _):_) -> 1
1257 [] -> 0 -- must be locally bound, if it's not an error...
1258 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
1259 pri (PTrue _ _) = 0
1260 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1261 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1262 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1263 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1264 pri (PTyped l r) = pri l
1265 pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
1266 pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1267 pri (PAlternative _ a as) = maximum (map pri as)
1268 pri (PConstant _ _) = 0
1269 pri Placeholder = 1
1270 pri _ = 3
1273addStatics :: Name -> Term -> PTerm -> Idris ()
1274addStatics n tm ptm =
1275 do let (statics, dynamics) = initStatics tm ptm
1276 ist <- getIState
1277 let paramnames
1278 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1279 Just p -> getNamesFrom 0 (fn_params p) tm ++
1280 concatMap (getParamNames ist) (map snd statics)
1281 _ -> concatMap (getParamNames ist) (map snd statics)
1283 let stnames = nub $ concatMap freeArgNames (map snd statics)
1284 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1285 \\ paramnames
1286 -- also get the arguments which are 'uniquely inferrable' from
1287 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1288 -- or parameters to the type of a static
1289 let statics' = nub $ map fst statics ++
1290 filter (\x -> not (elem x dnames)) stnames
1291 let stpos = staticList statics' tm
1292 i <- getIState
1293 when (not (null statics)) $
1294 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1295 ++ showTmImpls ptm ++ "\n"
1296 ++ show statics ++ "\n" ++ show dynamics
1297 ++ "\n" ++ show paramnames
1298 ++ "\n" ++ show stpos
1299 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1300 addIBC (IBCStatic n)
1301 where
1302 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1303 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
1304 (static, (n, ty) : dynamic)
1305 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)
1306 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1307 if pstatic p == Static then ((n, ty) : static, dynamic)
1308 else if (not (searchArg p))
1309 then (static, (n, ty) : dynamic)
1310 else (static, dynamic)
1311 initStatics t pt = ([], [])
1313 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1314 = case lookupCtxtExact n (idris_datatypes ist) of
1315 Just ti -> getNamePos 0 (param_pos ti) args
1316 Nothing -> []
1317 where getNamePos i ps [] = []
1318 getNamePos i ps (P _ n _ : as)
1319 | i `elem` ps = n : getNamePos (i + 1) ps as
1320 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1321 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1322 = n : getParamNames ist sc
1323 getParamNames ist _ = []
1325 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1326 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1327 | otherwise = getNamesFrom (i + 1) ps sc
1328 getNamesFrom i ps sc = []
1330 freeArgNames (Bind n (Pi _ ty _) sc)
1331 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1332 freeArgNames tm = let (_, args) = unApply tm in
1333 concatMap freeNames args
1335 -- if a name appears in a type class or tactic implicit index, it doesn't
1336 -- affect its 'uniquely inferrable' from a static status since these are
1337 -- resolved by searching.
1338 searchArg (Constraint _ _) = True
1339 searchArg (TacImp _ _ _) = True
1340 searchArg _ = False
1342 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1343 staticList _ _ = []
1345-- Dealing with implicit arguments
1347-- Add some bound implicits to the using block if they aren't there already
1349addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1350addToUsing us [] = us
1351addToUsing us ((n, t) : ns)
1352 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1353 | otherwise = addToUsing us ns
1354 where impName (UImplicit n _) = Just n
1355 impName _ = Nothing
1357-- Add constraint bindings from using block
1359addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1360addUsingConstraints syn fc t
1361 = do ist <- get
1362 let ns = namesIn [] ist t
1363 let cs = getConstraints t -- check declared constraints
1364 let addconsts = uconsts \\ cs
1365 return (doAdd addconsts ns t)
1366 where uconsts = filter uconst (using syn)
1367 uconst (UConstraint _ _) = True
1368 uconst _ = False
1370 doAdd [] _ t = t
1371 -- if all of args in ns, then add it
1372 doAdd (UConstraint c args : cs) ns t
1373 | all (\n -> elem n ns) args
1374 = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1375 (mkConst c args) (doAdd cs ns t)
1376 | otherwise = doAdd cs ns t
1378 mkConst c args = PApp fc (PRef fc [] c)
1379 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc [] n)) args)
1381 getConstraints (PPi (Constraint _ _) _ _ c sc)
1382 = getcapp c ++ getConstraints sc
1383 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1384 getConstraints _ = []
1386 getcapp (PApp _ (PRef _ _ c) args)
1387 = do ns <- mapM getName args
1388 return (UConstraint c ns)
1389 getcapp _ = []
1391 getName (PExp _ _ _ (PRef _ _ n)) = return n
1392 getName _ = []
1394-- Add implicit bindings from using block, and bind any missing names
1395addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1396addUsingImpls syn n fc t
1397 = do ist <- getIState
1398 let ns = implicitNamesIn (map iname uimpls) ist t
1399 let badnames = filter (\n -> not (implicitable n) &&
1400 n `notElem` (map iname uimpls)) ns
1401 when (not (null badnames)) $
1402 throwError (At fc (Elaborating "type of " n Nothing
1403 (NoSuchVariable (head badnames))))
1404 let cs = getArgnames t -- get already bound names
1405 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1406 -- if all names in the arguments of addconsts appear in ns,
1407 -- add the constraint implicitly
1408 return (bindFree ns (doAdd addimpls ns t))
1409 where uimpls = filter uimpl (using syn)
1410 uimpl (UImplicit _ _) = True
1411 uimpl _ = False
1413 iname (UImplicit n _) = n
1414 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1416 doAdd [] _ t = t
1417 -- if all of args in ns, then add it
1418 doAdd (UImplicit n ty : cs) ns t
1419 | elem n ns
1420 = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)
1421 | otherwise = doAdd cs ns t
1423 -- bind the free names which weren't in the using block
1424 bindFree [] tm = tm
1425 bindFree (n:ns) tm
1426 | elem n (map iname uimpls) = bindFree ns tm
1427 | otherwise
1428 = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1430 getArgnames (PPi _ n _ c sc)
1431 = n : getArgnames sc
1432 getArgnames _ = []
1434-- Given the original type and the elaborated type, return the implicitness
1435-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1437getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1438getUnboundImplicits i t tm = getImps t (collectImps tm)
1439 where collectImps (PPi p n _ t sc)
1440 = (n, (p, t)) : collectImps sc
1441 collectImps _ = []
1443 scopedimpl (Just i) = not (toplevel_imp i)
1444 scopedimpl _ = False
1446 getImps (Bind n (Pi i _ _) sc) imps
1447 | scopedimpl i = getImps sc imps
1448 getImps (Bind n (Pi _ t _) sc) imps
1449 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1450 where
1451 argInfo n (Imp opt _ _ _) Placeholder
1452 = (True, PImp 0 True opt n Placeholder)
1453 argInfo n (Imp opt _ _ _) t'
1454 = (False, PImp (getPriority i t') True opt n t')
1455 argInfo n (Exp opt _ _) t'
1456 = (InaccessibleArg `elem` opt,
1457 PExp (getPriority i t') opt n t')
1458 argInfo n (Constraint opt _) t'
1459 = (InaccessibleArg `elem` opt,
1460 PConstraint 10 opt n t')
1461 argInfo n (TacImp opt _ scr) t'
1462 = (InaccessibleArg `elem` opt,
1463 PTacImplicit 10 opt n scr t')
1464 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1465 where impBind n t = (True, PImp 1 True [] n Placeholder)
1466 getImps sc tm = []
1468-- Add implicit Pi bindings for any names in the term which appear in an
1469-- argument position.
1471-- This has become a right mess already. Better redo it some time...
1472-- TODO: This is obsoleted by the new way of elaborating types, (which
1473-- calls addUsingImpls) but there's still a couple of places which use
1474-- it. Clean them up!
1476-- Issue 1739 in the issue tracker
1477-- https://github.com/idris-lang/Idris-dev/issues/1739
1478implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1479implicit info syn n ptm = implicit' info syn [] n ptm
1481implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1482implicit' info syn ignore n ptm
1483 = do i <- getIState
1484 let (tm', impdata) = implicitise syn ignore i ptm
1485 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1486-- let (tm'', spos) = findStatics i tm'
1487 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1488 addIBC (IBCImp n)
1489 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1490-- i <- get
1491-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1492 return tm'
1493 where
1494 -- Detect unknown names in default arguments and throw error if found.
1495 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1496 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1498 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1499 notFoundInDefault kns (PTacImplicit _ _ n script _)
1500 = do i <- getIState
1501 case notFound kns (namesIn [] i script) of
1502 Nothing -> return (n:kns)
1503 Just name -> throwError (NoSuchVariable name)
1504 notFoundInDefault kns p = return ((pname p):kns)
1506 notFound :: [Name] -> [Name] -> Maybe Name
1507 notFound kns [] = Nothing
1508 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1509 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1511implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1512implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1513 let (declimps, ns') = execState (imps True [] tm) ([], [])
1514 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1515 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1516 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1517 if null ns
1518 then (tm, reverse declimps)
1519 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1520 where
1521 uvars = map ipair (filter uimplicit (using syn))
1522 pvars = syn_params syn
1524 inUsing n = n `elem` map fst uvars
1526 ipair (UImplicit x y) = (x, y)
1527 uimplicit (UImplicit _ _) = True
1528 uimplicit _ = False
1530 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1531 | otherwise = x : dropAll xs ys
1532 dropAll [] ys = []
1534 -- Find names in argument position in a type, suitable for implicit
1535 -- binding
1536 -- Not the function position, but do everything else...
1537 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1538 implNamesIn uv t = namesIn uv ist t
1540 imps top env (PApp _ f as)
1541 = do (decls, ns) <- get
1542 let isn = concatMap (namesIn uvars ist) (map getTm as)
1543 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1544 imps top env (PPi (Imp l _ _ _) n _ ty sc)
1545 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1546 (decls , ns) <- get
1547 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1548 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1549 imps True (n:env) sc
1550 imps top env (PPi (Exp l _ _) n _ ty sc)
1551 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1552 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1553 _ -> [])
1554 (decls, ns) <- get -- ignore decls in HO types
1555 put (PExp (getPriority ist ty) l n Placeholder : decls,
1556 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1557 imps True (n:env) sc
1558 imps top env (PPi (Constraint l _) n _ ty sc)
1559 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1560 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1561 _ -> [])
1562 (decls, ns) <- get -- ignore decls in HO types
1563 put (PConstraint 10 l n Placeholder : decls,
1564 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1565 imps True (n:env) sc
1566 imps top env (PPi (TacImp l _ scr) n _ ty sc)
1567 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1568 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1569 _ -> [])
1570 (decls, ns) <- get -- ignore decls in HO types
1571 put (PTacImplicit 10 l n scr Placeholder : decls,
1572 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1573 imps True (n:env) sc
1574 imps top env (PRewrite _ l r _)
1575 = do (decls, ns) <- get
1576 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1577 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1578 imps top env (PTyped l r)
1579 = imps top env l
1580 imps top env (PPair _ _ _ l r)
1581 = do (decls, ns) <- get
1582 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1583 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1584 imps top env (PDPair _ _ _ (PRef _ _ n) t r)
1585 = do (decls, ns) <- get
1586 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1587 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1588 imps top env (PDPair _ _ _ l t r)
1589 = do (decls, ns) <- get
1590 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1591 namesIn uvars ist r
1592 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1593 imps top env (PAlternative ms a as)
1594 = do (decls, ns) <- get
1595 let isn = concatMap (namesIn uvars ist) as
1596 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1597 imps top env (PLam fc n _ ty sc)
1598 = do imps False env ty
1599 imps False (n:env) sc
1600 imps top env (PHidden tm) = imps False env tm
1601 imps top env (PUnifyLog tm) = imps False env tm
1602 imps top env (PNoImplicits tm) = imps False env tm
1603 imps top env (PRunElab fc tm ns) = imps False env tm
1604 imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
1605 imps top env _ = return ()
1607 pibind using [] sc = sc
1608 pibind using (n:ns) sc
1609 = case lookup n using of
1610 Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))
1611 n NoFC ty (pibind using ns sc)
1612 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))
1613 n NoFC Placeholder (pibind using ns sc)
1615-- Add implicit arguments in function calls
1616addImplPat :: IState -> PTerm -> PTerm
1617addImplPat = addImpl' True [] [] []
1619addImplBound :: IState -> [Name] -> PTerm -> PTerm
1620addImplBound ist ns = addImpl' False ns [] [] ist
1622addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1623addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1625-- | Add the implicit arguments to applications in the term
1626-- [Name] gives the names to always expend, even when under a binder of
1627-- that name (this is to expand methods with implicit arguments in dependent
1628-- type classes).
1629addImpl :: [Name] -> IState -> PTerm -> PTerm
1630addImpl = addImpl' False [] []
1632-- TODO: in patterns, don't add implicits to function names guarded by constructors
1633-- and *not* inside a PHidden
1635addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1636addImpl' inpat env infns imp_meths ist ptm
1637 = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1638 where
1639 topname = case ptm of
1640 PRef _ _ n -> n
1641 PApp _ (PRef _ _ n) _ -> n
1642 _ -> sUN "" -- doesn't matter then
1644 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1645 ai inpat qq env ds (PRef fc fcs f)
1646 | f `elem` infns = PInferRef fc fcs f
1647 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] []
1648 ai inpat qq env ds (PHidden (PRef fc hl f))
1649 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] [])
1650 ai inpat qq env ds (PRewrite fc l r g)
1651 = let l' = ai inpat qq env ds l
1652 r' = ai inpat qq env ds r
1653 g' = fmap (ai inpat qq env ds) g in
1654 PRewrite fc l' r' g'
1655 ai inpat qq env ds (PTyped l r)
1656 = let l' = ai inpat qq env ds l
1657 r' = ai inpat qq env ds r in
1658 PTyped l' r'
1659 ai inpat qq env ds (PPair fc hls p l r)
1660 = let l' = ai inpat qq env ds l
1661 r' = ai inpat qq env ds r in
1662 PPair fc hls p l' r'
1663 ai inpat qq env ds (PDPair fc hls p l t r)
1664 = let l' = ai inpat qq env ds l
1665 t' = ai inpat qq env ds t
1666 r' = ai inpat qq env ds r in
1667 PDPair fc hls p l' t' r'
1668 ai inpat qq env ds (PAlternative ms a as)
1669 = let as' = map (ai inpat qq env ds) as in
1670 PAlternative ms a as'
1671 ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1672 ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1673 = let as' = map (fmap (ai inpat qq env ds)) as in
1674 PApp fc (PInferRef ffc hl f) as'
1675 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1676 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1677 | not (f `elem` map fst env)
1678 = let as' = map (fmap (ai inpat qq env ds)) as
1679 asdotted' = map (fmap (ai False qq env ds)) as in
1680 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'
1681 | Just (Just ty) <- lookup f env =
1682 let as' = map (fmap (ai inpat qq env ds)) as
1683 arity = getPArity ty in
1684 mkPApp fc arity ftm as'
1685 ai inpat qq env ds (PApp fc f as)
1686 = let f' = ai inpat qq env ds f
1687 as' = map (fmap (ai inpat qq env ds)) as in
1688 mkPApp fc 1 f' as'
1689 ai inpat qq env ds (PCase fc c os)
1690 = let c' = ai inpat qq env ds c in
1691 -- leave os alone, because they get lifted into a new pattern match
1692 -- definition which is passed through addImpl agai inpatn with more scope
1693 -- information
1694 PCase fc c' os
1696 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1697 (ai inpat qq env ds t)
1698 (ai inpat qq env ds f)
1700 -- If the name in a lambda is a constructor name, do this as a 'case'
1701 -- instead (it is harmless to do so, especially since the lambda will
1702 -- be lifted anyway!)
1703 ai inpat qq env ds (PLam fc n nfc ty sc)
1704 = case lookupDef n (tt_ctxt ist) of
1705 [] -> let ty' = ai inpat qq env ds ty
1706 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1707 PLam fc n nfc ty' sc'
1708 _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1709 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1710 [(PRef fc [] n, sc)]))
1711 ai inpat qq env ds (PLet fc n nfc ty val sc)
1712 = case lookupDef n (tt_ctxt ist) of
1713 [] -> let ty' = ai inpat qq env ds ty
1714 val' = ai inpat qq env ds val
1715 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1716 PLet fc n nfc ty' val' sc'
1717 defs ->
1718 ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1719 ai inpat qq env ds (PPi p n nfc ty sc)
1720 = let ty' = ai inpat qq env ds ty
1721 env' = if n `elem` imp_meths then env
1722 else ((n, Just ty) : env)
1723 sc' = ai inpat qq env' ds sc in
1724 PPi p n nfc ty' sc'
1725 ai inpat qq env ds (PGoal fc r n sc)
1726 = let r' = ai inpat qq env ds r
1727 sc' = ai inpat qq ((n, Nothing):env) ds sc in
1728 PGoal fc r' n sc'
1729 ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1730 -- Don't do PProof or PTactics since implicits get added when scope is
1731 -- properly known in ElabTerm.runTac
1732 ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1733 ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1734 ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1735 (fmap (ai inpat True env ds) g)
1736 ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1737 ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1738 ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1739 ai inpat qq env ds tm = tm
1741 handleErr (Left err) = PElabError err
1742 handleErr (Right x) = x
1744-- if in a pattern, and there are no arguments, and there's no possible
1745-- names with zero explicit arguments, don't add implicits.
1747aiFn :: Name -> Bool -> Bool -> Bool
1748 -> [Name]
1749 -> IState -> FC
1750 -> Name -- ^ function being applied
1751 -> FC -> [[T.Text]]
1752 -> [PArg] -- ^ initial arguments (if in a pattern)
1753 -> [PArg] -- ^ initial arguments (if in an expression)
1754 -> Either Err PTerm
1755aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _
1756 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
1757 | otherwise
1758 = case lookupDef f (tt_ctxt ist) of
1759 [] -> Right $ PPatvar ffc f
1760 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1761 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1762 if (not (vname f) || tcname f
1763 || any (conCaf (tt_ctxt ist)) ialts)
1764-- any constructor alts || any allImp ialts))
1765 then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor
1766 else Right $ PPatvar ffc f
1767 where imp (PExp _ _ _ _) = False
1768 imp _ = True
1769-- allImp [] = False
1770 allImp xs = all imp xs
1772 unqualified (NS _ _) = False
1773 unqualified _ = True
1775 constructor (TyDecl (DCon _ _ _) _) = True
1776 constructor _ = False
1778 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1780 vname (UN n) = True -- non qualified
1781 vname _ = False
1783aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1784 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1785aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1786 -- This is where namespaces get resolved by adding PAlternative
1787 = do let ns = lookupCtxtName f (idris_implicits ist)
1788 let nh = filter (\(n, _) -> notHidden n) ns
1789 let ns' = case trimAlts ds nh of
1790 [] -> nh
1791 x -> x
1792 case ns' of
1793 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1794 (insertImpl ns (chooseArgs f' as asexp))
1795 [] -> if f `elem` (map fst (idris_metavars ist))
1796 then Right $ PApp fc (PRef ffc [ffc] f) as
1797 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1798 alts -> Right $
1799 PAlternative [] (ExactlyOne True) $
1800 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1801 (insertImpl ns (chooseArgs f' as asexp))) alts
1802 where
1803 -- choose whether to treat the arguments as patterns or expressions
1804 -- if 'f' is a defined function, treat as expression, otherwise do the default.
1805 -- This is so any names which later go under a PHidden are treated
1806 -- as function names rather than bound pattern variables
1807 chooseArgs f as asexp | isConName f (tt_ctxt ist) = as
1808 | f == topname = as
1809 | Nothing <- lookupDefExact f (tt_ctxt ist) = as
1810 | otherwise = asexp
1812 -- if the name is in imp_meths, we should actually refer to the bound
1813 -- name rather than the global one after expanding implicits
1814 isImpName f f' | f `elem` imp_meths = f
1815 | otherwise = f'
1817 trimAlts [] alts = alts
1818 trimAlts ns alts
1819 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1821 nspace (NS _ s) = s
1822 nspace _ = []
1824 notHidden n = case getAccessibility n of
1825 Hidden -> False
1826 _ -> True
1828 getAccessibility n
1829 = case lookupDefAccExact n False (tt_ctxt ist) of
1830 Just (n,t) -> t
1831 _ -> Public
1833 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)
1834 -> [PArg] -- ^ given arguments
1835 -> [PArg]
1836 insertImpl ps as
1837 = let (as', badimpls) = partition (impIn ps) as in
1838 map addUnknownImp badimpls ++
1839 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
1841 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1842 -> [PArg] -- parameters
1843 -> [PArg] -- explicit arguments
1844 -> [PArg] -- implicits given
1845 -> [PArg]
1846 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1847 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1848 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1849 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1850 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1851 let rtc = PResolveTC fc in
1852 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1853 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1854 case find n imps [] of
1855 Just (tm, imps') ->
1856 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1857 Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in
1858 PImp p True l n ph :
1859 insImpAcc (M.insert n ph pnas) ps given imps
1860 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1861 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1862 case find n imps [] of
1863 Just (tm, imps') ->
1864 PTacImplicit p l n sc tm :
1865 insImpAcc (M.insert n tm pnas) ps given imps'
1866 Nothing ->
1867 if inpat
1868 then PTacImplicit p l n sc Placeholder :
1869 insImpAcc (M.insert n Placeholder pnas) ps given imps
1870 else PTacImplicit p l n sc sc :
1871 insImpAcc (M.insert n sc pnas) ps given imps
1872 insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error
1873 insImpAcc _ _ given imps = given ++ imps
1875 addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }
1877 find n [] acc = Nothing
1878 find n (PImp _ _ _ n' t : gs) acc
1879 | n == n' = Just (t, reverse acc ++ gs)
1880 find n (PTacImplicit _ _ n' _ t : gs) acc
1881 | n == n' = Just (t, reverse acc ++ gs)
1882 find n (g : gs) acc = find n gs (g : acc)
1884-- return True if the second argument is an implicit argument which is
1885-- expected in the implicits, or if it's not an implicit
1886impIn :: [PArg] -> PArg -> Bool
1887impIn ps (PExp _ _ _ _) = True
1888impIn ps (PConstraint _ _ _ _) = True
1889impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1891expArg (PExp _ _ _ _) = True
1892expArg (PConstraint _ _ _ _) = True
1893expArg _ = False
1895-- replace non-linear occurrences with _
1897stripLinear :: IState -> PTerm -> PTerm
1898stripLinear i tm = evalState (sl tm) [] where
1899 sl :: PTerm -> State [Name] PTerm
1900 sl (PRef fc hl f)
1901 | (_:_) <- lookupTy f (tt_ctxt i)
1902 = return $ PRef fc hl f
1903 | otherwise = do ns <- get
1904 if (f `elem` ns)
1905 then return $ PHidden (PRef fc hl f) -- Placeholder
1906 else do put (f : ns)
1907 return (PRef fc hl f)
1908 sl (PPatvar fc f)
1909 = do ns <- get
1910 if (f `elem` ns)
1911 then return $ PHidden (PPatvar fc f) -- Placeholder
1912 else do put (f : ns)
1913 return (PPatvar fc f)
1914 -- Assumption is that variables are all the same in each alternative
1915 sl t@(PAlternative ms b as) = do ns <- get
1916 as' <- slAlts ns as
1917 return (PAlternative ms b as')
1918 where slAlts ns (a : as) = do put ns
1919 a' <- sl a
1920 as' <- slAlts ns as
1921 return (a' : as')
1922 slAlts ns [] = return []
1923 sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')
1924 sl (PDPair fc hls p l t r) = do l' <- sl l
1925 t' <- sl t
1926 r' <- sl r
1927 return (PDPair fc hls p l' t' r')
1928 sl (PApp fc fn args) = do fn' <- case fn of
1929 -- Just the args, fn isn't matchable as a var
1930 PRef _ _ _ -> return fn
1931 t -> sl t
1932 args' <- mapM slA args
1933 return $ PApp fc fn' args'
1934 where slA (PImp p m l n t) = do t' <- sl t
1935 return $ PImp p m l n t'
1936 slA (PExp p l n t) = do t' <- sl t
1937 return $ PExp p l n t'
1938 slA (PConstraint p l n t)
1939 = do t' <- sl t
1940 return $ PConstraint p l n t'
1941 slA (PTacImplicit p l n sc t)
1942 = do t' <- sl t
1943 return $ PTacImplicit p l n sc t'
1944 sl x = return x
1946-- | Remove functions which aren't applied to anything, which must then
1947-- be resolved by unification. Assume names resolved and alternatives
1948-- filled in (so no ambiguity).
1949stripUnmatchable :: IState -> PTerm -> PTerm
1950stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1951 su :: PTerm -> PTerm
1952 su tm@(PRef fc hl f)
1953 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1954 = Placeholder
1955 | (TType _ : _) <- lookupTy f (tt_ctxt i),
1956 not (implicitable f)
1957 = PHidden tm
1958 | (UType _ : _) <- lookupTy f (tt_ctxt i),
1959 not (implicitable f)
1960 = PHidden tm
1961 su (PApp fc f@(PRef _ _ fn) args)
1962 -- here we use canBeDConName because the impossible pattern
1963 -- check will not necessarily fully resolve constructor names,
1964 -- and these bare names will otherwise get in the way of
1965 -- impossbility checking.
1966 | canBeDConName fn ctxt
1967 = PApp fc f (fmap (fmap su) args)
1968 su (PApp fc f args)
1969 = PHidden (PApp fc f args)
1970 su (PAlternative ms b alts)
1971 = let alts' = filter (/= Placeholder) (map su alts) in
1972 if null alts' then Placeholder
1973 else PAlternative ms b alts'
1974 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)
1975 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)
1976 su t@(PLam fc _ _ _ _) = PHidden t
1977 su t@(PPi _ _ _ _ _) = PHidden t
1978 su t@(PConstant _ c) | isTypeConst c = PHidden t
1979 su t = t
1981 ctxt = tt_ctxt i
1983stripUnmatchable i tm = tm
1985mkPApp fc a f [] = f
1986mkPApp fc a f as = let rest = drop a as in
1987 if a == 0 then appRest fc f rest
1988 else appRest fc (PApp fc f (take a as)) rest
1989 where
1990 appRest fc f [] = f
1991 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1993-- Find 'static' argument positions
1994-- (the declared ones, plus any names in argument position in the declared
1995-- statics)
1996-- FIXME: It's possible that this really has to happen after elaboration
1998findStatics :: IState -> PTerm -> (PTerm, [Bool])
1999findStatics ist tm = let (ns, ss) = fs tm
2000 in runState (pos ns ss tm) []
2001 where fs (PPi p n fc t sc)
2002 | Static <- pstatic p
2003 = let (ns, ss) = fs sc in
2004 (namesIn [] ist t : ns, n : ss)
2005 | otherwise = let (ns, ss) = fs sc in
2006 (ns, ss)
2007 fs _ = ([], [])
2009 inOne n ns = length (filter id (map (elem n) ns)) == 1
2011 pos ns ss (PPi p n fc t sc)
2012 | elem n ss = do sc' <- pos ns ss sc
2013 spos <- get
2014 put (True : spos)
2015 return (PPi (p { pstatic = Static }) n fc t sc')
2016 | otherwise = do sc' <- pos ns ss sc
2017 spos <- get
2018 put (False : spos)
2019 return (PPi p n fc t sc')
2020 pos ns ss t = return t
2022-- for 6.12/7 compatibility
2023data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
2025instance Applicative (EitherErr a) where
2026 pure = return
2027 (<*>) = ap
2029instance Monad (EitherErr a) where
2030 return = RightOK
2032 (LeftErr e) >>= k = LeftErr e
2033 RightOK v >>= k = k v
2035toEither (LeftErr e) = Left e
2036toEither (RightOK ho) = Right ho
2038-- | Syntactic match of a against b, returning pair of variables in a
2039-- and what they match. Returns the pair that failed if not a match.
2040matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2041matchClause = matchClause' False
2043matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
2044matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
2045 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
2047 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2048 fullApp x = x
2050 match' x y = match (fullApp x) (fullApp y)
2051 match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'
2052 | fi == txt "fromInteger" && b == txt "builtins",
2053 PConstant _ (I _) <- getTm x = match (getTm x) x'
2054 match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])
2055 | fi == txt "fromInteger" && b == txt "builtins",
2056 PConstant _ (I _) <- getTm x = match (getTm x) x'
2057 match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
2058 match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
2059 match (PApp _ f args) (PApp _ f' args')
2060 | length args == length args'
2061 = do mf <- match' f f'
2062 ms <- zipWithM matchArg args args'
2063 return (mf ++ concat ms)
2064 match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x
2065 match (PPatvar f n) xr = match (PRef f [f] n) xr
2066 match xr (PPatvar f n) = match xr (PRef f [f] n)
2067 match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)
2068 match (PRef _ _ n) tm@(PRef _ _ n')
2069 | n == n' && not names &&
2070 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
2071 || tm == Placeholder)
2072 = return [(n, tm)]
2073 -- if one namespace is missing, drop the other
2074 | n == n' || n == dropNS n' || dropNS n == n' = return []
2075 where dropNS (NS n _) = n
2076 dropNS n = n
2077 match (PRef _ _ n) tm
2078 | not names && (not (isConName n (tt_ctxt i) ||
2079 isFnName n (tt_ctxt i)) || tm == Placeholder)
2080 = return [(n, tm)]
2081 match (PRewrite _ l r _) (PRewrite _ l' r' _)
2082 = do ml <- match' l l'
2083 mr <- match' r r'
2084 return (ml ++ mr)
2085 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
2086 mr <- match r r'
2087 return (ml ++ mr)
2088 match (PTyped l r) x = match l x
2089 match x (PTyped l r) = match x l
2090 match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'
2091 mr <- match' r r'
2092 return (ml ++ mr)
2093 match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'
2094 mt <- match' t t'
2095 mr <- match' r r'
2096 return (ml ++ mt ++ mr)
2097 match (PAlternative _ a as) (PAlternative _ a' as')
2098 = do ms <- zipWithM match' as as'
2099 return (concat ms)
2100 match a@(PAlternative _ _ as) b
2101 = do let ms = zipWith match' as (repeat b)
2102 case (rights (map toEither ms)) of
2103 (x: _) -> return x
2104 _ -> LeftErr (a, b)
2105 match (PCase _ _ _) _ = return [] -- lifted out
2106 match (PMetavar _ _) _ = return [] -- modified
2107 match (PInferRef _ _ _) _ = return [] -- modified
2108 match (PQuote _) _ = return []
2109 match (PProof _) _ = return []
2110 match (PTactics _) _ = return []
2111 match (PResolveTC _) (PResolveTC _) = return []
2112 match (PTrue _ _) (PTrue _ _) = return []
2113 match (PReturn _) (PReturn _) = return []
2114 match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
2115 ms <- match' s s'
2116 return (mt ++ ms)
2117 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
2118 ms <- match' s s'
2119 return (mt ++ ms)
2120 match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'
2121 mty <- match' ty ty'
2122 ms <- match' s s'
2123 return (mt ++ mty ++ ms)
2124 match (PHidden x) (PHidden y)
2125 | RightOK xs <- match x y = return xs -- to collect variables
2126 | otherwise = return [] -- Otherwise hidden things are unmatchable
2127 match (PHidden x) y
2128 | RightOK xs <- match x y = return xs
2129 | otherwise = return []
2130 match x (PHidden y)
2131 | RightOK xs <- match x y = return xs
2132 | otherwise = return []
2133 match (PUnifyLog x) y = match' x y
2134 match x (PUnifyLog y) = match' x y
2135 match (PNoImplicits x) y = match' x y
2136 match x (PNoImplicits y) = match' x y
2137 match Placeholder _ = return []
2138 match _ Placeholder = return []
2139 match (PResolveTC _) _ = return []
2140 match a b | a == b = return []
2141 | otherwise = LeftErr (a, b)
2143 checkRpts (RightOK ms) = check ms where
2144 check ((n,t):xs)
2145 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
2146 then Left (t, t')
2147 else check xs
2148 check (_:xs) = check xs
2149 check [] = Right ms
2150 checkRpts (LeftErr x) = Left x
2152substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
2153substMatches ms = substMatchesShadow ms []
2155substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
2156substMatchesShadow [] shs t = t
2157substMatchesShadow ((n,tm):ns) shs t
2158 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
2160substMatch :: Name -> PTerm -> PTerm -> PTerm
2161substMatch n = substMatchShadow n []
2163substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
2164substMatchShadow n shs tm t = sm shs t where
2165 sm xs (PRef _ _ n') | n == n' = tm
2166 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2167 sm xs (PPi p x fc t sc)
2168 | x `elem` xs
2169 = let x' = nextName x in
2170 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2171 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2172 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2173 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2174 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2175 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)
2176 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2177 (fmap (sm xs) tm)
2178 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2179 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)
2180 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)
2181 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)
2182 sm xs (PHidden x) = PHidden (sm xs x)
2183 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2184 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2185 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns
2186 sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)
2187 sm xs x = x
2189 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2190 fullApp x = x
2192shadow :: Name -> Name -> PTerm -> PTerm
2193shadow n n' t = sm 0 t where
2194 sm 0 (PRef fc hl x) | n == x = PRef fc hl n'
2195 sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)
2196 | otherwise = PLam fc x xfc (sm 0 t) sc
2197 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)
2198 | otherwise = PPi p x fc (sm 0 t) sc
2199 sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)
2200 | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc
2201 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)
2202 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)
2203 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)
2204 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)
2205 sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)
2206 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2207 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2208 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2209 sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)
2210 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2211 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2212 sm 0 (PHidden x) = PHidden (sm 0 x)
2213 sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)
2214 sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)
2215 sm 0 (PCoerced t) = PCoerced (sm 0 t)
2216 sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)
2217 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)
2218 sm ql x = descend (sm ql) x
2220-- | Rename any binders which are repeated (so that we don't have to mess
2221-- about with shadowing anywhere else).
2222mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
2223mkUniqueNames env shadows tm
2224 = evalState (mkUniq 0 initMap tm) (S.fromList env) where
2226 initMap = M.fromList shadows
2228 inScope :: S.Set Name
2229 inScope = S.fromList $ boundNamesIn tm
2231 mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)
2232 return (arg { getTm = t' })
2234 -- Initialise the unique name with the environment length (so we're not
2235 -- looking for too long...)
2236 initN (UN n) l = UN $ txt (str n ++ show l)
2237 initN (MN i s) l = MN (i+l) s
2238 initN n l = n
2240 -- FIXME: Probably ought to do this for completeness! It's fine as
2241 -- long as there are no bindings inside tactics though.
2242 mkUniqT _ nmap tac = return tac
2244 mkUniq :: Int -- ^ The number of quotations that we're under
2245 -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm
2246 mkUniq 0 nmap (PLam fc n nfc ty sc)
2247 = do env <- get
2248 (n', sc') <-
2249 if n `S.member` env
2250 then do let n' = uniqueNameSet (initN n (S.size env))
2251 (S.union env inScope)
2252 return (n', sc) -- shadow n n' sc)
2253 else return (n, sc)
2254 put (S.insert n' env)
2255 let nmap' = M.insert n n' nmap
2256 ty' <- mkUniq 0 nmap ty
2257 sc'' <- mkUniq 0 nmap' sc'
2258 return $! PLam fc n' nfc ty' sc''
2259 mkUniq 0 nmap (PPi p n fc ty sc)
2260 = do env <- get
2261 (n', sc') <-
2262 if n `S.member` env
2263 then do let n' = uniqueNameSet (initN n (S.size env))
2264 (S.union env inScope)
2265 return (n', sc) -- shadow n n' sc)
2266 else return (n, sc)
2267 put (S.insert n' env)
2268 let nmap' = M.insert n n' nmap
2269 ty' <- mkUniq 0 nmap ty
2270 sc'' <- mkUniq 0 nmap' sc'
2271 return $! PPi p n' fc ty' sc''
2272 mkUniq 0 nmap (PLet fc n nfc ty val sc)
2273 = do env <- get
2274 (n', sc') <-
2275 if n `S.member` env
2276 then do let n' = uniqueNameSet (initN n (S.size env))
2277 (S.union env inScope)
2278 return (n', sc) -- shadow n n' sc)
2279 else return (n, sc)
2280 put (S.insert n' env)
2281 let nmap' = M.insert n n' nmap
2282 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val
2283 sc'' <- mkUniq 0 nmap' sc'
2284 return $! PLet fc n' nfc ty' val' sc''
2285 mkUniq 0 nmap (PApp fc t args)
2286 = do t' <- mkUniq 0 nmap t
2287 args' <- mapM (mkUniqA 0 nmap) args
2288 return $! PApp fc t' args'
2289 mkUniq 0 nmap (PAppBind fc t args)
2290 = do t' <- mkUniq 0 nmap t
2291 args' <- mapM (mkUniqA 0 nmap) args
2292 return $! PAppBind fc t' args'
2293 mkUniq 0 nmap (PCase fc t alts)
2294 = do t' <- mkUniq 0 nmap t
2295 alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y
2296 return (x', y')) alts
2297 return $! PCase fc t' alts'
2298 mkUniq 0 nmap (PIfThenElse fc c t f)
2299 = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)
2300 mkUniq 0 nmap (PPair fc hls p l r)
2301 = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r
2302 return $! PPair fc hls p l' r'
2303 mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)
2304 | t /= Placeholder
2305 = do env <- get
2306 (n', sc') <- if n `S.member` env
2307 then do let n' = uniqueNameSet n (S.union env inScope)
2308 return (n', sc) -- shadow n n' sc)
2309 else return (n, sc)
2310 put (S.insert n' env)
2311 let nmap' = M.insert n n' nmap
2312 t' <- mkUniq 0 nmap t
2313 sc'' <- mkUniq 0 nmap' sc'
2314 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''
2315 mkUniq 0 nmap (PDPair fc hls p l t r)
2316 = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r
2317 return $! PDPair fc hls p l' t' r'
2318 mkUniq 0 nmap (PAlternative ns b as)
2319 -- store the nmap and defer the rest until we've pruned the set
2320 -- during elaboration
2321 = return $ PAlternative (M.toList nmap ++ ns) b as
2322 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)
2323 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)
2324 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)
2325 mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)
2326 mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)
2327 mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)
2328 mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)
2329 mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)
2330 mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)
2331 mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t
2332 where
2333 shadowAll [] t = t
2334 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)
2336 mkUniq ql nmap (PQuasiquote tm ty) =
2337 do tm' <- mkUniq (ql + 1) nmap tm
2338 ty' <- case ty of
2339 Nothing -> return Nothing
2340 Just t -> fmap Just $ mkUniq ql nmap t
2341 return $! PQuasiquote tm' ty'
2342 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)
2344 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm