git.iko.soy/Idris-dev
on c87350c 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 hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.State
23import Control.Monad.Error(throwError)
25import Data.List
26import Data.Char
27import qualified Data.Text as T
28import Data.Either
29import qualified Data.Map as M
30import Data.Maybe
31import qualified Data.Set as S
32import Data.Word (Word)
34import Debug.Trace
36import Control.Monad.Error (throwError, catchError)
37import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
39import Util.Pretty
40import Util.ScreenSize
41import Util.System
43getContext :: Idris Context
44getContext = do i <- getIState; return (tt_ctxt i)
46forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
49getObjectFiles :: Codegen -> Idris [FilePath]
50getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
52addObjectFile :: Codegen -> FilePath -> Idris ()
53addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
55getLibs :: Codegen -> Idris [String]
56getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
58addLib :: Codegen -> String -> Idris ()
59addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
61getFlags :: Codegen -> Idris [String]
62getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
64addFlag :: Codegen -> String -> Idris ()
65addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
67addDyLib :: [String] -> Idris (Either DynamicLib String)
68addDyLib libs = do i <- getIState
69 let ls = idris_dynamic_libs i
70 let importdirs = opt_importdirs (idris_options i)
71 case mapMaybe (findDyLib ls) libs of
72 x:_ -> return (Left x)
73 [] -> do
74 handle <- lift . lift .
75 mapM (\l -> catchIO (tryLoadLib importdirs l)
76 (\_ -> return Nothing)) $ libs
77 case msum handle of
78 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
79 concat (intersperse "," libs) ++ "\"")
80 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
81 return (Left x)
82 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
83 findDyLib [] l = Nothing
84 findDyLib (lib:libs) l | l == lib_name lib = Just lib
85 | otherwise = findDyLib libs l
88addHdr :: Codegen -> String -> Idris ()
89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
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 -- Just the args, fn isn't matchable as a var
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