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