git.iko.soy/Idris-dev
on ee11033 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1851 lines 77 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 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 }
788 setColour' PostulateColour c t = t { postulateColour = c }
790logLvl :: Int -> String -> Idris ()
791logLvl l str = do i <- getIState
792 let lvl = opt_logLevel (idris_options i)
793 when (lvl >= l) $
794 case idris_outputmode i of
795 RawOutput -> do runIO $ putStrLn str
796 IdeSlave n ->
797 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
798 runIO $ putStrLn $ convSExp "log" good n
800cmdOptType :: Opt -> Idris Bool
801cmdOptType x = do i <- getIState
802 return $ x `elem` opt_cmdline (idris_options i)
804iLOG :: String -> Idris ()
805iLOG = logLvl 1
807noErrors :: Idris Bool
808noErrors = do i <- getIState
809 case errSpan i of
810 Nothing -> return True
811 _ -> return False
813setTypeCase :: Bool -> Idris ()
814setTypeCase t = do i <- getIState
815 let opts = idris_options i
816 let opt' = opts { opt_typecase = t }
817 putIState $ i { idris_options = opt' }
820-- Dealing with parameters
822expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
823 [Name] -> -- all names
824 [Name] -> -- names with no declaration
825 PTerm -> PTerm
826expandParams dec ps ns infs tm = en tm
827 where
828 -- if we shadow a name (say in a lambda binding) that is used in a call to
829 -- a lifted function, we need access to both names - once in the scope of the
830 -- binding and once to call the lifted functions. So we'll explicitly shadow
831 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
832 -- but we didn't...)
834 mkShadow (UN n) = MN 0 n
835 mkShadow (MN i n) = MN (i+1) n
836 mkShadow (NS x s) = NS (mkShadow x) s
838 en (PLam n t s)
839 | n `elem` (map fst ps ++ ns)
840 = let n' = mkShadow n in
841 PLam n' (en t) (en (shadow n n' s))
842 | otherwise = PLam n (en t) (en s)
843 en (PPi p n t s)
844 | n `elem` (map fst ps ++ ns)
845 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
846 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
847 | otherwise = PPi (enTacImp p) n (en t) (en s)
848 en (PLet n ty v s)
849 | n `elem` (map fst ps ++ ns)
850 = let n' = mkShadow n in
851 PLet n' (en ty) (en v) (en (shadow n n' s))
852 | otherwise = PLet n (en ty) (en v) (en s)
853 -- FIXME: Should only do this in a type signature!
854 en (PDPair f p (PRef f' n) t r)
855 | n `elem` (map fst ps ++ ns) && t /= Placeholder
856 = let n' = mkShadow n in
857 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
858 en (PEq f l r) = PEq f (en l) (en r)
859 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
860 en (PTyped l r) = PTyped (en l) (en r)
861 en (PPair f p l r) = PPair f p (en l) (en r)
862 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
863 en (PAlternative a as) = PAlternative a (map en as)
864 en (PHidden t) = PHidden (en t)
865 en (PUnifyLog t) = PUnifyLog (en t)
866 en (PDisamb ds t) = PDisamb ds (en t)
867 en (PNoImplicits t) = PNoImplicits (en t)
868 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
869 en (PProof ts) = PProof (map (fmap en) ts)
870 en (PTactics ts) = PTactics (map (fmap en) ts)
872 en (PQuote (Var n))
873 | n `nselem` ns = PQuote (Var (dec n))
874 en (PApp fc (PInferRef fc' n) as)
875 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
876 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
877 en (PApp fc (PRef fc' n) as)
878 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
879 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
880 | n `nselem` ns = PApp fc (PRef fc' (dec n))
881 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
882 en (PAppBind fc (PRef fc' n) as)
883 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
884 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
885 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
886 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
887 en (PRef fc n)
888 | n `elem` infs = PApp fc (PInferRef fc (dec n))
889 (map (pexp . (PRef fc)) (map fst ps))
890 | n `nselem` ns = PApp fc (PRef fc (dec n))
891 (map (pexp . (PRef fc)) (map fst ps))
892 en (PInferRef fc n)
893 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
894 (map (pexp . (PRef fc)) (map fst ps))
895 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
896 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
897 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
898 en t = t
900 nselem x [] = False
901 nselem x (y : xs) | nseq x y = True
902 | otherwise = nselem x xs
904 nseq x y = nsroot x == nsroot y
906 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
907 enTacImp other = other
909expandParamsD :: Bool -> -- True = RHS only
910 IState ->
911 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
912expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
913 = if n `elem` ns && (not rhsonly)
914 then -- trace (show (n, expandParams dec ps ns ty)) $
915 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
916 else --trace (show (n, expandParams dec ps ns ty)) $
917 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
918expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
919 = if n `elem` ns && (not rhsonly)
920 then -- trace (show (n, expandParams dec ps ns ty)) $
921 PPostulate doc syn fc o (dec n) (piBind ps
922 (expandParams dec ps ns [] ty))
923 else --trace (show (n, expandParams dec ps ns ty)) $
924 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
925expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
926 = let n' = if n `elem` ns then dec n else n in
927 PClauses fc opts n' (map expandParamsC cs)
928 where
929 expandParamsC (PClause fc n lhs ws rhs ds)
930 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
931 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
932 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
933 n' = if n `elem` ns then dec n else n
934 -- names bound on the lhs should not be expanded on the rhs
935 ns' = removeBound lhs ns in
936 PClause fc n' lhs'
937 (map (expandParams dec ps'' ns' []) ws)
938 (expandParams dec ps'' ns' [] rhs)
939 (map (expandParamsD True ist dec ps'' ns') ds)
940 expandParamsC (PWith fc n lhs ws wval ds)
941 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
942 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
943 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
944 n' = if n `elem` ns then dec n else n
945 ns' = removeBound lhs ns in
946 PWith fc n' lhs'
947 (map (expandParams dec ps'' ns' []) ws)
948 (expandParams dec ps'' ns' [] wval)
949 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
950 updateps yn nm [] = []
951 updateps yn nm (((a, t), i):as)
952 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
953 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
955 removeBound lhs ns = ns \\ nub (bnames lhs)
957 bnames (PRef _ n) = [n]
958 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
959 bnames (PPair _ _ l r) = bnames l ++ bnames r
960 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
961 bnames _ = []
963-- | Expands parameters defined in parameter and where blocks inside of declarations
964expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
965 = PData doc argDocs syn fc co (expandPData pd)
966 where
967 -- just do the type decl, leave constructors alone (parameters will be
968 -- added implicitly)
969 expandPData (PDatadecl n ty cons)
970 = if n `elem` ns
971 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
972 (map econ cons)
973 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
974 econ (doc, argDocs, n, t, fc, fs)
975 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
976expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
977 = if tn `elem` ns
978 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
979 opts cdoc (dec cn) conty
980 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
981 opts cdoc (dec cn) conty
982 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
983expandParamsD rhs ist dec ps ns (PParams f params pds)
984 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
985 (map (expandParamsD True ist dec ps ns) pds)
986-- (map (expandParamsD ist dec ps ns) pds)
987expandParamsD rhs ist dec ps ns (PMutual f pds)
988 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
989expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
990 = PClass doc info f
991 (map (expandParams dec ps ns []) cs)
992 n
993 (map (mapsnd (expandParams dec ps ns [])) params)
994 pDocs
995 (map (expandParamsD rhs ist dec ps ns) decls)
996expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
997 = PInstance info f
998 (map (expandParams dec ps ns []) cs)
999 n
1000 (map (expandParams dec ps ns []) params)
1001 (expandParams dec ps ns [] ty)
1002 cn
1003 (map (expandParamsD rhs ist dec ps ns) decls)
1004expandParamsD rhs ist dec ps ns d = d
1006mapsnd f (x, t) = (x, f t)
1008-- Calculate a priority for a type, for deciding elaboration order
1009-- * if it's just a type variable or concrete type, do it early (0)
1010-- * if there's only type variables and injective constructors, do it next (1)
1011-- * if there's a function type, next (2)
1012-- * finally, everything else (3)
1014getPriority :: IState -> PTerm -> Int
1015getPriority i tm = 1 -- pri tm
1016 where
1017 pri (PRef _ n) =
1018 case lookupP n (tt_ctxt i) of
1019 ((P (DCon _ _) _ _):_) -> 1
1020 ((P (TCon _ _) _ _):_) -> 1
1021 ((P Ref _ _):_) -> 1
1022 [] -> 0 -- must be locally bound, if it's not an error...
1023 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1024 pri (PTrue _ _) = 0
1025 pri (PFalse _) = 0
1026 pri (PRefl _ _) = 1
1027 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1028 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1029 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1030 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1031 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1032 pri (PTyped l r) = pri l
1033 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1034 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1035 pri (PAlternative a as) = maximum (map pri as)
1036 pri (PConstant _) = 0
1037 pri Placeholder = 1
1038 pri _ = 3
1041addStatics :: Name -> Term -> PTerm -> Idris ()
1042addStatics n tm ptm =
1043 do let (statics, dynamics) = initStatics tm ptm
1044 let stnames = nub $ concatMap freeArgNames (map snd statics)
1045 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1046 -- also get the arguments which are 'uniquely inferrable' from
1047 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1048 let statics' = nub $ map fst statics ++
1049 filter (\x -> not (elem x dnames)) stnames
1050 let stpos = staticList statics' tm
1051 i <- getIState
1052 when (not (null statics)) $
1053 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1054 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1055 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1056 addIBC (IBCStatic n)
1057 where
1058 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1059 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1060 if pstatic p == Static then ((n, ty) : static, dynamic)
1061 else if (not (searchArg p))
1062 then (static, (n, ty) : dynamic)
1063 else (static, dynamic)
1064 initStatics t pt = ([], [])
1066 freeArgNames (Bind n (Pi ty) sc)
1067 = nub $ freeArgNames ty
1068 freeArgNames tm = let (_, args) = unApply tm in
1069 concatMap freeNames args
1071 -- if a name appears in a type class or tactic implicit index, it doesn't
1072 -- affect its 'uniquely inferrable' from a static status since these are
1073 -- resolved by searching.
1074 searchArg (Constraint _ _) = True
1075 searchArg (TacImp _ _ _) = True
1076 searchArg _ = False
1078 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1079 staticList _ _ = []
1081-- Dealing with implicit arguments
1083-- Add constraint bindings from using block
1085addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1086addUsingConstraints syn fc t
1087 = do ist <- get
1088 let ns = namesIn [] ist t
1089 let cs = getConstraints t -- check declared constraints
1090 let addconsts = uconsts \\ cs
1091 -- if all names in the arguments of addconsts appear in ns,
1092 -- add the constraint implicitly
1093 return (doAdd addconsts ns t)
1094 where uconsts = filter uconst (using syn)
1095 uconst (UConstraint _ _) = True
1096 uconst _ = False
1098 doAdd [] _ t = t
1099 -- if all of args in ns, then add it
1100 doAdd (UConstraint c args : cs) ns t
1101 | all (\n -> elem n ns) args
1102 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1103 (mkConst c args) (doAdd cs ns t)
1104 | otherwise = doAdd cs ns t
1106 mkConst c args = PApp fc (PRef fc c)
1107 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1109 getConstraints (PPi (Constraint _ _) _ c sc)
1110 = getcapp c ++ getConstraints sc
1111 getConstraints (PPi _ _ c sc) = getConstraints sc
1112 getConstraints _ = []
1114 getcapp (PApp _ (PRef _ c) args)
1115 = do ns <- mapM getName args
1116 return (UConstraint c ns)
1117 getcapp _ = []
1119 getName (PExp _ _ _ (PRef _ n)) = return n
1120 getName _ = []
1122-- Add implicit Pi bindings for any names in the term which appear in an
1123-- argument position.
1125-- This has become a right mess already. Better redo it some time...
1127implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1128implicit info syn n ptm = implicit' info syn [] n ptm
1130implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1131implicit' info syn ignore n ptm
1132 = do i <- getIState
1133 let (tm', impdata) = implicitise syn ignore i ptm
1134 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1135-- let (tm'', spos) = findStatics i tm'
1136 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1137 addIBC (IBCImp n)
1138 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1139-- i <- get
1140-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1141 return tm'
1142 where
1143 -- Detect unknown names in default arguments and throw error if found.
1144 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1145 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1147 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1148 notFoundInDefault kns (PTacImplicit _ _ n script _)
1149 = do i <- getIState
1150 case notFound kns (namesIn [] i script) of
1151 Nothing -> return (n:kns)
1152 Just name -> throwError (NoSuchVariable name)
1153 notFoundInDefault kns p = return ((pname p):kns)
1155 notFound :: [Name] -> [Name] -> Maybe Name
1156 notFound kns [] = Nothing
1157 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1158 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1160implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1161implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1162 let (declimps, ns') = execState (imps True [] tm) ([], [])
1163 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1164 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1165 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1166 if null ns
1167 then (tm, reverse declimps)
1168 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1169 where
1170 uvars = map ipair (filter uimplicit (using syn))
1171 pvars = syn_params syn
1173 inUsing n = n `elem` map fst uvars
1175 ipair (UImplicit x y) = (x, y)
1176 uimplicit (UImplicit _ _) = True
1177 uimplicit _ = False
1179 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1180 | otherwise = x : dropAll xs ys
1181 dropAll [] ys = []
1183 -- Find names in argument position in a type, suitable for implicit
1184 -- binding
1185 -- Not the function position, but do everything else...
1186 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1187 implNamesIn uv t = namesIn uv ist t
1189 imps top env (PApp _ f as)
1190 = do (decls, ns) <- get
1191 let isn = concatMap (namesIn uvars ist) (map getTm as)
1192 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1193 imps top env (PPi (Imp l _ _) n ty sc)
1194 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1195 (decls , ns) <- get
1196 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1197 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1198 imps True (n:env) sc
1199 imps top env (PPi (Exp l _ _) n ty sc)
1200 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1201 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1202 _ -> [])
1203 (decls, ns) <- get -- ignore decls in HO types
1204 put (PExp (getPriority ist ty) l n Placeholder : decls,
1205 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1206 imps True (n:env) sc
1207 imps top env (PPi (Constraint l _) n ty sc)
1208 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1209 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1210 _ -> [])
1211 (decls, ns) <- get -- ignore decls in HO types
1212 put (PConstraint 10 l n Placeholder : decls,
1213 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1214 imps True (n:env) sc
1215 imps top env (PPi (TacImp l _ scr) n ty sc)
1216 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1217 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1218 _ -> [])
1219 (decls, ns) <- get -- ignore decls in HO types
1220 put (PTacImplicit 10 l n scr Placeholder : decls,
1221 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1222 imps True (n:env) sc
1223 imps top env (PEq _ l r)
1224 = do (decls, ns) <- get
1225 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1226 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1227 imps top env (PRewrite _ l r _)
1228 = do (decls, ns) <- get
1229 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1230 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1231 imps top env (PTyped l r)
1232 = imps top env l
1233 imps top env (PPair _ _ l r)
1234 = do (decls, ns) <- get
1235 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1236 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1237 imps top env (PDPair _ _ (PRef _ n) t r)
1238 = do (decls, ns) <- get
1239 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1240 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1241 imps top env (PDPair _ _ l t r)
1242 = do (decls, ns) <- get
1243 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1244 namesIn uvars ist r
1245 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1246 imps top env (PAlternative a as)
1247 = do (decls, ns) <- get
1248 let isn = concatMap (namesIn uvars ist) as
1249 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1250 imps top env (PLam n ty sc)
1251 = do imps False env ty
1252 imps False (n:env) sc
1253 imps top env (PHidden tm) = imps False env tm
1254 imps top env (PUnifyLog tm) = imps False env tm
1255 imps top env (PNoImplicits tm) = imps False env tm
1256 imps top env _ = return ()
1258 pibind using [] sc = sc
1259 pibind using (n:ns) sc
1260 = case lookup n using of
1261 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1262 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1263 (pibind using ns sc)
1265-- Add implicit arguments in function calls
1266addImplPat :: IState -> PTerm -> PTerm
1267addImplPat = addImpl' True [] []
1269addImplBound :: IState -> [Name] -> PTerm -> PTerm
1270addImplBound ist ns = addImpl' False ns [] ist
1272addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1273addImplBoundInf ist ns inf = addImpl' False ns inf ist
1275-- | Add the implicit arguments to applications in the term
1276addImpl :: IState -> PTerm -> PTerm
1277addImpl = addImpl' False [] []
1279-- TODO: in patterns, don't add implicits to function names guarded by constructors
1280-- and *not* inside a PHidden
1282addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1283addImpl' inpat env infns ist ptm
1284 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1285 where
1286 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1287 ai qq env ds (PRef fc f)
1288 | f `elem` infns = PInferRef fc f
1289 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1290 ai qq env ds (PHidden (PRef fc f))
1291 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1292 ai qq env ds (PEq fc l r)
1293 = let l' = ai qq env ds l
1294 r' = ai qq env ds r in
1295 PEq fc l' r'
1296 ai qq env ds (PRewrite fc l r g)
1297 = let l' = ai qq env ds l
1298 r' = ai qq env ds r
1299 g' = fmap (ai qq env ds) g in
1300 PRewrite fc l' r' g'
1301 ai qq env ds (PTyped l r)
1302 = let l' = ai qq env ds l
1303 r' = ai qq env ds r in
1304 PTyped l' r'
1305 ai qq env ds (PPair fc p l r)
1306 = let l' = ai qq env ds l
1307 r' = ai qq env ds r in
1308 PPair fc p l' r'
1309 ai qq env ds (PDPair fc p l t r)
1310 = let l' = ai qq env ds l
1311 t' = ai qq env ds t
1312 r' = ai qq env ds r in
1313 PDPair fc p l' t' r'
1314 ai qq env ds (PAlternative a as)
1315 = let as' = map (ai qq env ds) as in
1316 PAlternative a as'
1317 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1318 ai qq env ds (PApp fc (PInferRef _ f) as)
1319 = let as' = map (fmap (ai qq env ds)) as in
1320 PApp fc (PInferRef fc f) as'
1321 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1322 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1323 | not (f `elem` map fst env)
1324 = let as' = map (fmap (ai qq env ds)) as in
1325 handleErr $ aiFn inpat False qq ist fc f ds as'
1326 | Just (Just ty) <- lookup f env =
1327 let as' = map (fmap (ai qq env ds)) as
1328 arity = getPArity ty in
1329 mkPApp fc arity ftm as'
1330 ai qq env ds (PApp fc f as)
1331 = let f' = ai qq env ds f
1332 as' = map (fmap (ai qq env ds)) as in
1333 mkPApp fc 1 f' as'
1334 ai qq env ds (PCase fc c os)
1335 = let c' = ai qq env ds c in
1336 -- leave os alone, because they get lifted into a new pattern match
1337 -- definition which is passed through addImpl again with more scope
1338 -- information
1339 PCase fc c' os
1340 ai qq env ds (PLam n ty sc)
1341 = let ty' = ai qq env ds ty
1342 sc' = ai qq ((n, Just ty):env) ds sc in
1343 PLam n ty' sc'
1344 ai qq env ds (PLet n ty val sc)
1345 = let ty' = ai qq env ds ty
1346 val' = ai qq env ds val
1347 sc' = ai qq ((n, Just ty):env) ds sc in
1348 PLet n ty' val' sc'
1349 ai qq env ds (PPi p n ty sc)
1350 = let ty' = ai qq env ds ty
1351 sc' = ai qq ((n, Just ty):env) ds sc in
1352 PPi p n ty' sc'
1353 ai qq env ds (PGoal fc r n sc)
1354 = let r' = ai qq env ds r
1355 sc' = ai qq ((n, Nothing):env) ds sc in
1356 PGoal fc r' n sc'
1357 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1358 ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)
1359 ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)
1360 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1361 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1362 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1363 ai qq env ds (PQuasiquote tm) = PQuasiquote (ai True env ds tm)
1364 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1365 ai qq env ds tm = tm
1367 handleErr (Left err) = PElabError err
1368 handleErr (Right x) = x
1370-- if in a pattern, and there are no arguments, and there's no possible
1371-- names with zero explicit arguments, don't add implicits.
1373aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1374aiFn inpat True qq ist fc f ds []
1375 = case lookupDef f (tt_ctxt ist) of
1376 [] -> Right $ PPatvar fc f
1377 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1378 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1379 if (not (vname f) || tcname f
1380 || any (conCaf (tt_ctxt ist)) ialts)
1381-- any constructor alts || any allImp ialts))
1382 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1383 else Right $ PPatvar fc f
1384 where imp (PExp _ _ _ _) = False
1385 imp _ = True
1386-- allImp [] = False
1387 allImp xs = all imp xs
1388 constructor (TyDecl (DCon _ _) _) = True
1389 constructor _ = False
1391 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1393 vname (UN n) = True -- non qualified
1394 vname _ = False
1396aiFn inpat expat qq ist fc f ds as
1397 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1398aiFn inpat expat qq ist fc f ds as
1399 -- This is where namespaces get resolved by adding PAlternative
1400 = do let ns = lookupCtxtName f (idris_implicits ist)
1401 let nh = filter (\(n, _) -> notHidden n) ns
1402 let ns' = case trimAlts ds nh of
1403 [] -> nh
1404 x -> x
1405 case ns' of
1406 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1407 [] -> if f `elem` (map fst (idris_metavars ist))
1408 then Right $ PApp fc (PRef fc f) as
1409 else Right $ mkPApp fc (length as) (PRef fc f) as
1410 alts -> Right $
1411 PAlternative True $
1412 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1413 (insertImpl ns as)) alts
1414 where
1415 trimAlts [] alts = alts
1416 trimAlts ns alts
1417 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1419 nspace (NS _ s) = s
1420 nspace _ = []
1422 notHidden n = case getAccessibility n of
1423 Hidden -> False
1424 _ -> True
1426 getAccessibility n
1427 = case lookupDefAcc n False (tt_ctxt ist) of
1428 [(n,t)] -> t
1429 _ -> Public
1431 insertImpl :: [PArg] -> [PArg] -> [PArg]
1432 insertImpl ps as = insImpAcc M.empty ps as
1434 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1435 -> [PArg] -- parameters
1436 -> [PArg] -- arguments
1437 -> [PArg]
1438 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1439 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1440 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1441 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1442 insImpAcc pnas (PConstraint p l n ty : ps) given =
1443 let rtc = PResolveTC fc in
1444 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1445 insImpAcc pnas (PImp p _ l n ty : ps) given =
1446 case find n given [] of
1447 Just (tm, given') ->
1448 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1449 Nothing ->
1450 PImp p True l n Placeholder :
1451 insImpAcc (M.insert n Placeholder pnas) ps given
1452 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1453 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1454 case find n given [] of
1455 Just (tm, given') ->
1456 PTacImplicit p l n sc tm :
1457 insImpAcc (M.insert n tm pnas) ps given'
1458 Nothing ->
1459 if inpat
1460 then PTacImplicit p l n sc Placeholder :
1461 insImpAcc (M.insert n Placeholder pnas) ps given
1462 else PTacImplicit p l n sc sc :
1463 insImpAcc (M.insert n sc pnas) ps given
1464 insImpAcc _ expected [] = []
1465 insImpAcc _ _ given = given
1467 find n [] acc = Nothing
1468 find n (PImp _ _ _ n' t : gs) acc
1469 | n == n' = Just (t, reverse acc ++ gs)
1470 find n (PTacImplicit _ _ n' _ t : gs) acc
1471 | n == n' = Just (t, reverse acc ++ gs)
1472 find n (g : gs) acc = find n gs (g : acc)
1474-- replace non-linear occurrences with _
1475-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1476-- it is hard to get right!
1478stripLinear :: IState -> PTerm -> PTerm
1479stripLinear i tm = evalState (sl tm) [] where
1480 sl :: PTerm -> State [Name] PTerm
1481 sl (PRef fc f)
1482 | (_:_) <- lookupTy f (tt_ctxt i)
1483 = return $ PRef fc f
1484 | otherwise = do ns <- get
1485 if (f `elem` ns)
1486 then return Placeholder
1487 else do put (f : ns)
1488 return (PRef fc f)
1489 sl (PPatvar fc f)
1490 = do ns <- get
1491 if (f `elem` ns)
1492 then return Placeholder
1493 else do put (f : ns)
1494 return (PPatvar fc f)
1495 sl t@(PAlternative _ (a : as)) = do sl a
1496 return t
1497 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1498 args' <- mapM slA args
1499 return $ PApp fc fn args'
1500 where slA (PImp p m l n t) = do t' <- sl t
1501 return $ PImp p m l n t'
1502 slA (PExp p l n t) = do t' <- sl t
1503 return $ PExp p l n t'
1504 slA (PConstraint p l n t)
1505 = do t' <- sl t
1506 return $ PConstraint p l n t'
1507 slA (PTacImplicit p l n sc t)
1508 = do t' <- sl t
1509 return $ PTacImplicit p l n sc t'
1510 sl x = return x
1512-- Remove functions which aren't applied to anything, which must then
1513-- be resolved by unification. Assume names resolved and alternatives
1514-- filled in (so no ambiguity).
1516stripUnmatchable :: IState -> PTerm -> PTerm
1517stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1518 su :: PTerm -> PTerm
1519 su (PRef fc f)
1520 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1521 = Placeholder
1522 su (PApp fc fn args)
1523 = PApp fc fn (fmap (fmap su) args)
1524 su (PAlternative b alts)
1525 = let alts' = filter (/= Placeholder) (map su alts) in
1526 if null alts' then Placeholder
1527 else PAlternative b alts'
1528 su (PPair fc p l r) = PPair fc p (su l) (su r)
1529 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1530 su t = t
1531stripUnmatchable i tm = tm
1533mkPApp fc a f [] = f
1534mkPApp fc a f as = let rest = drop a as in
1535 appRest fc (PApp fc f (take a as)) rest
1536 where
1537 appRest fc f [] = f
1538 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1540-- Find 'static' argument positions
1541-- (the declared ones, plus any names in argument position in the declared
1542-- statics)
1543-- FIXME: It's possible that this really has to happen after elaboration
1545findStatics :: IState -> PTerm -> (PTerm, [Bool])
1546findStatics ist tm = trace (show tm) $
1547 let (ns, ss) = fs tm in
1548 runState (pos ns ss tm) []
1549 where fs (PPi p n t sc)
1550 | Static <- pstatic p
1551 = let (ns, ss) = fs sc in
1552 (namesIn [] ist t : ns, n : ss)
1553 | otherwise = let (ns, ss) = fs sc in
1554 (ns, ss)
1555 fs _ = ([], [])
1557 inOne n ns = length (filter id (map (elem n) ns)) == 1
1559 pos ns ss (PPi p n t sc)
1560 | elem n ss = do sc' <- pos ns ss sc
1561 spos <- get
1562 put (True : spos)
1563 return (PPi (p { pstatic = Static }) n t sc')
1564 | otherwise = do sc' <- pos ns ss sc
1565 spos <- get
1566 put (False : spos)
1567 return (PPi p n t sc')
1568 pos ns ss t = return t
1570-- for 6.12/7 compatibility
1571data EitherErr a b = LeftErr a | RightOK b
1573instance Monad (EitherErr a) where
1574 return = RightOK
1576 (LeftErr e) >>= k = LeftErr e
1577 RightOK v >>= k = k v
1579toEither (LeftErr e) = Left e
1580toEither (RightOK ho) = Right ho
1582-- syntactic match of a against b, returning pair of variables in a
1583-- and what they match. Returns the pair that failed if not a match.
1585matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1586matchClause = matchClause' False
1588matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1589matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1590 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1592 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1593 fullApp x = x
1595 match' x y = match (fullApp x) (fullApp y)
1596 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1597 | fi == txt "fromInteger" && b == txt "builtins",
1598 PConstant (I _) <- getTm x = match (getTm x) x'
1599 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1600 | fi == txt "fromInteger" && b == txt "builtins",
1601 PConstant (I _) <- getTm x = match (getTm x) x'
1602 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1603 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1604 match (PApp _ f args) (PApp _ f' args')
1605 | length args == length args'
1606 = do mf <- match' f f'
1607 ms <- zipWithM matchArg args args'
1608 return (mf ++ concat ms)
1609 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1610 match (PPatvar f n) xr = match (PRef f n) xr
1611 match xr (PPatvar f n) = match xr (PRef f n)
1612 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1613 match (PRef _ n) tm@(PRef _ n')
1614 | n == n' && not names &&
1615 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1616 || tm == Placeholder)
1617 = return [(n, tm)]
1618 -- if one namespace is missing, drop the other
1619 | n == n' || n == dropNS n' || dropNS n == n' = return []
1620 where dropNS (NS n _) = n
1621 dropNS n = n
1622 match (PRef _ n) tm
1623 | not names && (not (isConName n (tt_ctxt i) ||
1624 isFnName n (tt_ctxt i)) || tm == Placeholder)
1625 = return [(n, tm)]
1626 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1627 mr <- match' r r'
1628 return (ml ++ mr)
1629 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1630 = do ml <- match' l l'
1631 mr <- match' r r'
1632 return (ml ++ mr)
1633 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1634 mr <- match r r'
1635 return (ml ++ mr)
1636 match (PTyped l r) x = match l x
1637 match x (PTyped l r) = match x l
1638 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1639 mr <- match' r r'
1640 return (ml ++ mr)
1641 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1642 mt <- match' t t'
1643 mr <- match' r r'
1644 return (ml ++ mt ++ mr)
1645 match (PAlternative a as) (PAlternative a' as')
1646 = do ms <- zipWithM match' as as'
1647 return (concat ms)
1648 match a@(PAlternative _ as) b
1649 = do let ms = zipWith match' as (repeat b)
1650 case (rights (map toEither ms)) of
1651 (x: _) -> return x
1652 _ -> LeftErr (a, b)
1653 match (PCase _ _ _) _ = return [] -- lifted out
1654 match (PMetavar _) _ = return [] -- modified
1655 match (PInferRef _ _) _ = return [] -- modified
1656 match (PQuote _) _ = return []
1657 match (PProof _) _ = return []
1658 match (PTactics _) _ = return []
1659 match (PRefl _ _) (PRefl _ _) = return []
1660 match (PResolveTC _) (PResolveTC _) = return []
1661 match (PTrue _ _) (PTrue _ _) = return []
1662 match (PFalse _) (PFalse _) = return []
1663 match (PReturn _) (PReturn _) = return []
1664 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1665 ms <- match' s s'
1666 return (mt ++ ms)
1667 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1668 ms <- match' s s'
1669 return (mt ++ ms)
1670 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1671 mty <- match' ty ty'
1672 ms <- match' s s'
1673 return (mt ++ mty ++ ms)
1674 match (PHidden x) (PHidden y) = match' x y
1675 match (PUnifyLog x) y = match' x y
1676 match x (PUnifyLog y) = match' x y
1677 match (PNoImplicits x) y = match' x y
1678 match x (PNoImplicits y) = match' x y
1679 match Placeholder _ = return []
1680 match _ Placeholder = return []
1681 match (PResolveTC _) _ = return []
1682 match a b | a == b = return []
1683 | otherwise = LeftErr (a, b)
1685 checkRpts (RightOK ms) = check ms where
1686 check ((n,t):xs)
1687 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1688 then Left (t, t')
1689 else check xs
1690 check (_:xs) = check xs
1691 check [] = Right ms
1692 checkRpts (LeftErr x) = Left x
1694substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1695substMatches ms = substMatchesShadow ms []
1697substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1698substMatchesShadow [] shs t = t
1699substMatchesShadow ((n,tm):ns) shs t
1700 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1702substMatch :: Name -> PTerm -> PTerm -> PTerm
1703substMatch n = substMatchShadow n []
1705substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1706substMatchShadow n shs tm t = sm shs t where
1707 sm xs (PRef _ n') | n == n' = tm
1708 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1709 sm xs (PPi p x t sc)
1710 | x `elem` xs
1711 = let x' = nextName x in
1712 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1713 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1714 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1715 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1716 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1717 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1718 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1719 (fmap (sm xs) tm)
1720 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1721 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1722 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1723 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1724 sm xs (PHidden x) = PHidden (sm xs x)
1725 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1726 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1727 sm xs x = x
1729 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1730 fullApp x = x
1732shadow :: Name -> Name -> PTerm -> PTerm
1733shadow n n' t = sm t where
1734 sm (PRef fc x) | n == x = PRef fc n'
1735 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1736 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1737 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1738 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1739 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1740 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1741 sm (PEq f x y) = PEq f (sm x) (sm y)
1742 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1743 sm (PTyped x y) = PTyped (sm x) (sm y)
1744 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1745 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1746 sm (PAlternative a as) = PAlternative a (map sm as)
1747 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1748 sm (PProof ts) = PProof (map (fmap sm) ts)
1749 sm (PHidden x) = PHidden (sm x)
1750 sm (PUnifyLog x) = PUnifyLog (sm x)
1751 sm (PNoImplicits x) = PNoImplicits (sm x)
1752 sm x = x
1754-- Rename any binders which are repeated (so that we don't have to mess
1755-- about with shadowing anywhere else).
1757mkUniqueNames :: [Name] -> PTerm -> PTerm
1758mkUniqueNames env tm = evalState (mkUniq tm) env where
1759 inScope = boundNamesIn tm
1761 mkUniqA arg = do t' <- mkUniq (getTm arg)
1762 return (arg { getTm = t' })
1764 -- Initialise the unique name with the environment length (so we're not
1765 -- looking for too long...)
1766 initN (UN n) l = UN $ txt (str n ++ show l)
1767 initN (MN i s) l = MN (i+l) s
1768 initN n l = n
1770 -- FIXME: Probably ought to do this for completeness! It's fine as
1771 -- long as there are no bindings inside tactics though.
1772 mkUniqT tac = return tac
1774 mkUniq :: PTerm -> State [Name] PTerm
1775 mkUniq (PLam n ty sc)
1776 = do env <- get
1777 (n', sc') <-
1778 if n `elem` env
1779 then do let n' = uniqueName (initN n (length env))
1780 (env ++ inScope)
1781 return (n', shadow n n' sc)
1782 else return (n, sc)
1783 put (n' : env)
1784 ty' <- mkUniq ty
1785 sc'' <- mkUniq sc'
1786 return $! PLam n' ty' sc''
1787 mkUniq (PPi p n ty sc)
1788 = do env <- get
1789 (n', sc') <-
1790 if n `elem` env
1791 then do let n' = uniqueName (initN n (length env))
1792 (env ++ inScope)
1793 return (n', shadow n n' sc)
1794 else return (n, sc)
1795 put (n' : env)
1796 ty' <- mkUniq ty
1797 sc'' <- mkUniq sc'
1798 return $! PPi p n' ty' sc''
1799 mkUniq (PLet n ty val sc)
1800 = do env <- get
1801 (n', sc') <-
1802 if n `elem` env
1803 then do let n' = uniqueName (initN n (length env))
1804 (env ++ inScope)
1805 return (n', shadow n n' sc)
1806 else return (n, sc)
1807 put (n' : env)
1808 ty' <- mkUniq ty; val' <- mkUniq val
1809 sc'' <- mkUniq sc'
1810 return $! PLet n' ty' val' sc''
1811 mkUniq (PApp fc t args)
1812 = do t' <- mkUniq t
1813 args' <- mapM mkUniqA args
1814 return $! PApp fc t' args'
1815 mkUniq (PAppBind fc t args)
1816 = do t' <- mkUniq t
1817 args' <- mapM mkUniqA args
1818 return $! PAppBind fc t' args'
1819 mkUniq (PCase fc t alts)
1820 = do t' <- mkUniq t
1821 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1822 return (x', y')) alts
1823 return $! PCase fc t' alts'
1824 mkUniq (PPair fc p l r)
1825 = do l' <- mkUniq l; r' <- mkUniq r
1826 return $! PPair fc p l' r'
1827 mkUniq (PDPair fc p (PRef fc' n) t sc)
1828 | t /= Placeholder
1829 = do env <- get
1830 (n', sc') <- if n `elem` env
1831 then do let n' = uniqueName n (env ++ inScope)
1832 return (n', shadow n n' sc)
1833 else return (n, sc)
1834 put (n' : env)
1835 t' <- mkUniq t
1836 sc'' <- mkUniq sc'
1837 return $! PDPair fc p (PRef fc' n') t' sc''
1838 mkUniq (PDPair fc p l t r)
1839 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1840 return $! PDPair fc p l' t' r'
1841 mkUniq (PAlternative b as)
1842 = liftM (PAlternative b) (mapM mkUniq as)
1843 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1844 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1845 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1846 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1847 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1848 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1849 mkUniq t = return t