git.iko.soy/Idris-dev
on 4be2fba help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1830 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
391withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
392withContext ctx name dflt action = do
393 ist <- getIState
394 case lookupCtxt name (ctx ist) of
395 [x] -> action x
396 _ -> return dflt
398withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
399withContext_ ctx name action = withContext ctx name () action
401-- | A version of liftIO that puts errors into the exception type of the Idris monad
402runIO :: IO a -> Idris a
403runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
404-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
406getName :: Idris Int
407getName = do i <- getIState;
408 let idx = idris_name i;
409 putIState $ (i { idris_name = idx + 1 })
410 return idx
412-- InternalApp keeps track of the real function application for making case splits from, not the application the
413-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
414addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
415addInternalApp fp l t
416 = do i <- getIState
417 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
419getInternalApp :: FilePath -> Int -> Idris PTerm
420getInternalApp fp l = do i <- getIState
421 case lookup (fp, l) (idris_lineapps i) of
422 Just n' -> return n'
423 Nothing -> return Placeholder
424 -- TODO: What if it's not there?
426-- Pattern definitions are only used for coverage checking, so erase them
427-- when we're done
428clearOrigPats :: Idris ()
429clearOrigPats = do i <- get
430 let ps = idris_patdefs i
431 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
432 put (i { idris_patdefs = ps' })
434-- Erase types from Ps in the context (basically ending up with what's in
435-- the .ibc, which is all we need after all the analysis is done)
436clearPTypes :: Idris ()
437clearPTypes = do i <- get
438 let ctxt = tt_ctxt i
439 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
440 where pErase (CaseOp c t tys orig tot cds)
441 = CaseOp c t tys orig [] (pErase' cds)
442 pErase x = x
443 pErase' (CaseDefs _ (cs, c) _ rs)
444 = let c' = (cs, fmap pEraseType c) in
445 CaseDefs c' c' c' rs
447checkUndefined :: FC -> Name -> Idris ()
448checkUndefined fc n
449 = do i <- getContext
450 case lookupTy n i of
451 (_:_) -> throwError . Msg $ show fc ++ ":" ++
452 show n ++ " already defined"
453 _ -> return ()
455isUndefined :: FC -> Name -> Idris Bool
456isUndefined fc n
457 = do i <- getContext
458 case lookupTy n i of
459 (_:_) -> return False
460 _ -> return True
462setContext :: Context -> Idris ()
463setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
465updateContext :: (Context -> Context) -> Idris ()
466updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
468addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
469addConstraints fc (v, cs)
470 = do i <- getIState
471 let ctxt = tt_ctxt i
472 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
473 next_tvar = v }
474 let ics = zip cs (repeat fc) ++ idris_constraints i
475 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
477addDeferred = addDeferred' Ref
478addDeferredTyCon = addDeferred' (TCon 0 0)
480addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
481addDeferred' nt ns
482 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
483 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
484 i <- getIState
485 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
486 idris_metavars i }
487 where tidyNames used (Bind (MN i x) b sc)
488 = let n' = uniqueName (UN x) used in
489 Bind n' b $ tidyNames (n':used) sc
490 tidyNames used (Bind n b sc)
491 = let n' = uniqueName n used in
492 Bind n' b $ tidyNames (n':used) sc
493 tidyNames used b = b
495solveDeferred :: Name -> Idris ()
496solveDeferred n = do i <- getIState
497 putIState $ i { idris_metavars =
498 filter (\(n', _) -> n/=n')
499 (idris_metavars i),
500 ibc_write =
501 filter (notMV n) (ibc_write i)
502 }
503 where notMV n (IBCMetavar n') = not (n == n')
504 notMV n _ = True
506getUndefined :: Idris [Name]
507getUndefined = do i <- getIState
508 return (map fst (idris_metavars i) \\ primDefs)
510isMetavarName :: Name -> IState -> Bool
511isMetavarName n ist
512 = case lookupNames n (tt_ctxt ist) of
513 (t:_) -> isJust $ lookup t (idris_metavars ist)
514 _ -> False
516getWidth :: Idris ConsoleWidth
517getWidth = fmap idris_consolewidth getIState
519setWidth :: ConsoleWidth -> Idris ()
520setWidth w = do ist <- getIState
521 put ist { idris_consolewidth = w }
523renderWidth :: Idris Int
524renderWidth = do iw <- getWidth
525 case iw of
526 InfinitelyWide -> return 100000000
527 ColsWide n -> return (max n 1)
528 AutomaticWidth -> runIO getScreenWidth
532type1Doc :: Doc OutputAnnotation
533type1Doc = (annotate AnnConstType $ text "Type 1")
536isetPrompt :: String -> Idris ()
537isetPrompt p = do i <- getIState
538 case idris_outputmode i of
539 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
541setLogLevel :: Int -> Idris ()
542setLogLevel l = do i <- getIState
543 let opts = idris_options i
544 let opt' = opts { opt_logLevel = l }
545 putIState $ i { idris_options = opt' }
547setCmdLine :: [Opt] -> Idris ()
548setCmdLine opts = do i <- getIState
549 let iopts = idris_options i
550 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
552getCmdLine :: Idris [Opt]
553getCmdLine = do i <- getIState
554 return (opt_cmdline (idris_options i))
556getDumpDefun :: Idris (Maybe FilePath)
557getDumpDefun = do i <- getIState
558 return $ findC (opt_cmdline (idris_options i))
559 where findC [] = Nothing
560 findC (DumpDefun x : _) = Just x
561 findC (_ : xs) = findC xs
563getDumpCases :: Idris (Maybe FilePath)
564getDumpCases = do i <- getIState
565 return $ findC (opt_cmdline (idris_options i))
566 where findC [] = Nothing
567 findC (DumpCases x : _) = Just x
568 findC (_ : xs) = findC xs
570logLevel :: Idris Int
571logLevel = do i <- getIState
572 return (opt_logLevel (idris_options i))
574setErrContext :: Bool -> Idris ()
575setErrContext t = do i <- getIState
576 let opts = idris_options i
577 let opt' = opts { opt_errContext = t }
578 putIState $ i { idris_options = opt' }
580errContext :: Idris Bool
581errContext = do i <- getIState
582 return (opt_errContext (idris_options i))
584useREPL :: Idris Bool
585useREPL = do i <- getIState
586 return (opt_repl (idris_options i))
588setREPL :: Bool -> Idris ()
589setREPL t = do i <- getIState
590 let opts = idris_options i
591 let opt' = opts { opt_repl = t }
592 putIState $ i { idris_options = opt' }
594showOrigErr :: Idris Bool
595showOrigErr = do i <- getIState
596 return (opt_origerr (idris_options i))
598setShowOrigErr :: Bool -> Idris ()
599setShowOrigErr b = do i <- getIState
600 let opts = idris_options i
601 let opt' = opts { opt_origerr = b }
602 putIState $ i { idris_options = opt' }
604setAutoSolve :: Bool -> Idris ()
605setAutoSolve b = do i <- getIState
606 let opts = idris_options i
607 let opt' = opts { opt_autoSolve = b }
608 putIState $ i { idris_options = opt' }
610setNoBanner :: Bool -> Idris ()
611setNoBanner n = do i <- getIState
612 let opts = idris_options i
613 let opt' = opts { opt_nobanner = n }
614 putIState $ i { idris_options = opt' }
616getNoBanner :: Idris Bool
617getNoBanner = do i <- getIState
618 let opts = idris_options i
619 return (opt_nobanner opts)
621setQuiet :: Bool -> Idris ()
622setQuiet q = do i <- getIState
623 let opts = idris_options i
624 let opt' = opts { opt_quiet = q }
625 putIState $ i { idris_options = opt' }
627getQuiet :: Idris Bool
628getQuiet = do i <- getIState
629 let opts = idris_options i
630 return (opt_quiet opts)
632setCodegen :: Codegen -> Idris ()
633setCodegen t = do i <- getIState
634 let opts = idris_options i
635 let opt' = opts { opt_codegen = t }
636 putIState $ i { idris_options = opt' }
638codegen :: Idris Codegen
639codegen = do i <- getIState
640 return (opt_codegen (idris_options i))
642setOutputTy :: OutputType -> Idris ()
643setOutputTy t = do i <- getIState
644 let opts = idris_options i
645 let opt' = opts { opt_outputTy = t }
646 putIState $ i { idris_options = opt' }
648outputTy :: Idris OutputType
649outputTy = do i <- getIState
650 return $ opt_outputTy $ idris_options i
652setIdeSlave :: Bool -> Idris ()
653setIdeSlave True = do i <- getIState
654 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
655setIdeSlave False = return ()
657setTargetTriple :: String -> Idris ()
658setTargetTriple t = do i <- getIState
659 let opts = idris_options i
660 opt' = opts { opt_triple = t }
661 putIState $ i { idris_options = opt' }
663targetTriple :: Idris String
664targetTriple = do i <- getIState
665 return (opt_triple (idris_options i))
667setTargetCPU :: String -> Idris ()
668setTargetCPU t = do i <- getIState
669 let opts = idris_options i
670 opt' = opts { opt_cpu = t }
671 putIState $ i { idris_options = opt' }
673targetCPU :: Idris String
674targetCPU = do i <- getIState
675 return (opt_cpu (idris_options i))
677setOptLevel :: Word -> Idris ()
678setOptLevel t = do i <- getIState
679 let opts = idris_options i
680 opt' = opts { opt_optLevel = t }
681 putIState $ i { idris_options = opt' }
683optLevel :: Idris Word
684optLevel = do i <- getIState
685 return (opt_optLevel (idris_options i))
687verbose :: Idris Bool
688verbose = do i <- getIState
689 return (opt_verbose (idris_options i))
691setVerbose :: Bool -> Idris ()
692setVerbose t = do i <- getIState
693 let opts = idris_options i
694 let opt' = opts { opt_verbose = t }
695 putIState $ i { idris_options = opt' }
697typeInType :: Idris Bool
698typeInType = do i <- getIState
699 return (opt_typeintype (idris_options i))
701setTypeInType :: Bool -> Idris ()
702setTypeInType t = do i <- getIState
703 let opts = idris_options i
704 let opt' = opts { opt_typeintype = t }
705 putIState $ i { idris_options = opt' }
707coverage :: Idris Bool
708coverage = do i <- getIState
709 return (opt_coverage (idris_options i))
711setCoverage :: Bool -> Idris ()
712setCoverage t = do i <- getIState
713 let opts = idris_options i
714 let opt' = opts { opt_coverage = t }
715 putIState $ i { idris_options = opt' }
717setIBCSubDir :: FilePath -> Idris ()
718setIBCSubDir fp = do i <- getIState
719 let opts = idris_options i
720 let opt' = opts { opt_ibcsubdir = fp }
721 putIState $ i { idris_options = opt' }
723valIBCSubDir :: IState -> Idris FilePath
724valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
726addImportDir :: FilePath -> Idris ()
727addImportDir fp = do i <- getIState
728 let opts = idris_options i
729 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
730 putIState $ i { idris_options = opt' }
732setImportDirs :: [FilePath] -> Idris ()
733setImportDirs fps = do i <- getIState
734 let opts = idris_options i
735 let opt' = opts { opt_importdirs = fps }
736 putIState $ i { idris_options = opt' }
738allImportDirs :: Idris [FilePath]
739allImportDirs = do i <- getIState
740 let optdirs = opt_importdirs (idris_options i)
741 return ("." : reverse optdirs)
743colourise :: Idris Bool
744colourise = do i <- getIState
745 return $ idris_colourRepl i
747setColourise :: Bool -> Idris ()
748setColourise b = do i <- getIState
749 putIState $ i { idris_colourRepl = b }
751setOutH :: Handle -> Idris ()
752setOutH h = do i <- getIState
753 putIState $ i { idris_outh = h }
755impShow :: Idris Bool
756impShow = do i <- getIState
757 return (opt_showimp (idris_options i))
759setImpShow :: Bool -> Idris ()
760setImpShow t = do i <- getIState
761 let opts = idris_options i
762 let opt' = opts { opt_showimp = t }
763 putIState $ i { idris_options = opt' }
765setColour :: ColourType -> IdrisColour -> Idris ()
766setColour ct c = do i <- getIState
767 let newTheme = setColour' ct c (idris_colourTheme i)
768 putIState $ i { idris_colourTheme = newTheme }
769 where setColour' KeywordColour c t = t { keywordColour = c }
770 setColour' BoundVarColour c t = t { boundVarColour = c }
771 setColour' ImplicitColour c t = t { implicitColour = c }
772 setColour' FunctionColour c t = t { functionColour = c }
773 setColour' TypeColour c t = t { typeColour = c }
774 setColour' DataColour c t = t { dataColour = c }
775 setColour' PromptColour c t = t { promptColour = c }
777logLvl :: Int -> String -> Idris ()
778logLvl l str = do i <- getIState
779 let lvl = opt_logLevel (idris_options i)
780 when (lvl >= l) $
781 case idris_outputmode i of
782 RawOutput -> do runIO $ putStrLn str
783 IdeSlave n ->
784 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
785 runIO $ putStrLn $ convSExp "log" good n
787cmdOptType :: Opt -> Idris Bool
788cmdOptType x = do i <- getIState
789 return $ x `elem` opt_cmdline (idris_options i)
791iLOG :: String -> Idris ()
792iLOG = logLvl 1
794noErrors :: Idris Bool
795noErrors = do i <- getIState
796 case errSpan i of
797 Nothing -> return True
798 _ -> return False
800setTypeCase :: Bool -> Idris ()
801setTypeCase t = do i <- getIState
802 let opts = idris_options i
803 let opt' = opts { opt_typecase = t }
804 putIState $ i { idris_options = opt' }
807-- Dealing with parameters
809expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
810 [Name] -> -- all names
811 [Name] -> -- names with no declaration
812 PTerm -> PTerm
813expandParams dec ps ns infs tm = en tm
814 where
815 -- if we shadow a name (say in a lambda binding) that is used in a call to
816 -- a lifted function, we need access to both names - once in the scope of the
817 -- binding and once to call the lifted functions. So we'll explicitly shadow
818 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
819 -- but we didn't...)
821 mkShadow (UN n) = MN 0 n
822 mkShadow (MN i n) = MN (i+1) n
823 mkShadow (NS x s) = NS (mkShadow x) s
825 en (PLam n t s)
826 | n `elem` (map fst ps ++ ns)
827 = let n' = mkShadow n in
828 PLam n' (en t) (en (shadow n n' s))
829 | otherwise = PLam n (en t) (en s)
830 en (PPi p n t s)
831 | n `elem` (map fst ps ++ ns)
832 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
833 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
834 | otherwise = PPi (enTacImp p) n (en t) (en s)
835 en (PLet n ty v s)
836 | n `elem` (map fst ps ++ ns)
837 = let n' = mkShadow n in
838 PLet n' (en ty) (en v) (en (shadow n n' s))
839 | otherwise = PLet n (en ty) (en v) (en s)
840 -- FIXME: Should only do this in a type signature!
841 en (PDPair f p (PRef f' n) t r)
842 | n `elem` (map fst ps ++ ns) && t /= Placeholder
843 = let n' = mkShadow n in
844 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
845 en (PEq f l r) = PEq f (en l) (en r)
846 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
847 en (PTyped l r) = PTyped (en l) (en r)
848 en (PPair f p l r) = PPair f p (en l) (en r)
849 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
850 en (PAlternative a as) = PAlternative a (map en as)
851 en (PHidden t) = PHidden (en t)
852 en (PUnifyLog t) = PUnifyLog (en t)
853 en (PDisamb ds t) = PDisamb ds (en t)
854 en (PNoImplicits t) = PNoImplicits (en t)
855 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
856 en (PProof ts) = PProof (map (fmap en) ts)
857 en (PTactics ts) = PTactics (map (fmap en) ts)
859 en (PQuote (Var n))
860 | n `nselem` ns = PQuote (Var (dec n))
861 en (PApp fc (PInferRef fc' n) as)
862 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
863 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
864 en (PApp fc (PRef fc' n) as)
865 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
866 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
867 | n `nselem` ns = PApp fc (PRef fc' (dec n))
868 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
869 en (PAppBind fc (PRef fc' n) as)
870 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
871 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
872 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
873 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
874 en (PRef fc n)
875 | n `elem` infs = PApp fc (PInferRef fc (dec n))
876 (map (pexp . (PRef fc)) (map fst ps))
877 | n `nselem` ns = PApp fc (PRef fc (dec n))
878 (map (pexp . (PRef fc)) (map fst ps))
879 en (PInferRef fc n)
880 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
881 (map (pexp . (PRef fc)) (map fst ps))
882 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
883 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
884 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
885 en t = t
887 nselem x [] = False
888 nselem x (y : xs) | nseq x y = True
889 | otherwise = nselem x xs
891 nseq x y = nsroot x == nsroot y
893 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
894 enTacImp other = other
896expandParamsD :: Bool -> -- True = RHS only
897 IState ->
898 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
899expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
900 = if n `elem` ns && (not rhsonly)
901 then -- trace (show (n, expandParams dec ps ns ty)) $
902 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
903 else --trace (show (n, expandParams dec ps ns ty)) $
904 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
905expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
906 = if n `elem` ns && (not rhsonly)
907 then -- trace (show (n, expandParams dec ps ns ty)) $
908 PPostulate doc syn fc o (dec n) (piBind ps
909 (expandParams dec ps ns [] ty))
910 else --trace (show (n, expandParams dec ps ns ty)) $
911 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
912expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
913 = let n' = if n `elem` ns then dec n else n in
914 PClauses fc opts n' (map expandParamsC cs)
915 where
916 expandParamsC (PClause fc n lhs ws rhs ds)
917 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
918 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
919 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
920 n' = if n `elem` ns then dec n else n
921 -- names bound on the lhs should not be expanded on the rhs
922 ns' = removeBound lhs ns in
923 PClause fc n' lhs'
924 (map (expandParams dec ps'' ns' []) ws)
925 (expandParams dec ps'' ns' [] rhs)
926 (map (expandParamsD True ist dec ps'' ns') ds)
927 expandParamsC (PWith fc n lhs ws wval ds)
928 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
929 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
930 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
931 n' = if n `elem` ns then dec n else n
932 ns' = removeBound lhs ns in
933 PWith fc n' lhs'
934 (map (expandParams dec ps'' ns' []) ws)
935 (expandParams dec ps'' ns' [] wval)
936 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
937 updateps yn nm [] = []
938 updateps yn nm (((a, t), i):as)
939 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
940 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
942 removeBound lhs ns = ns \\ nub (bnames lhs)
944 bnames (PRef _ n) = [n]
945 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
946 bnames (PPair _ _ l r) = bnames l ++ bnames r
947 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
948 bnames _ = []
950expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
951 = PData doc argDocs syn fc co (expandPData pd)
952 where
953 -- just do the type decl, leave constructors alone (parameters will be
954 -- added implicitly)
955 expandPData (PDatadecl n ty cons)
956 = if n `elem` ns
957 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
958 (map econ cons)
959 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
960 econ (doc, argDocs, n, t, fc, fs)
961 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
962expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
963 = if tn `elem` ns
964 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
965 cdoc (dec cn) conty
966 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
967 cdoc (dec cn) conty
968 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
969expandParamsD rhs ist dec ps ns (PParams f params pds)
970 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
971 (map (expandParamsD True ist dec ps ns) pds)
972-- (map (expandParamsD ist dec ps ns) pds)
973expandParamsD rhs ist dec ps ns (PMutual f pds)
974 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
975expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
976 = PClass doc info f
977 (map (expandParams dec ps ns []) cs)
978 n
979 (map (mapsnd (expandParams dec ps ns [])) params)
980 (map (expandParamsD rhs ist dec ps ns) decls)
981expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
982 = PInstance info f
983 (map (expandParams dec ps ns []) cs)
984 n
985 (map (expandParams dec ps ns []) params)
986 (expandParams dec ps ns [] ty)
987 cn
988 (map (expandParamsD rhs ist dec ps ns) decls)
989expandParamsD rhs ist dec ps ns d = d
991mapsnd f (x, t) = (x, f t)
993-- Calculate a priority for a type, for deciding elaboration order
994-- * if it's just a type variable or concrete type, do it early (0)
995-- * if there's only type variables and injective constructors, do it next (1)
996-- * if there's a function type, next (2)
997-- * finally, everything else (3)
999getPriority :: IState -> PTerm -> Int
1000getPriority i tm = 1 -- pri tm
1001 where
1002 pri (PRef _ n) =
1003 case lookupP n (tt_ctxt i) of
1004 ((P (DCon _ _) _ _):_) -> 1
1005 ((P (TCon _ _) _ _):_) -> 1
1006 ((P Ref _ _):_) -> 1
1007 [] -> 0 -- must be locally bound, if it's not an error...
1008 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1009 pri (PTrue _ _) = 0
1010 pri (PFalse _) = 0
1011 pri (PRefl _ _) = 1
1012 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1013 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1014 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1015 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1016 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1017 pri (PTyped l r) = pri l
1018 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1019 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1020 pri (PAlternative a as) = maximum (map pri as)
1021 pri (PConstant _) = 0
1022 pri Placeholder = 1
1023 pri _ = 3
1026addStatics :: Name -> Term -> PTerm -> Idris ()
1027addStatics n tm ptm =
1028 do let (statics, dynamics) = initStatics tm ptm
1029 let stnames = nub $ concatMap freeArgNames (map snd statics)
1030 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1031 -- also get the arguments which are 'uniquely inferrable' from
1032 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1033 let statics' = nub $ map fst statics ++
1034 filter (\x -> not (elem x dnames)) stnames
1035 let stpos = staticList statics' tm
1036 i <- getIState
1037 when (not (null statics)) $
1038 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1039 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1040 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1041 addIBC (IBCStatic n)
1042 where
1043 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1044 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1045 if pstatic p == Static then ((n, ty) : static, dynamic)
1046 else if (not (searchArg p))
1047 then (static, (n, ty) : dynamic)
1048 else (static, dynamic)
1049 initStatics t pt = ([], [])
1051 freeArgNames (Bind n (Pi ty) sc)
1052 = nub $ freeArgNames ty
1053 freeArgNames tm = let (_, args) = unApply tm in
1054 concatMap freeNames args
1056 -- if a name appears in a type class or tactic implicit index, it doesn't
1057 -- affect its 'uniquely inferrable' from a static status since these are
1058 -- resolved by searching.
1059 searchArg (Constraint _ _) = True
1060 searchArg (TacImp _ _ _) = True
1061 searchArg _ = False
1063 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1064 staticList _ _ = []
1066-- Dealing with implicit arguments
1068-- Add constraint bindings from using block
1070addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1071addUsingConstraints syn fc t
1072 = do ist <- get
1073 let ns = namesIn [] ist t
1074 let cs = getConstraints t -- check declared constraints
1075 let addconsts = uconsts \\ cs
1076 -- if all names in the arguments of addconsts appear in ns,
1077 -- add the constraint implicitly
1078 return (doAdd addconsts ns t)
1079 where uconsts = filter uconst (using syn)
1080 uconst (UConstraint _ _) = True
1081 uconst _ = False
1083 doAdd [] _ t = t
1084 -- if all of args in ns, then add it
1085 doAdd (UConstraint c args : cs) ns t
1086 | all (\n -> elem n ns) args
1087 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1088 (mkConst c args) (doAdd cs ns t)
1089 | otherwise = doAdd cs ns t
1091 mkConst c args = PApp fc (PRef fc c)
1092 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1094 getConstraints (PPi (Constraint _ _) _ c sc)
1095 = getcapp c ++ getConstraints sc
1096 getConstraints (PPi _ _ c sc) = getConstraints sc
1097 getConstraints _ = []
1099 getcapp (PApp _ (PRef _ c) args)
1100 = do ns <- mapM getName args
1101 return (UConstraint c ns)
1102 getcapp _ = []
1104 getName (PExp _ _ _ (PRef _ n)) = return n
1105 getName _ = []
1107-- Add implicit Pi bindings for any names in the term which appear in an
1108-- argument position.
1110-- This has become a right mess already. Better redo it some time...
1112implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1113implicit info syn n ptm = implicit' info syn [] n ptm
1115implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1116implicit' info syn ignore n ptm
1117 = do i <- getIState
1118 let (tm', impdata) = implicitise syn ignore i ptm
1119 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1120-- let (tm'', spos) = findStatics i tm'
1121 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1122 addIBC (IBCImp n)
1123 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1124-- i <- get
1125-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1126 return tm'
1127 where
1128 -- Detect unknown names in default arguments and throw error if found.
1129 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1130 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1132 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1133 notFoundInDefault kns (PTacImplicit _ _ n script _)
1134 = do i <- getIState
1135 case notFound kns (namesIn [] i script) of
1136 Nothing -> return (n:kns)
1137 Just name -> throwError (NoSuchVariable name)
1138 notFoundInDefault kns p = return ((pname p):kns)
1140 notFound :: [Name] -> [Name] -> Maybe Name
1141 notFound kns [] = Nothing
1142 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1143 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1145implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1146implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1147 let (declimps, ns') = execState (imps True [] tm) ([], [])
1148 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1149 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1150 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1151 if null ns
1152 then (tm, reverse declimps)
1153 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1154 where
1155 uvars = map ipair (filter uimplicit (using syn))
1156 pvars = syn_params syn
1158 inUsing n = n `elem` map fst uvars
1160 ipair (UImplicit x y) = (x, y)
1161 uimplicit (UImplicit _ _) = True
1162 uimplicit _ = False
1164 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1165 | otherwise = x : dropAll xs ys
1166 dropAll [] ys = []
1168 -- Find names in argument position in a type, suitable for implicit
1169 -- binding
1170 -- Not the function position, but do everything else...
1171 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1172 implNamesIn uv t = namesIn uv ist t
1174 imps top env (PApp _ f as)
1175 = do (decls, ns) <- get
1176 let isn = concatMap (namesIn uvars ist) (map getTm as)
1177 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1178 imps top env (PPi (Imp l _ _) n ty sc)
1179 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1180 (decls , ns) <- get
1181 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1182 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1183 imps True (n:env) sc
1184 imps top env (PPi (Exp l _ _) n ty sc)
1185 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1186 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1187 _ -> [])
1188 (decls, ns) <- get -- ignore decls in HO types
1189 put (PExp (getPriority ist ty) l n Placeholder : decls,
1190 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1191 imps True (n:env) sc
1192 imps top env (PPi (Constraint l _) n ty sc)
1193 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1194 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1195 _ -> [])
1196 (decls, ns) <- get -- ignore decls in HO types
1197 put (PConstraint 10 l n Placeholder : decls,
1198 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1199 imps True (n:env) sc
1200 imps top env (PPi (TacImp l _ scr) n ty sc)
1201 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1202 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1203 _ -> [])
1204 (decls, ns) <- get -- ignore decls in HO types
1205 put (PTacImplicit 10 l n scr Placeholder : decls,
1206 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1207 imps True (n:env) sc
1208 imps top env (PEq _ 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 (PRewrite _ l r _)
1213 = do (decls, ns) <- get
1214 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1215 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1216 imps top env (PTyped l r)
1217 = imps top env l
1218 imps top env (PPair _ _ l r)
1219 = do (decls, ns) <- get
1220 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1221 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1222 imps top env (PDPair _ _ (PRef _ n) t r)
1223 = do (decls, ns) <- get
1224 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1225 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1226 imps top env (PDPair _ _ l t r)
1227 = do (decls, ns) <- get
1228 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1229 namesIn uvars ist r
1230 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1231 imps top env (PAlternative a as)
1232 = do (decls, ns) <- get
1233 let isn = concatMap (namesIn uvars ist) as
1234 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1235 imps top env (PLam n ty sc)
1236 = do imps False env ty
1237 imps False (n:env) sc
1238 imps top env (PHidden tm) = imps False env tm
1239 imps top env (PUnifyLog tm) = imps False env tm
1240 imps top env (PNoImplicits tm) = imps False env tm
1241 imps top env _ = return ()
1243 pibind using [] sc = sc
1244 pibind using (n:ns) sc
1245 = case lookup n using of
1246 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1247 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1248 (pibind using ns sc)
1250-- Add implicit arguments in function calls
1251addImplPat :: IState -> PTerm -> PTerm
1252addImplPat = addImpl' True [] []
1254addImplBound :: IState -> [Name] -> PTerm -> PTerm
1255addImplBound ist ns = addImpl' False ns [] ist
1257addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1258addImplBoundInf ist ns inf = addImpl' False ns inf ist
1260addImpl :: IState -> PTerm -> PTerm
1261addImpl = addImpl' False [] []
1263-- TODO: in patterns, don't add implicits to function names guarded by constructors
1264-- and *not* inside a PHidden
1266addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1267addImpl' inpat env infns ist ptm
1268 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1269 where
1270 ai env ds (PRef fc f)
1271 | f `elem` infns = PInferRef fc f
1272 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1273 ai env ds (PHidden (PRef fc f))
1274 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1275 ai env ds (PEq fc l r)
1276 = let l' = ai env ds l
1277 r' = ai env ds r in
1278 PEq fc l' r'
1279 ai env ds (PRewrite fc l r g)
1280 = let l' = ai env ds l
1281 r' = ai env ds r
1282 g' = fmap (ai env ds) g in
1283 PRewrite fc l' r' g'
1284 ai env ds (PTyped l r)
1285 = let l' = ai env ds l
1286 r' = ai env ds r in
1287 PTyped l' r'
1288 ai env ds (PPair fc p l r)
1289 = let l' = ai env ds l
1290 r' = ai env ds r in
1291 PPair fc p l' r'
1292 ai env ds (PDPair fc p l t r)
1293 = let l' = ai env ds l
1294 t' = ai env ds t
1295 r' = ai env ds r in
1296 PDPair fc p l' t' r'
1297 ai env ds (PAlternative a as)
1298 = let as' = map (ai env ds) as in
1299 PAlternative a as'
1300 ai env _ (PDisamb ds' as) = ai env ds' as
1301 ai env ds (PApp fc (PInferRef _ f) as)
1302 = let as' = map (fmap (ai env ds)) as in
1303 PApp fc (PInferRef fc f) as'
1304 ai env ds (PApp fc ftm@(PRef _ f) as)
1305 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1306 | not (f `elem` map fst env)
1307 = let as' = map (fmap (ai env ds)) as in
1308 handleErr $ aiFn inpat False ist fc f ds as'
1309 | Just (Just ty) <- lookup f env =
1310 let as' = map (fmap (ai env ds)) as
1311 arity = getPArity ty in
1312 mkPApp fc arity ftm as'
1313 ai env ds (PApp fc f as)
1314 = let f' = ai env ds f
1315 as' = map (fmap (ai env ds)) as in
1316 mkPApp fc 1 f' as'
1317 ai env ds (PCase fc c os)
1318 = let c' = ai env ds c
1319 os' = map (pmap (ai env ds)) os in
1320 PCase fc c' os'
1321 ai env ds (PLam n ty sc)
1322 = let ty' = ai env ds ty
1323 sc' = ai ((n, Just ty):env) ds sc in
1324 PLam n ty' sc'
1325 ai env ds (PLet n ty val sc)
1326 = let ty' = ai env ds ty
1327 val' = ai env ds val
1328 sc' = ai ((n, Just ty):env) ds sc in
1329 PLet n ty' val' sc'
1330 ai env ds (PPi p n ty sc)
1331 = let ty' = ai env ds ty
1332 sc' = ai ((n, Just ty):env) ds sc in
1333 PPi p n ty' sc'
1334 ai env ds (PGoal fc r n sc)
1335 = let r' = ai env ds r
1336 sc' = ai ((n, Nothing):env) ds sc in
1337 PGoal fc r' n sc'
1338 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1339 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1340 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1341 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1342 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1343 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1344 ai env ds tm = tm
1346 handleErr (Left err) = PElabError err
1347 handleErr (Right x) = x
1349-- if in a pattern, and there are no arguments, and there's no possible
1350-- names with zero explicit arguments, don't add implicits.
1352aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1353aiFn inpat True ist fc f ds []
1354 = case lookupDef f (tt_ctxt ist) of
1355 [] -> Right $ PPatvar fc f
1356 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1357 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1358 if (not (vname f) || tcname f
1359 || any (conCaf (tt_ctxt ist)) ialts)
1360-- any constructor alts || any allImp ialts))
1361 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1362 else Right $ PPatvar fc f
1363 where imp (PExp _ _ _ _) = False
1364 imp _ = True
1365-- allImp [] = False
1366 allImp xs = all imp xs
1367 constructor (TyDecl (DCon _ _) _) = True
1368 constructor _ = False
1370 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1372 vname (UN n) = True -- non qualified
1373 vname _ = False
1375aiFn inpat expat ist fc f ds as
1376 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1377aiFn inpat expat ist fc f ds as
1378 -- This is where namespaces get resolved by adding PAlternative
1379 = do let ns = lookupCtxtName f (idris_implicits ist)
1380 let nh = filter (\(n, _) -> notHidden n) ns
1381 let ns' = case trimAlts ds nh of
1382 [] -> nh
1383 x -> x
1384 case ns' of
1385 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1386 [] -> if f `elem` (map fst (idris_metavars ist))
1387 then Right $ PApp fc (PRef fc f) as
1388 else Right $ mkPApp fc (length as) (PRef fc f) as
1389 alts -> Right $
1390 PAlternative True $
1391 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1392 (insertImpl ns as)) alts
1393 where
1394 trimAlts [] alts = alts
1395 trimAlts ns alts
1396 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1398 nspace (NS _ s) = s
1399 nspace _ = []
1401 notHidden n = case getAccessibility n of
1402 Hidden -> False
1403 _ -> True
1405 getAccessibility n
1406 = case lookupDefAcc n False (tt_ctxt ist) of
1407 [(n,t)] -> t
1408 _ -> Public
1410 insertImpl :: [PArg] -> [PArg] -> [PArg]
1411 insertImpl ps as = insImpAcc M.empty ps as
1413 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1414 -> [PArg] -- parameters
1415 -> [PArg] -- arguments
1416 -> [PArg]
1417 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1418 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1419 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1420 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1421 insImpAcc pnas (PConstraint p l n ty : ps) given =
1422 let rtc = PResolveTC fc in
1423 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1424 insImpAcc pnas (PImp p _ l n ty : ps) given =
1425 case find n given [] of
1426 Just (tm, given') ->
1427 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1428 Nothing ->
1429 PImp p True l n Placeholder :
1430 insImpAcc (M.insert n Placeholder pnas) ps given
1431 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1432 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1433 case find n given [] of
1434 Just (tm, given') ->
1435 PTacImplicit p l n sc tm :
1436 insImpAcc (M.insert n tm pnas) ps given'
1437 Nothing ->
1438 if inpat
1439 then PTacImplicit p l n sc Placeholder :
1440 insImpAcc (M.insert n Placeholder pnas) ps given
1441 else PTacImplicit p l n sc sc :
1442 insImpAcc (M.insert n sc pnas) ps given
1443 insImpAcc _ expected [] = []
1444 insImpAcc _ _ given = given
1446 find n [] acc = Nothing
1447 find n (PImp _ _ _ n' t : gs) acc
1448 | n == n' = Just (t, reverse acc ++ gs)
1449 find n (PTacImplicit _ _ n' _ t : gs) acc
1450 | n == n' = Just (t, reverse acc ++ gs)
1451 find n (g : gs) acc = find n gs (g : acc)
1453-- replace non-linear occurrences with _
1454-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1455-- it is hard to get right!
1457stripLinear :: IState -> PTerm -> PTerm
1458stripLinear i tm = evalState (sl tm) [] where
1459 sl :: PTerm -> State [Name] PTerm
1460 sl (PRef fc f)
1461 | (_:_) <- lookupTy f (tt_ctxt i)
1462 = return $ PRef fc f
1463 | otherwise = do ns <- get
1464 if (f `elem` ns)
1465 then return Placeholder
1466 else do put (f : ns)
1467 return (PRef fc f)
1468 sl (PPatvar fc f)
1469 = do ns <- get
1470 if (f `elem` ns)
1471 then return Placeholder
1472 else do put (f : ns)
1473 return (PPatvar fc f)
1474 sl t@(PAlternative _ (a : as)) = do sl a
1475 return t
1476 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1477 args' <- mapM slA args
1478 return $ PApp fc fn args'
1479 where slA (PImp p m l n t) = do t' <- sl t
1480 return $ PImp p m l n t'
1481 slA (PExp p l n t) = do t' <- sl t
1482 return $ PExp p l n t'
1483 slA (PConstraint p l n t)
1484 = do t' <- sl t
1485 return $ PConstraint p l n t'
1486 slA (PTacImplicit p l n sc t)
1487 = do t' <- sl t
1488 return $ PTacImplicit p l n sc t'
1489 sl x = return x
1491-- Remove functions which aren't applied to anything, which must then
1492-- be resolved by unification. Assume names resolved and alternatives
1493-- filled in (so no ambiguity).
1495stripUnmatchable :: IState -> PTerm -> PTerm
1496stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1497 su :: PTerm -> PTerm
1498 su (PRef fc f)
1499 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1500 = Placeholder
1501 su (PApp fc fn args)
1502 = PApp fc fn (fmap (fmap su) args)
1503 su (PAlternative b alts)
1504 = let alts' = filter (/= Placeholder) (map su alts) in
1505 if null alts' then Placeholder
1506 else PAlternative b alts'
1507 su (PPair fc p l r) = PPair fc p (su l) (su r)
1508 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1509 su t = t
1510stripUnmatchable i tm = tm
1512mkPApp fc a f [] = f
1513mkPApp fc a f as = let rest = drop a as in
1514 appRest fc (PApp fc f (take a as)) rest
1515 where
1516 appRest fc f [] = f
1517 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1519-- Find 'static' argument positions
1520-- (the declared ones, plus any names in argument position in the declared
1521-- statics)
1522-- FIXME: It's possible that this really has to happen after elaboration
1524findStatics :: IState -> PTerm -> (PTerm, [Bool])
1525findStatics ist tm = trace (show tm) $
1526 let (ns, ss) = fs tm in
1527 runState (pos ns ss tm) []
1528 where fs (PPi p n t sc)
1529 | Static <- pstatic p
1530 = let (ns, ss) = fs sc in
1531 (namesIn [] ist t : ns, n : ss)
1532 | otherwise = let (ns, ss) = fs sc in
1533 (ns, ss)
1534 fs _ = ([], [])
1536 inOne n ns = length (filter id (map (elem n) ns)) == 1
1538 pos ns ss (PPi p n t sc)
1539 | elem n ss = do sc' <- pos ns ss sc
1540 spos <- get
1541 put (True : spos)
1542 return (PPi (p { pstatic = Static }) n t sc')
1543 | otherwise = do sc' <- pos ns ss sc
1544 spos <- get
1545 put (False : spos)
1546 return (PPi p n t sc')
1547 pos ns ss t = return t
1549-- for 6.12/7 compatibility
1550data EitherErr a b = LeftErr a | RightOK b
1552instance Monad (EitherErr a) where
1553 return = RightOK
1555 (LeftErr e) >>= k = LeftErr e
1556 RightOK v >>= k = k v
1558toEither (LeftErr e) = Left e
1559toEither (RightOK ho) = Right ho
1561-- syntactic match of a against b, returning pair of variables in a
1562-- and what they match. Returns the pair that failed if not a match.
1564matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1565matchClause = matchClause' False
1567matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1568matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1569 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1571 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1572 fullApp x = x
1574 match' x y = match (fullApp x) (fullApp y)
1575 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1576 | fi == txt "fromInteger" && b == txt "builtins",
1577 PConstant (I _) <- getTm x = match (getTm x) x'
1578 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1579 | fi == txt "fromInteger" && b == txt "builtins",
1580 PConstant (I _) <- getTm x = match (getTm x) x'
1581 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1582 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1583 match (PApp _ f args) (PApp _ f' args')
1584 | length args == length args'
1585 = do mf <- match' f f'
1586 ms <- zipWithM matchArg args args'
1587 return (mf ++ concat ms)
1588 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1589 match (PPatvar f n) xr = match (PRef f n) xr
1590 match xr (PPatvar f n) = match xr (PRef f n)
1591 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1592 match (PRef _ n) tm@(PRef _ n')
1593 | n == n' && not names &&
1594 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1595 || tm == Placeholder)
1596 = return [(n, tm)]
1597 -- if one namespace is missing, drop the other
1598 | n == n' || n == dropNS n' || dropNS n == n' = return []
1599 where dropNS (NS n _) = n
1600 dropNS n = n
1601 match (PRef _ n) tm
1602 | not names && (not (isConName n (tt_ctxt i) ||
1603 isFnName n (tt_ctxt i)) || tm == Placeholder)
1604 = return [(n, tm)]
1605 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1606 mr <- match' r r'
1607 return (ml ++ mr)
1608 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1609 = do ml <- match' l l'
1610 mr <- match' r r'
1611 return (ml ++ mr)
1612 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1613 mr <- match r r'
1614 return (ml ++ mr)
1615 match (PTyped l r) x = match l x
1616 match x (PTyped l r) = match x l
1617 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1618 mr <- match' r r'
1619 return (ml ++ mr)
1620 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1621 mt <- match' t t'
1622 mr <- match' r r'
1623 return (ml ++ mt ++ mr)
1624 match (PAlternative a as) (PAlternative a' as')
1625 = do ms <- zipWithM match' as as'
1626 return (concat ms)
1627 match a@(PAlternative _ as) b
1628 = do let ms = zipWith match' as (repeat b)
1629 case (rights (map toEither ms)) of
1630 (x: _) -> return x
1631 _ -> LeftErr (a, b)
1632 match (PCase _ _ _) _ = return [] -- lifted out
1633 match (PMetavar _) _ = return [] -- modified
1634 match (PInferRef _ _) _ = return [] -- modified
1635 match (PQuote _) _ = return []
1636 match (PProof _) _ = return []
1637 match (PTactics _) _ = return []
1638 match (PRefl _ _) (PRefl _ _) = return []
1639 match (PResolveTC _) (PResolveTC _) = return []
1640 match (PTrue _ _) (PTrue _ _) = return []
1641 match (PFalse _) (PFalse _) = return []
1642 match (PReturn _) (PReturn _) = return []
1643 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1644 ms <- match' s s'
1645 return (mt ++ ms)
1646 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1647 ms <- match' s s'
1648 return (mt ++ ms)
1649 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1650 mty <- match' ty ty'
1651 ms <- match' s s'
1652 return (mt ++ mty ++ ms)
1653 match (PHidden x) (PHidden y) = match' x y
1654 match (PUnifyLog x) y = match' x y
1655 match x (PUnifyLog y) = match' x y
1656 match (PNoImplicits x) y = match' x y
1657 match x (PNoImplicits y) = match' x y
1658 match Placeholder _ = return []
1659 match _ Placeholder = return []
1660 match (PResolveTC _) _ = return []
1661 match a b | a == b = return []
1662 | otherwise = LeftErr (a, b)
1664 checkRpts (RightOK ms) = check ms where
1665 check ((n,t):xs)
1666 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1667 then Left (t, t')
1668 else check xs
1669 check (_:xs) = check xs
1670 check [] = Right ms
1671 checkRpts (LeftErr x) = Left x
1673substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1674substMatches ms = substMatchesShadow ms []
1676substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1677substMatchesShadow [] shs t = t
1678substMatchesShadow ((n,tm):ns) shs t
1679 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1681substMatch :: Name -> PTerm -> PTerm -> PTerm
1682substMatch n = substMatchShadow n []
1684substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1685substMatchShadow n shs tm t = sm shs t where
1686 sm xs (PRef _ n') | n == n' = tm
1687 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1688 sm xs (PPi p x t sc)
1689 | x `elem` xs
1690 = let x' = nextName x in
1691 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1692 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1693 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1694 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1695 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1696 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1697 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1698 (fmap (sm xs) tm)
1699 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1700 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1701 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1702 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1703 sm xs (PHidden x) = PHidden (sm xs x)
1704 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1705 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1706 sm xs x = x
1708 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1709 fullApp x = x
1711shadow :: Name -> Name -> PTerm -> PTerm
1712shadow n n' t = sm t where
1713 sm (PRef fc x) | n == x = PRef fc n'
1714 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1715 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1716 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1717 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1718 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1719 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1720 sm (PEq f x y) = PEq f (sm x) (sm y)
1721 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1722 sm (PTyped x y) = PTyped (sm x) (sm y)
1723 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1724 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1725 sm (PAlternative a as) = PAlternative a (map sm as)
1726 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1727 sm (PProof ts) = PProof (map (fmap sm) ts)
1728 sm (PHidden x) = PHidden (sm x)
1729 sm (PUnifyLog x) = PUnifyLog (sm x)
1730 sm (PNoImplicits x) = PNoImplicits (sm x)
1731 sm x = x
1733-- Rename any binders which are repeated (so that we don't have to mess
1734-- about with shadowing anywhere else).
1736mkUniqueNames :: [Name] -> PTerm -> PTerm
1737mkUniqueNames env tm = evalState (mkUniq tm) env where
1738 inScope = boundNamesIn tm
1740 mkUniqA arg = do t' <- mkUniq (getTm arg)
1741 return (arg { getTm = t' })
1743 -- Initialise the unique name with the environment length (so we're not
1744 -- looking for too long...)
1745 initN (UN n) l = UN $ txt (str n ++ show l)
1746 initN (MN i s) l = MN (i+l) s
1747 initN n l = n
1749 -- FIXME: Probably ought to do this for completeness! It's fine as
1750 -- long as there are no bindings inside tactics though.
1751 mkUniqT tac = return tac
1753 mkUniq :: PTerm -> State [Name] PTerm
1754 mkUniq (PLam n ty sc)
1755 = do env <- get
1756 (n', sc') <-
1757 if n `elem` env
1758 then do let n' = uniqueName (initN n (length env))
1759 (env ++ inScope)
1760 return (n', shadow n n' sc)
1761 else return (n, sc)
1762 put (n' : env)
1763 ty' <- mkUniq ty
1764 sc'' <- mkUniq sc'
1765 return $! PLam n' ty' sc''
1766 mkUniq (PPi p n ty sc)
1767 = do env <- get
1768 (n', sc') <-
1769 if n `elem` env
1770 then do let n' = uniqueName (initN n (length env))
1771 (env ++ inScope)
1772 return (n', shadow n n' sc)
1773 else return (n, sc)
1774 put (n' : env)
1775 ty' <- mkUniq ty
1776 sc'' <- mkUniq sc'
1777 return $! PPi p n' ty' sc''
1778 mkUniq (PLet n ty val sc)
1779 = do env <- get
1780 (n', sc') <-
1781 if n `elem` env
1782 then do let n' = uniqueName (initN n (length env))
1783 (env ++ inScope)
1784 return (n', shadow n n' sc)
1785 else return (n, sc)
1786 put (n' : env)
1787 ty' <- mkUniq ty; val' <- mkUniq val
1788 sc'' <- mkUniq sc'
1789 return $! PLet n' ty' val' sc''
1790 mkUniq (PApp fc t args)
1791 = do t' <- mkUniq t
1792 args' <- mapM mkUniqA args
1793 return $! PApp fc t' args'
1794 mkUniq (PAppBind fc t args)
1795 = do t' <- mkUniq t
1796 args' <- mapM mkUniqA args
1797 return $! PAppBind fc t' args'
1798 mkUniq (PCase fc t alts)
1799 = do t' <- mkUniq t
1800 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1801 return (x', y')) alts
1802 return $! PCase fc t' alts'
1803 mkUniq (PPair fc p l r)
1804 = do l' <- mkUniq l; r' <- mkUniq r
1805 return $! PPair fc p l' r'
1806 mkUniq (PDPair fc p (PRef fc' n) t sc)
1807 | t /= Placeholder
1808 = do env <- get
1809 (n', sc') <- if n `elem` env
1810 then do let n' = uniqueName n (env ++ inScope)
1811 return (n', shadow n n' sc)
1812 else return (n, sc)
1813 put (n' : env)
1814 t' <- mkUniq t
1815 sc'' <- mkUniq sc'
1816 return $! PDPair fc p (PRef fc' n') t' sc''
1817 mkUniq (PDPair fc p l t r)
1818 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1819 return $! PDPair fc p l' t' r'
1820 mkUniq (PAlternative b as)
1821 = liftM (PAlternative b) (mapM mkUniq as)
1822 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1823 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1824 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1825 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1826 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1827 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1828 mkUniq t = return t