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