git.iko.soy/Idris-dev
on e1f139a help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2137 lines 91 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.IdeMode hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import System.Console.Haskeline
18import System.IO
20import Control.Applicative
21import Control.Monad.State
23import Data.List hiding (insert,union)
24import Data.Char
25import qualified Data.Text as T
26import Data.Either
27import qualified Data.Map as M
28import Data.Maybe
29import qualified Data.Set as S
30import Data.Word (Word)
32import Debug.Trace
34import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
36import Util.Pretty
37import Util.ScreenSize
38import Util.System
40getContext :: Idris Context
41getContext = do i <- getIState; return (tt_ctxt i)
43forCodegen :: Codegen -> [(Codegen, a)] -> [a]
44forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
46getObjectFiles :: Codegen -> Idris [FilePath]
47getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
49addObjectFile :: Codegen -> FilePath -> Idris ()
50addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
52getLibs :: Codegen -> Idris [String]
53getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
55addLib :: Codegen -> String -> Idris ()
56addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
58getFlags :: Codegen -> Idris [String]
59getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
61addFlag :: Codegen -> String -> Idris ()
62addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
64addDyLib :: [String] -> Idris (Either DynamicLib String)
65addDyLib libs = do i <- getIState
66 let ls = idris_dynamic_libs i
67 let importdirs = opt_importdirs (idris_options i)
68 case mapMaybe (findDyLib ls) libs of
69 x:_ -> return (Left x)
70 [] -> do
71 handle <- lift . lift .
72 mapM (\l -> catchIO (tryLoadLib importdirs l)
73 (\_ -> return Nothing)) $ libs
74 case msum handle of
75 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
76 concat (intersperse "," libs) ++ "\"")
77 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
78 return (Left x)
79 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
80 findDyLib [] l = Nothing
81 findDyLib (lib:libs) l | l == lib_name lib = Just lib
82 | otherwise = findDyLib libs l
84getAutoImports :: Idris [FilePath]
85getAutoImports = do i <- getIState
86 return (opt_autoImport (idris_options i))
88addAutoImport :: FilePath -> Idris ()
89addAutoImport fp = do i <- getIState
90 let opts = idris_options i
91 let autoimps = opt_autoImport opts
92 put (i { idris_options = opts { opt_autoImport =
93 fp : opt_autoImport opts } } )
95addHdr :: Codegen -> String -> Idris ()
96addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
98addImported :: Bool -> FilePath -> Idris ()
99addImported pub f
100 = do i <- getIState
101 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }
103addLangExt :: LanguageExt -> Idris ()
104addLangExt TypeProviders = do i <- getIState
105 putIState $ i {
106 idris_language_extensions = TypeProviders : idris_language_extensions i
107 }
108addLangExt ErrorReflection = do i <- getIState
109 putIState $ i {
110 idris_language_extensions = ErrorReflection : idris_language_extensions i
111 }
113-- Transforms are organised by the function being applied on the lhs of the
114-- transform, to make looking up appropriate transforms quicker
115addTrans :: Name -> (Term, Term) -> Idris ()
116addTrans basefn t
117 = do i <- getIState
118 let t' = case lookupCtxtExact basefn (idris_transforms i) of
119 Just def -> (t : def)
120 Nothing -> [t]
121 putIState $ i { idris_transforms = addDef basefn t'
122 (idris_transforms i) }
124addErrRev :: (Term, Term) -> Idris ()
125addErrRev t = do i <- getIState
126 putIState $ i { idris_errRev = t : idris_errRev i }
128addErasureUsage :: Name -> Int -> Idris ()
129addErasureUsage n i = do ist <- getIState
130 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
132addExport :: Name -> Idris ()
133addExport n = do ist <- getIState
134 putIState $ ist { idris_exports = n : idris_exports ist }
136addUsedName :: FC -> Name -> Name -> Idris ()
137addUsedName fc n arg
138 = do ist <- getIState
139 case lookupTyName n (tt_ctxt ist) of
140 [(n', ty)] -> addUsage n' 0 ty
141 [] -> throwError (At fc (NoSuchVariable n))
142 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
143 where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
144 addErasureUsage n i
145 | otherwise = addUsage n (i + 1) sc
146 addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
148getErasureUsage :: Idris [(Name, Int)]
149getErasureUsage = do ist <- getIState;
150 return (idris_erasureUsed ist)
152getExports :: Idris [Name]
153getExports = do ist <- getIState
154 return (idris_exports ist)
156totcheck :: (FC, Name) -> Idris ()
157totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
159defer_totcheck :: (FC, Name) -> Idris ()
160defer_totcheck n
161 = do i <- getIState;
162 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
164clear_totcheck :: Idris ()
165clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
167setFlags :: Name -> [FnOpt] -> Idris ()
168setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
170setFnInfo :: Name -> FnInfo -> Idris ()
171setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
173setAccessibility :: Name -> Accessibility -> Idris ()
174setAccessibility n a
175 = do i <- getIState
176 let ctxt = setAccess n a (tt_ctxt i)
177 putIState $ i { tt_ctxt = ctxt }
179setTotality :: Name -> Totality -> Idris ()
180setTotality n a
181 = do i <- getIState
182 let ctxt = setTotal n a (tt_ctxt i)
183 putIState $ i { tt_ctxt = ctxt }
185getTotality :: Name -> Idris Totality
186getTotality n
187 = do i <- getIState
188 case lookupTotal n (tt_ctxt i) of
189 [t] -> return t
190 _ -> return (Total [])
192-- Get coercions which might return the required type
193getCoercionsTo :: IState -> Type -> [Name]
194getCoercionsTo i ty =
195 let cs = idris_coercions i
196 (fn,_) = unApply (getRetTy ty) in
197 findCoercions fn cs
198 where findCoercions t [] = []
199 findCoercions t (n : ns) =
200 let ps = case lookupTy n (tt_ctxt i) of
201 [ty'] -> case unApply (getRetTy ty') of
202 (t', _) ->
203 if t == t' then [n] else []
204 _ -> [] in
205 ps ++ findCoercions t ns
207addToCG :: Name -> CGInfo -> Idris ()
208addToCG n cg
209 = do i <- getIState
210 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
212addTyInferred :: Name -> Idris ()
213addTyInferred n
214 = do i <- getIState
215 putIState $ i { idris_tyinfodata =
216 addDef n TIPartial (idris_tyinfodata i) }
218addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
219addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
220 mapM_ addConstraint ts
221 return ()
222 where addConstraint (x, y) = findMVApps x y
224 findMVApps x y
225 = do let (fx, argsx) = unApply x
226 let (fy, argsy) = unApply y
227 if (not (fx == fy))
228 then do
229 tryAddMV fx y
230 tryAddMV fy x
231 else mapM_ addConstraint (zip argsx argsy)
233 tryAddMV (P _ mv _) y =
234 do ist <- get
235 case lookup mv (idris_metavars ist) of
236 Just _ -> addConstraintRule mv y
237 _ -> return ()
238 tryAddMV _ _ = return ()
240 addConstraintRule :: Name -> Term -> Idris ()
241 addConstraintRule n t
242 = do ist <- get
243 logLvl 1 $ "TI constraint: " ++ show (n, t)
244 case lookupCtxt n (idris_tyinfodata ist) of
245 [TISolution ts] ->
246 do mapM_ (checkConsistent t) ts
247 let ti' = addDef n (TISolution (t : ts))
248 (idris_tyinfodata ist)
249 put $ ist { idris_tyinfodata = ti' }
250 _ ->
251 do let ti' = addDef n (TISolution [t])
252 (idris_tyinfodata ist)
253 put $ ist { idris_tyinfodata = ti' }
255 -- Check a solution is consistent with previous solutions
256 -- Meaning: If heads are both data types, they had better be the
257 -- same.
258 checkConsistent :: Term -> Term -> Idris ()
259 checkConsistent x y =
260 do let (fx, _) = unApply x
261 let (fy, _) = unApply y
262 case (fx, fy) of
263 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
264 (P (TCon _ _) n _, Constant _) -> errWhen True
265 (Constant _, P (TCon _ _) n' _) -> errWhen True
266 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
267 _ -> return ()
269 where errWhen True
270 = throwError (At fc
271 (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
272 errWhen False = return ()
274isTyInferred :: Name -> Idris Bool
275isTyInferred n
276 = do i <- getIState
277 case lookupCtxt n (idris_tyinfodata i) of
278 [TIPartial] -> return True
279 _ -> return False
281-- | Adds error handlers for a particular function and argument. If names are
282-- ambiguous, all matching handlers are updated.
283addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
284addFunctionErrorHandlers f arg hs =
285 do i <- getIState
286 let oldHandlers = idris_function_errorhandlers i
287 let newHandlers = flip (addDef f) oldHandlers $
288 case lookupCtxtExact f oldHandlers of
289 Nothing -> M.singleton arg (S.fromList hs)
290 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
291 -- will always be one of those two, thus no extra case
292 putIState $ i { idris_function_errorhandlers = newHandlers }
294getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
295getFunctionErrorHandlers f arg = do i <- getIState
296 return . maybe [] S.toList $
297 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
300-- Trace all the names in a call graph starting at the given name
301getAllNames :: Name -> Idris [Name]
302getAllNames n = allNames [] n
304allNames :: [Name] -> Name -> Idris [Name]
305allNames ns n | n `elem` ns = return []
306allNames ns n = do i <- getIState
307 case lookupCtxtExact n (idris_callgraph i) of
308 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
309 return (nub (n : concat more))
310 _ -> return [n]
312addCoercion :: Name -> Idris ()
313addCoercion n = do i <- getIState
314 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
316addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
317addDocStr n doc args
318 = do i <- getIState
319 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
321addNameHint :: Name -> Name -> Idris ()
322addNameHint ty n
323 = do i <- getIState
324 ty' <- case lookupCtxtName ty (idris_implicits i) of
325 [(tyn, _)] -> return tyn
326 [] -> throwError (NoSuchVariable ty)
327 tyns -> throwError (CantResolveAlts (map fst tyns))
328 let ns' = case lookupCtxt ty' (idris_namehints i) of
329 [ns] -> ns ++ [n]
330 _ -> [n]
331 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
333getNameHints :: IState -> Name -> [Name]
334getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
335getNameHints i n =
336 case lookupCtxt n (idris_namehints i) of
337 [ns] -> ns
338 _ -> []
340-- Issue #1737 in the Issue Tracker.
341-- https://github.com/idris-lang/Idris-dev/issues/1737
342addToCalledG :: Name -> [Name] -> Idris ()
343addToCalledG n ns = return () -- TODO
345push_estack :: Name -> Idris ()
346push_estack n = do i <- getIState
347 putIState (i { elab_stack = n : elab_stack i })
349pop_estack :: Idris ()
350pop_estack = do i <- getIState
351 putIState (i { elab_stack = ptail (elab_stack i) })
352 where ptail [] = []
353 ptail (x : xs) = xs
355-- Add a class instance function. Dodgy hack: Put integer instances first in the
356-- list so they are resolved by default.
357-- Dodgy hack 2: put constraint chasers (@@) last
359addInstance :: Bool -> Name -> Name -> Idris ()
360addInstance int n i
361 = do ist <- getIState
362 case lookupCtxt n (idris_classes ist) of
363 [CI a b c d e ins fds] ->
364 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)
365 putIState $ ist { idris_classes = cs }
366 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i] []) (idris_classes ist)
367 putIState $ ist { idris_classes = cs }
368 where addI i ins | int = i : ins
369 | chaser n = ins ++ [i]
370 | otherwise = insI i ins
371 insI i [] = [i]
372 insI i (n : ns) | chaser n = i : n : ns
373 | otherwise = n : insI i ns
375 chaser (UN nm)
376 | ('@':'@':_) <- str nm = True
377 chaser (NS n _) = chaser n
378 chaser _ = False
380addClass :: Name -> ClassInfo -> Idris ()
381addClass n i
382 = do ist <- getIState
383 let i' = case lookupCtxt n (idris_classes ist) of
384 [c] -> c { class_instances = class_instances i }
385 _ -> i
386 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
388addIBC :: IBCWrite -> Idris ()
389addIBC ibc@(IBCDef n)
390 = do i <- getIState
391 when (notDef (ibc_write i)) $
392 putIState $ i { ibc_write = ibc : ibc_write i }
393 where notDef [] = True
394 notDef (IBCDef n': is) | n == n' = False
395 notDef (_ : is) = notDef is
396addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
398clearIBC :: Idris ()
399clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
401resetNameIdx :: Idris ()
402resetNameIdx = do i <- getIState
403 put (i { idris_nameIdx = (0, emptyContext) })
405-- Used to preserve sharing of names
406addNameIdx :: Name -> Idris (Int, Name)
407addNameIdx n = do i <- getIState
408 let (i', x) = addNameIdx' i n
409 putIState i'
410 return x
412addNameIdx' :: IState -> Name -> (IState, (Int, Name))
413addNameIdx' i n
414 = let idxs = snd (idris_nameIdx i) in
415 case lookupCtxt n idxs of
416 [x] -> (i, x)
417 _ -> let i' = fst (idris_nameIdx i) + 1 in
418 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
420getSymbol :: Name -> Idris Name
421getSymbol n = do i <- getIState
422 case M.lookup n (idris_symbols i) of
423 Just n' -> return n'
424 Nothing -> do let sym' = M.insert n n (idris_symbols i)
425 put (i { idris_symbols = sym' })
426 return n
428getHdrs :: Codegen -> Idris [String]
429getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
431getImported :: Idris [(FilePath, Bool)]
432getImported = do i <- getIState; return (idris_imported i)
434setErrSpan :: FC -> Idris ()
435setErrSpan x = do i <- getIState;
436 case (errSpan i) of
437 Nothing -> putIState $ i { errSpan = Just x }
438 Just _ -> return ()
440clearErr :: Idris ()
441clearErr = do i <- getIState
442 putIState $ i { errSpan = Nothing }
444getSO :: Idris (Maybe String)
445getSO = do i <- getIState
446 return (compiled_so i)
448setSO :: Maybe String -> Idris ()
449setSO s = do i <- getIState
450 putIState $ (i { compiled_so = s })
452getIState :: Idris IState
453getIState = get
455putIState :: IState -> Idris ()
456putIState = put
458updateIState :: (IState -> IState) -> Idris ()
459updateIState f = do i <- getIState
460 putIState $ f i
462withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
463withContext ctx name dflt action = do
464 ist <- getIState
465 case lookupCtxt name (ctx ist) of
466 [x] -> action x
467 _ -> return dflt
469withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
470withContext_ ctx name action = withContext ctx name () action
472-- | A version of liftIO that puts errors into the exception type of the Idris monad
473runIO :: IO a -> Idris a
474runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
475-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
476--
477-- Issue #1738 on the issue tracker.
478-- https://github.com/idris-lang/Idris-dev/issues/1738
480getName :: Idris Int
481getName = do i <- getIState;
482 let idx = idris_name i;
483 putIState $ (i { idris_name = idx + 1 })
484 return idx
486-- InternalApp keeps track of the real function application for making case splits from, not the application the
487-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
488addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
489addInternalApp fp l t
490 = do i <- getIState
491 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
493getInternalApp :: FilePath -> Int -> Idris PTerm
494getInternalApp fp l = do i <- getIState
495 case lookup (fp, l) (idris_lineapps i) of
496 Just n' -> return n'
497 Nothing -> return Placeholder
498 -- TODO: What if it's not there?
500-- Pattern definitions are only used for coverage checking, so erase them
501-- when we're done
502clearOrigPats :: Idris ()
503clearOrigPats = do i <- get
504 let ps = idris_patdefs i
505 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
506 put (i { idris_patdefs = ps' })
508-- Erase types from Ps in the context (basically ending up with what's in
509-- the .ibc, which is all we need after all the analysis is done)
510clearPTypes :: Idris ()
511clearPTypes = do i <- get
512 let ctxt = tt_ctxt i
513 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
514 where pErase (CaseOp c t tys orig tot cds)
515 = CaseOp c t tys orig [] (pErase' cds)
516 pErase x = x
517 pErase' (CaseDefs _ (cs, c) _ rs)
518 = let c' = (cs, fmap pEraseType c) in
519 CaseDefs c' c' c' rs
521checkUndefined :: FC -> Name -> Idris ()
522checkUndefined fc n
523 = do i <- getContext
524 case lookupTy n i of
525 (_:_) -> throwError . Msg $ show fc ++ ":" ++
526 show n ++ " already defined"
527 _ -> return ()
529isUndefined :: FC -> Name -> Idris Bool
530isUndefined fc n
531 = do i <- getContext
532 case lookupTyExact n i of
533 Just _ -> return False
534 _ -> return True
536setContext :: Context -> Idris ()
537setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
539updateContext :: (Context -> Context) -> Idris ()
540updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
542addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
543addConstraints fc (v, cs)
544 = do i <- getIState
545 let ctxt = tt_ctxt i
546 let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,
547 next_tvar = v }
548 let ics = zip cs (repeat fc) ++ idris_constraints i
549 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
551addDeferred = addDeferred' Ref
552addDeferredTyCon = addDeferred' (TCon 0 0)
554-- | Save information about a name that is not yet defined
555addDeferred' :: NameType
556 -> [(Name, (Int, Maybe Name, Type, Bool))]
557 -- ^ The Name is the name being made into a metavar,
558 -- the Int is the number of vars that are part of a
559 -- putative proof context, the Maybe Name is the
560 -- top-level function containing the new metavariable,
561 -- the Type is its type, and the Bool is whether :p is
562 -- allowed
563 -> Idris ()
564addDeferred' nt ns
565 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
566 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
567 i <- getIState
568 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
569 idris_metavars i }
570 where
571 -- 'tidyNames' is to generate user accessible names in case they are
572 -- needed in tactic scripts
573 tidyNames used (Bind (MN i x) b sc)
574 = let n' = uniqueNameSet (UN x) used in
575 Bind n' b $ tidyNames (S.insert n' used) sc
576 tidyNames used (Bind n b sc)
577 = let n' = uniqueNameSet n used in
578 Bind n' b $ tidyNames (S.insert n' used) sc
579 tidyNames used b = b
581solveDeferred :: Name -> Idris ()
582solveDeferred n = do i <- getIState
583 putIState $ i { idris_metavars =
584 filter (\(n', _) -> n/=n')
585 (idris_metavars i),
586 ibc_write =
587 filter (notMV n) (ibc_write i)
588 }
589 where notMV n (IBCMetavar n') = not (n == n')
590 notMV n _ = True
592getUndefined :: Idris [Name]
593getUndefined = do i <- getIState
594 return (map fst (idris_metavars i) \\ primDefs)
596isMetavarName :: Name -> IState -> Bool
597isMetavarName n ist
598 = case lookupNames n (tt_ctxt ist) of
599 (t:_) -> isJust $ lookup t (idris_metavars ist)
600 _ -> False
602getWidth :: Idris ConsoleWidth
603getWidth = fmap idris_consolewidth getIState
605setWidth :: ConsoleWidth -> Idris ()
606setWidth w = do ist <- getIState
607 put ist { idris_consolewidth = w }
609renderWidth :: Idris Int
610renderWidth = do iw <- getWidth
611 case iw of
612 InfinitelyWide -> return 100000000
613 ColsWide n -> return (max n 1)
614 AutomaticWidth -> runIO getScreenWidth
618type1Doc :: Doc OutputAnnotation
619type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
622isetPrompt :: String -> Idris ()
623isetPrompt p = do i <- getIState
624 case idris_outputmode i of
625 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
627-- | Tell clients how much was parsed and loaded
628isetLoadedRegion :: Idris ()
629isetLoadedRegion = do i <- getIState
630 let span = idris_parsedSpan i
631 case span of
632 Just fc ->
633 case idris_outputmode i of
634 IdeMode n h ->
635 runIO . hPutStrLn h $
636 convSExp "set-loaded-region" fc n
637 Nothing -> return ()
639setLogLevel :: Int -> Idris ()
640setLogLevel l = do i <- getIState
641 let opts = idris_options i
642 let opt' = opts { opt_logLevel = l }
643 putIState $ i { idris_options = opt' }
645setCmdLine :: [Opt] -> Idris ()
646setCmdLine opts = do i <- getIState
647 let iopts = idris_options i
648 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
650getCmdLine :: Idris [Opt]
651getCmdLine = do i <- getIState
652 return (opt_cmdline (idris_options i))
654getDumpDefun :: Idris (Maybe FilePath)
655getDumpDefun = do i <- getIState
656 return $ findC (opt_cmdline (idris_options i))
657 where findC [] = Nothing
658 findC (DumpDefun x : _) = Just x
659 findC (_ : xs) = findC xs
661getDumpCases :: Idris (Maybe FilePath)
662getDumpCases = do i <- getIState
663 return $ findC (opt_cmdline (idris_options i))
664 where findC [] = Nothing
665 findC (DumpCases x : _) = Just x
666 findC (_ : xs) = findC xs
668logLevel :: Idris Int
669logLevel = do i <- getIState
670 return (opt_logLevel (idris_options i))
672setErrContext :: Bool -> Idris ()
673setErrContext t = do i <- getIState
674 let opts = idris_options i
675 let opts' = opts { opt_errContext = t }
676 putIState $ i { idris_options = opts' }
678errContext :: Idris Bool
679errContext = do i <- getIState
680 return (opt_errContext (idris_options i))
682getOptimise :: Idris [Optimisation]
683getOptimise = do i <- getIState
684 return (opt_optimise (idris_options i))
686setOptimise :: [Optimisation] -> Idris ()
687setOptimise newopts = do i <- getIState
688 let opts = idris_options i
689 let opts' = opts { opt_optimise = newopts }
690 putIState $ i { idris_options = opts' }
692addOptimise :: Optimisation -> Idris ()
693addOptimise opt = do opts <- getOptimise
694 setOptimise (nub (opt : opts))
696removeOptimise :: Optimisation -> Idris ()
697removeOptimise opt = do opts <- getOptimise
698 setOptimise ((nub opts) \\ [opt])
700-- Set appropriate optimisation set for the given level. We only have
701-- one optimisation that is configurable at the moment, however!
702setOptLevel :: Int -> Idris ()
703setOptLevel n | n <= 0 = setOptimise []
704setOptLevel 1 = setOptimise []
705setOptLevel 2 = setOptimise [PETransform]
706setOptLevel n | n >= 3 = setOptimise [PETransform]
708useREPL :: Idris Bool
709useREPL = do i <- getIState
710 return (opt_repl (idris_options i))
712setREPL :: Bool -> Idris ()
713setREPL t = do i <- getIState
714 let opts = idris_options i
715 let opt' = opts { opt_repl = t }
716 putIState $ i { idris_options = opt' }
718showOrigErr :: Idris Bool
719showOrigErr = do i <- getIState
720 return (opt_origerr (idris_options i))
722setShowOrigErr :: Bool -> Idris ()
723setShowOrigErr b = do i <- getIState
724 let opts = idris_options i
725 let opt' = opts { opt_origerr = b }
726 putIState $ i { idris_options = opt' }
728setAutoSolve :: Bool -> Idris ()
729setAutoSolve b = do i <- getIState
730 let opts = idris_options i
731 let opt' = opts { opt_autoSolve = b }
732 putIState $ i { idris_options = opt' }
734setNoBanner :: Bool -> Idris ()
735setNoBanner n = do i <- getIState
736 let opts = idris_options i
737 let opt' = opts { opt_nobanner = n }
738 putIState $ i { idris_options = opt' }
740getNoBanner :: Idris Bool
741getNoBanner = do i <- getIState
742 let opts = idris_options i
743 return (opt_nobanner opts)
745setQuiet :: Bool -> Idris ()
746setQuiet q = do i <- getIState
747 let opts = idris_options i
748 let opt' = opts { opt_quiet = q }
749 putIState $ i { idris_options = opt' }
751getQuiet :: Idris Bool
752getQuiet = do i <- getIState
753 let opts = idris_options i
754 return (opt_quiet opts)
756setCodegen :: Codegen -> Idris ()
757setCodegen t = do i <- getIState
758 let opts = idris_options i
759 let opt' = opts { opt_codegen = t }
760 putIState $ i { idris_options = opt' }
762codegen :: Idris Codegen
763codegen = do i <- getIState
764 return (opt_codegen (idris_options i))
766setOutputTy :: OutputType -> Idris ()
767setOutputTy t = do i <- getIState
768 let opts = idris_options i
769 let opt' = opts { opt_outputTy = t }
770 putIState $ i { idris_options = opt' }
772outputTy :: Idris OutputType
773outputTy = do i <- getIState
774 return $ opt_outputTy $ idris_options i
776setIdeMode :: Bool -> Handle -> Idris ()
777setIdeMode True h = do i <- getIState
778 putIState $ i { idris_outputmode = IdeMode 0 h
779 , idris_colourRepl = False
780 }
781setIdeMode False _ = return ()
783setTargetTriple :: String -> Idris ()
784setTargetTriple t = do i <- getIState
785 let opts = idris_options i
786 opt' = opts { opt_triple = t }
787 putIState $ i { idris_options = opt' }
789targetTriple :: Idris String
790targetTriple = do i <- getIState
791 return (opt_triple (idris_options i))
793setTargetCPU :: String -> Idris ()
794setTargetCPU t = do i <- getIState
795 let opts = idris_options i
796 opt' = opts { opt_cpu = t }
797 putIState $ i { idris_options = opt' }
799targetCPU :: Idris String
800targetCPU = do i <- getIState
801 return (opt_cpu (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 = nub $ 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 }
867impShow :: Idris Bool
868impShow = do i <- getIState
869 return (opt_showimp (idris_options i))
871setImpShow :: Bool -> Idris ()
872setImpShow t = do i <- getIState
873 let opts = idris_options i
874 let opt' = opts { opt_showimp = t }
875 putIState $ i { idris_options = opt' }
877setColour :: ColourType -> IdrisColour -> Idris ()
878setColour ct c = do i <- getIState
879 let newTheme = setColour' ct c (idris_colourTheme i)
880 putIState $ i { idris_colourTheme = newTheme }
881 where setColour' KeywordColour c t = t { keywordColour = c }
882 setColour' BoundVarColour c t = t { boundVarColour = c }
883 setColour' ImplicitColour c t = t { implicitColour = c }
884 setColour' FunctionColour c t = t { functionColour = c }
885 setColour' TypeColour c t = t { typeColour = c }
886 setColour' DataColour c t = t { dataColour = c }
887 setColour' PromptColour c t = t { promptColour = c }
888 setColour' PostulateColour c t = t { postulateColour = c }
890logLvl :: Int -> String -> Idris ()
891logLvl l str = do i <- getIState
892 let lvl = opt_logLevel (idris_options i)
893 when (lvl >= l) $
894 case idris_outputmode i of
895 RawOutput h -> do runIO $ hPutStrLn h str
896 IdeMode n h ->
897 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
898 runIO . hPutStrLn h $ convSExp "log" good n
900cmdOptType :: Opt -> Idris Bool
901cmdOptType x = do i <- getIState
902 return $ x `elem` opt_cmdline (idris_options i)
904iLOG :: String -> Idris ()
905iLOG = logLvl 1
907noErrors :: Idris Bool
908noErrors = do i <- getIState
909 case errSpan i of
910 Nothing -> return True
911 _ -> return False
913setTypeCase :: Bool -> Idris ()
914setTypeCase t = do i <- getIState
915 let opts = idris_options i
916 let opt' = opts { opt_typecase = t }
917 putIState $ i { idris_options = opt' }
920-- Dealing with parameters
922expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
923 [Name] -> -- all names
924 [Name] -> -- names with no declaration
925 PTerm -> PTerm
926expandParams dec ps ns infs tm = en tm
927 where
928 -- if we shadow a name (say in a lambda binding) that is used in a call to
929 -- a lifted function, we need access to both names - once in the scope of the
930 -- binding and once to call the lifted functions. So we'll explicitly shadow
931 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
932 -- but we didn't...)
934 mkShadow (UN n) = MN 0 n
935 mkShadow (MN i n) = MN (i+1) n
936 mkShadow (NS x s) = NS (mkShadow x) s
938 en (PLam fc n t s)
939 | n `elem` (map fst ps ++ ns)
940 = let n' = mkShadow n in
941 PLam fc n' (en t) (en (shadow n n' s))
942 | otherwise = PLam fc n (en t) (en s)
943 en (PPi p n t s)
944 | n `elem` (map fst ps ++ ns)
945 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
946 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
947 | otherwise = PPi (enTacImp p) n (en t) (en s)
948 en (PLet fc n ty v s)
949 | n `elem` (map fst ps ++ ns)
950 = let n' = mkShadow n in
951 PLet fc n' (en ty) (en v) (en (shadow n n' s))
952 | otherwise = PLet fc n (en ty) (en v) (en s)
953 -- FIXME: Should only do this in a type signature!
954 en (PDPair f p (PRef f' n) t r)
955 | n `elem` (map fst ps ++ ns) && t /= Placeholder
956 = let n' = mkShadow n in
957 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
958 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
959 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
960 en (PTyped l r) = PTyped (en l) (en r)
961 en (PPair f p l r) = PPair f p (en l) (en r)
962 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
963 en (PAlternative a as) = PAlternative a (map en as)
964 en (PHidden t) = PHidden (en t)
965 en (PUnifyLog t) = PUnifyLog (en t)
966 en (PDisamb ds t) = PDisamb ds (en t)
967 en (PNoImplicits t) = PNoImplicits (en t)
968 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
969 en (PProof ts) = PProof (map (fmap en) ts)
970 en (PTactics ts) = PTactics (map (fmap en) ts)
972 en (PQuote (Var n))
973 | n `nselem` ns = PQuote (Var (dec n))
974 en (PApp fc (PInferRef fc' n) as)
975 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
976 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
977 en (PApp fc (PRef fc' n) as)
978 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
979 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
980 | n `nselem` ns = PApp fc (PRef fc' (dec n))
981 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
982 en (PAppBind fc (PRef fc' n) as)
983 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
984 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
985 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
986 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
987 en (PRef fc n)
988 | n `elem` infs = PApp fc (PInferRef fc (dec n))
989 (map (pexp . (PRef fc)) (map fst ps))
990 | n `nselem` ns = PApp fc (PRef fc (dec n))
991 (map (pexp . (PRef fc)) (map fst ps))
992 en (PInferRef fc n)
993 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
994 (map (pexp . (PRef fc)) (map fst ps))
995 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
996 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
997 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
998 en (PRunTactics fc tm) = PRunTactics fc (en tm)
999 en t = t
1001 nselem x [] = False
1002 nselem x (y : xs) | nseq x y = True
1003 | otherwise = nselem x xs
1005 nseq x y = nsroot x == nsroot y
1007 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1008 enTacImp other = other
1010expandParamsD :: Bool -> -- True = RHS only
1011 IState ->
1012 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1013expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
1014 = if n `elem` ns && (not rhsonly)
1015 then -- trace (show (n, expandParams dec ps ns ty)) $
1016 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
1017 else --trace (show (n, expandParams dec ps ns ty)) $
1018 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
1019expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
1020 = if n `elem` ns && (not rhsonly)
1021 then -- trace (show (n, expandParams dec ps ns ty)) $
1022 PPostulate doc syn fc o (dec n) (piBind ps
1023 (expandParams dec ps ns [] ty))
1024 else --trace (show (n, expandParams dec ps ns ty)) $
1025 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1026expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1027 = let n' = if n `elem` ns then dec n else n in
1028 PClauses fc opts n' (map expandParamsC cs)
1029 where
1030 expandParamsC (PClause fc n lhs ws rhs ds)
1031 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1032 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1033 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1034 n' = if n `elem` ns then dec n else n
1035 -- names bound on the lhs should not be expanded on the rhs
1036 ns' = removeBound lhs ns in
1037 PClause fc n' lhs'
1038 (map (expandParams dec ps'' ns' []) ws)
1039 (expandParams dec ps'' ns' [] rhs)
1040 (map (expandParamsD True ist dec ps'' ns') ds)
1041 expandParamsC (PWith fc n lhs ws wval pn ds)
1042 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1043 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1044 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1045 n' = if n `elem` ns then dec n else n
1046 ns' = removeBound lhs ns in
1047 PWith fc n' lhs'
1048 (map (expandParams dec ps'' ns' []) ws)
1049 (expandParams dec ps'' ns' [] wval)
1050 pn
1051 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1052 updateps yn nm [] = []
1053 updateps yn nm (((a, t), i):as)
1054 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1055 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1057 removeBound lhs ns = ns \\ nub (bnames lhs)
1059 bnames (PRef _ n) = [n]
1060 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1061 bnames (PPair _ _ l r) = bnames l ++ bnames r
1062 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1063 bnames _ = []
1065-- | Expands parameters defined in parameter and where blocks inside of declarations
1066expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1067 = PData doc argDocs syn fc co (expandPData pd)
1068 where
1069 -- just do the type decl, leave constructors alone (parameters will be
1070 -- added implicitly)
1071 expandPData (PDatadecl n ty cons)
1072 = if n `elem` ns
1073 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1074 (map econ cons)
1075 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1076 econ (doc, argDocs, n, t, fc, fs)
1077 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1078expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
1079 = if tn `elem` ns
1080 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1081 opts cdoc (dec cn) conty
1082 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1083 opts cdoc (dec cn) conty
1084 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1085expandParamsD rhs ist dec ps ns (PParams f params pds)
1086 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1087 (map (expandParamsD True ist dec ps ns) pds)
1088-- (map (expandParamsD ist dec ps ns) pds)
1089expandParamsD rhs ist dec ps ns (PMutual f pds)
1090 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1091expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)
1092 = PClass doc info f
1093 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1095 (map (mapsnd (expandParams dec ps ns [])) params)
1096 pDocs
1097 fds
1098 (map (expandParamsD rhs ist dec ps ns) decls)
1099expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)
1100 = PInstance doc argDocs info f
1101 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1103 (map (expandParams dec ps ns []) params)
1104 (expandParams dec ps ns [] ty)
1105 cn
1106 (map (expandParamsD rhs ist dec ps ns) decls)
1107expandParamsD rhs ist dec ps ns d = d
1109mapsnd f (x, t) = (x, f t)
1111-- Calculate a priority for a type, for deciding elaboration order
1112-- * if it's just a type variable or concrete type, do it early (0)
1113-- * if there's only type variables and injective constructors, do it next (1)
1114-- * if there's a function type, next (2)
1115-- * finally, everything else (3)
1117getPriority :: IState -> PTerm -> Int
1118getPriority i tm = 1 -- pri tm
1119 where
1120 pri (PRef _ n) =
1121 case lookupP n (tt_ctxt i) of
1122 ((P (DCon _ _ _) _ _):_) -> 1
1123 ((P (TCon _ _) _ _):_) -> 1
1124 ((P Ref _ _):_) -> 1
1125 [] -> 0 -- must be locally bound, if it's not an error...
1126 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1127 pri (PTrue _ _) = 0
1128 pri (PRefl _ _) = 1
1129 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1130 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1131 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1132 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1133 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1134 pri (PTyped l r) = pri l
1135 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1136 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1137 pri (PAlternative a as) = maximum (map pri as)
1138 pri (PConstant _) = 0
1139 pri Placeholder = 1
1140 pri _ = 3
1143addStatics :: Name -> Term -> PTerm -> Idris ()
1144addStatics n tm ptm =
1145 do let (statics, dynamics) = initStatics tm ptm
1146 ist <- getIState
1147 let paramnames
1148 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1149 Just p -> getNamesFrom 0 (fn_params p) tm ++
1150 concatMap (getParamNames ist) (map snd statics)
1151 _ -> concatMap (getParamNames ist) (map snd statics)
1153 let stnames = nub $ concatMap freeArgNames (map snd statics)
1154 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1155 \\ paramnames
1156 -- also get the arguments which are 'uniquely inferrable' from
1157 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1158 -- or parameters to the type of a static
1159 let statics' = nub $ map fst statics ++
1160 filter (\x -> not (elem x dnames)) stnames
1161 let stpos = staticList statics' tm
1162 i <- getIState
1163 when (not (null statics)) $
1164 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1165 ++ showTmImpls ptm ++ "\n"
1166 ++ show statics ++ "\n" ++ show dynamics
1167 ++ "\n" ++ show paramnames
1168 ++ "\n" ++ show stpos
1169 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1170 addIBC (IBCStatic n)
1171 where
1172 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
1173 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1174 (static, (n, ty) : dynamic)
1175 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)
1176 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1177 if pstatic p == Static then ((n, ty) : static, dynamic)
1178 else if (not (searchArg p))
1179 then (static, (n, ty) : dynamic)
1180 else (static, dynamic)
1181 initStatics t pt = ([], [])
1183 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1184 = case lookupCtxtExact n (idris_datatypes ist) of
1185 Just ti -> getNamePos 0 (param_pos ti) args
1186 Nothing -> []
1187 where getNamePos i ps [] = []
1188 getNamePos i ps (P _ n _ : as)
1189 | i `elem` ps = n : getNamePos (i + 1) ps as
1190 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1191 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1192 = n : getParamNames ist sc
1193 getParamNames ist _ = []
1195 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1196 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1197 | otherwise = getNamesFrom (i + 1) ps sc
1198 getNamesFrom i ps sc = []
1200 freeArgNames (Bind n (Pi _ ty _) sc)
1201 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1202 freeArgNames tm = let (_, args) = unApply tm in
1203 concatMap freeNames args
1205 -- if a name appears in a type class or tactic implicit index, it doesn't
1206 -- affect its 'uniquely inferrable' from a static status since these are
1207 -- resolved by searching.
1208 searchArg (Constraint _ _) = True
1209 searchArg (TacImp _ _ _) = True
1210 searchArg _ = False
1212 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1213 staticList _ _ = []
1215-- Dealing with implicit arguments
1217-- Add some bound implicits to the using block if they aren't there already
1219addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1220addToUsing us [] = us
1221addToUsing us ((n, t) : ns)
1222 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1223 | otherwise = addToUsing us ns
1224 where impName (UImplicit n _) = Just n
1225 impName _ = Nothing
1227-- Add constraint bindings from using block
1229addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1230addUsingConstraints syn fc t
1231 = do ist <- get
1232 let ns = namesIn [] ist t
1233 let cs = getConstraints t -- check declared constraints
1234 let addconsts = uconsts \\ cs
1235 return (doAdd addconsts ns t)
1236 where uconsts = filter uconst (using syn)
1237 uconst (UConstraint _ _) = True
1238 uconst _ = False
1240 doAdd [] _ t = t
1241 -- if all of args in ns, then add it
1242 doAdd (UConstraint c args : cs) ns t
1243 | all (\n -> elem n ns) args
1244 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1245 (mkConst c args) (doAdd cs ns t)
1246 | otherwise = doAdd cs ns t
1248 mkConst c args = PApp fc (PRef fc c)
1249 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1251 getConstraints (PPi (Constraint _ _) _ c sc)
1252 = getcapp c ++ getConstraints sc
1253 getConstraints (PPi _ _ c sc) = getConstraints sc
1254 getConstraints _ = []
1256 getcapp (PApp _ (PRef _ c) args)
1257 = do ns <- mapM getName args
1258 return (UConstraint c ns)
1259 getcapp _ = []
1261 getName (PExp _ _ _ (PRef _ n)) = return n
1262 getName _ = []
1264-- Add implicit bindings from using block, and bind any missing names
1265addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1266addUsingImpls syn n fc t
1267 = do ist <- getIState
1268 let ns = implicitNamesIn (map iname uimpls) ist t
1269 let badnames = filter (\n -> not (implicitable n) &&
1270 n `notElem` (map iname uimpls)) ns
1271 when (not (null badnames)) $
1272 throwError (At fc (Elaborating "type of " n
1273 (NoSuchVariable (head badnames))))
1274 let cs = getArgnames t -- get already bound names
1275 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1276 -- if all names in the arguments of addconsts appear in ns,
1277 -- add the constraint implicitly
1278 return (bindFree ns (doAdd addimpls ns t))
1279 where uimpls = filter uimpl (using syn)
1280 uimpl (UImplicit _ _) = True
1281 uimpl _ = False
1283 iname (UImplicit n _) = n
1284 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1286 doAdd [] _ t = t
1287 -- if all of args in ns, then add it
1288 doAdd (UImplicit n ty : cs) ns t
1289 | elem n ns
1290 = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)
1291 | otherwise = doAdd cs ns t
1293 -- bind the free names which weren't in the using block
1294 bindFree [] tm = tm
1295 bindFree (n:ns) tm
1296 | elem n (map iname uimpls) = bindFree ns tm
1297 | otherwise
1298 = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
1300 getArgnames (PPi _ n c sc)
1301 = n : getArgnames sc
1302 getArgnames _ = []
1304-- Given the original type and the elaborated type, return the implicitness
1305-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1307getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1308getUnboundImplicits i t tm = getImps t (collectImps tm)
1309 where collectImps (PPi p n t sc)
1310 = (n, (p, t)) : collectImps sc
1311 collectImps _ = []
1313 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1314 getImps (Bind n (Pi _ t _) sc) imps
1315 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1316 where
1317 argInfo n (Imp opt _ _ _) Placeholder
1318 = (True, PImp 0 True opt n Placeholder)
1319 argInfo n (Imp opt _ _ _) t'
1320 = (False, PImp (getPriority i t') True opt n t')
1321 argInfo n (Exp opt _ _) t'
1322 = (InaccessibleArg `elem` opt,
1323 PExp (getPriority i t') opt n t')
1324 argInfo n (Constraint opt _) t'
1325 = (InaccessibleArg `elem` opt,
1326 PConstraint 10 opt n t')
1327 argInfo n (TacImp opt _ scr) t'
1328 = (InaccessibleArg `elem` opt,
1329 PTacImplicit 10 opt n scr t')
1330 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1331 where impBind n t = (True, PImp 1 True [] n Placeholder)
1332 getImps sc tm = []
1334-- Add implicit Pi bindings for any names in the term which appear in an
1335-- argument position.
1337-- This has become a right mess already. Better redo it some time...
1338-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1339-- a couple of places which use it. Clean them up!
1341-- Issue 1739 in the issue tracker
1342-- https://github.com/idris-lang/Idris-dev/issues/1739
1343implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1344implicit info syn n ptm = implicit' info syn [] n ptm
1346implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1347implicit' info syn ignore n ptm
1348 = do i <- getIState
1349 let (tm', impdata) = implicitise syn ignore i ptm
1350 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1351-- let (tm'', spos) = findStatics i tm'
1352 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1353 addIBC (IBCImp n)
1354 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1355-- i <- get
1356-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1357 return tm'
1358 where
1359 -- Detect unknown names in default arguments and throw error if found.
1360 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1361 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1363 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1364 notFoundInDefault kns (PTacImplicit _ _ n script _)
1365 = do i <- getIState
1366 case notFound kns (namesIn [] i script) of
1367 Nothing -> return (n:kns)
1368 Just name -> throwError (NoSuchVariable name)
1369 notFoundInDefault kns p = return ((pname p):kns)
1371 notFound :: [Name] -> [Name] -> Maybe Name
1372 notFound kns [] = Nothing
1373 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1374 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1376implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1377implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1378 let (declimps, ns') = execState (imps True [] tm) ([], [])
1379 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1380 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1381 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1382 if null ns
1383 then (tm, reverse declimps)
1384 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1385 where
1386 uvars = map ipair (filter uimplicit (using syn))
1387 pvars = syn_params syn
1389 inUsing n = n `elem` map fst uvars
1391 ipair (UImplicit x y) = (x, y)
1392 uimplicit (UImplicit _ _) = True
1393 uimplicit _ = False
1395 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1396 | otherwise = x : dropAll xs ys
1397 dropAll [] ys = []
1399 -- Find names in argument position in a type, suitable for implicit
1400 -- binding
1401 -- Not the function position, but do everything else...
1402 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1403 implNamesIn uv t = namesIn uv ist t
1405 imps top env (PApp _ f as)
1406 = do (decls, ns) <- get
1407 let isn = concatMap (namesIn uvars ist) (map getTm as)
1408 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1409 imps top env (PPi (Imp l _ _ _) n ty sc)
1410 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1411 (decls , ns) <- get
1412 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1413 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1414 imps True (n:env) sc
1415 imps top env (PPi (Exp l _ _) n ty sc)
1416 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1417 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1418 _ -> [])
1419 (decls, ns) <- get -- ignore decls in HO types
1420 put (PExp (getPriority ist ty) l n Placeholder : decls,
1421 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1422 imps True (n:env) sc
1423 imps top env (PPi (Constraint l _) n ty sc)
1424 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1425 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1426 _ -> [])
1427 (decls, ns) <- get -- ignore decls in HO types
1428 put (PConstraint 10 l n Placeholder : decls,
1429 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1430 imps True (n:env) sc
1431 imps top env (PPi (TacImp l _ scr) n ty sc)
1432 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1433 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1434 _ -> [])
1435 (decls, ns) <- get -- ignore decls in HO types
1436 put (PTacImplicit 10 l n scr Placeholder : decls,
1437 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1438 imps True (n:env) sc
1439 imps top env (PEq _ _ _ l r)
1440 = do (decls, ns) <- get
1441 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1442 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1443 imps top env (PRewrite _ l r _)
1444 = do (decls, ns) <- get
1445 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1446 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1447 imps top env (PTyped l r)
1448 = imps top env l
1449 imps top env (PPair _ _ l r)
1450 = do (decls, ns) <- get
1451 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1452 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1453 imps top env (PDPair _ _ (PRef _ n) t r)
1454 = do (decls, ns) <- get
1455 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1456 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1457 imps top env (PDPair _ _ l t r)
1458 = do (decls, ns) <- get
1459 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1460 namesIn uvars ist r
1461 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1462 imps top env (PAlternative a as)
1463 = do (decls, ns) <- get
1464 let isn = concatMap (namesIn uvars ist) as
1465 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1466 imps top env (PLam fc n ty sc)
1467 = do imps False env ty
1468 imps False (n:env) sc
1469 imps top env (PHidden tm) = imps False env tm
1470 imps top env (PUnifyLog tm) = imps False env tm
1471 imps top env (PNoImplicits tm) = imps False env tm
1472 imps top env (PRunTactics fc tm) = imps False env tm
1473 imps top env _ = return ()
1475 pibind using [] sc = sc
1476 pibind using (n:ns) sc
1477 = case lookup n using of
1478 Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1479 Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1480 (pibind using ns sc)
1482-- Add implicit arguments in function calls
1483addImplPat :: IState -> PTerm -> PTerm
1484addImplPat = addImpl' True [] [] []
1486addImplBound :: IState -> [Name] -> PTerm -> PTerm
1487addImplBound ist ns = addImpl' False ns [] [] ist
1489addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1490addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1492-- | Add the implicit arguments to applications in the term
1493-- [Name] gives the names to always expend, even when under a binder of
1494-- that name (this is to expand methods with implicit arguments in dependent
1495-- type classes).
1496addImpl :: [Name] -> IState -> PTerm -> PTerm
1497addImpl = addImpl' False [] []
1499-- TODO: in patterns, don't add implicits to function names guarded by constructors
1500-- and *not* inside a PHidden
1502addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1503addImpl' inpat env infns imp_meths ist ptm
1504 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1505 where
1506 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1507 ai qq env ds (PRef fc f)
1508 | f `elem` infns = PInferRef fc f
1509 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []
1510 ai qq env ds (PHidden (PRef fc f))
1511 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])
1512 ai qq env ds (PEq fc lt rt l r)
1513 = let lt' = ai qq env ds lt
1514 rt' = ai qq env ds rt
1515 l' = ai qq env ds l
1516 r' = ai qq env ds r in
1517 PEq fc lt' rt' l' r'
1518 ai qq env ds (PRewrite fc l r g)
1519 = let l' = ai qq env ds l
1520 r' = ai qq env ds r
1521 g' = fmap (ai qq env ds) g in
1522 PRewrite fc l' r' g'
1523 ai qq env ds (PTyped l r)
1524 = let l' = ai qq env ds l
1525 r' = ai qq env ds r in
1526 PTyped l' r'
1527 ai qq env ds (PPair fc p l r)
1528 = let l' = ai qq env ds l
1529 r' = ai qq env ds r in
1530 PPair fc p l' r'
1531 ai qq env ds (PDPair fc p l t r)
1532 = let l' = ai qq env ds l
1533 t' = ai qq env ds t
1534 r' = ai qq env ds r in
1535 PDPair fc p l' t' r'
1536 ai qq env ds (PAlternative a as)
1537 = let as' = map (ai qq env ds) as in
1538 PAlternative a as'
1539 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1540 ai qq env ds (PApp fc (PInferRef _ f) as)
1541 = let as' = map (fmap (ai qq env ds)) as in
1542 PApp fc (PInferRef fc f) as'
1543 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1544 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1545 | not (f `elem` map fst env)
1546 = let as' = map (fmap (ai qq env ds)) as in
1547 handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'
1548 | Just (Just ty) <- lookup f env =
1549 let as' = map (fmap (ai qq env ds)) as
1550 arity = getPArity ty in
1551 mkPApp fc arity ftm as'
1552 ai qq env ds (PApp fc f as)
1553 = let f' = ai qq env ds f
1554 as' = map (fmap (ai qq env ds)) as in
1555 mkPApp fc 1 f' as'
1556 ai qq env ds (PCase fc c os)
1557 = let c' = ai qq env ds c in
1558 -- leave os alone, because they get lifted into a new pattern match
1559 -- definition which is passed through addImpl again with more scope
1560 -- information
1561 PCase fc c' os
1562 -- If the name in a lambda is a constructor name, do this as a 'case'
1563 -- instead (it is harmless to do so, especially since the lambda will
1564 -- be lifted anyway!)
1565 ai qq env ds (PLam fc n ty sc)
1566 = case lookupDef n (tt_ctxt ist) of
1567 [] -> let ty' = ai qq env ds ty
1568 sc' = ai qq ((n, Just ty):env) ds sc in
1569 PLam fc n ty' sc'
1570 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1571 (PCase fc (PRef fc (sMN 0 "lamp") )
1572 [(PRef fc n, sc)]))
1573 ai qq env ds (PLet fc n ty val sc)
1574 = case lookupDef n (tt_ctxt ist) of
1575 [] -> let ty' = ai qq env ds ty
1576 val' = ai qq env ds val
1577 sc' = ai qq ((n, Just ty):env) ds sc in
1578 PLet fc n ty' val' sc'
1579 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1580 ai qq env ds (PPi p n ty sc)
1581 = let ty' = ai qq env ds ty
1582 env' = if n `elem` imp_meths then env
1583 else ((n, Just ty) : env)
1584 sc' = ai qq env' ds sc in
1585 PPi p n ty' sc'
1586 ai qq env ds (PGoal fc r n sc)
1587 = let r' = ai qq env ds r
1588 sc' = ai qq ((n, Nothing):env) ds sc in
1589 PGoal fc r' n sc'
1590 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1591 -- Don't do PProof or PTactics since implicits get added when scope is
1592 -- properly known in ElabTerm.runTac
1593 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1594 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1595 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1596 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1597 (fmap (ai True env ds) g)
1598 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1599 ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
1600 ai qq env ds tm = tm
1602 handleErr (Left err) = PElabError err
1603 handleErr (Right x) = x
1605-- if in a pattern, and there are no arguments, and there's no possible
1606-- names with zero explicit arguments, don't add implicits.
1608aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1609aiFn inpat True qq imp_meths ist fc f ds []
1610 = case lookupDef f (tt_ctxt ist) of
1611 [] -> Right $ PPatvar fc f
1612 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1613 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1614 if (not (vname f) || tcname f
1615 || any (conCaf (tt_ctxt ist)) ialts)
1616-- any constructor alts || any allImp ialts))
1617 then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor
1618 else Right $ PPatvar fc f
1619 where imp (PExp _ _ _ _) = False
1620 imp _ = True
1621-- allImp [] = False
1622 allImp xs = all imp xs
1623 constructor (TyDecl (DCon _ _ _) _) = True
1624 constructor _ = False
1626 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1628 vname (UN n) = True -- non qualified
1629 vname _ = False
1631aiFn inpat expat qq imp_meths ist fc f ds as
1632 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1633aiFn inpat expat qq imp_meths ist fc f ds as
1634 -- This is where namespaces get resolved by adding PAlternative
1635 = do let ns = lookupCtxtName f (idris_implicits ist)
1636 let nh = filter (\(n, _) -> notHidden n) ns
1637 let ns' = case trimAlts ds nh of
1638 [] -> nh
1639 x -> x
1640 case ns' of
1641 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)
1642 [] -> if f `elem` (map fst (idris_metavars ist))
1643 then Right $ PApp fc (PRef fc f) as
1644 else Right $ mkPApp fc (length as) (PRef fc f) as
1645 alts -> Right $
1646 PAlternative True $
1647 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))
1648 (insertImpl ns as)) alts
1649 where
1650 -- if the name is in imp_meths, we should actually refer to the bound
1651 -- name rather than the global one after expanding implicits
1652 isImpName f f' | f `elem` imp_meths = f
1653 | otherwise = f'
1655 trimAlts [] alts = alts
1656 trimAlts ns alts
1657 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1659 nspace (NS _ s) = s
1660 nspace _ = []
1662 notHidden n = case getAccessibility n of
1663 Hidden -> False
1664 _ -> True
1666 getAccessibility n
1667 = case lookupDefAccExact n False (tt_ctxt ist) of
1668 Just (n,t) -> t
1669 _ -> Public
1671 insertImpl :: [PArg] -> [PArg] -> [PArg]
1672 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1674 exp (PExp _ _ _ _) = True
1675 exp (PConstraint _ _ _ _) = True
1676 exp _ = False
1678 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1679 -> [PArg] -- parameters
1680 -> [PArg] -- explicit arguments
1681 -> [PArg] -- implicits given
1682 -> [PArg]
1683 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1684 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1685 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1686 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1687 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1688 let rtc = PResolveTC fc in
1689 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1690 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1691 case find n imps [] of
1692 Just (tm, imps') ->
1693 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1694 Nothing ->
1695 PImp p True l n Placeholder :
1696 insImpAcc (M.insert n Placeholder pnas) ps given imps
1697 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1698 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1699 case find n imps [] of
1700 Just (tm, imps') ->
1701 PTacImplicit p l n sc tm :
1702 insImpAcc (M.insert n tm pnas) ps given imps'
1703 Nothing ->
1704 if inpat
1705 then PTacImplicit p l n sc Placeholder :
1706 insImpAcc (M.insert n Placeholder pnas) ps given imps
1707 else PTacImplicit p l n sc sc :
1708 insImpAcc (M.insert n sc pnas) ps given imps
1709 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1710 -- TODO: report here, and prune alternatives
1711 -- Issue #1740 in the Issue Tracker
1712-- https://github.com/idris-lang/Idris-dev/issues/1740
1713 insImpAcc _ _ given imps = given ++ imps
1715 find n [] acc = Nothing
1716 find n (PImp _ _ _ n' t : gs) acc
1717 | n == n' = Just (t, reverse acc ++ gs)
1718 find n (PTacImplicit _ _ n' _ t : gs) acc
1719 | n == n' = Just (t, reverse acc ++ gs)
1720 find n (g : gs) acc = find n gs (g : acc)
1722-- replace non-linear occurrences with _
1724stripLinear :: IState -> PTerm -> PTerm
1725stripLinear i tm = evalState (sl tm) [] where
1726 sl :: PTerm -> State [Name] PTerm
1727 sl (PRef fc f)
1728 | (_:_) <- lookupTy f (tt_ctxt i)
1729 = return $ PRef fc f
1730 | otherwise = do ns <- get
1731 if (f `elem` ns)
1732 then return $ PHidden (PRef fc f) -- Placeholder
1733 else do put (f : ns)
1734 return (PRef fc f)
1735 sl (PPatvar fc f)
1736 = do ns <- get
1737 if (f `elem` ns)
1738 then return $ PHidden (PPatvar fc f) -- Placeholder
1739 else do put (f : ns)
1740 return (PPatvar fc f)
1741 -- Assumption is that variables are all the same in each alternative
1742 sl t@(PAlternative b as) = do ns <- get
1743 as' <- slAlts ns as
1744 return (PAlternative b as')
1745 where slAlts ns (a : as) = do put ns
1746 a' <- sl a
1747 as' <- slAlts ns as
1748 return (a' : as')
1749 slAlts ns [] = return []
1750 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1751 sl (PDPair fc p l t r) = do l' <- sl l
1752 t' <- sl t
1753 r' <- sl r
1754 return (PDPair fc p l' t' r')
1755 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1756 args' <- mapM slA args
1757 return $ PApp fc fn args'
1758 where slA (PImp p m l n t) = do t' <- sl t
1759 return $ PImp p m l n t'
1760 slA (PExp p l n t) = do t' <- sl t
1761 return $ PExp p l n t'
1762 slA (PConstraint p l n t)
1763 = do t' <- sl t
1764 return $ PConstraint p l n t'
1765 slA (PTacImplicit p l n sc t)
1766 = do t' <- sl t
1767 return $ PTacImplicit p l n sc t'
1768 sl x = return x
1770-- Remove functions which aren't applied to anything, which must then
1771-- be resolved by unification. Assume names resolved and alternatives
1772-- filled in (so no ambiguity).
1774stripUnmatchable :: IState -> PTerm -> PTerm
1775stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1776 su :: PTerm -> PTerm
1777 su (PRef fc f)
1778 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1779 = Placeholder
1780 su (PApp fc f@(PRef _ fn) args)
1781 -- here we use canBeDConName because the impossible pattern
1782 -- check will not necessarily fully resolve constructor names,
1783 -- and these bare names will otherwise get in the way of
1784 -- impossbility checking.
1785 | canBeDConName fn ctxt
1786 = PApp fc f (fmap (fmap su) args)
1787 su (PApp fc f args)
1788 = PHidden (PApp fc f args)
1789 su (PAlternative b alts)
1790 = let alts' = filter (/= Placeholder) (map su alts) in
1791 if null alts' then Placeholder
1792 else PAlternative b alts'
1793 su (PPair fc p l r) = PPair fc p (su l) (su r)
1794 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1795 su t@(PLam fc _ _ _) = PHidden t
1796 su t@(PPi _ _ _ _) = PHidden t
1797 su t@(PEq _ _ _ _ _) = PHidden t
1798 su t = t
1800 ctxt = tt_ctxt i
1802stripUnmatchable i tm = tm
1804mkPApp fc a f [] = f
1805mkPApp fc a f as = let rest = drop a as in
1806 appRest fc (PApp fc f (take a as)) rest
1807 where
1808 appRest fc f [] = f
1809 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1811-- Find 'static' argument positions
1812-- (the declared ones, plus any names in argument position in the declared
1813-- statics)
1814-- FIXME: It's possible that this really has to happen after elaboration
1816findStatics :: IState -> PTerm -> (PTerm, [Bool])
1817findStatics ist tm = trace (show tm) $
1818 let (ns, ss) = fs tm in
1819 runState (pos ns ss tm) []
1820 where fs (PPi p n t sc)
1821 | Static <- pstatic p
1822 = let (ns, ss) = fs sc in
1823 (namesIn [] ist t : ns, n : ss)
1824 | otherwise = let (ns, ss) = fs sc in
1825 (ns, ss)
1826 fs _ = ([], [])
1828 inOne n ns = length (filter id (map (elem n) ns)) == 1
1830 pos ns ss (PPi p n t sc)
1831 | elem n ss = do sc' <- pos ns ss sc
1832 spos <- get
1833 put (True : spos)
1834 return (PPi (p { pstatic = Static }) n t sc')
1835 | otherwise = do sc' <- pos ns ss sc
1836 spos <- get
1837 put (False : spos)
1838 return (PPi p n t sc')
1839 pos ns ss t = return t
1841-- for 6.12/7 compatibility
1842data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1844instance Applicative (EitherErr a) where
1845 pure = return
1846 (<*>) = ap
1848instance Monad (EitherErr a) where
1849 return = RightOK
1851 (LeftErr e) >>= k = LeftErr e
1852 RightOK v >>= k = k v
1854toEither (LeftErr e) = Left e
1855toEither (RightOK ho) = Right ho
1857-- syntactic match of a against b, returning pair of variables in a
1858-- and what they match. Returns the pair that failed if not a match.
1860matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1861matchClause = matchClause' False
1863matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1864matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1865 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1867 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1868 fullApp x = x
1870 match' x y = match (fullApp x) (fullApp y)
1871 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1872 | fi == txt "fromInteger" && b == txt "builtins",
1873 PConstant (I _) <- getTm x = match (getTm x) x'
1874 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1875 | fi == txt "fromInteger" && b == txt "builtins",
1876 PConstant (I _) <- getTm x = match (getTm x) x'
1877 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1878 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1879 match (PApp _ f args) (PApp _ f' args')
1880 | length args == length args'
1881 = do mf <- match' f f'
1882 ms <- zipWithM matchArg args args'
1883 return (mf ++ concat ms)
1884 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1885 match (PPatvar f n) xr = match (PRef f n) xr
1886 match xr (PPatvar f n) = match xr (PRef f n)
1887 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1888 match (PRef _ n) tm@(PRef _ n')
1889 | n == n' && not names &&
1890 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1891 || tm == Placeholder)
1892 = return [(n, tm)]
1893 -- if one namespace is missing, drop the other
1894 | n == n' || n == dropNS n' || dropNS n == n' = return []
1895 where dropNS (NS n _) = n
1896 dropNS n = n
1897 match (PRef _ n) tm
1898 | not names && (not (isConName n (tt_ctxt i) ||
1899 isFnName n (tt_ctxt i)) || tm == Placeholder)
1900 = return [(n, tm)]
1901 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1902 = do ml <- match' l l'
1903 mr <- match' r r'
1904 return (ml ++ mr)
1905 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1906 = do ml <- match' l l'
1907 mr <- match' r r'
1908 return (ml ++ mr)
1909 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1910 mr <- match r r'
1911 return (ml ++ mr)
1912 match (PTyped l r) x = match l x
1913 match x (PTyped l r) = match x l
1914 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1915 mr <- match' r r'
1916 return (ml ++ mr)
1917 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1918 mt <- match' t t'
1919 mr <- match' r r'
1920 return (ml ++ mt ++ mr)
1921 match (PAlternative a as) (PAlternative a' as')
1922 = do ms <- zipWithM match' as as'
1923 return (concat ms)
1924 match a@(PAlternative _ as) b
1925 = do let ms = zipWith match' as (repeat b)
1926 case (rights (map toEither ms)) of
1927 (x: _) -> return x
1928 _ -> LeftErr (a, b)
1929 match (PCase _ _ _) _ = return [] -- lifted out
1930 match (PMetavar _) _ = return [] -- modified
1931 match (PInferRef _ _) _ = return [] -- modified
1932 match (PQuote _) _ = return []
1933 match (PProof _) _ = return []
1934 match (PTactics _) _ = return []
1935 match (PRefl _ _) (PRefl _ _) = return []
1936 match (PResolveTC _) (PResolveTC _) = return []
1937 match (PTrue _ _) (PTrue _ _) = return []
1938 match (PReturn _) (PReturn _) = return []
1939 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1940 ms <- match' s s'
1941 return (mt ++ ms)
1942 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1943 ms <- match' s s'
1944 return (mt ++ ms)
1945 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1946 mty <- match' ty ty'
1947 ms <- match' s s'
1948 return (mt ++ mty ++ ms)
1949 match (PHidden x) (PHidden y)
1950 | RightOK xs <- match x y = return xs -- to collect variables
1951 | otherwise = return [] -- Otherwise hidden things are unmatchable
1952 match (PHidden x) y
1953 | RightOK xs <- match x y = return xs
1954 | otherwise = return []
1955 match x (PHidden y)
1956 | RightOK xs <- match x y = return xs
1957 | otherwise = return []
1958 match (PUnifyLog x) y = match' x y
1959 match x (PUnifyLog y) = match' x y
1960 match (PNoImplicits x) y = match' x y
1961 match x (PNoImplicits y) = match' x y
1962 match Placeholder _ = return []
1963 match _ Placeholder = return []
1964 match (PResolveTC _) _ = return []
1965 match a b | a == b = return []
1966 | otherwise = LeftErr (a, b)
1968 checkRpts (RightOK ms) = check ms where
1969 check ((n,t):xs)
1970 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1971 then Left (t, t')
1972 else check xs
1973 check (_:xs) = check xs
1974 check [] = Right ms
1975 checkRpts (LeftErr x) = Left x
1977substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1978substMatches ms = substMatchesShadow ms []
1980substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1981substMatchesShadow [] shs t = t
1982substMatchesShadow ((n,tm):ns) shs t
1983 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1985substMatch :: Name -> PTerm -> PTerm -> PTerm
1986substMatch n = substMatchShadow n []
1988substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1989substMatchShadow n shs tm t = sm shs t where
1990 sm xs (PRef _ n') | n == n' = tm
1991 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1992 sm xs (PPi p x t sc)
1993 | x `elem` xs
1994 = let x' = nextName x in
1995 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1996 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1997 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1998 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1999 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2000 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
2001 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
2002 (fmap (sm xs) tm)
2003 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2004 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
2005 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
2006 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
2007 sm xs (PHidden x) = PHidden (sm xs x)
2008 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2009 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2010 sm xs x = x
2012 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2013 fullApp x = x
2015shadow :: Name -> Name -> PTerm -> PTerm
2016shadow n n' t = sm t where
2017 sm (PRef fc x) | n == x = PRef fc n'
2018 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
2019 | otherwise = PLam fc x (sm t) sc
2020 sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
2021 | otherwise = PPi p x (sm t) sc
2022 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
2023 | otherwise = PLet fc x (sm t) (sm v) sc
2024 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
2025 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
2026 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
2027 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
2028 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
2029 sm (PTyped x y) = PTyped (sm x) (sm y)
2030 sm (PPair f p x y) = PPair f p (sm x) (sm y)
2031 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
2032 sm (PAlternative a as) = PAlternative a (map sm as)
2033 sm (PTactics ts) = PTactics (map (fmap sm) ts)
2034 sm (PProof ts) = PProof (map (fmap sm) ts)
2035 sm (PHidden x) = PHidden (sm x)
2036 sm (PUnifyLog x) = PUnifyLog (sm x)
2037 sm (PNoImplicits x) = PNoImplicits (sm x)
2038 sm x = x
2040-- Rename any binders which are repeated (so that we don't have to mess
2041-- about with shadowing anywhere else).
2043mkUniqueNames :: [Name] -> PTerm -> PTerm
2044mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2045 inScope :: S.Set Name
2046 inScope = S.fromList $ boundNamesIn tm
2048 mkUniqA arg = do t' <- mkUniq (getTm arg)
2049 return (arg { getTm = t' })
2051 -- Initialise the unique name with the environment length (so we're not
2052 -- looking for too long...)
2053 initN (UN n) l = UN $ txt (str n ++ show l)
2054 initN (MN i s) l = MN (i+l) s
2055 initN n l = n
2057 -- FIXME: Probably ought to do this for completeness! It's fine as
2058 -- long as there are no bindings inside tactics though.
2059 mkUniqT tac = return tac
2061 mkUniq :: PTerm -> State (S.Set Name) PTerm
2062 mkUniq (PLam fc n ty sc)
2063 = do env <- get
2064 (n', sc') <-
2065 if n `S.member` env
2066 then do let n' = uniqueNameSet (initN n (S.size env))
2067 (S.union env inScope)
2068 return (n', shadow n n' sc)
2069 else return (n, sc)
2070 put (S.insert n' env)
2071 ty' <- mkUniq ty
2072 sc'' <- mkUniq sc'
2073 return $! PLam fc n' ty' sc''
2074 mkUniq (PPi p n ty sc)
2075 = do env <- get
2076 (n', sc') <-
2077 if n `S.member` env
2078 then do let n' = uniqueNameSet (initN n (S.size env))
2079 (S.union env inScope)
2080 return (n', shadow n n' sc)
2081 else return (n, sc)
2082 put (S.insert n' env)
2083 ty' <- mkUniq ty
2084 sc'' <- mkUniq sc'
2085 return $! PPi p n' ty' sc''
2086 mkUniq (PLet fc n ty val sc)
2087 = do env <- get
2088 (n', sc') <-
2089 if n `S.member` env
2090 then do let n' = uniqueNameSet (initN n (S.size env))
2091 (S.union env inScope)
2092 return (n', shadow n n' sc)
2093 else return (n, sc)
2094 put (S.insert n' env)
2095 ty' <- mkUniq ty; val' <- mkUniq val
2096 sc'' <- mkUniq sc'
2097 return $! PLet fc n' ty' val' sc''
2098 mkUniq (PApp fc t args)
2099 = do t' <- mkUniq t
2100 args' <- mapM mkUniqA args
2101 return $! PApp fc t' args'
2102 mkUniq (PAppBind fc t args)
2103 = do t' <- mkUniq t
2104 args' <- mapM mkUniqA args
2105 return $! PAppBind fc t' args'
2106 mkUniq (PCase fc t alts)
2107 = do t' <- mkUniq t
2108 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2109 return (x', y')) alts
2110 return $! PCase fc t' alts'
2111 mkUniq (PPair fc p l r)
2112 = do l' <- mkUniq l; r' <- mkUniq r
2113 return $! PPair fc p l' r'
2114 mkUniq (PDPair fc p (PRef fc' n) t sc)
2115 | t /= Placeholder
2116 = do env <- get
2117 (n', sc') <- if n `S.member` env
2118 then do let n' = uniqueNameSet n (S.union env inScope)
2119 return (n', shadow n n' sc)
2120 else return (n, sc)
2121 put (S.insert n' env)
2122 t' <- mkUniq t
2123 sc'' <- mkUniq sc'
2124 return $! PDPair fc p (PRef fc' n') t' sc''
2125 mkUniq (PDPair fc p l t r)
2126 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2127 return $! PDPair fc p l' t' r'
2128 mkUniq (PAlternative b as)
2129 = liftM (PAlternative b) (mapM mkUniq as)
2130 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2131 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2132 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2133 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2134 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2135 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2136 mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
2137 mkUniq t = return t