git.iko.soy/Idris-dev
on dfa272d help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1849 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) = PQuasiquote (ai True env ds tm)
1362 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1363 ai qq env ds tm = tm
1365 handleErr (Left err) = PElabError err
1366 handleErr (Right x) = x
1368-- if in a pattern, and there are no arguments, and there's no possible
1369-- names with zero explicit arguments, don't add implicits.
1371aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1372aiFn inpat True qq ist fc f ds []
1373 = case lookupDef f (tt_ctxt ist) of
1374 [] -> Right $ PPatvar fc f
1375 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1376 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1377 if (not (vname f) || tcname f
1378 || any (conCaf (tt_ctxt ist)) ialts)
1379-- any constructor alts || any allImp ialts))
1380 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1381 else Right $ PPatvar fc f
1382 where imp (PExp _ _ _ _) = False
1383 imp _ = True
1384-- allImp [] = False
1385 allImp xs = all imp xs
1386 constructor (TyDecl (DCon _ _) _) = True
1387 constructor _ = False
1389 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1391 vname (UN n) = True -- non qualified
1392 vname _ = False
1394aiFn inpat expat qq ist fc f ds as
1395 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1396aiFn inpat expat qq ist fc f ds as
1397 -- This is where namespaces get resolved by adding PAlternative
1398 = do let ns = lookupCtxtName f (idris_implicits ist)
1399 let nh = filter (\(n, _) -> notHidden n) ns
1400 let ns' = case trimAlts ds nh of
1401 [] -> nh
1402 x -> x
1403 case ns' of
1404 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1405 [] -> if f `elem` (map fst (idris_metavars ist))
1406 then Right $ PApp fc (PRef fc f) as
1407 else Right $ mkPApp fc (length as) (PRef fc f) as
1408 alts -> Right $
1409 PAlternative True $
1410 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1411 (insertImpl ns as)) alts
1412 where
1413 trimAlts [] alts = alts
1414 trimAlts ns alts
1415 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1417 nspace (NS _ s) = s
1418 nspace _ = []
1420 notHidden n = case getAccessibility n of
1421 Hidden -> False
1422 _ -> True
1424 getAccessibility n
1425 = case lookupDefAcc n False (tt_ctxt ist) of
1426 [(n,t)] -> t
1427 _ -> Public
1429 insertImpl :: [PArg] -> [PArg] -> [PArg]
1430 insertImpl ps as = insImpAcc M.empty ps as
1432 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1433 -> [PArg] -- parameters
1434 -> [PArg] -- arguments
1435 -> [PArg]
1436 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1437 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1438 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1439 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1440 insImpAcc pnas (PConstraint p l n ty : ps) given =
1441 let rtc = PResolveTC fc in
1442 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1443 insImpAcc pnas (PImp p _ l n ty : ps) given =
1444 case find n given [] of
1445 Just (tm, given') ->
1446 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1447 Nothing ->
1448 PImp p True l n Placeholder :
1449 insImpAcc (M.insert n Placeholder pnas) ps given
1450 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1451 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1452 case find n given [] of
1453 Just (tm, given') ->
1454 PTacImplicit p l n sc tm :
1455 insImpAcc (M.insert n tm pnas) ps given'
1456 Nothing ->
1457 if inpat
1458 then PTacImplicit p l n sc Placeholder :
1459 insImpAcc (M.insert n Placeholder pnas) ps given
1460 else PTacImplicit p l n sc sc :
1461 insImpAcc (M.insert n sc pnas) ps given
1462 insImpAcc _ expected [] = []
1463 insImpAcc _ _ given = given
1465 find n [] acc = Nothing
1466 find n (PImp _ _ _ n' t : gs) acc
1467 | n == n' = Just (t, reverse acc ++ gs)
1468 find n (PTacImplicit _ _ n' _ t : gs) acc
1469 | n == n' = Just (t, reverse acc ++ gs)
1470 find n (g : gs) acc = find n gs (g : acc)
1472-- replace non-linear occurrences with _
1473-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1474-- it is hard to get right!
1476stripLinear :: IState -> PTerm -> PTerm
1477stripLinear i tm = evalState (sl tm) [] where
1478 sl :: PTerm -> State [Name] PTerm
1479 sl (PRef fc f)
1480 | (_:_) <- lookupTy f (tt_ctxt i)
1481 = return $ PRef fc f
1482 | otherwise = do ns <- get
1483 if (f `elem` ns)
1484 then return Placeholder
1485 else do put (f : ns)
1486 return (PRef fc f)
1487 sl (PPatvar fc f)
1488 = do ns <- get
1489 if (f `elem` ns)
1490 then return Placeholder
1491 else do put (f : ns)
1492 return (PPatvar fc f)
1493 sl t@(PAlternative _ (a : as)) = do sl a
1494 return t
1495 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1496 args' <- mapM slA args
1497 return $ PApp fc fn args'
1498 where slA (PImp p m l n t) = do t' <- sl t
1499 return $ PImp p m l n t'
1500 slA (PExp p l n t) = do t' <- sl t
1501 return $ PExp p l n t'
1502 slA (PConstraint p l n t)
1503 = do t' <- sl t
1504 return $ PConstraint p l n t'
1505 slA (PTacImplicit p l n sc t)
1506 = do t' <- sl t
1507 return $ PTacImplicit p l n sc t'
1508 sl x = return x
1510-- Remove functions which aren't applied to anything, which must then
1511-- be resolved by unification. Assume names resolved and alternatives
1512-- filled in (so no ambiguity).
1514stripUnmatchable :: IState -> PTerm -> PTerm
1515stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1516 su :: PTerm -> PTerm
1517 su (PRef fc f)
1518 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1519 = Placeholder
1520 su (PApp fc fn args)
1521 = PApp fc fn (fmap (fmap su) args)
1522 su (PAlternative b alts)
1523 = let alts' = filter (/= Placeholder) (map su alts) in
1524 if null alts' then Placeholder
1525 else PAlternative b alts'
1526 su (PPair fc p l r) = PPair fc p (su l) (su r)
1527 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1528 su t = t
1529stripUnmatchable i tm = tm
1531mkPApp fc a f [] = f
1532mkPApp fc a f as = let rest = drop a as in
1533 appRest fc (PApp fc f (take a as)) rest
1534 where
1535 appRest fc f [] = f
1536 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1538-- Find 'static' argument positions
1539-- (the declared ones, plus any names in argument position in the declared
1540-- statics)
1541-- FIXME: It's possible that this really has to happen after elaboration
1543findStatics :: IState -> PTerm -> (PTerm, [Bool])
1544findStatics ist tm = trace (show tm) $
1545 let (ns, ss) = fs tm in
1546 runState (pos ns ss tm) []
1547 where fs (PPi p n t sc)
1548 | Static <- pstatic p
1549 = let (ns, ss) = fs sc in
1550 (namesIn [] ist t : ns, n : ss)
1551 | otherwise = let (ns, ss) = fs sc in
1552 (ns, ss)
1553 fs _ = ([], [])
1555 inOne n ns = length (filter id (map (elem n) ns)) == 1
1557 pos ns ss (PPi p n t sc)
1558 | elem n ss = do sc' <- pos ns ss sc
1559 spos <- get
1560 put (True : spos)
1561 return (PPi (p { pstatic = Static }) n t sc')
1562 | otherwise = do sc' <- pos ns ss sc
1563 spos <- get
1564 put (False : spos)
1565 return (PPi p n t sc')
1566 pos ns ss t = return t
1568-- for 6.12/7 compatibility
1569data EitherErr a b = LeftErr a | RightOK b
1571instance Monad (EitherErr a) where
1572 return = RightOK
1574 (LeftErr e) >>= k = LeftErr e
1575 RightOK v >>= k = k v
1577toEither (LeftErr e) = Left e
1578toEither (RightOK ho) = Right ho
1580-- syntactic match of a against b, returning pair of variables in a
1581-- and what they match. Returns the pair that failed if not a match.
1583matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1584matchClause = matchClause' False
1586matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1587matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1588 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1590 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1591 fullApp x = x
1593 match' x y = match (fullApp x) (fullApp y)
1594 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1595 | fi == txt "fromInteger" && b == txt "builtins",
1596 PConstant (I _) <- getTm x = match (getTm x) x'
1597 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1598 | fi == txt "fromInteger" && b == txt "builtins",
1599 PConstant (I _) <- getTm x = match (getTm x) x'
1600 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1601 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1602 match (PApp _ f args) (PApp _ f' args')
1603 | length args == length args'
1604 = do mf <- match' f f'
1605 ms <- zipWithM matchArg args args'
1606 return (mf ++ concat ms)
1607 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1608 match (PPatvar f n) xr = match (PRef f n) xr
1609 match xr (PPatvar f n) = match xr (PRef f n)
1610 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1611 match (PRef _ n) tm@(PRef _ n')
1612 | n == n' && not names &&
1613 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1614 || tm == Placeholder)
1615 = return [(n, tm)]
1616 -- if one namespace is missing, drop the other
1617 | n == n' || n == dropNS n' || dropNS n == n' = return []
1618 where dropNS (NS n _) = n
1619 dropNS n = n
1620 match (PRef _ n) tm
1621 | not names && (not (isConName n (tt_ctxt i) ||
1622 isFnName n (tt_ctxt i)) || tm == Placeholder)
1623 = return [(n, tm)]
1624 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1625 mr <- match' r r'
1626 return (ml ++ mr)
1627 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1628 = do ml <- match' l l'
1629 mr <- match' r r'
1630 return (ml ++ mr)
1631 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1632 mr <- match r r'
1633 return (ml ++ mr)
1634 match (PTyped l r) x = match l x
1635 match x (PTyped l r) = match x l
1636 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1637 mr <- match' r r'
1638 return (ml ++ mr)
1639 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1640 mt <- match' t t'
1641 mr <- match' r r'
1642 return (ml ++ mt ++ mr)
1643 match (PAlternative a as) (PAlternative a' as')
1644 = do ms <- zipWithM match' as as'
1645 return (concat ms)
1646 match a@(PAlternative _ as) b
1647 = do let ms = zipWith match' as (repeat b)
1648 case (rights (map toEither ms)) of
1649 (x: _) -> return x
1650 _ -> LeftErr (a, b)
1651 match (PCase _ _ _) _ = return [] -- lifted out
1652 match (PMetavar _) _ = return [] -- modified
1653 match (PInferRef _ _) _ = return [] -- modified
1654 match (PQuote _) _ = return []
1655 match (PProof _) _ = return []
1656 match (PTactics _) _ = return []
1657 match (PRefl _ _) (PRefl _ _) = return []
1658 match (PResolveTC _) (PResolveTC _) = return []
1659 match (PTrue _ _) (PTrue _ _) = return []
1660 match (PFalse _) (PFalse _) = return []
1661 match (PReturn _) (PReturn _) = return []
1662 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1663 ms <- match' s s'
1664 return (mt ++ ms)
1665 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1666 ms <- match' s s'
1667 return (mt ++ ms)
1668 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1669 mty <- match' ty ty'
1670 ms <- match' s s'
1671 return (mt ++ mty ++ ms)
1672 match (PHidden x) (PHidden y) = match' x y
1673 match (PUnifyLog x) y = match' x y
1674 match x (PUnifyLog y) = match' x y
1675 match (PNoImplicits x) y = match' x y
1676 match x (PNoImplicits y) = match' x y
1677 match Placeholder _ = return []
1678 match _ Placeholder = return []
1679 match (PResolveTC _) _ = return []
1680 match a b | a == b = return []
1681 | otherwise = LeftErr (a, b)
1683 checkRpts (RightOK ms) = check ms where
1684 check ((n,t):xs)
1685 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1686 then Left (t, t')
1687 else check xs
1688 check (_:xs) = check xs
1689 check [] = Right ms
1690 checkRpts (LeftErr x) = Left x
1692substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1693substMatches ms = substMatchesShadow ms []
1695substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1696substMatchesShadow [] shs t = t
1697substMatchesShadow ((n,tm):ns) shs t
1698 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1700substMatch :: Name -> PTerm -> PTerm -> PTerm
1701substMatch n = substMatchShadow n []
1703substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1704substMatchShadow n shs tm t = sm shs t where
1705 sm xs (PRef _ n') | n == n' = tm
1706 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1707 sm xs (PPi p x t sc)
1708 | x `elem` xs
1709 = let x' = nextName x in
1710 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1711 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1712 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1713 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1714 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1715 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1716 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1717 (fmap (sm xs) tm)
1718 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1719 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1720 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1721 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1722 sm xs (PHidden x) = PHidden (sm xs x)
1723 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1724 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1725 sm xs x = x
1727 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1728 fullApp x = x
1730shadow :: Name -> Name -> PTerm -> PTerm
1731shadow n n' t = sm t where
1732 sm (PRef fc x) | n == x = PRef fc n'
1733 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1734 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1735 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1736 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1737 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1738 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1739 sm (PEq f x y) = PEq f (sm x) (sm y)
1740 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1741 sm (PTyped x y) = PTyped (sm x) (sm y)
1742 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1743 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1744 sm (PAlternative a as) = PAlternative a (map sm as)
1745 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1746 sm (PProof ts) = PProof (map (fmap sm) ts)
1747 sm (PHidden x) = PHidden (sm x)
1748 sm (PUnifyLog x) = PUnifyLog (sm x)
1749 sm (PNoImplicits x) = PNoImplicits (sm x)
1750 sm x = x
1752-- Rename any binders which are repeated (so that we don't have to mess
1753-- about with shadowing anywhere else).
1755mkUniqueNames :: [Name] -> PTerm -> PTerm
1756mkUniqueNames env tm = evalState (mkUniq tm) env where
1757 inScope = boundNamesIn tm
1759 mkUniqA arg = do t' <- mkUniq (getTm arg)
1760 return (arg { getTm = t' })
1762 -- Initialise the unique name with the environment length (so we're not
1763 -- looking for too long...)
1764 initN (UN n) l = UN $ txt (str n ++ show l)
1765 initN (MN i s) l = MN (i+l) s
1766 initN n l = n
1768 -- FIXME: Probably ought to do this for completeness! It's fine as
1769 -- long as there are no bindings inside tactics though.
1770 mkUniqT tac = return tac
1772 mkUniq :: PTerm -> State [Name] PTerm
1773 mkUniq (PLam n ty sc)
1774 = do env <- get
1775 (n', sc') <-
1776 if n `elem` env
1777 then do let n' = uniqueName (initN n (length env))
1778 (env ++ inScope)
1779 return (n', shadow n n' sc)
1780 else return (n, sc)
1781 put (n' : env)
1782 ty' <- mkUniq ty
1783 sc'' <- mkUniq sc'
1784 return $! PLam n' ty' sc''
1785 mkUniq (PPi p n ty sc)
1786 = do env <- get
1787 (n', sc') <-
1788 if n `elem` env
1789 then do let n' = uniqueName (initN n (length env))
1790 (env ++ inScope)
1791 return (n', shadow n n' sc)
1792 else return (n, sc)
1793 put (n' : env)
1794 ty' <- mkUniq ty
1795 sc'' <- mkUniq sc'
1796 return $! PPi p n' ty' sc''
1797 mkUniq (PLet n ty val sc)
1798 = do env <- get
1799 (n', sc') <-
1800 if n `elem` env
1801 then do let n' = uniqueName (initN n (length env))
1802 (env ++ inScope)
1803 return (n', shadow n n' sc)
1804 else return (n, sc)
1805 put (n' : env)
1806 ty' <- mkUniq ty; val' <- mkUniq val
1807 sc'' <- mkUniq sc'
1808 return $! PLet n' ty' val' sc''
1809 mkUniq (PApp fc t args)
1810 = do t' <- mkUniq t
1811 args' <- mapM mkUniqA args
1812 return $! PApp fc t' args'
1813 mkUniq (PAppBind fc t args)
1814 = do t' <- mkUniq t
1815 args' <- mapM mkUniqA args
1816 return $! PAppBind fc t' args'
1817 mkUniq (PCase fc t alts)
1818 = do t' <- mkUniq t
1819 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1820 return (x', y')) alts
1821 return $! PCase fc t' alts'
1822 mkUniq (PPair fc p l r)
1823 = do l' <- mkUniq l; r' <- mkUniq r
1824 return $! PPair fc p l' r'
1825 mkUniq (PDPair fc p (PRef fc' n) t sc)
1826 | t /= Placeholder
1827 = do env <- get
1828 (n', sc') <- if n `elem` env
1829 then do let n' = uniqueName n (env ++ inScope)
1830 return (n', shadow n n' sc)
1831 else return (n, sc)
1832 put (n' : env)
1833 t' <- mkUniq t
1834 sc'' <- mkUniq sc'
1835 return $! PDPair fc p (PRef fc' n') t' sc''
1836 mkUniq (PDPair fc p l t r)
1837 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1838 return $! PDPair fc p l' t' r'
1839 mkUniq (PAlternative b as)
1840 = liftM (PAlternative b) (mapM mkUniq as)
1841 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1842 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1843 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1844 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1845 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1846 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1847 mkUniq t = return t