git.iko.soy/Idris-dev
on af6eaeb help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1897 lines 79 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.IdeSlave
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.State
22import Control.Monad.Error(throwError)
24import Data.List
25import Data.Char
26import qualified Data.Text as T
27import Data.Either
28import qualified Data.Map as M
29import Data.Maybe
30import qualified Data.Set as S
31import Data.Word (Word)
33import Debug.Trace
35import Control.Monad.Error (throwError, catchError)
36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
38import Util.Pretty
39import Util.ScreenSize
40import Util.System
42getContext :: Idris Context
43getContext = do i <- getIState; return (tt_ctxt i)
45forCodegen :: Codegen -> [(Codegen, a)] -> [a]
46forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
48getObjectFiles :: Codegen -> Idris [FilePath]
49getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
51addObjectFile :: Codegen -> FilePath -> Idris ()
52addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
54getLibs :: Codegen -> Idris [String]
55getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
57addLib :: Codegen -> String -> Idris ()
58addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
60getFlags :: Codegen -> Idris [String]
61getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
63addFlag :: Codegen -> String -> Idris ()
64addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
66addDyLib :: [String] -> Idris (Either DynamicLib String)
67addDyLib libs = do i <- getIState
68 let ls = idris_dynamic_libs i
69 let importdirs = opt_importdirs (idris_options i)
70 case mapMaybe (findDyLib ls) libs of
71 x:_ -> return (Left x)
72 [] -> do
73 handle <- lift . lift .
74 mapM (\l -> catchIO (tryLoadLib importdirs l)
75 (\_ -> return Nothing)) $ libs
76 case msum handle of
77 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
78 concat (intersperse "," libs) ++ "\"")
79 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
80 return (Left x)
81 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
82 findDyLib [] l = Nothing
83 findDyLib (lib:libs) l | l == lib_name lib = Just lib
84 | otherwise = findDyLib libs l
87addHdr :: Codegen -> String -> Idris ()
88addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
90addLangExt :: LanguageExt -> Idris ()
91addLangExt TypeProviders = do i <- getIState
92 putIState $ i {
93 idris_language_extensions = TypeProviders : idris_language_extensions i
94 }
95addLangExt ErrorReflection = do i <- getIState
96 putIState $ i {
97 idris_language_extensions = ErrorReflection : idris_language_extensions i
98 }
100addTrans :: (Term, Term) -> Idris ()
101addTrans t = do i <- getIState
102 putIState $ i { idris_transforms = t : idris_transforms i }
104addErrRev :: (Term, Term) -> Idris ()
105addErrRev t = do i <- getIState
106 putIState $ i { idris_errRev = t : idris_errRev i }
108totcheck :: (FC, Name) -> Idris ()
109totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
111defer_totcheck :: (FC, Name) -> Idris ()
112defer_totcheck n
113 = do i <- getIState;
114 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
116clear_totcheck :: Idris ()
117clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
119setFlags :: Name -> [FnOpt] -> Idris ()
120setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
122setAccessibility :: Name -> Accessibility -> Idris ()
123setAccessibility n a
124 = do i <- getIState
125 let ctxt = setAccess n a (tt_ctxt i)
126 putIState $ i { tt_ctxt = ctxt }
128setTotality :: Name -> Totality -> Idris ()
129setTotality n a
130 = do i <- getIState
131 let ctxt = setTotal n a (tt_ctxt i)
132 putIState $ i { tt_ctxt = ctxt }
134getTotality :: Name -> Idris Totality
135getTotality n
136 = do i <- getIState
137 case lookupTotal n (tt_ctxt i) of
138 [t] -> return t
139 _ -> return (Total [])
141-- Get coercions which might return the required type
142getCoercionsTo :: IState -> Type -> [Name]
143getCoercionsTo i ty =
144 let cs = idris_coercions i
145 (fn,_) = unApply (getRetTy ty) in
146 findCoercions fn cs
147 where findCoercions t [] = []
148 findCoercions t (n : ns) =
149 let ps = case lookupTy n (tt_ctxt i) of
150 [ty'] -> case unApply (getRetTy ty') of
151 (t', _) ->
152 if t == t' then [n] else []
153 _ -> [] in
154 ps ++ findCoercions t ns
156addToCG :: Name -> CGInfo -> Idris ()
157addToCG n cg
158 = do i <- getIState
159 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
161addTyInferred :: Name -> Idris ()
162addTyInferred n
163 = do i <- getIState
164 putIState $ i { idris_tyinfodata =
165 addDef n TIPartial (idris_tyinfodata i) }
167addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
168addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
169 mapM_ addConstraint ts
170 return ()
171 where addConstraint (x, y) = findMVApps x y
173 findMVApps x y
174 = do let (fx, argsx) = unApply x
175 let (fy, argsy) = unApply y
176 if (not (fx == fy))
177 then do
178 tryAddMV fx y
179 tryAddMV fy x
180 else mapM_ addConstraint (zip argsx argsy)
182 tryAddMV (P _ mv _) y =
183 do ist <- get
184 case lookup mv (idris_metavars ist) of
185 Just _ -> addConstraintRule mv y
186 _ -> return ()
187 tryAddMV _ _ = return ()
189 addConstraintRule :: Name -> Term -> Idris ()
190 addConstraintRule n t
191 = do ist <- get
192 logLvl 1 $ "TI constraint: " ++ show (n, t)
193 case lookupCtxt n (idris_tyinfodata ist) of
194 [TISolution ts] ->
195 do mapM_ (checkConsistent t) ts
196 let ti' = addDef n (TISolution (t : ts))
197 (idris_tyinfodata ist)
198 put $ ist { idris_tyinfodata = ti' }
199 _ ->
200 do let ti' = addDef n (TISolution [t])
201 (idris_tyinfodata ist)
202 put $ ist { idris_tyinfodata = ti' }
204 -- Check a solution is consistent with previous solutions
205 -- Meaning: If heads are both data types, they had better be the
206 -- same.
207 checkConsistent :: Term -> Term -> Idris ()
208 checkConsistent x y =
209 do let (fx, _) = unApply x
210 let (fy, _) = unApply y
211 case (fx, fy) of
212 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
213 (P (TCon _ _) n _, Constant _) -> errWhen True
214 (Constant _, P (TCon _ _) n' _) -> errWhen True
215 (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)
216 _ -> return ()
218 where errWhen True
219 = throwError (At fc
220 (CantUnify False x y (Msg "") [] 0))
221 errWhen False = return ()
223isTyInferred :: Name -> Idris Bool
224isTyInferred n
225 = do i <- getIState
226 case lookupCtxt n (idris_tyinfodata i) of
227 [TIPartial] -> return True
228 _ -> return False
230-- | Adds error handlers for a particular function and argument. If names are
231-- ambiguous, all matching handlers are updated.
232addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
233addFunctionErrorHandlers f arg hs =
234 do i <- getIState
235 let oldHandlers = idris_function_errorhandlers i
236 let newHandlers = flip (addDef f) oldHandlers $
237 case lookupCtxtExact f oldHandlers of
238 Nothing -> M.singleton arg (S.fromList hs)
239 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
240 -- will always be one of those two, thus no extra case
241 putIState $ i { idris_function_errorhandlers = newHandlers }
243getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
244getFunctionErrorHandlers f arg = do i <- getIState
245 return . maybe [] S.toList $
246 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
249-- Trace all the names in a call graph starting at the given name
250getAllNames :: Name -> Idris [Name]
251getAllNames n = allNames [] n
253allNames :: [Name] -> Name -> Idris [Name]
254allNames ns n | n `elem` ns = return []
255allNames ns n = do i <- getIState
256 case lookupCtxtExact n (idris_callgraph i) of
257 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
258 return (nub (n : concat more))
259 _ -> return [n]
261addCoercion :: Name -> Idris ()
262addCoercion n = do i <- getIState
263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
265addDocStr :: Name -> String -> [(Name, String)] -> Idris ()
266addDocStr n doc args
267 = do i <- getIState
268 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
270addNameHint :: Name -> Name -> Idris ()
271addNameHint ty n
272 = do i <- getIState
273 ty' <- case lookupCtxtName ty (idris_implicits i) of
274 [(tyn, _)] -> return tyn
275 [] -> throwError (NoSuchVariable ty)
276 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
277 let ns' = case lookupCtxt ty' (idris_namehints i) of
278 [ns] -> ns ++ [n]
279 _ -> [n]
280 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
282getNameHints :: IState -> Name -> [Name]
283getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
284getNameHints i n =
285 case lookupCtxt n (idris_namehints i) of
286 [ns] -> ns
287 _ -> []
289addToCalledG :: Name -> [Name] -> Idris ()
290addToCalledG n ns = return () -- TODO
292-- Add a class instance function. Dodgy hack: Put integer instances first in the
293-- list so they are resolved by default.
294-- Dodgy hack 2: put constraint chasers (@@) last
296addInstance :: Bool -> Name -> Name -> Idris ()
297addInstance int n i
298 = do ist <- getIState
299 case lookupCtxt n (idris_classes ist) of
300 [CI a b c d e ins] ->
301 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
302 putIState $ ist { idris_classes = cs }
303 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
304 putIState $ ist { idris_classes = cs }
305 where addI i ins | int = i : ins
306 | chaser n = ins ++ [i]
307 | otherwise = insI i ins
308 insI i [] = [i]
309 insI i (n : ns) | chaser n = i : n : ns
310 | otherwise = n : insI i ns
312 chaser (UN nm)
313 | ('@':'@':_) <- str nm = True
314 chaser (NS n _) = chaser n
315 chaser _ = False
317addClass :: Name -> ClassInfo -> Idris ()
318addClass n i
319 = do ist <- getIState
320 let i' = case lookupCtxt n (idris_classes ist) of
321 [c] -> c { class_instances = class_instances i }
322 _ -> i
323 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
325addIBC :: IBCWrite -> Idris ()
326addIBC ibc@(IBCDef n)
327 = do i <- getIState
328 when (notDef (ibc_write i)) $
329 putIState $ i { ibc_write = ibc : ibc_write i }
330 where notDef [] = True
331 notDef (IBCDef n': is) | n == n' = False
332 notDef (_ : is) = notDef is
333addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
335clearIBC :: Idris ()
336clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
338resetNameIdx :: Idris ()
339resetNameIdx = do i <- getIState
340 put (i { idris_nameIdx = (0, emptyContext) })
342-- Used to preserve sharing of names
343addNameIdx :: Name -> Idris (Int, Name)
344addNameIdx n = do i <- getIState
345 let (i', x) = addNameIdx' i n
346 return x
348addNameIdx' :: IState -> Name -> (IState, (Int, Name))
349addNameIdx' i n
350 = let idxs = snd (idris_nameIdx i) in
351 case lookupCtxt n idxs of
352 [x] -> (i, x)
353 _ -> let i' = fst (idris_nameIdx i) + 1 in
354 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
356getHdrs :: Codegen -> Idris [String]
357getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
359setErrLine :: Int -> Idris ()
360setErrLine x = do i <- getIState;
361 case (errLine i) of
362 Nothing -> putIState $ i { errLine = Just x }
363 Just _ -> return ()
365clearErr :: Idris ()
366clearErr = do i <- getIState
367 putIState $ i { errLine = Nothing }
369getSO :: Idris (Maybe String)
370getSO = do i <- getIState
371 return (compiled_so i)
373setSO :: Maybe String -> Idris ()
374setSO s = do i <- getIState
375 putIState $ (i { compiled_so = s })
377getIState :: Idris IState
378getIState = get
380putIState :: IState -> Idris ()
381putIState = put
383-- | A version of liftIO that puts errors into the exception type of the Idris monad
384runIO :: IO a -> Idris a
385runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
386-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
388getName :: Idris Int
389getName = do i <- getIState;
390 let idx = idris_name i;
391 putIState $ (i { idris_name = idx + 1 })
392 return idx
394addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
395addInternalApp fp l t
396 = do i <- getIState
397 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
399getInternalApp :: FilePath -> Int -> Idris PTerm
400getInternalApp fp l = do i <- getIState
401 case lookup (fp, l) (idris_lineapps i) of
402 Just n' -> return n'
403 Nothing -> return Placeholder
404 -- TODO: What if it's not there?
406-- Pattern definitions are only used for coverage checking, so erase them
407-- when we're done
408clearOrigPats :: Idris ()
409clearOrigPats = do i <- get
410 let ps = idris_patdefs i
411 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
412 put (i { idris_patdefs = ps' })
414-- Erase types from Ps in the context (basically ending up with what's in
415-- the .ibc, which is all we need after all the analysis is done)
416clearPTypes :: Idris ()
417clearPTypes = do i <- get
418 let ctxt = tt_ctxt i
419 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
420 where pErase (CaseOp c t tys orig tot cds)
421 = CaseOp c t tys orig [] (pErase' cds)
422 pErase x = x
423 pErase' (CaseDefs _ (cs, c) _ rs)
424 = let c' = (cs, fmap pEraseType c) in
425 CaseDefs c' c' c' rs
427checkUndefined :: FC -> Name -> Idris ()
428checkUndefined fc n
429 = do i <- getContext
430 case lookupTy n i of
431 (_:_) -> throwError . Msg $ show fc ++ ":" ++
432 show n ++ " already defined"
433 _ -> return ()
435isUndefined :: FC -> Name -> Idris Bool
436isUndefined fc n
437 = do i <- getContext
438 case lookupTy n i of
439 (_:_) -> return False
440 _ -> return True
442setContext :: Context -> Idris ()
443setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
445updateContext :: (Context -> Context) -> Idris ()
446updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
448addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
449addConstraints fc (v, cs)
450 = do i <- getIState
451 let ctxt = tt_ctxt i
452 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
453 next_tvar = v }
454 let ics = zip cs (repeat fc) ++ idris_constraints i
455 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
457addDeferred = addDeferred' Ref
458addDeferredTyCon = addDeferred' (TCon 0 0)
460addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
461addDeferred' nt ns
462 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
463 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
464 i <- getIState
465 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
466 idris_metavars i }
467 where tidyNames used (Bind (MN i x) b sc)
468 = let n' = uniqueName (UN x) used in
469 Bind n' b $ tidyNames (n':used) sc
470 tidyNames used (Bind n b sc)
471 = let n' = uniqueName n used in
472 Bind n' b $ tidyNames (n':used) sc
473 tidyNames used b = b
475solveDeferred :: Name -> Idris ()
476solveDeferred n = do i <- getIState
477 putIState $ i { idris_metavars =
478 filter (\(n', _) -> n/=n')
479 (idris_metavars i),
480 ibc_write =
481 filter (notMV n) (ibc_write i)
482 }
483 where notMV n (IBCMetavar n') = not (n == n')
484 notMV n _ = True
486getUndefined :: Idris [Name]
487getUndefined = do i <- getIState
488 return (map fst (idris_metavars i) \\ primDefs)
490getWidth :: Idris ConsoleWidth
491getWidth = fmap idris_consolewidth getIState
493setWidth :: ConsoleWidth -> Idris ()
494setWidth w = do ist <- getIState
495 put ist { idris_consolewidth = w }
497renderWidth :: Idris Int
498renderWidth = do iw <- getWidth
499 case iw of
500 InfinitelyWide -> return 100000000
501 ColsWide n -> return (max n 1)
502 AutomaticWidth -> runIO getScreenWidth
505iRender :: Doc a -> Idris (SimpleDoc a)
506iRender d = do w <- getWidth
507 ist <- getIState
508 let ideSlave = case idris_outputmode ist of
509 IdeSlave _ -> True
510 _ -> False
511 case w of
512 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
513 ColsWide n -> return $
514 if n < 1
515 then renderPretty 1.0 1000000000 d
516 else renderPretty 0.8 n d
517 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
518 | otherwise -> do width <- runIO getScreenWidth
519 return $ renderPretty 0.8 width d
521ihPrintResult :: Handle -> String -> Idris ()
522ihPrintResult h s = do i <- getIState
523 case idris_outputmode i of
524 RawOutput -> case s of
525 "" -> return ()
526 s -> runIO $ hPutStrLn h s
527 IdeSlave n ->
528 let good = SexpList [SymbolAtom "ok", toSExp s] in
529 runIO $ hPutStrLn h $ convSExp "return" good n
531-- | Write a pretty-printed term to the console with semantic coloring
532consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
533consoleDisplayAnnotated h output = do ist <- getIState
534 rendered <- iRender $ output
535 runIO . hPutStrLn h .
536 displayDecorated (consoleDecorate ist) $
537 rendered
540-- | Write pretty-printed output to IDESlave with semantic annotations
541ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
542ideSlaveReturnAnnotated n h out = do ist <- getIState
543 (str, spans) <- fmap displaySpans .
544 iRender .
545 fmap (fancifyAnnots ist) $
546 out
547 let good = [SymbolAtom "ok", toSExp str, toSExp spans]
548 runIO . hPutStrLn h $ convSExp "return" good n
550ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
551ihPrintTermWithType h tm ty = do ist <- getIState
552 let output = tm <+> colon <+> ty
553 case idris_outputmode ist of
554 RawOutput -> consoleDisplayAnnotated h output
555 IdeSlave n -> ideSlaveReturnAnnotated n h output
557-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
558ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
559ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
560ihPrintFunTypes h bnd n overloads = do imp <- impShow
561 ist <- getIState
562 let output = vsep (map (uncurry (ppOverload imp)) overloads)
563 case idris_outputmode ist of
564 RawOutput -> consoleDisplayAnnotated h output
565 IdeSlave n -> ideSlaveReturnAnnotated n h output
566 where fullName n = prettyName True bnd n
567 ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd tm)
569ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
570ihRenderResult h d = do ist <- getIState
571 case idris_outputmode ist of
572 RawOutput -> consoleDisplayAnnotated h d
573 IdeSlave n -> ideSlaveReturnAnnotated n h d
575fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
576fancifyAnnots ist annot@(AnnName n _ _) =
577 do let ctxt = tt_ctxt ist
578 case () of
579 _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
580 _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
581 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
582 _ | otherwise -> annot
583fancifyAnnots _ annot = annot
585type1Doc :: Doc OutputAnnotation
586type1Doc = (annotate AnnConstType $ text "Type 1")
588-- | Show an error with semantic highlighting
589ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
590ihRenderError h e = do ist <- getIState
591 case idris_outputmode ist of
592 RawOutput -> consoleDisplayAnnotated h e
593 IdeSlave n -> do
594 (str, spans) <- fmap displaySpans .
595 iRender .
596 fmap (fancifyAnnots ist) $
597 e
598 let good = [SymbolAtom "error", toSExp str, toSExp spans]
599 runIO . hPutStrLn h $ convSExp "return" good n
601ihPrintError :: Handle -> String -> Idris ()
602ihPrintError h s = do i <- getIState
603 case idris_outputmode i of
604 RawOutput -> case s of
605 "" -> return ()
606 s -> runIO $ hPutStrLn h s
607 IdeSlave n ->
608 let good = SexpList [SymbolAtom "error", toSExp s] in
609 runIO . hPutStrLn h $ convSExp "return" good n
611ihputStrLn :: Handle -> String -> Idris ()
612ihputStrLn h s = do i <- getIState
613 case idris_outputmode i of
614 RawOutput -> runIO $ hPutStrLn h s
615 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
617iputStrLn = ihputStrLn stdout
618iPrintError = ihPrintError stdout
619iPrintResult = ihPrintResult stdout
620iWarn = ihWarn stdout
622ideslavePutSExp :: SExpable a => String -> a -> Idris ()
623ideslavePutSExp cmd info = do i <- getIState
624 case idris_outputmode i of
625 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
626 _ -> return ()
628-- this needs some typing magic and more structured output towards emacs
629iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
630iputGoal g = do i <- getIState
631 case idris_outputmode i of
632 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
633 IdeSlave n -> runIO . putStrLn $
634 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
636isetPrompt :: String -> Idris ()
637isetPrompt p = do i <- getIState
638 case idris_outputmode i of
639 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
641ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
642ihWarn h fc err = do i <- getIState
643 err' <- iRender . fmap (fancifyAnnots i) $ err
644 case idris_outputmode i of
645 RawOutput ->
646 runIO $
647 hPutStrLn h (show fc ++ ":" ++ displayDecorated (consoleDecorate i) err')
648 IdeSlave n ->
649 do let (str, spans) = displaySpans err'
650 runIO . hPutStrLn h $
651 convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, str, spans) n
653setLogLevel :: Int -> Idris ()
654setLogLevel l = do i <- getIState
655 let opts = idris_options i
656 let opt' = opts { opt_logLevel = l }
657 putIState $ i { idris_options = opt' }
659setCmdLine :: [Opt] -> Idris ()
660setCmdLine opts = do i <- getIState
661 let iopts = idris_options i
662 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
664getCmdLine :: Idris [Opt]
665getCmdLine = do i <- getIState
666 return (opt_cmdline (idris_options i))
668getDumpDefun :: Idris (Maybe FilePath)
669getDumpDefun = do i <- getIState
670 return $ findC (opt_cmdline (idris_options i))
671 where findC [] = Nothing
672 findC (DumpDefun x : _) = Just x
673 findC (_ : xs) = findC xs
675getDumpCases :: Idris (Maybe FilePath)
676getDumpCases = do i <- getIState
677 return $ findC (opt_cmdline (idris_options i))
678 where findC [] = Nothing
679 findC (DumpCases x : _) = Just x
680 findC (_ : xs) = findC xs
682logLevel :: Idris Int
683logLevel = do i <- getIState
684 return (opt_logLevel (idris_options i))
686setErrContext :: Bool -> Idris ()
687setErrContext t = do i <- getIState
688 let opts = idris_options i
689 let opt' = opts { opt_errContext = t }
690 putIState $ i { idris_options = opt' }
692errContext :: Idris Bool
693errContext = do i <- getIState
694 return (opt_errContext (idris_options i))
696useREPL :: Idris Bool
697useREPL = do i <- getIState
698 return (opt_repl (idris_options i))
700setREPL :: Bool -> Idris ()
701setREPL t = do i <- getIState
702 let opts = idris_options i
703 let opt' = opts { opt_repl = t }
704 putIState $ i { idris_options = opt' }
706showOrigErr :: Idris Bool
707showOrigErr = do i <- getIState
708 return (opt_origerr (idris_options i))
710setShowOrigErr :: Bool -> Idris ()
711setShowOrigErr b = do i <- getIState
712 let opts = idris_options i
713 let opt' = opts { opt_origerr = b }
714 putIState $ i { idris_options = opt' }
716setAutoSolve :: Bool -> Idris ()
717setAutoSolve b = do i <- getIState
718 let opts = idris_options i
719 let opt' = opts { opt_autoSolve = b }
720 putIState $ i { idris_options = opt' }
722setNoBanner :: Bool -> Idris ()
723setNoBanner n = do i <- getIState
724 let opts = idris_options i
725 let opt' = opts { opt_nobanner = n }
726 putIState $ i { idris_options = opt' }
728getNoBanner :: Idris Bool
729getNoBanner = do i <- getIState
730 let opts = idris_options i
731 return (opt_nobanner opts)
733setQuiet :: Bool -> Idris ()
734setQuiet q = do i <- getIState
735 let opts = idris_options i
736 let opt' = opts { opt_quiet = q }
737 putIState $ i { idris_options = opt' }
739getQuiet :: Idris Bool
740getQuiet = do i <- getIState
741 let opts = idris_options i
742 return (opt_quiet opts)
744setCodegen :: Codegen -> Idris ()
745setCodegen t = do i <- getIState
746 let opts = idris_options i
747 let opt' = opts { opt_codegen = t }
748 putIState $ i { idris_options = opt' }
750codegen :: Idris Codegen
751codegen = do i <- getIState
752 return (opt_codegen (idris_options i))
754setOutputTy :: OutputType -> Idris ()
755setOutputTy t = do i <- getIState
756 let opts = idris_options i
757 let opt' = opts { opt_outputTy = t }
758 putIState $ i { idris_options = opt' }
760outputTy :: Idris OutputType
761outputTy = do i <- getIState
762 return $ opt_outputTy $ idris_options i
764setIdeSlave :: Bool -> Idris ()
765setIdeSlave True = do i <- getIState
766 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
767setIdeSlave False = return ()
769setTargetTriple :: String -> Idris ()
770setTargetTriple t = do i <- getIState
771 let opts = idris_options i
772 opt' = opts { opt_triple = t }
773 putIState $ i { idris_options = opt' }
775targetTriple :: Idris String
776targetTriple = do i <- getIState
777 return (opt_triple (idris_options i))
779setTargetCPU :: String -> Idris ()
780setTargetCPU t = do i <- getIState
781 let opts = idris_options i
782 opt' = opts { opt_cpu = t }
783 putIState $ i { idris_options = opt' }
785targetCPU :: Idris String
786targetCPU = do i <- getIState
787 return (opt_cpu (idris_options i))
789setOptLevel :: Word -> Idris ()
790setOptLevel t = do i <- getIState
791 let opts = idris_options i
792 opt' = opts { opt_optLevel = t }
793 putIState $ i { idris_options = opt' }
795optLevel :: Idris Word
796optLevel = do i <- getIState
797 return (opt_optLevel (idris_options i))
799verbose :: Idris Bool
800verbose = do i <- getIState
801 return (opt_verbose (idris_options i))
803setVerbose :: Bool -> Idris ()
804setVerbose t = do i <- getIState
805 let opts = idris_options i
806 let opt' = opts { opt_verbose = t }
807 putIState $ i { idris_options = opt' }
809typeInType :: Idris Bool
810typeInType = do i <- getIState
811 return (opt_typeintype (idris_options i))
813setTypeInType :: Bool -> Idris ()
814setTypeInType t = do i <- getIState
815 let opts = idris_options i
816 let opt' = opts { opt_typeintype = t }
817 putIState $ i { idris_options = opt' }
819coverage :: Idris Bool
820coverage = do i <- getIState
821 return (opt_coverage (idris_options i))
823setCoverage :: Bool -> Idris ()
824setCoverage t = do i <- getIState
825 let opts = idris_options i
826 let opt' = opts { opt_coverage = t }
827 putIState $ i { idris_options = opt' }
829setIBCSubDir :: FilePath -> Idris ()
830setIBCSubDir fp = do i <- getIState
831 let opts = idris_options i
832 let opt' = opts { opt_ibcsubdir = fp }
833 putIState $ i { idris_options = opt' }
835valIBCSubDir :: IState -> Idris FilePath
836valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
838addImportDir :: FilePath -> Idris ()
839addImportDir fp = do i <- getIState
840 let opts = idris_options i
841 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
842 putIState $ i { idris_options = opt' }
844setImportDirs :: [FilePath] -> Idris ()
845setImportDirs fps = do i <- getIState
846 let opts = idris_options i
847 let opt' = opts { opt_importdirs = fps }
848 putIState $ i { idris_options = opt' }
850allImportDirs :: Idris [FilePath]
851allImportDirs = do i <- getIState
852 let optdirs = opt_importdirs (idris_options i)
853 return ("." : reverse optdirs)
855colourise :: Idris Bool
856colourise = do i <- getIState
857 return $ idris_colourRepl i
859setColourise :: Bool -> Idris ()
860setColourise b = do i <- getIState
861 putIState $ i { idris_colourRepl = b }
863setOutH :: Handle -> Idris ()
864setOutH h = do i <- getIState
865 putIState $ i { idris_outh = h }
867impShow :: Idris Bool
868impShow = do i <- getIState
869 return (opt_showimp (idris_options i))
871setImpShow :: Bool -> Idris ()
872setImpShow t = do i <- getIState
873 let opts = idris_options i
874 let opt' = opts { opt_showimp = t }
875 putIState $ i { idris_options = opt' }
877setColour :: ColourType -> IdrisColour -> Idris ()
878setColour ct c = do i <- getIState
879 let newTheme = setColour' ct c (idris_colourTheme i)
880 putIState $ i { idris_colourTheme = newTheme }
881 where setColour' KeywordColour c t = t { keywordColour = c }
882 setColour' BoundVarColour c t = t { boundVarColour = c }
883 setColour' ImplicitColour c t = t { implicitColour = c }
884 setColour' FunctionColour c t = t { functionColour = c }
885 setColour' TypeColour c t = t { typeColour = c }
886 setColour' DataColour c t = t { dataColour = c }
887 setColour' PromptColour c t = t { promptColour = c }
889logLvl :: Int -> String -> Idris ()
890logLvl l str = do i <- getIState
891 let lvl = opt_logLevel (idris_options i)
892 when (lvl >= l) $
893 case idris_outputmode i of
894 RawOutput -> do runIO $ putStrLn str
895 IdeSlave n ->
896 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
897 runIO $ putStrLn $ convSExp "log" good n
899cmdOptType :: Opt -> Idris Bool
900cmdOptType x = do i <- getIState
901 return $ x `elem` opt_cmdline (idris_options i)
903iLOG :: String -> Idris ()
904iLOG = logLvl 1
906noErrors :: Idris Bool
907noErrors = do i <- getIState
908 case errLine i of
909 Nothing -> return True
910 _ -> return False
912setTypeCase :: Bool -> Idris ()
913setTypeCase t = do i <- getIState
914 let opts = idris_options i
915 let opt' = opts { opt_typecase = t }
916 putIState $ i { idris_options = opt' }
919-- Dealing with parameters
921expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
922 [Name] -> -- all names
923 [Name] -> -- names with no declaration
924 PTerm -> PTerm
925expandParams dec ps ns infs tm = en tm
926 where
927 -- if we shadow a name (say in a lambda binding) that is used in a call to
928 -- a lifted function, we need access to both names - once in the scope of the
929 -- binding and once to call the lifted functions. So we'll explicitly shadow
930 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
931 -- but we didn't...)
933 mkShadow (UN n) = MN 0 n
934 mkShadow (MN i n) = MN (i+1) n
935 mkShadow (NS x s) = NS (mkShadow x) s
937 en (PLam n t s)
938 | n `elem` (map fst ps ++ ns)
939 = let n' = mkShadow n in
940 PLam n' (en t) (en (shadow n n' s))
941 | otherwise = PLam n (en t) (en s)
942 en (PPi p n t s)
943 | n `elem` (map fst ps ++ ns)
944 = let n' = mkShadow n in
945 PPi p n' (en t) (en (shadow n n' s))
946 | otherwise = PPi p n (en t) (en s)
947 en (PLet n ty v s)
948 | n `elem` (map fst ps ++ ns)
949 = let n' = mkShadow n in
950 PLet n' (en ty) (en v) (en (shadow n n' s))
951 | otherwise = PLet n (en ty) (en v) (en s)
952 -- FIXME: Should only do this in a type signature!
953 en (PDPair f p (PRef f' n) t r)
954 | n `elem` (map fst ps ++ ns) && t /= Placeholder
955 = let n' = mkShadow n in
956 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
957 en (PEq f l r) = PEq f (en l) (en r)
958 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
959 en (PTyped l r) = PTyped (en l) (en r)
960 en (PPair f p l r) = PPair f p (en l) (en r)
961 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
962 en (PAlternative a as) = PAlternative a (map en as)
963 en (PHidden t) = PHidden (en t)
964 en (PUnifyLog t) = PUnifyLog (en t)
965 en (PDisamb ds t) = PDisamb ds (en t)
966 en (PNoImplicits t) = PNoImplicits (en t)
967 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
968 en (PProof ts) = PProof (map (fmap en) ts)
969 en (PTactics ts) = PTactics (map (fmap en) ts)
971 en (PQuote (Var n))
972 | n `nselem` ns = PQuote (Var (dec n))
973 en (PApp fc (PInferRef fc' n) as)
974 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
975 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
976 en (PApp fc (PRef fc' n) as)
977 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
978 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
979 | n `nselem` ns = PApp fc (PRef fc' (dec n))
980 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
981 en (PAppBind fc (PRef fc' n) as)
982 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
983 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
984 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
985 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
986 en (PRef fc n)
987 | n `elem` infs = PApp fc (PInferRef fc (dec n))
988 (map (pexp . (PRef fc)) (map fst ps))
989 | n `nselem` ns = PApp fc (PRef fc (dec n))
990 (map (pexp . (PRef fc)) (map fst ps))
991 en (PInferRef fc n)
992 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
993 (map (pexp . (PRef fc)) (map fst ps))
994 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
995 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
996 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
997 en t = t
999 nselem x [] = False
1000 nselem x (y : xs) | nseq x y = True
1001 | otherwise = nselem x xs
1003 nseq x y = nsroot x == nsroot y
1005expandParamsD :: Bool -> -- True = RHS only
1006 IState ->
1007 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1008expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
1009 = if n `elem` ns && (not rhsonly)
1010 then -- trace (show (n, expandParams dec ps ns ty)) $
1011 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
1012 else --trace (show (n, expandParams dec ps ns ty)) $
1013 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
1014expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
1015 = if n `elem` ns && (not rhsonly)
1016 then -- trace (show (n, expandParams dec ps ns ty)) $
1017 PPostulate doc syn fc o (dec n) (piBind ps
1018 (expandParams dec ps ns [] ty))
1019 else --trace (show (n, expandParams dec ps ns ty)) $
1020 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1021expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1022 = let n' = if n `elem` ns then dec n else n in
1023 PClauses fc opts n' (map expandParamsC cs)
1024 where
1025 expandParamsC (PClause fc n lhs ws rhs ds)
1026 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1027 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1028 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1029 n' = if n `elem` ns then dec n else n
1030 -- names bound on the lhs should not be expanded on the rhs
1031 ns' = removeBound lhs ns in
1032 PClause fc n' lhs'
1033 (map (expandParams dec ps'' ns' []) ws)
1034 (expandParams dec ps'' ns' [] rhs)
1035 (map (expandParamsD True ist dec ps'' ns') ds)
1036 expandParamsC (PWith fc n lhs ws wval ds)
1037 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1038 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1039 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1040 n' = if n `elem` ns then dec n else n
1041 ns' = removeBound lhs ns in
1042 PWith fc n' lhs'
1043 (map (expandParams dec ps'' ns' []) ws)
1044 (expandParams dec ps'' ns' [] wval)
1045 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1046 updateps yn nm [] = []
1047 updateps yn nm (((a, t), i):as)
1048 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1049 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
1051 removeBound lhs ns = ns \\ nub (bnames lhs)
1053 bnames (PRef _ n) = [n]
1054 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1055 bnames (PPair _ _ l r) = bnames l ++ bnames r
1056 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1057 bnames _ = []
1059expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1060 = PData doc argDocs syn fc co (expandPData pd)
1061 where
1062 -- just do the type decl, leave constructors alone (parameters will be
1063 -- added implicitly)
1064 expandPData (PDatadecl n ty cons)
1065 = if n `elem` ns
1066 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1067 (map econ cons)
1068 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1069 econ (doc, argDocs, n, t, fc, fs)
1070 = (doc, argDocs, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)
1071expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
1072 = if tn `elem` ns
1073 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1074 cdoc (dec cn) conty
1075 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1076 cdoc (dec cn) conty
1077 where conty = piBindp impl ps (expandParams dec ps ns [] cty)
1078expandParamsD rhs ist dec ps ns (PParams f params pds)
1079 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1080 (map (expandParamsD True ist dec ps ns) pds)
1081-- (map (expandParamsD ist dec ps ns) pds)
1082expandParamsD rhs ist dec ps ns (PMutual f pds)
1083 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1084expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
1085 = PClass doc info f
1086 (map (expandParams dec ps ns []) cs)
1088 (map (mapsnd (expandParams dec ps ns [])) params)
1089 (map (expandParamsD rhs ist dec ps ns) decls)
1090expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1091 = PInstance info f
1092 (map (expandParams dec ps ns []) cs)
1094 (map (expandParams dec ps ns []) params)
1095 (expandParams dec ps ns [] ty)
1096 cn
1097 (map (expandParamsD rhs ist dec ps ns) decls)
1098expandParamsD rhs ist dec ps ns d = d
1100mapsnd f (x, t) = (x, f t)
1102-- Calculate a priority for a type, for deciding elaboration order
1103-- * if it's just a type variable or concrete type, do it early (0)
1104-- * if there's only type variables and injective constructors, do it next (1)
1105-- * if there's a function type, next (2)
1106-- * finally, everything else (3)
1108getPriority :: IState -> PTerm -> Int
1109getPriority i tm = 1 -- pri tm
1110 where
1111 pri (PRef _ n) =
1112 case lookupP n (tt_ctxt i) of
1113 ((P (DCon _ _) _ _):_) -> 1
1114 ((P (TCon _ _) _ _):_) -> 1
1115 ((P Ref _ _):_) -> 1
1116 [] -> 0 -- must be locally bound, if it's not an error...
1117 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1118 pri (PTrue _ _) = 0
1119 pri (PFalse _) = 0
1120 pri (PRefl _ _) = 1
1121 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1122 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1123 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1124 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1125 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1126 pri (PTyped l r) = pri l
1127 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1128 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1129 pri (PAlternative a as) = maximum (map pri as)
1130 pri (PConstant _) = 0
1131 pri Placeholder = 1
1132 pri _ = 3
1135addStatics :: Name -> Term -> PTerm -> Idris ()
1136addStatics n tm ptm =
1137 do let (statics, dynamics) = initStatics tm ptm
1138 let stnames = nub $ concatMap freeArgNames (map snd statics)
1139 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1140 -- also get the arguments which are 'uniquely inferrable' from
1141 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1142 let statics' = nub $ map fst statics ++
1143 filter (\x -> not (elem x dnames)) stnames
1144 let stpos = staticList statics' tm
1145 i <- getIState
1146 when (not (null statics)) $
1147 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1148 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1149 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1150 addIBC (IBCStatic n)
1151 where
1152 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1153 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1154 if pstatic p == Static then ((n, ty) : static, dynamic)
1155 else if (not (searchArg p))
1156 then (static, (n, ty) : dynamic)
1157 else (static, dynamic)
1158 initStatics t pt = ([], [])
1160 freeArgNames (Bind n (Pi ty) sc)
1161 = nub $ freeArgNames ty
1162 freeArgNames tm = let (_, args) = unApply tm in
1163 concatMap freeNames args
1165 -- if a name appears in a type class or tactic implicit index, it doesn't
1166 -- affect its 'uniquely inferrable' from a static status since these are
1167 -- resolved by searching.
1168 searchArg (Constraint _ _) = True
1169 searchArg (TacImp _ _ _) = True
1170 searchArg _ = False
1172 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1173 staticList _ _ = []
1175-- Dealing with implicit arguments
1177-- Add constraint bindings from using block
1179addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1180addUsingConstraints syn fc t
1181 = do ist <- get
1182 let ns = namesIn [] ist t
1183 let cs = getConstraints t -- check declared constraints
1184 let addconsts = uconsts \\ cs
1185 -- if all names in the arguments of addconsts appear in ns,
1186 -- add the constraint implicitly
1187 return (doAdd addconsts ns t)
1188 where uconsts = filter uconst (using syn)
1189 uconst (UConstraint _ _) = True
1190 uconst _ = False
1192 doAdd [] _ t = t
1193 -- if all of args in ns, then add it
1194 doAdd (UConstraint c args : cs) ns t
1195 | all (\n -> elem n ns) args
1196 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1197 (mkConst c args) (doAdd cs ns t)
1198 | otherwise = doAdd cs ns t
1200 mkConst c args = PApp fc (PRef fc c)
1201 (map (\n -> PExp 0 [] (PRef fc n)) args)
1203 getConstraints (PPi (Constraint _ _) _ c sc)
1204 = getcapp c ++ getConstraints sc
1205 getConstraints (PPi _ _ c sc) = getConstraints sc
1206 getConstraints _ = []
1208 getcapp (PApp _ (PRef _ c) args)
1209 = do ns <- mapM getName args
1210 return (UConstraint c ns)
1211 getcapp _ = []
1213 getName (PExp _ _ (PRef _ n)) = return n
1214 getName _ = []
1216-- Add implicit Pi bindings for any names in the term which appear in an
1217-- argument position.
1219-- This has become a right mess already. Better redo it some time...
1221implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1222implicit syn n ptm = implicit' syn [] n ptm
1224implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1225implicit' syn ignore n ptm
1226 = do i <- getIState
1227 let (tm', impdata) = implicitise syn ignore i ptm
1228-- let (tm'', spos) = findStatics i tm'
1229 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1230 addIBC (IBCImp n)
1231 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1232-- i <- get
1233-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1234 return tm'
1236implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1237implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1238 let (declimps, ns') = execState (imps True [] tm) ([], [])
1239 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1240 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1241 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1242 if null ns
1243 then (tm, reverse declimps)
1244 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1245 where
1246 uvars = map ipair (filter uimplicit (using syn))
1247 pvars = syn_params syn
1249 inUsing n = n `elem` map fst uvars
1251 ipair (UImplicit x y) = (x, y)
1252 uimplicit (UImplicit _ _) = True
1253 uimplicit _ = False
1255 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1256 | otherwise = x : dropAll xs ys
1257 dropAll [] ys = []
1259 -- Find names in argument position in a type, suitable for implicit
1260 -- binding
1261 -- Not the function position, but do everything else...
1262 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1263 implNamesIn uv t = namesIn uv ist t
1265 imps top env (PApp _ f as)
1266 = do (decls, ns) <- get
1267 let isn = concatMap (namesIn uvars ist) (map getTm as)
1268 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1269 imps top env (PPi (Imp l _ _) n ty sc)
1270 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1271 (decls , ns) <- get
1272 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1273 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1274 imps True (n:env) sc
1275 imps top env (PPi (Exp l _ _) n ty sc)
1276 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1277 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1278 _ -> [])
1279 (decls, ns) <- get -- ignore decls in HO types
1280 put (PExp (getPriority ist ty) l Placeholder : decls,
1281 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1282 imps True (n:env) sc
1283 imps top env (PPi (Constraint l _) n ty sc)
1284 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1285 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1286 _ -> [])
1287 (decls, ns) <- get -- ignore decls in HO types
1288 put (PConstraint 10 l Placeholder : decls,
1289 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1290 imps True (n:env) sc
1291 imps top env (PPi (TacImp l _ scr) n ty sc)
1292 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1293 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1294 _ -> [])
1295 (decls, ns) <- get -- ignore decls in HO types
1296 put (PTacImplicit 10 l n scr Placeholder : decls,
1297 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1298 imps True (n:env) sc
1299 imps top env (PEq _ l r)
1300 = do (decls, ns) <- get
1301 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1302 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1303 imps top env (PRewrite _ l r _)
1304 = do (decls, ns) <- get
1305 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1306 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1307 imps top env (PTyped l r)
1308 = imps top env l
1309 imps top env (PPair _ _ l r)
1310 = do (decls, ns) <- get
1311 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1312 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1313 imps top env (PDPair _ _ (PRef _ n) t r)
1314 = do (decls, ns) <- get
1315 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1316 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1317 imps top env (PDPair _ _ l t r)
1318 = do (decls, ns) <- get
1319 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1320 namesIn uvars ist r
1321 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1322 imps top env (PAlternative a as)
1323 = do (decls, ns) <- get
1324 let isn = concatMap (namesIn uvars ist) as
1325 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1326 imps top env (PLam n ty sc)
1327 = do imps False env ty
1328 imps False (n:env) sc
1329 imps top env (PHidden tm) = imps False env tm
1330 imps top env (PUnifyLog tm) = imps False env tm
1331 imps top env (PNoImplicits tm) = imps False env tm
1332 imps top env _ = return ()
1334 pibind using [] sc = sc
1335 pibind using (n:ns) sc
1336 = case lookup n using of
1337 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1338 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1339 (pibind using ns sc)
1341-- Add implicit arguments in function calls
1342addImplPat :: IState -> PTerm -> PTerm
1343addImplPat = addImpl' True [] []
1345addImplBound :: IState -> [Name] -> PTerm -> PTerm
1346addImplBound ist ns = addImpl' False ns [] ist
1348addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1349addImplBoundInf ist ns inf = addImpl' False ns inf ist
1351addImpl :: IState -> PTerm -> PTerm
1352addImpl = addImpl' False [] []
1354-- TODO: in patterns, don't add implicits to function names guarded by constructors
1355-- and *not* inside a PHidden
1357addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1358addImpl' inpat env infns ist ptm
1359 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1360 where
1361 ai env ds (PRef fc f)
1362 | f `elem` infns = PInferRef fc f
1363 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1364 ai env ds (PHidden (PRef fc f))
1365 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1366 ai env ds (PEq fc l r)
1367 = let l' = ai env ds l
1368 r' = ai env ds r in
1369 PEq fc l' r'
1370 ai env ds (PRewrite fc l r g)
1371 = let l' = ai env ds l
1372 r' = ai env ds r
1373 g' = fmap (ai env ds) g in
1374 PRewrite fc l' r' g'
1375 ai env ds (PTyped l r)
1376 = let l' = ai env ds l
1377 r' = ai env ds r in
1378 PTyped l' r'
1379 ai env ds (PPair fc p l r)
1380 = let l' = ai env ds l
1381 r' = ai env ds r in
1382 PPair fc p l' r'
1383 ai env ds (PDPair fc p l t r)
1384 = let l' = ai env ds l
1385 t' = ai env ds t
1386 r' = ai env ds r in
1387 PDPair fc p l' t' r'
1388 ai env ds (PAlternative a as)
1389 = let as' = map (ai env ds) as in
1390 PAlternative a as'
1391 ai env _ (PDisamb ds' as) = ai env ds' as
1392 ai env ds (PApp fc (PInferRef _ f) as)
1393 = let as' = map (fmap (ai env ds)) as in
1394 PApp fc (PInferRef fc f) as'
1395 ai env ds (PApp fc ftm@(PRef _ f) as)
1396 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1397 | not (f `elem` map fst env)
1398 = let as' = map (fmap (ai env ds)) as in
1399 handleErr $ aiFn inpat False ist fc f ds as'
1400 | Just (Just ty) <- lookup f env =
1401 let as' = map (fmap (ai env ds)) as
1402 arity = getPArity ty in
1403 mkPApp fc arity ftm as'
1404 ai env ds (PApp fc f as)
1405 = let f' = ai env ds f
1406 as' = map (fmap (ai env ds)) as in
1407 mkPApp fc 1 f' as'
1408 ai env ds (PCase fc c os)
1409 = let c' = ai env ds c
1410 os' = map (pmap (ai env ds)) os in
1411 PCase fc c' os'
1412 ai env ds (PLam n ty sc)
1413 = let ty' = ai env ds ty
1414 sc' = ai ((n, Just ty):env) ds sc in
1415 PLam n ty' sc'
1416 ai env ds (PLet n ty val sc)
1417 = let ty' = ai env ds ty
1418 val' = ai env ds val
1419 sc' = ai ((n, Just ty):env) ds sc in
1420 PLet n ty' val' sc'
1421 ai env ds (PPi p n ty sc)
1422 = let ty' = ai env ds ty
1423 sc' = ai ((n, Just ty):env) ds sc in
1424 PPi p n ty' sc'
1425 ai env ds (PGoal fc r n sc)
1426 = let r' = ai env ds r
1427 sc' = ai ((n, Nothing):env) ds sc in
1428 PGoal fc r' n sc'
1429 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1430 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1431 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1432 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1433 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1434 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1435 ai env ds tm = tm
1437 handleErr (Left err) = PElabError err
1438 handleErr (Right x) = x
1440-- if in a pattern, and there are no arguments, and there's no possible
1441-- names with zero explicit arguments, don't add implicits.
1443aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1444aiFn inpat True ist fc f ds []
1445 = case lookupDef f (tt_ctxt ist) of
1446 [] -> Right $ PPatvar fc f
1447 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1448 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1449 if (not (vname f) || tcname f
1450 || any (conCaf (tt_ctxt ist)) ialts)
1451-- any constructor alts || any allImp ialts))
1452 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1453 else Right $ PPatvar fc f
1454 where imp (PExp _ _ _) = False
1455 imp _ = True
1456-- allImp [] = False
1457 allImp xs = all imp xs
1458 constructor (TyDecl (DCon _ _) _) = True
1459 constructor _ = False
1461 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1463 vname (UN n) = True -- non qualified
1464 vname _ = False
1466aiFn inpat expat ist fc f ds as
1467 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1468aiFn inpat expat ist fc f ds as
1469 -- This is where namespaces get resolved by adding PAlternative
1470 = do let ns = lookupCtxtName f (idris_implicits ist)
1471 let nh = filter (\(n, _) -> notHidden n) ns
1472 let ns' = case trimAlts ds nh of
1473 [] -> nh
1474 x -> x
1475 case ns' of
1476 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1477 [] -> if f `elem` (map fst (idris_metavars ist))
1478 then Right $ PApp fc (PRef fc f) as
1479 else Right $ mkPApp fc (length as) (PRef fc f) as
1480 alts -> Right $
1481 PAlternative True $
1482 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1483 (insertImpl ns as)) alts
1484 where
1485 trimAlts [] alts = alts
1486 trimAlts ns alts
1487 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1489 nspace (NS _ s) = s
1490 nspace _ = []
1492 notHidden n = case getAccessibility n of
1493 Hidden -> False
1494 _ -> True
1496 getAccessibility n
1497 = case lookupDefAcc n False (tt_ctxt ist) of
1498 [(n,t)] -> t
1499 _ -> Public
1502 insertImpl :: [PArg] -> [PArg] -> [PArg]
1503 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1504 PExp p l tm : insertImpl ps given
1505 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1506 PConstraint p l tm : insertImpl ps given
1507 insertImpl (PConstraint p l ty : ps) given =
1508 PConstraint p l (PResolveTC fc) : insertImpl ps given
1509 insertImpl (PImp p _ l n ty : ps) given =
1510 case find n given [] of
1511 Just (tm, given') -> PImp p False l n tm : insertImpl ps given'
1512 Nothing -> PImp p True l n Placeholder : insertImpl ps given
1513 insertImpl (PTacImplicit p l n sc' ty : ps) given =
1514 let sc = addImpl ist sc' in
1515 case find n given [] of
1516 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1517 Nothing -> if inpat
1518 then PTacImplicit p l n sc Placeholder : insertImpl ps given
1519 else PTacImplicit p l n sc sc : insertImpl ps given
1520 insertImpl expected [] = []
1521 insertImpl _ given = given
1523 find n [] acc = Nothing
1524 find n (PImp _ _ _ n' t : gs) acc
1525 | n == n' = Just (t, reverse acc ++ gs)
1526 find n (PTacImplicit _ _ n' _ t : gs) acc
1527 | n == n' = Just (t, reverse acc ++ gs)
1528 find n (g : gs) acc = find n gs (g : acc)
1530-- replace non-linear occurrences with _
1531-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1532-- it is hard to get right!
1534stripLinear :: IState -> PTerm -> PTerm
1535stripLinear i tm = evalState (sl tm) [] where
1536 sl :: PTerm -> State [Name] PTerm
1537 sl (PRef fc f)
1538 | (_:_) <- lookupTy f (tt_ctxt i)
1539 = return $ PRef fc f
1540 | otherwise = do ns <- get
1541 if (f `elem` ns)
1542 then return Placeholder
1543 else do put (f : ns)
1544 return (PRef fc f)
1545 sl (PPatvar fc f)
1546 = do ns <- get
1547 if (f `elem` ns)
1548 then return Placeholder
1549 else do put (f : ns)
1550 return (PPatvar fc f)
1551 sl t@(PAlternative _ (a : as)) = do sl a
1552 return t
1553 sl (PApp fc fn args) = do fn' <- sl fn
1554 args' <- mapM slA args
1555 return $ PApp fc fn' args'
1556 where slA (PImp p m l n t) = do t' <- sl t
1557 return $ PImp p m l n t'
1558 slA (PExp p l t) = do t' <- sl t
1559 return $ PExp p l t'
1560 slA (PConstraint p l t)
1561 = do t' <- sl t
1562 return $ PConstraint p l t'
1563 slA (PTacImplicit p l n sc t)
1564 = do t' <- sl t
1565 return $ PTacImplicit p l n sc t'
1566 sl x = return x
1568-- Remove functions which aren't applied to anything, which must then
1569-- be resolved by unification. Assume names resolved and alternatives
1570-- filled in (so no ambiguity).
1572stripUnmatchable :: IState -> PTerm -> PTerm
1573stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1574 su :: PTerm -> PTerm
1575 su (PRef fc f)
1576 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1577 = Placeholder
1578 su (PApp fc fn args)
1579 = PApp fc fn (fmap (fmap su) args)
1580 su (PAlternative b alts)
1581 = let alts' = filter (/= Placeholder) (map su alts) in
1582 if null alts' then Placeholder
1583 else PAlternative b alts'
1584 su (PPair fc p l r) = PPair fc p (su l) (su r)
1585 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1586 su t = t
1587stripUnmatchable i tm = tm
1589mkPApp fc a f [] = f
1590mkPApp fc a f as = let rest = drop a as in
1591 appRest fc (PApp fc f (take a as)) rest
1592 where
1593 appRest fc f [] = f
1594 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1596-- Find 'static' argument positions
1597-- (the declared ones, plus any names in argument position in the declared
1598-- statics)
1599-- FIXME: It's possible that this really has to happen after elaboration
1601findStatics :: IState -> PTerm -> (PTerm, [Bool])
1602findStatics ist tm = trace (show tm) $
1603 let (ns, ss) = fs tm in
1604 runState (pos ns ss tm) []
1605 where fs (PPi p n t sc)
1606 | Static <- pstatic p
1607 = let (ns, ss) = fs sc in
1608 (namesIn [] ist t : ns, n : ss)
1609 | otherwise = let (ns, ss) = fs sc in
1610 (ns, ss)
1611 fs _ = ([], [])
1613 inOne n ns = length (filter id (map (elem n) ns)) == 1
1615 pos ns ss (PPi p n t sc)
1616 | elem n ss = do sc' <- pos ns ss sc
1617 spos <- get
1618 put (True : spos)
1619 return (PPi (p { pstatic = Static }) n t sc')
1620 | otherwise = do sc' <- pos ns ss sc
1621 spos <- get
1622 put (False : spos)
1623 return (PPi p n t sc')
1624 pos ns ss t = return t
1626-- for 6.12/7 compatibility
1627data EitherErr a b = LeftErr a | RightOK b
1629instance Monad (EitherErr a) where
1630 return = RightOK
1632 (LeftErr e) >>= k = LeftErr e
1633 RightOK v >>= k = k v
1635toEither (LeftErr e) = Left e
1636toEither (RightOK ho) = Right ho
1638-- syntactic match of a against b, returning pair of variables in a
1639-- and what they match. Returns the pair that failed if not a match.
1641matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1642matchClause = matchClause' False
1644matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1645matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1646 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1648 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1649 fullApp x = x
1651 match' x y = match (fullApp x) (fullApp y)
1652 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1653 | fi == txt "fromInteger" && b == txt "builtins",
1654 PConstant (I _) <- getTm x = match (getTm x) x'
1655 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1656 | fi == txt "fromInteger" && b == txt "builtins",
1657 PConstant (I _) <- getTm x = match (getTm x) x'
1658 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1659 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1660 match (PApp _ f args) (PApp _ f' args')
1661 | length args == length args'
1662 = do mf <- match' f f'
1663 ms <- zipWithM matchArg args args'
1664 return (mf ++ concat ms)
1665-- match (PRef _ n) (PRef _ n') | n == n' = return []
1666-- | otherwise = Nothing
1667 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1668 match (PPatvar f n) xr = match (PRef f n) xr
1669 match xr (PPatvar f n) = match xr (PRef f n)
1670 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1671 match (PRef _ n) tm@(PRef _ n')
1672 | n == n' && not names &&
1673 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1674 || tm == Placeholder)
1675 = return [(n, tm)]
1676 | n == n' = return []
1677 match (PRef _ n) tm
1678 | not names && (not (isConName n (tt_ctxt i) ||
1679 isFnName n (tt_ctxt i)) || tm == Placeholder)
1680 = return [(n, tm)]
1681 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1682 mr <- match' r r'
1683 return (ml ++ mr)
1684 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1685 = do ml <- match' l l'
1686 mr <- match' r r'
1687 return (ml ++ mr)
1688 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1689 mr <- match r r'
1690 return (ml ++ mr)
1691 match (PTyped l r) x = match l x
1692 match x (PTyped l r) = match x l
1693 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1694 mr <- match' r r'
1695 return (ml ++ mr)
1696 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1697 mt <- match' t t'
1698 mr <- match' r r'
1699 return (ml ++ mt ++ mr)
1700 match (PAlternative a as) (PAlternative a' as')
1701 = do ms <- zipWithM match' as as'
1702 return (concat ms)
1703 match a@(PAlternative _ as) b
1704 = do let ms = zipWith match' as (repeat b)
1705 case (rights (map toEither ms)) of
1706 (x: _) -> return x
1707 _ -> LeftErr (a, b)
1708 match (PCase _ _ _) _ = return [] -- lifted out
1709 match (PMetavar _) _ = return [] -- modified
1710 match (PInferRef _ _) _ = return [] -- modified
1711 match (PQuote _) _ = return []
1712 match (PProof _) _ = return []
1713 match (PTactics _) _ = return []
1714 match (PRefl _ _) (PRefl _ _) = return []
1715 match (PResolveTC _) (PResolveTC _) = return []
1716 match (PTrue _ _) (PTrue _ _) = return []
1717 match (PFalse _) (PFalse _) = return []
1718 match (PReturn _) (PReturn _) = return []
1719 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1720 ms <- match' s s'
1721 return (mt ++ ms)
1722 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1723 ms <- match' s s'
1724 return (mt ++ ms)
1725 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1726 mty <- match' ty ty'
1727 ms <- match' s s'
1728 return (mt ++ mty ++ ms)
1729 match (PHidden x) (PHidden y) = match' x y
1730 match (PUnifyLog x) y = match' x y
1731 match x (PUnifyLog y) = match' x y
1732 match (PNoImplicits x) y = match' x y
1733 match x (PNoImplicits y) = match' x y
1734 match Placeholder _ = return []
1735 match _ Placeholder = return []
1736 match (PResolveTC _) _ = return []
1737 match a b | a == b = return []
1738 | otherwise = LeftErr (a, b)
1740 checkRpts (RightOK ms) = check ms where
1741 check ((n,t):xs)
1742 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1743 then Left (t, t')
1744 else check xs
1745 check (_:xs) = check xs
1746 check [] = Right ms
1747 checkRpts (LeftErr x) = Left x
1749substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1750substMatches ms = substMatchesShadow ms []
1752substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1753substMatchesShadow [] shs t = t
1754substMatchesShadow ((n,tm):ns) shs t
1755 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1757substMatch :: Name -> PTerm -> PTerm -> PTerm
1758substMatch n = substMatchShadow n []
1760substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1761substMatchShadow n shs tm t = sm shs t where
1762 sm xs (PRef _ n') | n == n' = tm
1763 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1764 sm xs (PPi p x t sc)
1765 | x `elem` xs
1766 = let x' = nextName x in
1767 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1768 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1769 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1770 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1771 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1772 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1773 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1774 (fmap (sm xs) tm)
1775 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1776 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1777 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1778 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1779 sm xs (PHidden x) = PHidden (sm xs x)
1780 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1781 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1782 sm xs x = x
1784 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1785 fullApp x = x
1787shadow :: Name -> Name -> PTerm -> PTerm
1788shadow n n' t = sm t where
1789 sm (PRef fc x) | n == x = PRef fc n'
1790 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1791 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1792 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1793 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1794 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1795 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1796 sm (PEq f x y) = PEq f (sm x) (sm y)
1797 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1798 sm (PTyped x y) = PTyped (sm x) (sm y)
1799 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1800 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1801 sm (PAlternative a as) = PAlternative a (map sm as)
1802 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1803 sm (PProof ts) = PProof (map (fmap sm) ts)
1804 sm (PHidden x) = PHidden (sm x)
1805 sm (PUnifyLog x) = PUnifyLog (sm x)
1806 sm (PNoImplicits x) = PNoImplicits (sm x)
1807 sm x = x
1809-- Rename any binders which are repeated (so that we don't have to mess
1810-- about with shadowing anywhere else).
1812mkUniqueNames :: [Name] -> PTerm -> PTerm
1813mkUniqueNames env tm = evalState (mkUniq tm) env where
1814 inScope = boundNamesIn tm
1816 mkUniqA arg = do t' <- mkUniq (getTm arg)
1817 return (arg { getTm = t' })
1819 -- FIXME: Probably ought to do this for completeness! It's fine as
1820 -- long as there are no bindings inside tactics though.
1821 mkUniqT tac = return tac
1823 mkUniq :: PTerm -> State [Name] PTerm
1824 mkUniq (PLam n ty sc)
1825 = do env <- get
1826 (n', sc') <-
1827 if n `elem` env
1828 then do let n' = uniqueName n (env ++ inScope)
1829 return (n', shadow n n' sc)
1830 else return (n, sc)
1831 put (n' : env)
1832 ty' <- mkUniq ty
1833 sc'' <- mkUniq sc'
1834 return $! PLam n' ty' sc''
1835 mkUniq (PPi p n ty sc)
1836 = do env <- get
1837 (n', sc') <-
1838 if n `elem` env
1839 then do let n' = uniqueName n (env ++ inScope)
1840 return (n', shadow n n' sc)
1841 else return (n, sc)
1842 put (n' : env)
1843 ty' <- mkUniq ty
1844 sc'' <- mkUniq sc'
1845 return $! PPi p n' ty' sc''
1846 mkUniq (PLet n ty val sc)
1847 = do env <- get
1848 (n', sc') <-
1849 if n `elem` env
1850 then do let n' = uniqueName n (env ++ inScope)
1851 return (n', shadow n n' sc)
1852 else return (n, sc)
1853 put (n' : env)
1854 ty' <- mkUniq ty; val' <- mkUniq val
1855 sc'' <- mkUniq sc'
1856 return $! PLet n' ty' val' sc''
1857 mkUniq (PApp fc t args)
1858 = do t' <- mkUniq t
1859 args' <- mapM mkUniqA args
1860 return $! PApp fc t' args'
1861 mkUniq (PAppBind fc t args)
1862 = do t' <- mkUniq t
1863 args' <- mapM mkUniqA args
1864 return $! PAppBind fc t' args'
1865 mkUniq (PCase fc t alts)
1866 = do t' <- mkUniq t
1867 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1868 return (x', y')) alts
1869 return $! PCase fc t' alts'
1870 mkUniq (PPair fc p l r)
1871 = do l' <- mkUniq l; r' <- mkUniq r
1872 return $! PPair fc p l' r'
1873 mkUniq (PDPair fc p (PRef fc' n) t sc)
1874 | t /= Placeholder
1875 = do env <- get
1876 (n', sc') <- if n `elem` env
1877 then do let n' = uniqueName n (env ++ inScope)
1878 return (n', shadow n n' sc)
1879 else return (n, sc)
1880 put (n' : env)
1881 t' <- mkUniq t
1882 sc'' <- mkUniq sc'
1883 return $! PDPair fc p (PRef fc' n') t' sc''
1884 mkUniq (PDPair fc p l t r)
1885 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1886 return $! PDPair fc p l' t' r'
1887 mkUniq (PAlternative b as)
1888 = liftM (PAlternative b) (mapM mkUniq as)
1889 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1890 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1891 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1892 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1893 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1894 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1895 mkUniq t = return t