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