git.iko.soy/Idris-dev
on dcdebfc help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1820 lines 75 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.IdeSlave hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.State
23import Control.Monad.Error(throwError)
25import Data.List
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 Control.Monad.Error (throwError, catchError)
37import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
39import Util.Pretty
40import Util.ScreenSize
41import Util.System
43getContext :: Idris Context
44getContext = do i <- getIState; return (tt_ctxt i)
46forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
49getObjectFiles :: Codegen -> Idris [FilePath]
50getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
52addObjectFile :: Codegen -> FilePath -> Idris ()
53addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
55getLibs :: Codegen -> Idris [String]
56getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
58addLib :: Codegen -> String -> Idris ()
59addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
61getFlags :: Codegen -> Idris [String]
62getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
64addFlag :: Codegen -> String -> Idris ()
65addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
67addDyLib :: [String] -> Idris (Either DynamicLib String)
68addDyLib libs = do i <- getIState
69 let ls = idris_dynamic_libs i
70 let importdirs = opt_importdirs (idris_options i)
71 case mapMaybe (findDyLib ls) libs of
72 x:_ -> return (Left x)
73 [] -> do
74 handle <- lift . lift .
75 mapM (\l -> catchIO (tryLoadLib importdirs l)
76 (\_ -> return Nothing)) $ libs
77 case msum handle of
78 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
79 concat (intersperse "," libs) ++ "\"")
80 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
81 return (Left x)
82 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
83 findDyLib [] l = Nothing
84 findDyLib (lib:libs) l | l == lib_name lib = Just lib
85 | otherwise = findDyLib libs l
88addHdr :: Codegen -> String -> Idris ()
89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
91addImported :: FilePath -> Idris ()
92addImported f = do i <- getIState
93 putIState $ i { idris_imported = nub $ f : idris_imported i }
95addLangExt :: LanguageExt -> Idris ()
96addLangExt TypeProviders = do i <- getIState
97 putIState $ i {
98 idris_language_extensions = TypeProviders : idris_language_extensions i
99 }
100addLangExt ErrorReflection = do i <- getIState
101 putIState $ i {
102 idris_language_extensions = ErrorReflection : idris_language_extensions i
103 }
105addTrans :: (Term, Term) -> Idris ()
106addTrans t = do i <- getIState
107 putIState $ i { idris_transforms = t : idris_transforms i }
109addErrRev :: (Term, Term) -> Idris ()
110addErrRev t = do i <- getIState
111 putIState $ i { idris_errRev = t : idris_errRev i }
113totcheck :: (FC, Name) -> Idris ()
114totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
116defer_totcheck :: (FC, Name) -> Idris ()
117defer_totcheck n
118 = do i <- getIState;
119 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
121clear_totcheck :: Idris ()
122clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
124setFlags :: Name -> [FnOpt] -> Idris ()
125setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
127setAccessibility :: Name -> Accessibility -> Idris ()
128setAccessibility n a
129 = do i <- getIState
130 let ctxt = setAccess n a (tt_ctxt i)
131 putIState $ i { tt_ctxt = ctxt }
133setTotality :: Name -> Totality -> Idris ()
134setTotality n a
135 = do i <- getIState
136 let ctxt = setTotal n a (tt_ctxt i)
137 putIState $ i { tt_ctxt = ctxt }
139getTotality :: Name -> Idris Totality
140getTotality n
141 = do i <- getIState
142 case lookupTotal n (tt_ctxt i) of
143 [t] -> return t
144 _ -> return (Total [])
146-- Get coercions which might return the required type
147getCoercionsTo :: IState -> Type -> [Name]
148getCoercionsTo i ty =
149 let cs = idris_coercions i
150 (fn,_) = unApply (getRetTy ty) in
151 findCoercions fn cs
152 where findCoercions t [] = []
153 findCoercions t (n : ns) =
154 let ps = case lookupTy n (tt_ctxt i) of
155 [ty'] -> case unApply (getRetTy ty') of
156 (t', _) ->
157 if t == t' then [n] else []
158 _ -> [] in
159 ps ++ findCoercions t ns
161addToCG :: Name -> CGInfo -> Idris ()
162addToCG n cg
163 = do i <- getIState
164 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
166addTyInferred :: Name -> Idris ()
167addTyInferred n
168 = do i <- getIState
169 putIState $ i { idris_tyinfodata =
170 addDef n TIPartial (idris_tyinfodata i) }
172addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
173addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
174 mapM_ addConstraint ts
175 return ()
176 where addConstraint (x, y) = findMVApps x y
178 findMVApps x y
179 = do let (fx, argsx) = unApply x
180 let (fy, argsy) = unApply y
181 if (not (fx == fy))
182 then do
183 tryAddMV fx y
184 tryAddMV fy x
185 else mapM_ addConstraint (zip argsx argsy)
187 tryAddMV (P _ mv _) y =
188 do ist <- get
189 case lookup mv (idris_metavars ist) of
190 Just _ -> addConstraintRule mv y
191 _ -> return ()
192 tryAddMV _ _ = return ()
194 addConstraintRule :: Name -> Term -> Idris ()
195 addConstraintRule n t
196 = do ist <- get
197 logLvl 1 $ "TI constraint: " ++ show (n, t)
198 case lookupCtxt n (idris_tyinfodata ist) of
199 [TISolution ts] ->
200 do mapM_ (checkConsistent t) ts
201 let ti' = addDef n (TISolution (t : ts))
202 (idris_tyinfodata ist)
203 put $ ist { idris_tyinfodata = ti' }
204 _ ->
205 do let ti' = addDef n (TISolution [t])
206 (idris_tyinfodata ist)
207 put $ ist { idris_tyinfodata = ti' }
209 -- Check a solution is consistent with previous solutions
210 -- Meaning: If heads are both data types, they had better be the
211 -- same.
212 checkConsistent :: Term -> Term -> Idris ()
213 checkConsistent x y =
214 do let (fx, _) = unApply x
215 let (fy, _) = unApply y
216 case (fx, fy) of
217 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
218 (P (TCon _ _) n _, Constant _) -> errWhen True
219 (Constant _, P (TCon _ _) n' _) -> errWhen True
220 (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)
221 _ -> return ()
223 where errWhen True
224 = throwError (At fc
225 (CantUnify False x y (Msg "") [] 0))
226 errWhen False = return ()
228isTyInferred :: Name -> Idris Bool
229isTyInferred n
230 = do i <- getIState
231 case lookupCtxt n (idris_tyinfodata i) of
232 [TIPartial] -> return True
233 _ -> return False
235-- | Adds error handlers for a particular function and argument. If names are
236-- ambiguous, all matching handlers are updated.
237addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
238addFunctionErrorHandlers f arg hs =
239 do i <- getIState
240 let oldHandlers = idris_function_errorhandlers i
241 let newHandlers = flip (addDef f) oldHandlers $
242 case lookupCtxtExact f oldHandlers of
243 Nothing -> M.singleton arg (S.fromList hs)
244 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
245 -- will always be one of those two, thus no extra case
246 putIState $ i { idris_function_errorhandlers = newHandlers }
248getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
249getFunctionErrorHandlers f arg = do i <- getIState
250 return . maybe [] S.toList $
251 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
254-- Trace all the names in a call graph starting at the given name
255getAllNames :: Name -> Idris [Name]
256getAllNames n = allNames [] n
258allNames :: [Name] -> Name -> Idris [Name]
259allNames ns n | n `elem` ns = return []
260allNames ns n = do i <- getIState
261 case lookupCtxtExact n (idris_callgraph i) of
262 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
263 return (nub (n : concat more))
264 _ -> return [n]
266addCoercion :: Name -> Idris ()
267addCoercion n = do i <- getIState
268 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
270addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
271addDocStr n doc args
272 = do i <- getIState
273 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
275addNameHint :: Name -> Name -> Idris ()
276addNameHint ty n
277 = do i <- getIState
278 ty' <- case lookupCtxtName ty (idris_implicits i) of
279 [(tyn, _)] -> return tyn
280 [] -> throwError (NoSuchVariable ty)
281 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
282 let ns' = case lookupCtxt ty' (idris_namehints i) of
283 [ns] -> ns ++ [n]
284 _ -> [n]
285 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
287getNameHints :: IState -> Name -> [Name]
288getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
289getNameHints i n =
290 case lookupCtxt n (idris_namehints i) of
291 [ns] -> ns
292 _ -> []
294addToCalledG :: Name -> [Name] -> Idris ()
295addToCalledG n ns = return () -- TODO
297-- Add a class instance function. Dodgy hack: Put integer instances first in the
298-- list so they are resolved by default.
299-- Dodgy hack 2: put constraint chasers (@@) last
301addInstance :: Bool -> Name -> Name -> Idris ()
302addInstance int n i
303 = do ist <- getIState
304 case lookupCtxt n (idris_classes ist) of
305 [CI a b c d e ins] ->
306 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
307 putIState $ ist { idris_classes = cs }
308 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
309 putIState $ ist { idris_classes = cs }
310 where addI i ins | int = i : ins
311 | chaser n = ins ++ [i]
312 | otherwise = insI i ins
313 insI i [] = [i]
314 insI i (n : ns) | chaser n = i : n : ns
315 | otherwise = n : insI i ns
317 chaser (UN nm)
318 | ('@':'@':_) <- str nm = True
319 chaser (NS n _) = chaser n
320 chaser _ = False
322addClass :: Name -> ClassInfo -> Idris ()
323addClass n i
324 = do ist <- getIState
325 let i' = case lookupCtxt n (idris_classes ist) of
326 [c] -> c { class_instances = class_instances i }
327 _ -> i
328 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
330addIBC :: IBCWrite -> Idris ()
331addIBC ibc@(IBCDef n)
332 = do i <- getIState
333 when (notDef (ibc_write i)) $
334 putIState $ i { ibc_write = ibc : ibc_write i }
335 where notDef [] = True
336 notDef (IBCDef n': is) | n == n' = False
337 notDef (_ : is) = notDef is
338addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
340clearIBC :: Idris ()
341clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
343resetNameIdx :: Idris ()
344resetNameIdx = do i <- getIState
345 put (i { idris_nameIdx = (0, emptyContext) })
347-- Used to preserve sharing of names
348addNameIdx :: Name -> Idris (Int, Name)
349addNameIdx n = do i <- getIState
350 let (i', x) = addNameIdx' i n
351 return x
353addNameIdx' :: IState -> Name -> (IState, (Int, Name))
354addNameIdx' i n
355 = let idxs = snd (idris_nameIdx i) in
356 case lookupCtxt n idxs of
357 [x] -> (i, x)
358 _ -> let i' = fst (idris_nameIdx i) + 1 in
359 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
361getHdrs :: Codegen -> Idris [String]
362getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
364getImported :: Idris [FilePath]
365getImported = do i <- getIState; return (idris_imported i)
367setErrSpan :: FC -> Idris ()
368setErrSpan x = do i <- getIState;
369 case (errSpan i) of
370 Nothing -> putIState $ i { errSpan = Just x }
371 Just _ -> return ()
373clearErr :: Idris ()
374clearErr = do i <- getIState
375 putIState $ i { errSpan = Nothing }
377getSO :: Idris (Maybe String)
378getSO = do i <- getIState
379 return (compiled_so i)
381setSO :: Maybe String -> Idris ()
382setSO s = do i <- getIState
383 putIState $ (i { compiled_so = s })
385getIState :: Idris IState
386getIState = get
388putIState :: IState -> Idris ()
389putIState = put
391-- | A version of liftIO that puts errors into the exception type of the Idris monad
392runIO :: IO a -> Idris a
393runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
394-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
396getName :: Idris Int
397getName = do i <- getIState;
398 let idx = idris_name i;
399 putIState $ (i { idris_name = idx + 1 })
400 return idx
402-- InternalApp keeps track of the real function application for making case splits from, not the application the
403-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
404addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
405addInternalApp fp l t
406 = do i <- getIState
407 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
409getInternalApp :: FilePath -> Int -> Idris PTerm
410getInternalApp fp l = do i <- getIState
411 case lookup (fp, l) (idris_lineapps i) of
412 Just n' -> return n'
413 Nothing -> return Placeholder
414 -- TODO: What if it's not there?
416-- Pattern definitions are only used for coverage checking, so erase them
417-- when we're done
418clearOrigPats :: Idris ()
419clearOrigPats = do i <- get
420 let ps = idris_patdefs i
421 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
422 put (i { idris_patdefs = ps' })
424-- Erase types from Ps in the context (basically ending up with what's in
425-- the .ibc, which is all we need after all the analysis is done)
426clearPTypes :: Idris ()
427clearPTypes = do i <- get
428 let ctxt = tt_ctxt i
429 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
430 where pErase (CaseOp c t tys orig tot cds)
431 = CaseOp c t tys orig [] (pErase' cds)
432 pErase x = x
433 pErase' (CaseDefs _ (cs, c) _ rs)
434 = let c' = (cs, fmap pEraseType c) in
435 CaseDefs c' c' c' rs
437checkUndefined :: FC -> Name -> Idris ()
438checkUndefined fc n
439 = do i <- getContext
440 case lookupTy n i of
441 (_:_) -> throwError . Msg $ show fc ++ ":" ++
442 show n ++ " already defined"
443 _ -> return ()
445isUndefined :: FC -> Name -> Idris Bool
446isUndefined fc n
447 = do i <- getContext
448 case lookupTy n i of
449 (_:_) -> return False
450 _ -> return True
452setContext :: Context -> Idris ()
453setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
455updateContext :: (Context -> Context) -> Idris ()
456updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
458addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
459addConstraints fc (v, cs)
460 = do i <- getIState
461 let ctxt = tt_ctxt i
462 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
463 next_tvar = v }
464 let ics = zip cs (repeat fc) ++ idris_constraints i
465 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
467addDeferred = addDeferred' Ref
468addDeferredTyCon = addDeferred' (TCon 0 0)
470addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
471addDeferred' nt ns
472 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
473 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
474 i <- getIState
475 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
476 idris_metavars i }
477 where tidyNames used (Bind (MN i x) b sc)
478 = let n' = uniqueName (UN x) used in
479 Bind n' b $ tidyNames (n':used) sc
480 tidyNames used (Bind n b sc)
481 = let n' = uniqueName n used in
482 Bind n' b $ tidyNames (n':used) sc
483 tidyNames used b = b
485solveDeferred :: Name -> Idris ()
486solveDeferred n = do i <- getIState
487 putIState $ i { idris_metavars =
488 filter (\(n', _) -> n/=n')
489 (idris_metavars i),
490 ibc_write =
491 filter (notMV n) (ibc_write i)
492 }
493 where notMV n (IBCMetavar n') = not (n == n')
494 notMV n _ = True
496getUndefined :: Idris [Name]
497getUndefined = do i <- getIState
498 return (map fst (idris_metavars i) \\ primDefs)
500isMetavarName :: Name -> IState -> Bool
501isMetavarName n ist
502 = case lookupNames n (tt_ctxt ist) of
503 (t:_) -> isJust $ lookup t (idris_metavars ist)
504 _ -> False
506getWidth :: Idris ConsoleWidth
507getWidth = fmap idris_consolewidth getIState
509setWidth :: ConsoleWidth -> Idris ()
510setWidth w = do ist <- getIState
511 put ist { idris_consolewidth = w }
513renderWidth :: Idris Int
514renderWidth = do iw <- getWidth
515 case iw of
516 InfinitelyWide -> return 100000000
517 ColsWide n -> return (max n 1)
518 AutomaticWidth -> runIO getScreenWidth
522type1Doc :: Doc OutputAnnotation
523type1Doc = (annotate AnnConstType $ text "Type 1")
526isetPrompt :: String -> Idris ()
527isetPrompt p = do i <- getIState
528 case idris_outputmode i of
529 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
531setLogLevel :: Int -> Idris ()
532setLogLevel l = do i <- getIState
533 let opts = idris_options i
534 let opt' = opts { opt_logLevel = l }
535 putIState $ i { idris_options = opt' }
537setCmdLine :: [Opt] -> Idris ()
538setCmdLine opts = do i <- getIState
539 let iopts = idris_options i
540 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
542getCmdLine :: Idris [Opt]
543getCmdLine = do i <- getIState
544 return (opt_cmdline (idris_options i))
546getDumpDefun :: Idris (Maybe FilePath)
547getDumpDefun = do i <- getIState
548 return $ findC (opt_cmdline (idris_options i))
549 where findC [] = Nothing
550 findC (DumpDefun x : _) = Just x
551 findC (_ : xs) = findC xs
553getDumpCases :: Idris (Maybe FilePath)
554getDumpCases = do i <- getIState
555 return $ findC (opt_cmdline (idris_options i))
556 where findC [] = Nothing
557 findC (DumpCases x : _) = Just x
558 findC (_ : xs) = findC xs
560logLevel :: Idris Int
561logLevel = do i <- getIState
562 return (opt_logLevel (idris_options i))
564setErrContext :: Bool -> Idris ()
565setErrContext t = do i <- getIState
566 let opts = idris_options i
567 let opt' = opts { opt_errContext = t }
568 putIState $ i { idris_options = opt' }
570errContext :: Idris Bool
571errContext = do i <- getIState
572 return (opt_errContext (idris_options i))
574useREPL :: Idris Bool
575useREPL = do i <- getIState
576 return (opt_repl (idris_options i))
578setREPL :: Bool -> Idris ()
579setREPL t = do i <- getIState
580 let opts = idris_options i
581 let opt' = opts { opt_repl = t }
582 putIState $ i { idris_options = opt' }
584showOrigErr :: Idris Bool
585showOrigErr = do i <- getIState
586 return (opt_origerr (idris_options i))
588setShowOrigErr :: Bool -> Idris ()
589setShowOrigErr b = do i <- getIState
590 let opts = idris_options i
591 let opt' = opts { opt_origerr = b }
592 putIState $ i { idris_options = opt' }
594setAutoSolve :: Bool -> Idris ()
595setAutoSolve b = do i <- getIState
596 let opts = idris_options i
597 let opt' = opts { opt_autoSolve = b }
598 putIState $ i { idris_options = opt' }
600setNoBanner :: Bool -> Idris ()
601setNoBanner n = do i <- getIState
602 let opts = idris_options i
603 let opt' = opts { opt_nobanner = n }
604 putIState $ i { idris_options = opt' }
606getNoBanner :: Idris Bool
607getNoBanner = do i <- getIState
608 let opts = idris_options i
609 return (opt_nobanner opts)
611setQuiet :: Bool -> Idris ()
612setQuiet q = do i <- getIState
613 let opts = idris_options i
614 let opt' = opts { opt_quiet = q }
615 putIState $ i { idris_options = opt' }
617getQuiet :: Idris Bool
618getQuiet = do i <- getIState
619 let opts = idris_options i
620 return (opt_quiet opts)
622setCodegen :: Codegen -> Idris ()
623setCodegen t = do i <- getIState
624 let opts = idris_options i
625 let opt' = opts { opt_codegen = t }
626 putIState $ i { idris_options = opt' }
628codegen :: Idris Codegen
629codegen = do i <- getIState
630 return (opt_codegen (idris_options i))
632setOutputTy :: OutputType -> Idris ()
633setOutputTy t = do i <- getIState
634 let opts = idris_options i
635 let opt' = opts { opt_outputTy = t }
636 putIState $ i { idris_options = opt' }
638outputTy :: Idris OutputType
639outputTy = do i <- getIState
640 return $ opt_outputTy $ idris_options i
642setIdeSlave :: Bool -> Idris ()
643setIdeSlave True = do i <- getIState
644 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
645setIdeSlave False = return ()
647setTargetTriple :: String -> Idris ()
648setTargetTriple t = do i <- getIState
649 let opts = idris_options i
650 opt' = opts { opt_triple = t }
651 putIState $ i { idris_options = opt' }
653targetTriple :: Idris String
654targetTriple = do i <- getIState
655 return (opt_triple (idris_options i))
657setTargetCPU :: String -> Idris ()
658setTargetCPU t = do i <- getIState
659 let opts = idris_options i
660 opt' = opts { opt_cpu = t }
661 putIState $ i { idris_options = opt' }
663targetCPU :: Idris String
664targetCPU = do i <- getIState
665 return (opt_cpu (idris_options i))
667setOptLevel :: Word -> Idris ()
668setOptLevel t = do i <- getIState
669 let opts = idris_options i
670 opt' = opts { opt_optLevel = t }
671 putIState $ i { idris_options = opt' }
673optLevel :: Idris Word
674optLevel = do i <- getIState
675 return (opt_optLevel (idris_options i))
677verbose :: Idris Bool
678verbose = do i <- getIState
679 return (opt_verbose (idris_options i))
681setVerbose :: Bool -> Idris ()
682setVerbose t = do i <- getIState
683 let opts = idris_options i
684 let opt' = opts { opt_verbose = t }
685 putIState $ i { idris_options = opt' }
687typeInType :: Idris Bool
688typeInType = do i <- getIState
689 return (opt_typeintype (idris_options i))
691setTypeInType :: Bool -> Idris ()
692setTypeInType t = do i <- getIState
693 let opts = idris_options i
694 let opt' = opts { opt_typeintype = t }
695 putIState $ i { idris_options = opt' }
697coverage :: Idris Bool
698coverage = do i <- getIState
699 return (opt_coverage (idris_options i))
701setCoverage :: Bool -> Idris ()
702setCoverage t = do i <- getIState
703 let opts = idris_options i
704 let opt' = opts { opt_coverage = t }
705 putIState $ i { idris_options = opt' }
707setIBCSubDir :: FilePath -> Idris ()
708setIBCSubDir fp = do i <- getIState
709 let opts = idris_options i
710 let opt' = opts { opt_ibcsubdir = fp }
711 putIState $ i { idris_options = opt' }
713valIBCSubDir :: IState -> Idris FilePath
714valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
716addImportDir :: FilePath -> Idris ()
717addImportDir fp = do i <- getIState
718 let opts = idris_options i
719 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
720 putIState $ i { idris_options = opt' }
722setImportDirs :: [FilePath] -> Idris ()
723setImportDirs fps = do i <- getIState
724 let opts = idris_options i
725 let opt' = opts { opt_importdirs = fps }
726 putIState $ i { idris_options = opt' }
728allImportDirs :: Idris [FilePath]
729allImportDirs = do i <- getIState
730 let optdirs = opt_importdirs (idris_options i)
731 return ("." : reverse optdirs)
733colourise :: Idris Bool
734colourise = do i <- getIState
735 return $ idris_colourRepl i
737setColourise :: Bool -> Idris ()
738setColourise b = do i <- getIState
739 putIState $ i { idris_colourRepl = b }
741setOutH :: Handle -> Idris ()
742setOutH h = do i <- getIState
743 putIState $ i { idris_outh = h }
745impShow :: Idris Bool
746impShow = do i <- getIState
747 return (opt_showimp (idris_options i))
749setImpShow :: Bool -> Idris ()
750setImpShow t = do i <- getIState
751 let opts = idris_options i
752 let opt' = opts { opt_showimp = t }
753 putIState $ i { idris_options = opt' }
755setColour :: ColourType -> IdrisColour -> Idris ()
756setColour ct c = do i <- getIState
757 let newTheme = setColour' ct c (idris_colourTheme i)
758 putIState $ i { idris_colourTheme = newTheme }
759 where setColour' KeywordColour c t = t { keywordColour = c }
760 setColour' BoundVarColour c t = t { boundVarColour = c }
761 setColour' ImplicitColour c t = t { implicitColour = c }
762 setColour' FunctionColour c t = t { functionColour = c }
763 setColour' TypeColour c t = t { typeColour = c }
764 setColour' DataColour c t = t { dataColour = c }
765 setColour' PromptColour c t = t { promptColour = c }
767logLvl :: Int -> String -> Idris ()
768logLvl l str = do i <- getIState
769 let lvl = opt_logLevel (idris_options i)
770 when (lvl >= l) $
771 case idris_outputmode i of
772 RawOutput -> do runIO $ putStrLn str
773 IdeSlave n ->
774 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
775 runIO $ putStrLn $ convSExp "log" good n
777cmdOptType :: Opt -> Idris Bool
778cmdOptType x = do i <- getIState
779 return $ x `elem` opt_cmdline (idris_options i)
781iLOG :: String -> Idris ()
782iLOG = logLvl 1
784noErrors :: Idris Bool
785noErrors = do i <- getIState
786 case errSpan i of
787 Nothing -> return True
788 _ -> return False
790setTypeCase :: Bool -> Idris ()
791setTypeCase t = do i <- getIState
792 let opts = idris_options i
793 let opt' = opts { opt_typecase = t }
794 putIState $ i { idris_options = opt' }
797-- Dealing with parameters
799expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
800 [Name] -> -- all names
801 [Name] -> -- names with no declaration
802 PTerm -> PTerm
803expandParams dec ps ns infs tm = en tm
804 where
805 -- if we shadow a name (say in a lambda binding) that is used in a call to
806 -- a lifted function, we need access to both names - once in the scope of the
807 -- binding and once to call the lifted functions. So we'll explicitly shadow
808 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
809 -- but we didn't...)
811 mkShadow (UN n) = MN 0 n
812 mkShadow (MN i n) = MN (i+1) n
813 mkShadow (NS x s) = NS (mkShadow x) s
815 en (PLam n t s)
816 | n `elem` (map fst ps ++ ns)
817 = let n' = mkShadow n in
818 PLam n' (en t) (en (shadow n n' s))
819 | otherwise = PLam n (en t) (en s)
820 en (PPi p n t s)
821 | n `elem` (map fst ps ++ ns)
822 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
823 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
824 | otherwise = PPi (enTacImp p) n (en t) (en s)
825 en (PLet n ty v s)
826 | n `elem` (map fst ps ++ ns)
827 = let n' = mkShadow n in
828 PLet n' (en ty) (en v) (en (shadow n n' s))
829 | otherwise = PLet n (en ty) (en v) (en s)
830 -- FIXME: Should only do this in a type signature!
831 en (PDPair f p (PRef f' n) t r)
832 | n `elem` (map fst ps ++ ns) && t /= Placeholder
833 = let n' = mkShadow n in
834 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
835 en (PEq f l r) = PEq f (en l) (en r)
836 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
837 en (PTyped l r) = PTyped (en l) (en r)
838 en (PPair f p l r) = PPair f p (en l) (en r)
839 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
840 en (PAlternative a as) = PAlternative a (map en as)
841 en (PHidden t) = PHidden (en t)
842 en (PUnifyLog t) = PUnifyLog (en t)
843 en (PDisamb ds t) = PDisamb ds (en t)
844 en (PNoImplicits t) = PNoImplicits (en t)
845 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
846 en (PProof ts) = PProof (map (fmap en) ts)
847 en (PTactics ts) = PTactics (map (fmap en) ts)
849 en (PQuote (Var n))
850 | n `nselem` ns = PQuote (Var (dec n))
851 en (PApp fc (PInferRef fc' n) as)
852 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
853 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
854 en (PApp fc (PRef fc' n) as)
855 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
856 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
857 | n `nselem` ns = PApp fc (PRef fc' (dec n))
858 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
859 en (PAppBind fc (PRef fc' n) as)
860 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
861 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
862 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
863 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
864 en (PRef fc n)
865 | n `elem` infs = PApp fc (PInferRef fc (dec n))
866 (map (pexp . (PRef fc)) (map fst ps))
867 | n `nselem` ns = PApp fc (PRef fc (dec n))
868 (map (pexp . (PRef fc)) (map fst ps))
869 en (PInferRef fc n)
870 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
871 (map (pexp . (PRef fc)) (map fst ps))
872 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
873 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
874 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
875 en t = t
877 nselem x [] = False
878 nselem x (y : xs) | nseq x y = True
879 | otherwise = nselem x xs
881 nseq x y = nsroot x == nsroot y
883 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
884 enTacImp other = other
886expandParamsD :: Bool -> -- True = RHS only
887 IState ->
888 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
889expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
890 = if n `elem` ns && (not rhsonly)
891 then -- trace (show (n, expandParams dec ps ns ty)) $
892 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
893 else --trace (show (n, expandParams dec ps ns ty)) $
894 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
895expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
896 = if n `elem` ns && (not rhsonly)
897 then -- trace (show (n, expandParams dec ps ns ty)) $
898 PPostulate doc syn fc o (dec n) (piBind ps
899 (expandParams dec ps ns [] ty))
900 else --trace (show (n, expandParams dec ps ns ty)) $
901 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
902expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
903 = let n' = if n `elem` ns then dec n else n in
904 PClauses fc opts n' (map expandParamsC cs)
905 where
906 expandParamsC (PClause fc n lhs ws rhs ds)
907 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
908 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
909 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
910 n' = if n `elem` ns then dec n else n
911 -- names bound on the lhs should not be expanded on the rhs
912 ns' = removeBound lhs ns in
913 PClause fc n' lhs'
914 (map (expandParams dec ps'' ns' []) ws)
915 (expandParams dec ps'' ns' [] rhs)
916 (map (expandParamsD True ist dec ps'' ns') ds)
917 expandParamsC (PWith fc n lhs ws wval ds)
918 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
919 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
920 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
921 n' = if n `elem` ns then dec n else n
922 ns' = removeBound lhs ns in
923 PWith fc n' lhs'
924 (map (expandParams dec ps'' ns' []) ws)
925 (expandParams dec ps'' ns' [] wval)
926 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
927 updateps yn nm [] = []
928 updateps yn nm (((a, t), i):as)
929 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
930 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
932 removeBound lhs ns = ns \\ nub (bnames lhs)
934 bnames (PRef _ n) = [n]
935 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
936 bnames (PPair _ _ l r) = bnames l ++ bnames r
937 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
938 bnames _ = []
940expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
941 = PData doc argDocs syn fc co (expandPData pd)
942 where
943 -- just do the type decl, leave constructors alone (parameters will be
944 -- added implicitly)
945 expandPData (PDatadecl n ty cons)
946 = if n `elem` ns
947 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
948 (map econ cons)
949 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
950 econ (doc, argDocs, n, t, fc, fs)
951 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
952expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
953 = if tn `elem` ns
954 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
955 cdoc (dec cn) conty
956 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
957 cdoc (dec cn) conty
958 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
959expandParamsD rhs ist dec ps ns (PParams f params pds)
960 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
961 (map (expandParamsD True ist dec ps ns) pds)
962-- (map (expandParamsD ist dec ps ns) pds)
963expandParamsD rhs ist dec ps ns (PMutual f pds)
964 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
965expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
966 = PClass doc info f
967 (map (expandParams dec ps ns []) cs)
968 n
969 (map (mapsnd (expandParams dec ps ns [])) params)
970 (map (expandParamsD rhs ist dec ps ns) decls)
971expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
972 = PInstance info f
973 (map (expandParams dec ps ns []) cs)
974 n
975 (map (expandParams dec ps ns []) params)
976 (expandParams dec ps ns [] ty)
977 cn
978 (map (expandParamsD rhs ist dec ps ns) decls)
979expandParamsD rhs ist dec ps ns d = d
981mapsnd f (x, t) = (x, f t)
983-- Calculate a priority for a type, for deciding elaboration order
984-- * if it's just a type variable or concrete type, do it early (0)
985-- * if there's only type variables and injective constructors, do it next (1)
986-- * if there's a function type, next (2)
987-- * finally, everything else (3)
989getPriority :: IState -> PTerm -> Int
990getPriority i tm = 1 -- pri tm
991 where
992 pri (PRef _ n) =
993 case lookupP n (tt_ctxt i) of
994 ((P (DCon _ _) _ _):_) -> 1
995 ((P (TCon _ _) _ _):_) -> 1
996 ((P Ref _ _):_) -> 1
997 [] -> 0 -- must be locally bound, if it's not an error...
998 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
999 pri (PTrue _ _) = 0
1000 pri (PFalse _) = 0
1001 pri (PRefl _ _) = 1
1002 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1003 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1004 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1005 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1006 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1007 pri (PTyped l r) = pri l
1008 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1009 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1010 pri (PAlternative a as) = maximum (map pri as)
1011 pri (PConstant _) = 0
1012 pri Placeholder = 1
1013 pri _ = 3
1016addStatics :: Name -> Term -> PTerm -> Idris ()
1017addStatics n tm ptm =
1018 do let (statics, dynamics) = initStatics tm ptm
1019 let stnames = nub $ concatMap freeArgNames (map snd statics)
1020 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1021 -- also get the arguments which are 'uniquely inferrable' from
1022 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1023 let statics' = nub $ map fst statics ++
1024 filter (\x -> not (elem x dnames)) stnames
1025 let stpos = staticList statics' tm
1026 i <- getIState
1027 when (not (null statics)) $
1028 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1029 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1030 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1031 addIBC (IBCStatic n)
1032 where
1033 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1034 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1035 if pstatic p == Static then ((n, ty) : static, dynamic)
1036 else if (not (searchArg p))
1037 then (static, (n, ty) : dynamic)
1038 else (static, dynamic)
1039 initStatics t pt = ([], [])
1041 freeArgNames (Bind n (Pi ty) sc)
1042 = nub $ freeArgNames ty
1043 freeArgNames tm = let (_, args) = unApply tm in
1044 concatMap freeNames args
1046 -- if a name appears in a type class or tactic implicit index, it doesn't
1047 -- affect its 'uniquely inferrable' from a static status since these are
1048 -- resolved by searching.
1049 searchArg (Constraint _ _) = True
1050 searchArg (TacImp _ _ _) = True
1051 searchArg _ = False
1053 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1054 staticList _ _ = []
1056-- Dealing with implicit arguments
1058-- Add constraint bindings from using block
1060addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1061addUsingConstraints syn fc t
1062 = do ist <- get
1063 let ns = namesIn [] ist t
1064 let cs = getConstraints t -- check declared constraints
1065 let addconsts = uconsts \\ cs
1066 -- if all names in the arguments of addconsts appear in ns,
1067 -- add the constraint implicitly
1068 return (doAdd addconsts ns t)
1069 where uconsts = filter uconst (using syn)
1070 uconst (UConstraint _ _) = True
1071 uconst _ = False
1073 doAdd [] _ t = t
1074 -- if all of args in ns, then add it
1075 doAdd (UConstraint c args : cs) ns t
1076 | all (\n -> elem n ns) args
1077 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1078 (mkConst c args) (doAdd cs ns t)
1079 | otherwise = doAdd cs ns t
1081 mkConst c args = PApp fc (PRef fc c)
1082 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1084 getConstraints (PPi (Constraint _ _) _ c sc)
1085 = getcapp c ++ getConstraints sc
1086 getConstraints (PPi _ _ c sc) = getConstraints sc
1087 getConstraints _ = []
1089 getcapp (PApp _ (PRef _ c) args)
1090 = do ns <- mapM getName args
1091 return (UConstraint c ns)
1092 getcapp _ = []
1094 getName (PExp _ _ _ (PRef _ n)) = return n
1095 getName _ = []
1097-- Add implicit Pi bindings for any names in the term which appear in an
1098-- argument position.
1100-- This has become a right mess already. Better redo it some time...
1102implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1103implicit info syn n ptm = implicit' info syn [] n ptm
1105implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1106implicit' info syn ignore n ptm
1107 = do i <- getIState
1108 let (tm', impdata) = implicitise syn ignore i ptm
1109 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1110-- let (tm'', spos) = findStatics i tm'
1111 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1112 addIBC (IBCImp n)
1113 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1114-- i <- get
1115-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1116 return tm'
1117 where
1118 -- Detect unknown names in default arguments and throw error if found.
1119 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1120 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1122 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1123 notFoundInDefault kns (PTacImplicit _ _ n script _)
1124 = do i <- getIState
1125 case notFound kns (namesIn [] i script) of
1126 Nothing -> return (n:kns)
1127 Just name -> throwError (NoSuchVariable name)
1128 notFoundInDefault kns p = return ((pname p):kns)
1130 notFound :: [Name] -> [Name] -> Maybe Name
1131 notFound kns [] = Nothing
1132 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1133 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1135implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1136implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1137 let (declimps, ns') = execState (imps True [] tm) ([], [])
1138 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1139 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1140 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1141 if null ns
1142 then (tm, reverse declimps)
1143 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1144 where
1145 uvars = map ipair (filter uimplicit (using syn))
1146 pvars = syn_params syn
1148 inUsing n = n `elem` map fst uvars
1150 ipair (UImplicit x y) = (x, y)
1151 uimplicit (UImplicit _ _) = True
1152 uimplicit _ = False
1154 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1155 | otherwise = x : dropAll xs ys
1156 dropAll [] ys = []
1158 -- Find names in argument position in a type, suitable for implicit
1159 -- binding
1160 -- Not the function position, but do everything else...
1161 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1162 implNamesIn uv t = namesIn uv ist t
1164 imps top env (PApp _ f as)
1165 = do (decls, ns) <- get
1166 let isn = concatMap (namesIn uvars ist) (map getTm as)
1167 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1168 imps top env (PPi (Imp l _ _) n ty sc)
1169 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1170 (decls , ns) <- get
1171 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1172 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1173 imps True (n:env) sc
1174 imps top env (PPi (Exp l _ _) n ty sc)
1175 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1176 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1177 _ -> [])
1178 (decls, ns) <- get -- ignore decls in HO types
1179 put (PExp (getPriority ist ty) l n Placeholder : decls,
1180 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1181 imps True (n:env) sc
1182 imps top env (PPi (Constraint l _) n ty sc)
1183 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1184 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1185 _ -> [])
1186 (decls, ns) <- get -- ignore decls in HO types
1187 put (PConstraint 10 l n Placeholder : decls,
1188 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1189 imps True (n:env) sc
1190 imps top env (PPi (TacImp l _ scr) n ty sc)
1191 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1192 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1193 _ -> [])
1194 (decls, ns) <- get -- ignore decls in HO types
1195 put (PTacImplicit 10 l n scr Placeholder : decls,
1196 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1197 imps True (n:env) sc
1198 imps top env (PEq _ l r)
1199 = do (decls, ns) <- get
1200 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1201 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1202 imps top env (PRewrite _ l r _)
1203 = do (decls, ns) <- get
1204 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1205 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1206 imps top env (PTyped l r)
1207 = imps top env l
1208 imps top env (PPair _ _ l r)
1209 = do (decls, ns) <- get
1210 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1211 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1212 imps top env (PDPair _ _ (PRef _ n) t r)
1213 = do (decls, ns) <- get
1214 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1215 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1216 imps top env (PDPair _ _ l t r)
1217 = do (decls, ns) <- get
1218 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1219 namesIn uvars ist r
1220 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1221 imps top env (PAlternative a as)
1222 = do (decls, ns) <- get
1223 let isn = concatMap (namesIn uvars ist) as
1224 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1225 imps top env (PLam n ty sc)
1226 = do imps False env ty
1227 imps False (n:env) sc
1228 imps top env (PHidden tm) = imps False env tm
1229 imps top env (PUnifyLog tm) = imps False env tm
1230 imps top env (PNoImplicits tm) = imps False env tm
1231 imps top env _ = return ()
1233 pibind using [] sc = sc
1234 pibind using (n:ns) sc
1235 = case lookup n using of
1236 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1237 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1238 (pibind using ns sc)
1240-- Add implicit arguments in function calls
1241addImplPat :: IState -> PTerm -> PTerm
1242addImplPat = addImpl' True [] []
1244addImplBound :: IState -> [Name] -> PTerm -> PTerm
1245addImplBound ist ns = addImpl' False ns [] ist
1247addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1248addImplBoundInf ist ns inf = addImpl' False ns inf ist
1250addImpl :: IState -> PTerm -> PTerm
1251addImpl = addImpl' False [] []
1253-- TODO: in patterns, don't add implicits to function names guarded by constructors
1254-- and *not* inside a PHidden
1256addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1257addImpl' inpat env infns ist ptm
1258 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1259 where
1260 ai env ds (PRef fc f)
1261 | f `elem` infns = PInferRef fc f
1262 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1263 ai env ds (PHidden (PRef fc f))
1264 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1265 ai env ds (PEq fc l r)
1266 = let l' = ai env ds l
1267 r' = ai env ds r in
1268 PEq fc l' r'
1269 ai env ds (PRewrite fc l r g)
1270 = let l' = ai env ds l
1271 r' = ai env ds r
1272 g' = fmap (ai env ds) g in
1273 PRewrite fc l' r' g'
1274 ai env ds (PTyped l r)
1275 = let l' = ai env ds l
1276 r' = ai env ds r in
1277 PTyped l' r'
1278 ai env ds (PPair fc p l r)
1279 = let l' = ai env ds l
1280 r' = ai env ds r in
1281 PPair fc p l' r'
1282 ai env ds (PDPair fc p l t r)
1283 = let l' = ai env ds l
1284 t' = ai env ds t
1285 r' = ai env ds r in
1286 PDPair fc p l' t' r'
1287 ai env ds (PAlternative a as)
1288 = let as' = map (ai env ds) as in
1289 PAlternative a as'
1290 ai env _ (PDisamb ds' as) = ai env ds' as
1291 ai env ds (PApp fc (PInferRef _ f) as)
1292 = let as' = map (fmap (ai env ds)) as in
1293 PApp fc (PInferRef fc f) as'
1294 ai env ds (PApp fc ftm@(PRef _ f) as)
1295 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1296 | not (f `elem` map fst env)
1297 = let as' = map (fmap (ai env ds)) as in
1298 handleErr $ aiFn inpat False ist fc f ds as'
1299 | Just (Just ty) <- lookup f env =
1300 let as' = map (fmap (ai env ds)) as
1301 arity = getPArity ty in
1302 mkPApp fc arity ftm as'
1303 ai env ds (PApp fc f as)
1304 = let f' = ai env ds f
1305 as' = map (fmap (ai env ds)) as in
1306 mkPApp fc 1 f' as'
1307 ai env ds (PCase fc c os)
1308 = let c' = ai env ds c
1309 os' = map (pmap (ai env ds)) os in
1310 PCase fc c' os'
1311 ai env ds (PLam n ty sc)
1312 = let ty' = ai env ds ty
1313 sc' = ai ((n, Just ty):env) ds sc in
1314 PLam n ty' sc'
1315 ai env ds (PLet n ty val sc)
1316 = let ty' = ai env ds ty
1317 val' = ai env ds val
1318 sc' = ai ((n, Just ty):env) ds sc in
1319 PLet n ty' val' sc'
1320 ai env ds (PPi p n ty sc)
1321 = let ty' = ai env ds ty
1322 sc' = ai ((n, Just ty):env) ds sc in
1323 PPi p n ty' sc'
1324 ai env ds (PGoal fc r n sc)
1325 = let r' = ai env ds r
1326 sc' = ai ((n, Nothing):env) ds sc in
1327 PGoal fc r' n sc'
1328 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1329 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1330 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1331 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1332 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1333 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1334 ai env ds tm = tm
1336 handleErr (Left err) = PElabError err
1337 handleErr (Right x) = x
1339-- if in a pattern, and there are no arguments, and there's no possible
1340-- names with zero explicit arguments, don't add implicits.
1342aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1343aiFn inpat True ist fc f ds []
1344 = case lookupDef f (tt_ctxt ist) of
1345 [] -> Right $ PPatvar fc f
1346 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1347 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1348 if (not (vname f) || tcname f
1349 || any (conCaf (tt_ctxt ist)) ialts)
1350-- any constructor alts || any allImp ialts))
1351 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1352 else Right $ PPatvar fc f
1353 where imp (PExp _ _ _ _) = False
1354 imp _ = True
1355-- allImp [] = False
1356 allImp xs = all imp xs
1357 constructor (TyDecl (DCon _ _) _) = True
1358 constructor _ = False
1360 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1362 vname (UN n) = True -- non qualified
1363 vname _ = False
1365aiFn inpat expat ist fc f ds as
1366 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1367aiFn inpat expat ist fc f ds as
1368 -- This is where namespaces get resolved by adding PAlternative
1369 = do let ns = lookupCtxtName f (idris_implicits ist)
1370 let nh = filter (\(n, _) -> notHidden n) ns
1371 let ns' = case trimAlts ds nh of
1372 [] -> nh
1373 x -> x
1374 case ns' of
1375 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1376 [] -> if f `elem` (map fst (idris_metavars ist))
1377 then Right $ PApp fc (PRef fc f) as
1378 else Right $ mkPApp fc (length as) (PRef fc f) as
1379 alts -> Right $
1380 PAlternative True $
1381 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1382 (insertImpl ns as)) alts
1383 where
1384 trimAlts [] alts = alts
1385 trimAlts ns alts
1386 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1388 nspace (NS _ s) = s
1389 nspace _ = []
1391 notHidden n = case getAccessibility n of
1392 Hidden -> False
1393 _ -> True
1395 getAccessibility n
1396 = case lookupDefAcc n False (tt_ctxt ist) of
1397 [(n,t)] -> t
1398 _ -> Public
1400 insertImpl :: [PArg] -> [PArg] -> [PArg]
1401 insertImpl ps as = insImpAcc M.empty ps as
1403 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1404 -> [PArg] -- parameters
1405 -> [PArg] -- arguments
1406 -> [PArg]
1407 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1408 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1409 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1410 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1411 insImpAcc pnas (PConstraint p l n ty : ps) given =
1412 let rtc = PResolveTC fc in
1413 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1414 insImpAcc pnas (PImp p _ l n ty : ps) given =
1415 case find n given [] of
1416 Just (tm, given') ->
1417 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1418 Nothing ->
1419 PImp p True l n Placeholder :
1420 insImpAcc (M.insert n Placeholder pnas) ps given
1421 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1422 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1423 case find n given [] of
1424 Just (tm, given') ->
1425 PTacImplicit p l n sc tm :
1426 insImpAcc (M.insert n tm pnas) ps given'
1427 Nothing ->
1428 if inpat
1429 then PTacImplicit p l n sc Placeholder :
1430 insImpAcc (M.insert n Placeholder pnas) ps given
1431 else PTacImplicit p l n sc sc :
1432 insImpAcc (M.insert n sc pnas) ps given
1433 insImpAcc _ expected [] = []
1434 insImpAcc _ _ given = given
1436 find n [] acc = Nothing
1437 find n (PImp _ _ _ n' t : gs) acc
1438 | n == n' = Just (t, reverse acc ++ gs)
1439 find n (PTacImplicit _ _ n' _ t : gs) acc
1440 | n == n' = Just (t, reverse acc ++ gs)
1441 find n (g : gs) acc = find n gs (g : acc)
1443-- replace non-linear occurrences with _
1444-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1445-- it is hard to get right!
1447stripLinear :: IState -> PTerm -> PTerm
1448stripLinear i tm = evalState (sl tm) [] where
1449 sl :: PTerm -> State [Name] PTerm
1450 sl (PRef fc f)
1451 | (_:_) <- lookupTy f (tt_ctxt i)
1452 = return $ PRef fc f
1453 | otherwise = do ns <- get
1454 if (f `elem` ns)
1455 then return Placeholder
1456 else do put (f : ns)
1457 return (PRef fc f)
1458 sl (PPatvar fc f)
1459 = do ns <- get
1460 if (f `elem` ns)
1461 then return Placeholder
1462 else do put (f : ns)
1463 return (PPatvar fc f)
1464 sl t@(PAlternative _ (a : as)) = do sl a
1465 return t
1466 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1467 args' <- mapM slA args
1468 return $ PApp fc fn args'
1469 where slA (PImp p m l n t) = do t' <- sl t
1470 return $ PImp p m l n t'
1471 slA (PExp p l n t) = do t' <- sl t
1472 return $ PExp p l n t'
1473 slA (PConstraint p l n t)
1474 = do t' <- sl t
1475 return $ PConstraint p l n t'
1476 slA (PTacImplicit p l n sc t)
1477 = do t' <- sl t
1478 return $ PTacImplicit p l n sc t'
1479 sl x = return x
1481-- Remove functions which aren't applied to anything, which must then
1482-- be resolved by unification. Assume names resolved and alternatives
1483-- filled in (so no ambiguity).
1485stripUnmatchable :: IState -> PTerm -> PTerm
1486stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1487 su :: PTerm -> PTerm
1488 su (PRef fc f)
1489 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1490 = Placeholder
1491 su (PApp fc fn args)
1492 = PApp fc fn (fmap (fmap su) args)
1493 su (PAlternative b alts)
1494 = let alts' = filter (/= Placeholder) (map su alts) in
1495 if null alts' then Placeholder
1496 else PAlternative b alts'
1497 su (PPair fc p l r) = PPair fc p (su l) (su r)
1498 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1499 su t = t
1500stripUnmatchable i tm = tm
1502mkPApp fc a f [] = f
1503mkPApp fc a f as = let rest = drop a as in
1504 appRest fc (PApp fc f (take a as)) rest
1505 where
1506 appRest fc f [] = f
1507 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1509-- Find 'static' argument positions
1510-- (the declared ones, plus any names in argument position in the declared
1511-- statics)
1512-- FIXME: It's possible that this really has to happen after elaboration
1514findStatics :: IState -> PTerm -> (PTerm, [Bool])
1515findStatics ist tm = trace (show tm) $
1516 let (ns, ss) = fs tm in
1517 runState (pos ns ss tm) []
1518 where fs (PPi p n t sc)
1519 | Static <- pstatic p
1520 = let (ns, ss) = fs sc in
1521 (namesIn [] ist t : ns, n : ss)
1522 | otherwise = let (ns, ss) = fs sc in
1523 (ns, ss)
1524 fs _ = ([], [])
1526 inOne n ns = length (filter id (map (elem n) ns)) == 1
1528 pos ns ss (PPi p n t sc)
1529 | elem n ss = do sc' <- pos ns ss sc
1530 spos <- get
1531 put (True : spos)
1532 return (PPi (p { pstatic = Static }) n t sc')
1533 | otherwise = do sc' <- pos ns ss sc
1534 spos <- get
1535 put (False : spos)
1536 return (PPi p n t sc')
1537 pos ns ss t = return t
1539-- for 6.12/7 compatibility
1540data EitherErr a b = LeftErr a | RightOK b
1542instance Monad (EitherErr a) where
1543 return = RightOK
1545 (LeftErr e) >>= k = LeftErr e
1546 RightOK v >>= k = k v
1548toEither (LeftErr e) = Left e
1549toEither (RightOK ho) = Right ho
1551-- syntactic match of a against b, returning pair of variables in a
1552-- and what they match. Returns the pair that failed if not a match.
1554matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1555matchClause = matchClause' False
1557matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1558matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1559 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1561 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1562 fullApp x = x
1564 match' x y = match (fullApp x) (fullApp y)
1565 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1566 | fi == txt "fromInteger" && b == txt "builtins",
1567 PConstant (I _) <- getTm x = match (getTm x) x'
1568 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1569 | fi == txt "fromInteger" && b == txt "builtins",
1570 PConstant (I _) <- getTm x = match (getTm x) x'
1571 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1572 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1573 match (PApp _ f args) (PApp _ f' args')
1574 | length args == length args'
1575 = do mf <- match' f f'
1576 ms <- zipWithM matchArg args args'
1577 return (mf ++ concat ms)
1578 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1579 match (PPatvar f n) xr = match (PRef f n) xr
1580 match xr (PPatvar f n) = match xr (PRef f n)
1581 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1582 match (PRef _ n) tm@(PRef _ n')
1583 | n == n' && not names &&
1584 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1585 || tm == Placeholder)
1586 = return [(n, tm)]
1587 -- if one namespace is missing, drop the other
1588 | n == n' || n == dropNS n' || dropNS n == n' = return []
1589 where dropNS (NS n _) = n
1590 dropNS n = n
1591 match (PRef _ n) tm
1592 | not names && (not (isConName n (tt_ctxt i) ||
1593 isFnName n (tt_ctxt i)) || tm == Placeholder)
1594 = return [(n, tm)]
1595 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1596 mr <- match' r r'
1597 return (ml ++ mr)
1598 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1599 = do ml <- match' l l'
1600 mr <- match' r r'
1601 return (ml ++ mr)
1602 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1603 mr <- match r r'
1604 return (ml ++ mr)
1605 match (PTyped l r) x = match l x
1606 match x (PTyped l r) = match x l
1607 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1608 mr <- match' r r'
1609 return (ml ++ mr)
1610 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1611 mt <- match' t t'
1612 mr <- match' r r'
1613 return (ml ++ mt ++ mr)
1614 match (PAlternative a as) (PAlternative a' as')
1615 = do ms <- zipWithM match' as as'
1616 return (concat ms)
1617 match a@(PAlternative _ as) b
1618 = do let ms = zipWith match' as (repeat b)
1619 case (rights (map toEither ms)) of
1620 (x: _) -> return x
1621 _ -> LeftErr (a, b)
1622 match (PCase _ _ _) _ = return [] -- lifted out
1623 match (PMetavar _) _ = return [] -- modified
1624 match (PInferRef _ _) _ = return [] -- modified
1625 match (PQuote _) _ = return []
1626 match (PProof _) _ = return []
1627 match (PTactics _) _ = return []
1628 match (PRefl _ _) (PRefl _ _) = return []
1629 match (PResolveTC _) (PResolveTC _) = return []
1630 match (PTrue _ _) (PTrue _ _) = return []
1631 match (PFalse _) (PFalse _) = return []
1632 match (PReturn _) (PReturn _) = return []
1633 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1634 ms <- match' s s'
1635 return (mt ++ ms)
1636 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1637 ms <- match' s s'
1638 return (mt ++ ms)
1639 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1640 mty <- match' ty ty'
1641 ms <- match' s s'
1642 return (mt ++ mty ++ ms)
1643 match (PHidden x) (PHidden y) = match' x y
1644 match (PUnifyLog x) y = match' x y
1645 match x (PUnifyLog y) = match' x y
1646 match (PNoImplicits x) y = match' x y
1647 match x (PNoImplicits y) = match' x y
1648 match Placeholder _ = return []
1649 match _ Placeholder = return []
1650 match (PResolveTC _) _ = return []
1651 match a b | a == b = return []
1652 | otherwise = LeftErr (a, b)
1654 checkRpts (RightOK ms) = check ms where
1655 check ((n,t):xs)
1656 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1657 then Left (t, t')
1658 else check xs
1659 check (_:xs) = check xs
1660 check [] = Right ms
1661 checkRpts (LeftErr x) = Left x
1663substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1664substMatches ms = substMatchesShadow ms []
1666substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1667substMatchesShadow [] shs t = t
1668substMatchesShadow ((n,tm):ns) shs t
1669 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1671substMatch :: Name -> PTerm -> PTerm -> PTerm
1672substMatch n = substMatchShadow n []
1674substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1675substMatchShadow n shs tm t = sm shs t where
1676 sm xs (PRef _ n') | n == n' = tm
1677 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1678 sm xs (PPi p x t sc)
1679 | x `elem` xs
1680 = let x' = nextName x in
1681 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1682 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1683 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1684 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1685 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1686 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1687 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1688 (fmap (sm xs) tm)
1689 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1690 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1691 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1692 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1693 sm xs (PHidden x) = PHidden (sm xs x)
1694 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1695 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1696 sm xs x = x
1698 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1699 fullApp x = x
1701shadow :: Name -> Name -> PTerm -> PTerm
1702shadow n n' t = sm t where
1703 sm (PRef fc x) | n == x = PRef fc n'
1704 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1705 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1706 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1707 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1708 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1709 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1710 sm (PEq f x y) = PEq f (sm x) (sm y)
1711 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1712 sm (PTyped x y) = PTyped (sm x) (sm y)
1713 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1714 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1715 sm (PAlternative a as) = PAlternative a (map sm as)
1716 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1717 sm (PProof ts) = PProof (map (fmap sm) ts)
1718 sm (PHidden x) = PHidden (sm x)
1719 sm (PUnifyLog x) = PUnifyLog (sm x)
1720 sm (PNoImplicits x) = PNoImplicits (sm x)
1721 sm x = x
1723-- Rename any binders which are repeated (so that we don't have to mess
1724-- about with shadowing anywhere else).
1726mkUniqueNames :: [Name] -> PTerm -> PTerm
1727mkUniqueNames env tm = evalState (mkUniq tm) env where
1728 inScope = boundNamesIn tm
1730 mkUniqA arg = do t' <- mkUniq (getTm arg)
1731 return (arg { getTm = t' })
1733 -- Initialise the unique name with the environment length (so we're not
1734 -- looking for too long...)
1735 initN (UN n) l = UN $ txt (str n ++ show l)
1736 initN (MN i s) l = MN (i+l) s
1737 initN n l = n
1739 -- FIXME: Probably ought to do this for completeness! It's fine as
1740 -- long as there are no bindings inside tactics though.
1741 mkUniqT tac = return tac
1743 mkUniq :: PTerm -> State [Name] PTerm
1744 mkUniq (PLam n ty sc)
1745 = do env <- get
1746 (n', sc') <-
1747 if n `elem` env
1748 then do let n' = uniqueName (initN n (length env))
1749 (env ++ inScope)
1750 return (n', shadow n n' sc)
1751 else return (n, sc)
1752 put (n' : env)
1753 ty' <- mkUniq ty
1754 sc'' <- mkUniq sc'
1755 return $! PLam n' ty' sc''
1756 mkUniq (PPi p n ty sc)
1757 = do env <- get
1758 (n', sc') <-
1759 if n `elem` env
1760 then do let n' = uniqueName (initN n (length env))
1761 (env ++ inScope)
1762 return (n', shadow n n' sc)
1763 else return (n, sc)
1764 put (n' : env)
1765 ty' <- mkUniq ty
1766 sc'' <- mkUniq sc'
1767 return $! PPi p n' ty' sc''
1768 mkUniq (PLet n ty val sc)
1769 = do env <- get
1770 (n', sc') <-
1771 if n `elem` env
1772 then do let n' = uniqueName (initN n (length env))
1773 (env ++ inScope)
1774 return (n', shadow n n' sc)
1775 else return (n, sc)
1776 put (n' : env)
1777 ty' <- mkUniq ty; val' <- mkUniq val
1778 sc'' <- mkUniq sc'
1779 return $! PLet n' ty' val' sc''
1780 mkUniq (PApp fc t args)
1781 = do t' <- mkUniq t
1782 args' <- mapM mkUniqA args
1783 return $! PApp fc t' args'
1784 mkUniq (PAppBind fc t args)
1785 = do t' <- mkUniq t
1786 args' <- mapM mkUniqA args
1787 return $! PAppBind fc t' args'
1788 mkUniq (PCase fc t alts)
1789 = do t' <- mkUniq t
1790 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1791 return (x', y')) alts
1792 return $! PCase fc t' alts'
1793 mkUniq (PPair fc p l r)
1794 = do l' <- mkUniq l; r' <- mkUniq r
1795 return $! PPair fc p l' r'
1796 mkUniq (PDPair fc p (PRef fc' n) t sc)
1797 | t /= Placeholder
1798 = do env <- get
1799 (n', sc') <- if n `elem` env
1800 then do let n' = uniqueName n (env ++ inScope)
1801 return (n', shadow n n' sc)
1802 else return (n, sc)
1803 put (n' : env)
1804 t' <- mkUniq t
1805 sc'' <- mkUniq sc'
1806 return $! PDPair fc p (PRef fc' n') t' sc''
1807 mkUniq (PDPair fc p l t r)
1808 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1809 return $! PDPair fc p l' t' r'
1810 mkUniq (PAlternative b as)
1811 = liftM (PAlternative b) (mapM mkUniq as)
1812 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1813 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1814 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1815 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1816 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1817 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1818 mkUniq t = return t