git.iko.soy/Idris-dev
on e541d7e help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1846 lines 76 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 (AnnType "Type" "The type of types, one level up") $ 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
541-- | Tell clients how much was parsed and loaded
542isetLoadedRegion :: Idris ()
543isetLoadedRegion = do i <- getIState
544 let span = idris_parsedSpan i
545 case span of
546 Just fc ->
547 case idris_outputmode i of
548 IdeSlave n ->
549 runIO . putStrLn $
550 convSExp "set-loaded-region" fc n
551 Nothing -> return ()
553setLogLevel :: Int -> Idris ()
554setLogLevel l = do i <- getIState
555 let opts = idris_options i
556 let opt' = opts { opt_logLevel = l }
557 putIState $ i { idris_options = opt' }
559setCmdLine :: [Opt] -> Idris ()
560setCmdLine opts = do i <- getIState
561 let iopts = idris_options i
562 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
564getCmdLine :: Idris [Opt]
565getCmdLine = do i <- getIState
566 return (opt_cmdline (idris_options i))
568getDumpDefun :: Idris (Maybe FilePath)
569getDumpDefun = do i <- getIState
570 return $ findC (opt_cmdline (idris_options i))
571 where findC [] = Nothing
572 findC (DumpDefun x : _) = Just x
573 findC (_ : xs) = findC xs
575getDumpCases :: Idris (Maybe FilePath)
576getDumpCases = do i <- getIState
577 return $ findC (opt_cmdline (idris_options i))
578 where findC [] = Nothing
579 findC (DumpCases x : _) = Just x
580 findC (_ : xs) = findC xs
582logLevel :: Idris Int
583logLevel = do i <- getIState
584 return (opt_logLevel (idris_options i))
586setErrContext :: Bool -> Idris ()
587setErrContext t = do i <- getIState
588 let opts = idris_options i
589 let opt' = opts { opt_errContext = t }
590 putIState $ i { idris_options = opt' }
592errContext :: Idris Bool
593errContext = do i <- getIState
594 return (opt_errContext (idris_options i))
596useREPL :: Idris Bool
597useREPL = do i <- getIState
598 return (opt_repl (idris_options i))
600setREPL :: Bool -> Idris ()
601setREPL t = do i <- getIState
602 let opts = idris_options i
603 let opt' = opts { opt_repl = t }
604 putIState $ i { idris_options = opt' }
606showOrigErr :: Idris Bool
607showOrigErr = do i <- getIState
608 return (opt_origerr (idris_options i))
610setShowOrigErr :: Bool -> Idris ()
611setShowOrigErr b = do i <- getIState
612 let opts = idris_options i
613 let opt' = opts { opt_origerr = b }
614 putIState $ i { idris_options = opt' }
616setAutoSolve :: Bool -> Idris ()
617setAutoSolve b = do i <- getIState
618 let opts = idris_options i
619 let opt' = opts { opt_autoSolve = b }
620 putIState $ i { idris_options = opt' }
622setNoBanner :: Bool -> Idris ()
623setNoBanner n = do i <- getIState
624 let opts = idris_options i
625 let opt' = opts { opt_nobanner = n }
626 putIState $ i { idris_options = opt' }
628getNoBanner :: Idris Bool
629getNoBanner = do i <- getIState
630 let opts = idris_options i
631 return (opt_nobanner opts)
633setQuiet :: Bool -> Idris ()
634setQuiet q = do i <- getIState
635 let opts = idris_options i
636 let opt' = opts { opt_quiet = q }
637 putIState $ i { idris_options = opt' }
639getQuiet :: Idris Bool
640getQuiet = do i <- getIState
641 let opts = idris_options i
642 return (opt_quiet opts)
644setCodegen :: Codegen -> Idris ()
645setCodegen t = do i <- getIState
646 let opts = idris_options i
647 let opt' = opts { opt_codegen = t }
648 putIState $ i { idris_options = opt' }
650codegen :: Idris Codegen
651codegen = do i <- getIState
652 return (opt_codegen (idris_options i))
654setOutputTy :: OutputType -> Idris ()
655setOutputTy t = do i <- getIState
656 let opts = idris_options i
657 let opt' = opts { opt_outputTy = t }
658 putIState $ i { idris_options = opt' }
660outputTy :: Idris OutputType
661outputTy = do i <- getIState
662 return $ opt_outputTy $ idris_options i
664setIdeSlave :: Bool -> Idris ()
665setIdeSlave True = do i <- getIState
666 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
667setIdeSlave False = return ()
669setTargetTriple :: String -> Idris ()
670setTargetTriple t = do i <- getIState
671 let opts = idris_options i
672 opt' = opts { opt_triple = t }
673 putIState $ i { idris_options = opt' }
675targetTriple :: Idris String
676targetTriple = do i <- getIState
677 return (opt_triple (idris_options i))
679setTargetCPU :: String -> Idris ()
680setTargetCPU t = do i <- getIState
681 let opts = idris_options i
682 opt' = opts { opt_cpu = t }
683 putIState $ i { idris_options = opt' }
685targetCPU :: Idris String
686targetCPU = do i <- getIState
687 return (opt_cpu (idris_options i))
689setOptLevel :: Word -> Idris ()
690setOptLevel t = do i <- getIState
691 let opts = idris_options i
692 opt' = opts { opt_optLevel = t }
693 putIState $ i { idris_options = opt' }
695optLevel :: Idris Word
696optLevel = do i <- getIState
697 return (opt_optLevel (idris_options i))
699verbose :: Idris Bool
700verbose = do i <- getIState
701 return (opt_verbose (idris_options i))
703setVerbose :: Bool -> Idris ()
704setVerbose t = do i <- getIState
705 let opts = idris_options i
706 let opt' = opts { opt_verbose = t }
707 putIState $ i { idris_options = opt' }
709typeInType :: Idris Bool
710typeInType = do i <- getIState
711 return (opt_typeintype (idris_options i))
713setTypeInType :: Bool -> Idris ()
714setTypeInType t = do i <- getIState
715 let opts = idris_options i
716 let opt' = opts { opt_typeintype = t }
717 putIState $ i { idris_options = opt' }
719coverage :: Idris Bool
720coverage = do i <- getIState
721 return (opt_coverage (idris_options i))
723setCoverage :: Bool -> Idris ()
724setCoverage t = do i <- getIState
725 let opts = idris_options i
726 let opt' = opts { opt_coverage = t }
727 putIState $ i { idris_options = opt' }
729setIBCSubDir :: FilePath -> Idris ()
730setIBCSubDir fp = do i <- getIState
731 let opts = idris_options i
732 let opt' = opts { opt_ibcsubdir = fp }
733 putIState $ i { idris_options = opt' }
735valIBCSubDir :: IState -> Idris FilePath
736valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
738addImportDir :: FilePath -> Idris ()
739addImportDir fp = do i <- getIState
740 let opts = idris_options i
741 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
742 putIState $ i { idris_options = opt' }
744setImportDirs :: [FilePath] -> Idris ()
745setImportDirs fps = do i <- getIState
746 let opts = idris_options i
747 let opt' = opts { opt_importdirs = fps }
748 putIState $ i { idris_options = opt' }
750allImportDirs :: Idris [FilePath]
751allImportDirs = do i <- getIState
752 let optdirs = opt_importdirs (idris_options i)
753 return ("." : reverse optdirs)
755colourise :: Idris Bool
756colourise = do i <- getIState
757 return $ idris_colourRepl i
759setColourise :: Bool -> Idris ()
760setColourise b = do i <- getIState
761 putIState $ i { idris_colourRepl = b }
763setOutH :: Handle -> Idris ()
764setOutH h = do i <- getIState
765 putIState $ i { idris_outh = h }
767impShow :: Idris Bool
768impShow = do i <- getIState
769 return (opt_showimp (idris_options i))
771setImpShow :: Bool -> Idris ()
772setImpShow t = do i <- getIState
773 let opts = idris_options i
774 let opt' = opts { opt_showimp = t }
775 putIState $ i { idris_options = opt' }
777setColour :: ColourType -> IdrisColour -> Idris ()
778setColour ct c = do i <- getIState
779 let newTheme = setColour' ct c (idris_colourTheme i)
780 putIState $ i { idris_colourTheme = newTheme }
781 where setColour' KeywordColour c t = t { keywordColour = c }
782 setColour' BoundVarColour c t = t { boundVarColour = c }
783 setColour' ImplicitColour c t = t { implicitColour = c }
784 setColour' FunctionColour c t = t { functionColour = c }
785 setColour' TypeColour c t = t { typeColour = c }
786 setColour' DataColour c t = t { dataColour = c }
787 setColour' PromptColour c t = t { promptColour = c }
789logLvl :: Int -> String -> Idris ()
790logLvl l str = do i <- getIState
791 let lvl = opt_logLevel (idris_options i)
792 when (lvl >= l) $
793 case idris_outputmode i of
794 RawOutput -> do runIO $ putStrLn str
795 IdeSlave n ->
796 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
797 runIO $ putStrLn $ convSExp "log" good n
799cmdOptType :: Opt -> Idris Bool
800cmdOptType x = do i <- getIState
801 return $ x `elem` opt_cmdline (idris_options i)
803iLOG :: String -> Idris ()
804iLOG = logLvl 1
806noErrors :: Idris Bool
807noErrors = do i <- getIState
808 case errSpan i of
809 Nothing -> return True
810 _ -> return False
812setTypeCase :: Bool -> Idris ()
813setTypeCase t = do i <- getIState
814 let opts = idris_options i
815 let opt' = opts { opt_typecase = t }
816 putIState $ i { idris_options = opt' }
819-- Dealing with parameters
821expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
822 [Name] -> -- all names
823 [Name] -> -- names with no declaration
824 PTerm -> PTerm
825expandParams dec ps ns infs tm = en tm
826 where
827 -- if we shadow a name (say in a lambda binding) that is used in a call to
828 -- a lifted function, we need access to both names - once in the scope of the
829 -- binding and once to call the lifted functions. So we'll explicitly shadow
830 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
831 -- but we didn't...)
833 mkShadow (UN n) = MN 0 n
834 mkShadow (MN i n) = MN (i+1) n
835 mkShadow (NS x s) = NS (mkShadow x) s
837 en (PLam n t s)
838 | n `elem` (map fst ps ++ ns)
839 = let n' = mkShadow n in
840 PLam n' (en t) (en (shadow n n' s))
841 | otherwise = PLam n (en t) (en s)
842 en (PPi p n t s)
843 | n `elem` (map fst ps ++ ns)
844 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
845 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
846 | otherwise = PPi (enTacImp p) n (en t) (en s)
847 en (PLet n ty v s)
848 | n `elem` (map fst ps ++ ns)
849 = let n' = mkShadow n in
850 PLet n' (en ty) (en v) (en (shadow n n' s))
851 | otherwise = PLet n (en ty) (en v) (en s)
852 -- FIXME: Should only do this in a type signature!
853 en (PDPair f p (PRef f' n) t r)
854 | n `elem` (map fst ps ++ ns) && t /= Placeholder
855 = let n' = mkShadow n in
856 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
857 en (PEq f l r) = PEq f (en l) (en r)
858 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
859 en (PTyped l r) = PTyped (en l) (en r)
860 en (PPair f p l r) = PPair f p (en l) (en r)
861 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
862 en (PAlternative a as) = PAlternative a (map en as)
863 en (PHidden t) = PHidden (en t)
864 en (PUnifyLog t) = PUnifyLog (en t)
865 en (PDisamb ds t) = PDisamb ds (en t)
866 en (PNoImplicits t) = PNoImplicits (en t)
867 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
868 en (PProof ts) = PProof (map (fmap en) ts)
869 en (PTactics ts) = PTactics (map (fmap en) ts)
871 en (PQuote (Var n))
872 | n `nselem` ns = PQuote (Var (dec n))
873 en (PApp fc (PInferRef fc' n) as)
874 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
875 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
876 en (PApp fc (PRef fc' n) as)
877 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
878 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
879 | n `nselem` ns = PApp fc (PRef fc' (dec n))
880 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
881 en (PAppBind fc (PRef fc' n) as)
882 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
883 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
884 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
885 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
886 en (PRef fc n)
887 | n `elem` infs = PApp fc (PInferRef fc (dec n))
888 (map (pexp . (PRef fc)) (map fst ps))
889 | n `nselem` ns = PApp fc (PRef fc (dec n))
890 (map (pexp . (PRef fc)) (map fst ps))
891 en (PInferRef fc n)
892 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
893 (map (pexp . (PRef fc)) (map fst ps))
894 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
895 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
896 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
897 en t = t
899 nselem x [] = False
900 nselem x (y : xs) | nseq x y = True
901 | otherwise = nselem x xs
903 nseq x y = nsroot x == nsroot y
905 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
906 enTacImp other = other
908expandParamsD :: Bool -> -- True = RHS only
909 IState ->
910 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
911expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
912 = if n `elem` ns && (not rhsonly)
913 then -- trace (show (n, expandParams dec ps ns ty)) $
914 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
915 else --trace (show (n, expandParams dec ps ns ty)) $
916 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
917expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
918 = if n `elem` ns && (not rhsonly)
919 then -- trace (show (n, expandParams dec ps ns ty)) $
920 PPostulate doc syn fc o (dec n) (piBind ps
921 (expandParams dec ps ns [] ty))
922 else --trace (show (n, expandParams dec ps ns ty)) $
923 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
924expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
925 = let n' = if n `elem` ns then dec n else n in
926 PClauses fc opts n' (map expandParamsC cs)
927 where
928 expandParamsC (PClause fc n lhs ws rhs ds)
929 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
930 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
931 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
932 n' = if n `elem` ns then dec n else n
933 -- names bound on the lhs should not be expanded on the rhs
934 ns' = removeBound lhs ns in
935 PClause fc n' lhs'
936 (map (expandParams dec ps'' ns' []) ws)
937 (expandParams dec ps'' ns' [] rhs)
938 (map (expandParamsD True ist dec ps'' ns') ds)
939 expandParamsC (PWith fc n lhs ws wval ds)
940 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
941 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
942 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
943 n' = if n `elem` ns then dec n else n
944 ns' = removeBound lhs ns in
945 PWith fc n' lhs'
946 (map (expandParams dec ps'' ns' []) ws)
947 (expandParams dec ps'' ns' [] wval)
948 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
949 updateps yn nm [] = []
950 updateps yn nm (((a, t), i):as)
951 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
952 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
954 removeBound lhs ns = ns \\ nub (bnames lhs)
956 bnames (PRef _ n) = [n]
957 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
958 bnames (PPair _ _ l r) = bnames l ++ bnames r
959 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
960 bnames _ = []
962-- | Expands parameters defined in parameter and where blocks inside of declarations
963expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
964 = PData doc argDocs syn fc co (expandPData pd)
965 where
966 -- just do the type decl, leave constructors alone (parameters will be
967 -- added implicitly)
968 expandPData (PDatadecl n ty cons)
969 = if n `elem` ns
970 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
971 (map econ cons)
972 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
973 econ (doc, argDocs, n, t, fc, fs)
974 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
975expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
976 = if tn `elem` ns
977 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
978 opts cdoc (dec cn) conty
979 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
980 opts cdoc (dec cn) conty
981 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
982expandParamsD rhs ist dec ps ns (PParams f params pds)
983 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
984 (map (expandParamsD True ist dec ps ns) pds)
985-- (map (expandParamsD ist dec ps ns) pds)
986expandParamsD rhs ist dec ps ns (PMutual f pds)
987 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
988expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
989 = PClass doc info f
990 (map (expandParams dec ps ns []) cs)
991 n
992 (map (mapsnd (expandParams dec ps ns [])) params)
993 pDocs
994 (map (expandParamsD rhs ist dec ps ns) decls)
995expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
996 = PInstance info f
997 (map (expandParams dec ps ns []) cs)
998 n
999 (map (expandParams dec ps ns []) params)
1000 (expandParams dec ps ns [] ty)
1001 cn
1002 (map (expandParamsD rhs ist dec ps ns) decls)
1003expandParamsD rhs ist dec ps ns d = d
1005mapsnd f (x, t) = (x, f t)
1007-- Calculate a priority for a type, for deciding elaboration order
1008-- * if it's just a type variable or concrete type, do it early (0)
1009-- * if there's only type variables and injective constructors, do it next (1)
1010-- * if there's a function type, next (2)
1011-- * finally, everything else (3)
1013getPriority :: IState -> PTerm -> Int
1014getPriority i tm = 1 -- pri tm
1015 where
1016 pri (PRef _ n) =
1017 case lookupP n (tt_ctxt i) of
1018 ((P (DCon _ _) _ _):_) -> 1
1019 ((P (TCon _ _) _ _):_) -> 1
1020 ((P Ref _ _):_) -> 1
1021 [] -> 0 -- must be locally bound, if it's not an error...
1022 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1023 pri (PTrue _ _) = 0
1024 pri (PFalse _) = 0
1025 pri (PRefl _ _) = 1
1026 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1027 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1028 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1029 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1030 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1031 pri (PTyped l r) = pri l
1032 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1033 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1034 pri (PAlternative a as) = maximum (map pri as)
1035 pri (PConstant _) = 0
1036 pri Placeholder = 1
1037 pri _ = 3
1040addStatics :: Name -> Term -> PTerm -> Idris ()
1041addStatics n tm ptm =
1042 do let (statics, dynamics) = initStatics tm ptm
1043 let stnames = nub $ concatMap freeArgNames (map snd statics)
1044 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1045 -- also get the arguments which are 'uniquely inferrable' from
1046 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1047 let statics' = nub $ map fst statics ++
1048 filter (\x -> not (elem x dnames)) stnames
1049 let stpos = staticList statics' tm
1050 i <- getIState
1051 when (not (null statics)) $
1052 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1053 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1054 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1055 addIBC (IBCStatic n)
1056 where
1057 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1058 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1059 if pstatic p == Static then ((n, ty) : static, dynamic)
1060 else if (not (searchArg p))
1061 then (static, (n, ty) : dynamic)
1062 else (static, dynamic)
1063 initStatics t pt = ([], [])
1065 freeArgNames (Bind n (Pi ty) sc)
1066 = nub $ freeArgNames ty
1067 freeArgNames tm = let (_, args) = unApply tm in
1068 concatMap freeNames args
1070 -- if a name appears in a type class or tactic implicit index, it doesn't
1071 -- affect its 'uniquely inferrable' from a static status since these are
1072 -- resolved by searching.
1073 searchArg (Constraint _ _) = True
1074 searchArg (TacImp _ _ _) = True
1075 searchArg _ = False
1077 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1078 staticList _ _ = []
1080-- Dealing with implicit arguments
1082-- Add constraint bindings from using block
1084addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1085addUsingConstraints syn fc t
1086 = do ist <- get
1087 let ns = namesIn [] ist t
1088 let cs = getConstraints t -- check declared constraints
1089 let addconsts = uconsts \\ cs
1090 -- if all names in the arguments of addconsts appear in ns,
1091 -- add the constraint implicitly
1092 return (doAdd addconsts ns t)
1093 where uconsts = filter uconst (using syn)
1094 uconst (UConstraint _ _) = True
1095 uconst _ = False
1097 doAdd [] _ t = t
1098 -- if all of args in ns, then add it
1099 doAdd (UConstraint c args : cs) ns t
1100 | all (\n -> elem n ns) args
1101 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1102 (mkConst c args) (doAdd cs ns t)
1103 | otherwise = doAdd cs ns t
1105 mkConst c args = PApp fc (PRef fc c)
1106 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1108 getConstraints (PPi (Constraint _ _) _ c sc)
1109 = getcapp c ++ getConstraints sc
1110 getConstraints (PPi _ _ c sc) = getConstraints sc
1111 getConstraints _ = []
1113 getcapp (PApp _ (PRef _ c) args)
1114 = do ns <- mapM getName args
1115 return (UConstraint c ns)
1116 getcapp _ = []
1118 getName (PExp _ _ _ (PRef _ n)) = return n
1119 getName _ = []
1121-- Add implicit Pi bindings for any names in the term which appear in an
1122-- argument position.
1124-- This has become a right mess already. Better redo it some time...
1126implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1127implicit info syn n ptm = implicit' info syn [] n ptm
1129implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1130implicit' info syn ignore n ptm
1131 = do i <- getIState
1132 let (tm', impdata) = implicitise syn ignore i ptm
1133 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1134-- let (tm'', spos) = findStatics i tm'
1135 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1136 addIBC (IBCImp n)
1137 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1138-- i <- get
1139-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1140 return tm'
1141 where
1142 -- Detect unknown names in default arguments and throw error if found.
1143 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1144 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1146 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1147 notFoundInDefault kns (PTacImplicit _ _ n script _)
1148 = do i <- getIState
1149 case notFound kns (namesIn [] i script) of
1150 Nothing -> return (n:kns)
1151 Just name -> throwError (NoSuchVariable name)
1152 notFoundInDefault kns p = return ((pname p):kns)
1154 notFound :: [Name] -> [Name] -> Maybe Name
1155 notFound kns [] = Nothing
1156 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1157 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1159implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1160implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1161 let (declimps, ns') = execState (imps True [] tm) ([], [])
1162 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1163 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1164 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1165 if null ns
1166 then (tm, reverse declimps)
1167 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1168 where
1169 uvars = map ipair (filter uimplicit (using syn))
1170 pvars = syn_params syn
1172 inUsing n = n `elem` map fst uvars
1174 ipair (UImplicit x y) = (x, y)
1175 uimplicit (UImplicit _ _) = True
1176 uimplicit _ = False
1178 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1179 | otherwise = x : dropAll xs ys
1180 dropAll [] ys = []
1182 -- Find names in argument position in a type, suitable for implicit
1183 -- binding
1184 -- Not the function position, but do everything else...
1185 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1186 implNamesIn uv t = namesIn uv ist t
1188 imps top env (PApp _ f as)
1189 = do (decls, ns) <- get
1190 let isn = concatMap (namesIn uvars ist) (map getTm as)
1191 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1192 imps top env (PPi (Imp l _ _) n ty sc)
1193 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1194 (decls , ns) <- get
1195 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1196 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1197 imps True (n:env) sc
1198 imps top env (PPi (Exp l _ _) n ty sc)
1199 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1200 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1201 _ -> [])
1202 (decls, ns) <- get -- ignore decls in HO types
1203 put (PExp (getPriority ist ty) l n Placeholder : decls,
1204 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1205 imps True (n:env) sc
1206 imps top env (PPi (Constraint l _) n ty sc)
1207 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1208 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1209 _ -> [])
1210 (decls, ns) <- get -- ignore decls in HO types
1211 put (PConstraint 10 l n Placeholder : decls,
1212 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1213 imps True (n:env) sc
1214 imps top env (PPi (TacImp l _ scr) n ty sc)
1215 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1216 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1217 _ -> [])
1218 (decls, ns) <- get -- ignore decls in HO types
1219 put (PTacImplicit 10 l n scr Placeholder : decls,
1220 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1221 imps True (n:env) sc
1222 imps top env (PEq _ l r)
1223 = do (decls, ns) <- get
1224 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1225 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1226 imps top env (PRewrite _ l r _)
1227 = do (decls, ns) <- get
1228 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1229 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1230 imps top env (PTyped l r)
1231 = imps top env l
1232 imps top env (PPair _ _ l r)
1233 = do (decls, ns) <- get
1234 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1235 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1236 imps top env (PDPair _ _ (PRef _ n) t r)
1237 = do (decls, ns) <- get
1238 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1239 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1240 imps top env (PDPair _ _ l t r)
1241 = do (decls, ns) <- get
1242 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1243 namesIn uvars ist r
1244 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1245 imps top env (PAlternative a as)
1246 = do (decls, ns) <- get
1247 let isn = concatMap (namesIn uvars ist) as
1248 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1249 imps top env (PLam n ty sc)
1250 = do imps False env ty
1251 imps False (n:env) sc
1252 imps top env (PHidden tm) = imps False env tm
1253 imps top env (PUnifyLog tm) = imps False env tm
1254 imps top env (PNoImplicits tm) = imps False env tm
1255 imps top env _ = return ()
1257 pibind using [] sc = sc
1258 pibind using (n:ns) sc
1259 = case lookup n using of
1260 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1261 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1262 (pibind using ns sc)
1264-- Add implicit arguments in function calls
1265addImplPat :: IState -> PTerm -> PTerm
1266addImplPat = addImpl' True [] []
1268addImplBound :: IState -> [Name] -> PTerm -> PTerm
1269addImplBound ist ns = addImpl' False ns [] ist
1271addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1272addImplBoundInf ist ns inf = addImpl' False ns inf ist
1274addImpl :: IState -> PTerm -> PTerm
1275addImpl = addImpl' False [] []
1277-- TODO: in patterns, don't add implicits to function names guarded by constructors
1278-- and *not* inside a PHidden
1280addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1281addImpl' inpat env infns ist ptm
1282 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1283 where
1284 ai env ds (PRef fc f)
1285 | f `elem` infns = PInferRef fc f
1286 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1287 ai env ds (PHidden (PRef fc f))
1288 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1289 ai env ds (PEq fc l r)
1290 = let l' = ai env ds l
1291 r' = ai env ds r in
1292 PEq fc l' r'
1293 ai env ds (PRewrite fc l r g)
1294 = let l' = ai env ds l
1295 r' = ai env ds r
1296 g' = fmap (ai env ds) g in
1297 PRewrite fc l' r' g'
1298 ai env ds (PTyped l r)
1299 = let l' = ai env ds l
1300 r' = ai env ds r in
1301 PTyped l' r'
1302 ai env ds (PPair fc p l r)
1303 = let l' = ai env ds l
1304 r' = ai env ds r in
1305 PPair fc p l' r'
1306 ai env ds (PDPair fc p l t r)
1307 = let l' = ai env ds l
1308 t' = ai env ds t
1309 r' = ai env ds r in
1310 PDPair fc p l' t' r'
1311 ai env ds (PAlternative a as)
1312 = let as' = map (ai env ds) as in
1313 PAlternative a as'
1314 ai env _ (PDisamb ds' as) = ai env ds' as
1315 ai env ds (PApp fc (PInferRef _ f) as)
1316 = let as' = map (fmap (ai env ds)) as in
1317 PApp fc (PInferRef fc f) as'
1318 ai env ds (PApp fc ftm@(PRef _ f) as)
1319 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1320 | not (f `elem` map fst env)
1321 = let as' = map (fmap (ai env ds)) as in
1322 handleErr $ aiFn inpat False ist fc f ds as'
1323 | Just (Just ty) <- lookup f env =
1324 let as' = map (fmap (ai env ds)) as
1325 arity = getPArity ty in
1326 mkPApp fc arity ftm as'
1327 ai env ds (PApp fc f as)
1328 = let f' = ai env ds f
1329 as' = map (fmap (ai env ds)) as in
1330 mkPApp fc 1 f' as'
1331 ai env ds (PCase fc c os)
1332 = let c' = ai env ds c in
1333 -- leave os alone, because they get lifted into a new pattern match
1334 -- definition which is passed through addImpl again with more scope
1335 -- information
1336 PCase fc c' os
1337 ai env ds (PLam n ty sc)
1338 = let ty' = ai env ds ty
1339 sc' = ai ((n, Just ty):env) ds sc in
1340 PLam n ty' sc'
1341 ai env ds (PLet n ty val sc)
1342 = let ty' = ai env ds ty
1343 val' = ai env ds val
1344 sc' = ai ((n, Just ty):env) ds sc in
1345 PLet n ty' val' sc'
1346 ai env ds (PPi p n ty sc)
1347 = let ty' = ai env ds ty
1348 sc' = ai ((n, Just ty):env) ds sc in
1349 PPi p n ty' sc'
1350 ai env ds (PGoal fc r n sc)
1351 = let r' = ai env ds r
1352 sc' = ai ((n, Nothing):env) ds sc in
1353 PGoal fc r' n sc'
1354 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1355 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1356 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1357 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1358 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1359 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1360 ai env ds tm = tm
1362 handleErr (Left err) = PElabError err
1363 handleErr (Right x) = x
1365-- if in a pattern, and there are no arguments, and there's no possible
1366-- names with zero explicit arguments, don't add implicits.
1368aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1369aiFn inpat True ist fc f ds []
1370 = case lookupDef f (tt_ctxt ist) of
1371 [] -> Right $ PPatvar fc f
1372 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1373 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1374 if (not (vname f) || tcname f
1375 || any (conCaf (tt_ctxt ist)) ialts)
1376-- any constructor alts || any allImp ialts))
1377 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1378 else Right $ PPatvar fc f
1379 where imp (PExp _ _ _ _) = False
1380 imp _ = True
1381-- allImp [] = False
1382 allImp xs = all imp xs
1383 constructor (TyDecl (DCon _ _) _) = True
1384 constructor _ = False
1386 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1388 vname (UN n) = True -- non qualified
1389 vname _ = False
1391aiFn inpat expat ist fc f ds as
1392 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1393aiFn inpat expat ist fc f ds as
1394 -- This is where namespaces get resolved by adding PAlternative
1395 = do let ns = lookupCtxtName f (idris_implicits ist)
1396 let nh = filter (\(n, _) -> notHidden n) ns
1397 let ns' = case trimAlts ds nh of
1398 [] -> nh
1399 x -> x
1400 case ns' of
1401 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1402 [] -> if f `elem` (map fst (idris_metavars ist))
1403 then Right $ PApp fc (PRef fc f) as
1404 else Right $ mkPApp fc (length as) (PRef fc f) as
1405 alts -> Right $
1406 PAlternative True $
1407 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1408 (insertImpl ns as)) alts
1409 where
1410 trimAlts [] alts = alts
1411 trimAlts ns alts
1412 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1414 nspace (NS _ s) = s
1415 nspace _ = []
1417 notHidden n = case getAccessibility n of
1418 Hidden -> False
1419 _ -> True
1421 getAccessibility n
1422 = case lookupDefAcc n False (tt_ctxt ist) of
1423 [(n,t)] -> t
1424 _ -> Public
1426 insertImpl :: [PArg] -> [PArg] -> [PArg]
1427 insertImpl ps as = insImpAcc M.empty ps as
1429 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1430 -> [PArg] -- parameters
1431 -> [PArg] -- arguments
1432 -> [PArg]
1433 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1434 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1435 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1436 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1437 insImpAcc pnas (PConstraint p l n ty : ps) given =
1438 let rtc = PResolveTC fc in
1439 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1440 insImpAcc pnas (PImp p _ l n ty : ps) given =
1441 case find n given [] of
1442 Just (tm, given') ->
1443 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1444 Nothing ->
1445 PImp p True l n Placeholder :
1446 insImpAcc (M.insert n Placeholder pnas) ps given
1447 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1448 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1449 case find n given [] of
1450 Just (tm, given') ->
1451 PTacImplicit p l n sc tm :
1452 insImpAcc (M.insert n tm pnas) ps given'
1453 Nothing ->
1454 if inpat
1455 then PTacImplicit p l n sc Placeholder :
1456 insImpAcc (M.insert n Placeholder pnas) ps given
1457 else PTacImplicit p l n sc sc :
1458 insImpAcc (M.insert n sc pnas) ps given
1459 insImpAcc _ expected [] = []
1460 insImpAcc _ _ given = given
1462 find n [] acc = Nothing
1463 find n (PImp _ _ _ n' t : gs) acc
1464 | n == n' = Just (t, reverse acc ++ gs)
1465 find n (PTacImplicit _ _ n' _ t : gs) acc
1466 | n == n' = Just (t, reverse acc ++ gs)
1467 find n (g : gs) acc = find n gs (g : acc)
1469-- replace non-linear occurrences with _
1470-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1471-- it is hard to get right!
1473stripLinear :: IState -> PTerm -> PTerm
1474stripLinear i tm = evalState (sl tm) [] where
1475 sl :: PTerm -> State [Name] PTerm
1476 sl (PRef fc f)
1477 | (_:_) <- lookupTy f (tt_ctxt i)
1478 = return $ PRef fc f
1479 | otherwise = do ns <- get
1480 if (f `elem` ns)
1481 then return Placeholder
1482 else do put (f : ns)
1483 return (PRef fc f)
1484 sl (PPatvar fc f)
1485 = do ns <- get
1486 if (f `elem` ns)
1487 then return Placeholder
1488 else do put (f : ns)
1489 return (PPatvar fc f)
1490 sl t@(PAlternative _ (a : as)) = do sl a
1491 return t
1492 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1493 args' <- mapM slA args
1494 return $ PApp fc fn args'
1495 where slA (PImp p m l n t) = do t' <- sl t
1496 return $ PImp p m l n t'
1497 slA (PExp p l n t) = do t' <- sl t
1498 return $ PExp p l n t'
1499 slA (PConstraint p l n t)
1500 = do t' <- sl t
1501 return $ PConstraint p l n t'
1502 slA (PTacImplicit p l n sc t)
1503 = do t' <- sl t
1504 return $ PTacImplicit p l n sc t'
1505 sl x = return x
1507-- Remove functions which aren't applied to anything, which must then
1508-- be resolved by unification. Assume names resolved and alternatives
1509-- filled in (so no ambiguity).
1511stripUnmatchable :: IState -> PTerm -> PTerm
1512stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1513 su :: PTerm -> PTerm
1514 su (PRef fc f)
1515 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1516 = Placeholder
1517 su (PApp fc fn args)
1518 = PApp fc fn (fmap (fmap su) args)
1519 su (PAlternative b alts)
1520 = let alts' = filter (/= Placeholder) (map su alts) in
1521 if null alts' then Placeholder
1522 else PAlternative b alts'
1523 su (PPair fc p l r) = PPair fc p (su l) (su r)
1524 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1525 su t = t
1526stripUnmatchable i tm = tm
1528mkPApp fc a f [] = f
1529mkPApp fc a f as = let rest = drop a as in
1530 appRest fc (PApp fc f (take a as)) rest
1531 where
1532 appRest fc f [] = f
1533 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1535-- Find 'static' argument positions
1536-- (the declared ones, plus any names in argument position in the declared
1537-- statics)
1538-- FIXME: It's possible that this really has to happen after elaboration
1540findStatics :: IState -> PTerm -> (PTerm, [Bool])
1541findStatics ist tm = trace (show tm) $
1542 let (ns, ss) = fs tm in
1543 runState (pos ns ss tm) []
1544 where fs (PPi p n t sc)
1545 | Static <- pstatic p
1546 = let (ns, ss) = fs sc in
1547 (namesIn [] ist t : ns, n : ss)
1548 | otherwise = let (ns, ss) = fs sc in
1549 (ns, ss)
1550 fs _ = ([], [])
1552 inOne n ns = length (filter id (map (elem n) ns)) == 1
1554 pos ns ss (PPi p n t sc)
1555 | elem n ss = do sc' <- pos ns ss sc
1556 spos <- get
1557 put (True : spos)
1558 return (PPi (p { pstatic = Static }) n t sc')
1559 | otherwise = do sc' <- pos ns ss sc
1560 spos <- get
1561 put (False : spos)
1562 return (PPi p n t sc')
1563 pos ns ss t = return t
1565-- for 6.12/7 compatibility
1566data EitherErr a b = LeftErr a | RightOK b
1568instance Monad (EitherErr a) where
1569 return = RightOK
1571 (LeftErr e) >>= k = LeftErr e
1572 RightOK v >>= k = k v
1574toEither (LeftErr e) = Left e
1575toEither (RightOK ho) = Right ho
1577-- syntactic match of a against b, returning pair of variables in a
1578-- and what they match. Returns the pair that failed if not a match.
1580matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1581matchClause = matchClause' False
1583matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1584matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1585 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1587 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1588 fullApp x = x
1590 match' x y = match (fullApp x) (fullApp y)
1591 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1592 | fi == txt "fromInteger" && b == txt "builtins",
1593 PConstant (I _) <- getTm x = match (getTm x) x'
1594 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1595 | fi == txt "fromInteger" && b == txt "builtins",
1596 PConstant (I _) <- getTm x = match (getTm x) x'
1597 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1598 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1599 match (PApp _ f args) (PApp _ f' args')
1600 | length args == length args'
1601 = do mf <- match' f f'
1602 ms <- zipWithM matchArg args args'
1603 return (mf ++ concat ms)
1604 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1605 match (PPatvar f n) xr = match (PRef f n) xr
1606 match xr (PPatvar f n) = match xr (PRef f n)
1607 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1608 match (PRef _ n) tm@(PRef _ n')
1609 | n == n' && not names &&
1610 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1611 || tm == Placeholder)
1612 = return [(n, tm)]
1613 -- if one namespace is missing, drop the other
1614 | n == n' || n == dropNS n' || dropNS n == n' = return []
1615 where dropNS (NS n _) = n
1616 dropNS n = n
1617 match (PRef _ n) tm
1618 | not names && (not (isConName n (tt_ctxt i) ||
1619 isFnName n (tt_ctxt i)) || tm == Placeholder)
1620 = return [(n, tm)]
1621 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1622 mr <- match' r r'
1623 return (ml ++ mr)
1624 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1625 = do ml <- match' l l'
1626 mr <- match' r r'
1627 return (ml ++ mr)
1628 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1629 mr <- match r r'
1630 return (ml ++ mr)
1631 match (PTyped l r) x = match l x
1632 match x (PTyped l r) = match x l
1633 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1634 mr <- match' r r'
1635 return (ml ++ mr)
1636 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1637 mt <- match' t t'
1638 mr <- match' r r'
1639 return (ml ++ mt ++ mr)
1640 match (PAlternative a as) (PAlternative a' as')
1641 = do ms <- zipWithM match' as as'
1642 return (concat ms)
1643 match a@(PAlternative _ as) b
1644 = do let ms = zipWith match' as (repeat b)
1645 case (rights (map toEither ms)) of
1646 (x: _) -> return x
1647 _ -> LeftErr (a, b)
1648 match (PCase _ _ _) _ = return [] -- lifted out
1649 match (PMetavar _) _ = return [] -- modified
1650 match (PInferRef _ _) _ = return [] -- modified
1651 match (PQuote _) _ = return []
1652 match (PProof _) _ = return []
1653 match (PTactics _) _ = return []
1654 match (PRefl _ _) (PRefl _ _) = return []
1655 match (PResolveTC _) (PResolveTC _) = return []
1656 match (PTrue _ _) (PTrue _ _) = return []
1657 match (PFalse _) (PFalse _) = return []
1658 match (PReturn _) (PReturn _) = return []
1659 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1660 ms <- match' s s'
1661 return (mt ++ ms)
1662 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1663 ms <- match' s s'
1664 return (mt ++ ms)
1665 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1666 mty <- match' ty ty'
1667 ms <- match' s s'
1668 return (mt ++ mty ++ ms)
1669 match (PHidden x) (PHidden y) = match' x y
1670 match (PUnifyLog x) y = match' x y
1671 match x (PUnifyLog y) = match' x y
1672 match (PNoImplicits x) y = match' x y
1673 match x (PNoImplicits y) = match' x y
1674 match Placeholder _ = return []
1675 match _ Placeholder = return []
1676 match (PResolveTC _) _ = return []
1677 match a b | a == b = return []
1678 | otherwise = LeftErr (a, b)
1680 checkRpts (RightOK ms) = check ms where
1681 check ((n,t):xs)
1682 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1683 then Left (t, t')
1684 else check xs
1685 check (_:xs) = check xs
1686 check [] = Right ms
1687 checkRpts (LeftErr x) = Left x
1689substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1690substMatches ms = substMatchesShadow ms []
1692substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1693substMatchesShadow [] shs t = t
1694substMatchesShadow ((n,tm):ns) shs t
1695 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1697substMatch :: Name -> PTerm -> PTerm -> PTerm
1698substMatch n = substMatchShadow n []
1700substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1701substMatchShadow n shs tm t = sm shs t where
1702 sm xs (PRef _ n') | n == n' = tm
1703 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1704 sm xs (PPi p x t sc)
1705 | x `elem` xs
1706 = let x' = nextName x in
1707 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1708 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1709 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1710 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1711 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1712 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1713 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1714 (fmap (sm xs) tm)
1715 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1716 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1717 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1718 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1719 sm xs (PHidden x) = PHidden (sm xs x)
1720 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1721 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1722 sm xs x = x
1724 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1725 fullApp x = x
1727shadow :: Name -> Name -> PTerm -> PTerm
1728shadow n n' t = sm t where
1729 sm (PRef fc x) | n == x = PRef fc n'
1730 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1731 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1732 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1733 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1734 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1735 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1736 sm (PEq f x y) = PEq f (sm x) (sm y)
1737 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1738 sm (PTyped x y) = PTyped (sm x) (sm y)
1739 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1740 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1741 sm (PAlternative a as) = PAlternative a (map sm as)
1742 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1743 sm (PProof ts) = PProof (map (fmap sm) ts)
1744 sm (PHidden x) = PHidden (sm x)
1745 sm (PUnifyLog x) = PUnifyLog (sm x)
1746 sm (PNoImplicits x) = PNoImplicits (sm x)
1747 sm x = x
1749-- Rename any binders which are repeated (so that we don't have to mess
1750-- about with shadowing anywhere else).
1752mkUniqueNames :: [Name] -> PTerm -> PTerm
1753mkUniqueNames env tm = evalState (mkUniq tm) env where
1754 inScope = boundNamesIn tm
1756 mkUniqA arg = do t' <- mkUniq (getTm arg)
1757 return (arg { getTm = t' })
1759 -- Initialise the unique name with the environment length (so we're not
1760 -- looking for too long...)
1761 initN (UN n) l = UN $ txt (str n ++ show l)
1762 initN (MN i s) l = MN (i+l) s
1763 initN n l = n
1765 -- FIXME: Probably ought to do this for completeness! It's fine as
1766 -- long as there are no bindings inside tactics though.
1767 mkUniqT tac = return tac
1769 mkUniq :: PTerm -> State [Name] PTerm
1770 mkUniq (PLam n ty sc)
1771 = do env <- get
1772 (n', sc') <-
1773 if n `elem` env
1774 then do let n' = uniqueName (initN n (length env))
1775 (env ++ inScope)
1776 return (n', shadow n n' sc)
1777 else return (n, sc)
1778 put (n' : env)
1779 ty' <- mkUniq ty
1780 sc'' <- mkUniq sc'
1781 return $! PLam n' ty' sc''
1782 mkUniq (PPi p n ty sc)
1783 = do env <- get
1784 (n', sc') <-
1785 if n `elem` env
1786 then do let n' = uniqueName (initN n (length env))
1787 (env ++ inScope)
1788 return (n', shadow n n' sc)
1789 else return (n, sc)
1790 put (n' : env)
1791 ty' <- mkUniq ty
1792 sc'' <- mkUniq sc'
1793 return $! PPi p n' ty' sc''
1794 mkUniq (PLet n ty val sc)
1795 = do env <- get
1796 (n', sc') <-
1797 if n `elem` env
1798 then do let n' = uniqueName (initN n (length env))
1799 (env ++ inScope)
1800 return (n', shadow n n' sc)
1801 else return (n, sc)
1802 put (n' : env)
1803 ty' <- mkUniq ty; val' <- mkUniq val
1804 sc'' <- mkUniq sc'
1805 return $! PLet n' ty' val' sc''
1806 mkUniq (PApp fc t args)
1807 = do t' <- mkUniq t
1808 args' <- mapM mkUniqA args
1809 return $! PApp fc t' args'
1810 mkUniq (PAppBind fc t args)
1811 = do t' <- mkUniq t
1812 args' <- mapM mkUniqA args
1813 return $! PAppBind fc t' args'
1814 mkUniq (PCase fc t alts)
1815 = do t' <- mkUniq t
1816 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1817 return (x', y')) alts
1818 return $! PCase fc t' alts'
1819 mkUniq (PPair fc p l r)
1820 = do l' <- mkUniq l; r' <- mkUniq r
1821 return $! PPair fc p l' r'
1822 mkUniq (PDPair fc p (PRef fc' n) t sc)
1823 | t /= Placeholder
1824 = do env <- get
1825 (n', sc') <- if n `elem` env
1826 then do let n' = uniqueName n (env ++ inScope)
1827 return (n', shadow n n' sc)
1828 else return (n, sc)
1829 put (n' : env)
1830 t' <- mkUniq t
1831 sc'' <- mkUniq sc'
1832 return $! PDPair fc p (PRef fc' n') t' sc''
1833 mkUniq (PDPair fc p l t r)
1834 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1835 return $! PDPair fc p l' t' r'
1836 mkUniq (PAlternative b as)
1837 = liftM (PAlternative b) (mapM mkUniq as)
1838 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1839 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1840 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1841 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1842 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1843 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1844 mkUniq t = return t