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