git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2134 lines 90 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 { next_tvar = v }
547 let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
548 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
549 where
550 insertAll [] c = c
551 insertAll ((c, fc) : cs) ics
552 = insertAll cs $ S.insert (ConstraintFC c fc) ics
554addDeferred = addDeferred' Ref
555addDeferredTyCon = addDeferred' (TCon 0 0)
557-- | Save information about a name that is not yet defined
558addDeferred' :: NameType
559 -> [(Name, (Int, Maybe Name, Type, Bool))]
560 -- ^ The Name is the name being made into a metavar,
561 -- the Int is the number of vars that are part of a
562 -- putative proof context, the Maybe Name is the
563 -- top-level function containing the new metavariable,
564 -- the Type is its type, and the Bool is whether :p is
565 -- allowed
566 -> Idris ()
567addDeferred' nt ns
568 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
569 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
570 i <- getIState
571 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
572 idris_metavars i }
573 where
574 -- 'tidyNames' is to generate user accessible names in case they are
575 -- needed in tactic scripts
576 tidyNames used (Bind (MN i x) b sc)
577 = let n' = uniqueNameSet (UN x) used in
578 Bind n' b $ tidyNames (S.insert n' used) sc
579 tidyNames used (Bind n b sc)
580 = let n' = uniqueNameSet n used in
581 Bind n' b $ tidyNames (S.insert n' used) sc
582 tidyNames used b = b
584solveDeferred :: Name -> Idris ()
585solveDeferred n = do i <- getIState
586 putIState $ i { idris_metavars =
587 filter (\(n', _) -> n/=n')
588 (idris_metavars i),
589 ibc_write =
590 filter (notMV n) (ibc_write i)
591 }
592 where notMV n (IBCMetavar n') = not (n == n')
593 notMV n _ = True
595getUndefined :: Idris [Name]
596getUndefined = do i <- getIState
597 return (map fst (idris_metavars i) \\ primDefs)
599isMetavarName :: Name -> IState -> Bool
600isMetavarName n ist
601 = case lookupNames n (tt_ctxt ist) of
602 (t:_) -> isJust $ lookup t (idris_metavars ist)
603 _ -> False
605getWidth :: Idris ConsoleWidth
606getWidth = fmap idris_consolewidth getIState
608setWidth :: ConsoleWidth -> Idris ()
609setWidth w = do ist <- getIState
610 put ist { idris_consolewidth = w }
615type1Doc :: Doc OutputAnnotation
616type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
619isetPrompt :: String -> Idris ()
620isetPrompt p = do i <- getIState
621 case idris_outputmode i of
622 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
624-- | Tell clients how much was parsed and loaded
625isetLoadedRegion :: Idris ()
626isetLoadedRegion = do i <- getIState
627 let span = idris_parsedSpan i
628 case span of
629 Just fc ->
630 case idris_outputmode i of
631 IdeMode n h ->
632 runIO . hPutStrLn h $
633 convSExp "set-loaded-region" fc n
634 Nothing -> return ()
636setLogLevel :: Int -> Idris ()
637setLogLevel l = do i <- getIState
638 let opts = idris_options i
639 let opt' = opts { opt_logLevel = l }
640 putIState $ i { idris_options = opt' }
642setCmdLine :: [Opt] -> Idris ()
643setCmdLine opts = do i <- getIState
644 let iopts = idris_options i
645 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
647getCmdLine :: Idris [Opt]
648getCmdLine = do i <- getIState
649 return (opt_cmdline (idris_options i))
651getDumpDefun :: Idris (Maybe FilePath)
652getDumpDefun = do i <- getIState
653 return $ findC (opt_cmdline (idris_options i))
654 where findC [] = Nothing
655 findC (DumpDefun x : _) = Just x
656 findC (_ : xs) = findC xs
658getDumpCases :: Idris (Maybe FilePath)
659getDumpCases = do i <- getIState
660 return $ findC (opt_cmdline (idris_options i))
661 where findC [] = Nothing
662 findC (DumpCases x : _) = Just x
663 findC (_ : xs) = findC xs
665logLevel :: Idris Int
666logLevel = do i <- getIState
667 return (opt_logLevel (idris_options i))
669setErrContext :: Bool -> Idris ()
670setErrContext t = do i <- getIState
671 let opts = idris_options i
672 let opts' = opts { opt_errContext = t }
673 putIState $ i { idris_options = opts' }
675errContext :: Idris Bool
676errContext = do i <- getIState
677 return (opt_errContext (idris_options i))
679getOptimise :: Idris [Optimisation]
680getOptimise = do i <- getIState
681 return (opt_optimise (idris_options i))
683setOptimise :: [Optimisation] -> Idris ()
684setOptimise newopts = do i <- getIState
685 let opts = idris_options i
686 let opts' = opts { opt_optimise = newopts }
687 putIState $ i { idris_options = opts' }
689addOptimise :: Optimisation -> Idris ()
690addOptimise opt = do opts <- getOptimise
691 setOptimise (nub (opt : opts))
693removeOptimise :: Optimisation -> Idris ()
694removeOptimise opt = do opts <- getOptimise
695 setOptimise ((nub opts) \\ [opt])
697-- Set appropriate optimisation set for the given level. We only have
698-- one optimisation that is configurable at the moment, however!
699setOptLevel :: Int -> Idris ()
700setOptLevel n | n <= 0 = setOptimise []
701setOptLevel 1 = setOptimise []
702setOptLevel 2 = setOptimise [PETransform]
703setOptLevel n | n >= 3 = setOptimise [PETransform]
705useREPL :: Idris Bool
706useREPL = do i <- getIState
707 return (opt_repl (idris_options i))
709setREPL :: Bool -> Idris ()
710setREPL t = do i <- getIState
711 let opts = idris_options i
712 let opt' = opts { opt_repl = t }
713 putIState $ i { idris_options = opt' }
715showOrigErr :: Idris Bool
716showOrigErr = do i <- getIState
717 return (opt_origerr (idris_options i))
719setShowOrigErr :: Bool -> Idris ()
720setShowOrigErr b = do i <- getIState
721 let opts = idris_options i
722 let opt' = opts { opt_origerr = b }
723 putIState $ i { idris_options = opt' }
725setAutoSolve :: Bool -> Idris ()
726setAutoSolve b = do i <- getIState
727 let opts = idris_options i
728 let opt' = opts { opt_autoSolve = b }
729 putIState $ i { idris_options = opt' }
731setNoBanner :: Bool -> Idris ()
732setNoBanner n = do i <- getIState
733 let opts = idris_options i
734 let opt' = opts { opt_nobanner = n }
735 putIState $ i { idris_options = opt' }
737getNoBanner :: Idris Bool
738getNoBanner = do i <- getIState
739 let opts = idris_options i
740 return (opt_nobanner opts)
742setQuiet :: Bool -> Idris ()
743setQuiet q = do i <- getIState
744 let opts = idris_options i
745 let opt' = opts { opt_quiet = q }
746 putIState $ i { idris_options = opt' }
748getQuiet :: Idris Bool
749getQuiet = do i <- getIState
750 let opts = idris_options i
751 return (opt_quiet opts)
753setCodegen :: Codegen -> Idris ()
754setCodegen t = do i <- getIState
755 let opts = idris_options i
756 let opt' = opts { opt_codegen = t }
757 putIState $ i { idris_options = opt' }
759codegen :: Idris Codegen
760codegen = do i <- getIState
761 return (opt_codegen (idris_options i))
763setOutputTy :: OutputType -> Idris ()
764setOutputTy t = do i <- getIState
765 let opts = idris_options i
766 let opt' = opts { opt_outputTy = t }
767 putIState $ i { idris_options = opt' }
769outputTy :: Idris OutputType
770outputTy = do i <- getIState
771 return $ opt_outputTy $ idris_options i
773setIdeMode :: Bool -> Handle -> Idris ()
774setIdeMode True h = do i <- getIState
775 putIState $ i { idris_outputmode = IdeMode 0 h
776 , idris_colourRepl = False
777 }
778setIdeMode False _ = return ()
780setTargetTriple :: String -> Idris ()
781setTargetTriple t = do i <- getIState
782 let opts = idris_options i
783 opt' = opts { opt_triple = t }
784 putIState $ i { idris_options = opt' }
786targetTriple :: Idris String
787targetTriple = do i <- getIState
788 return (opt_triple (idris_options i))
790setTargetCPU :: String -> Idris ()
791setTargetCPU t = do i <- getIState
792 let opts = idris_options i
793 opt' = opts { opt_cpu = t }
794 putIState $ i { idris_options = opt' }
796targetCPU :: Idris String
797targetCPU = do i <- getIState
798 return (opt_cpu (idris_options i))
800verbose :: Idris Bool
801verbose = do i <- getIState
802 return (opt_verbose (idris_options i))
804setVerbose :: Bool -> Idris ()
805setVerbose t = do i <- getIState
806 let opts = idris_options i
807 let opt' = opts { opt_verbose = t }
808 putIState $ i { idris_options = opt' }
810typeInType :: Idris Bool
811typeInType = do i <- getIState
812 return (opt_typeintype (idris_options i))
814setTypeInType :: Bool -> Idris ()
815setTypeInType t = do i <- getIState
816 let opts = idris_options i
817 let opt' = opts { opt_typeintype = t }
818 putIState $ i { idris_options = opt' }
820coverage :: Idris Bool
821coverage = do i <- getIState
822 return (opt_coverage (idris_options i))
824setCoverage :: Bool -> Idris ()
825setCoverage t = do i <- getIState
826 let opts = idris_options i
827 let opt' = opts { opt_coverage = t }
828 putIState $ i { idris_options = opt' }
830setIBCSubDir :: FilePath -> Idris ()
831setIBCSubDir fp = do i <- getIState
832 let opts = idris_options i
833 let opt' = opts { opt_ibcsubdir = fp }
834 putIState $ i { idris_options = opt' }
836valIBCSubDir :: IState -> Idris FilePath
837valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
839addImportDir :: FilePath -> Idris ()
840addImportDir fp = do i <- getIState
841 let opts = idris_options i
842 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
843 putIState $ i { idris_options = opt' }
845setImportDirs :: [FilePath] -> Idris ()
846setImportDirs fps = do i <- getIState
847 let opts = idris_options i
848 let opt' = opts { opt_importdirs = fps }
849 putIState $ i { idris_options = opt' }
851allImportDirs :: Idris [FilePath]
852allImportDirs = do i <- getIState
853 let optdirs = opt_importdirs (idris_options i)
854 return ("." : reverse optdirs)
856colourise :: Idris Bool
857colourise = do i <- getIState
858 return $ idris_colourRepl i
860setColourise :: Bool -> Idris ()
861setColourise b = do i <- getIState
862 putIState $ i { idris_colourRepl = b }
864impShow :: Idris Bool
865impShow = do i <- getIState
866 return (opt_showimp (idris_options i))
868setImpShow :: Bool -> Idris ()
869setImpShow t = do i <- getIState
870 let opts = idris_options i
871 let opt' = opts { opt_showimp = t }
872 putIState $ i { idris_options = opt' }
874setColour :: ColourType -> IdrisColour -> Idris ()
875setColour ct c = do i <- getIState
876 let newTheme = setColour' ct c (idris_colourTheme i)
877 putIState $ i { idris_colourTheme = newTheme }
878 where setColour' KeywordColour c t = t { keywordColour = c }
879 setColour' BoundVarColour c t = t { boundVarColour = c }
880 setColour' ImplicitColour c t = t { implicitColour = c }
881 setColour' FunctionColour c t = t { functionColour = c }
882 setColour' TypeColour c t = t { typeColour = c }
883 setColour' DataColour c t = t { dataColour = c }
884 setColour' PromptColour c t = t { promptColour = c }
885 setColour' PostulateColour c t = t { postulateColour = c }
887logLvl :: Int -> String -> Idris ()
888logLvl l str = do i <- getIState
889 let lvl = opt_logLevel (idris_options i)
890 when (lvl >= l) $
891 case idris_outputmode i of
892 RawOutput h -> do runIO $ hPutStrLn h str
893 IdeMode n h ->
894 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
895 runIO . hPutStrLn h $ convSExp "log" good n
897cmdOptType :: Opt -> Idris Bool
898cmdOptType x = do i <- getIState
899 return $ x `elem` opt_cmdline (idris_options i)
901iLOG :: String -> Idris ()
902iLOG = logLvl 1
904noErrors :: Idris Bool
905noErrors = do i <- getIState
906 case errSpan i of
907 Nothing -> return True
908 _ -> return False
910setTypeCase :: Bool -> Idris ()
911setTypeCase t = do i <- getIState
912 let opts = idris_options i
913 let opt' = opts { opt_typecase = t }
914 putIState $ i { idris_options = opt' }
917-- Dealing with parameters
919expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
920 [Name] -> -- all names
921 [Name] -> -- names with no declaration
922 PTerm -> PTerm
923expandParams dec ps ns infs tm = en tm
924 where
925 -- if we shadow a name (say in a lambda binding) that is used in a call to
926 -- a lifted function, we need access to both names - once in the scope of the
927 -- binding and once to call the lifted functions. So we'll explicitly shadow
928 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
929 -- but we didn't...)
931 mkShadow (UN n) = MN 0 n
932 mkShadow (MN i n) = MN (i+1) n
933 mkShadow (NS x s) = NS (mkShadow x) s
935 en (PLam fc n t s)
936 | n `elem` (map fst ps ++ ns)
937 = let n' = mkShadow n in
938 PLam fc n' (en t) (en (shadow n n' s))
939 | otherwise = PLam fc n (en t) (en s)
940 en (PPi p n t s)
941 | n `elem` (map fst ps ++ ns)
942 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
943 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
944 | otherwise = PPi (enTacImp p) n (en t) (en s)
945 en (PLet fc n ty v s)
946 | n `elem` (map fst ps ++ ns)
947 = let n' = mkShadow n in
948 PLet fc n' (en ty) (en v) (en (shadow n n' s))
949 | otherwise = PLet fc n (en ty) (en v) (en s)
950 -- FIXME: Should only do this in a type signature!
951 en (PDPair f p (PRef f' n) t r)
952 | n `elem` (map fst ps ++ ns) && t /= Placeholder
953 = let n' = mkShadow n in
954 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
955 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
956 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
957 en (PTyped l r) = PTyped (en l) (en r)
958 en (PPair f p l r) = PPair f p (en l) (en r)
959 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
960 en (PAlternative a as) = PAlternative a (map en as)
961 en (PHidden t) = PHidden (en t)
962 en (PUnifyLog t) = PUnifyLog (en t)
963 en (PDisamb ds t) = PDisamb ds (en t)
964 en (PNoImplicits t) = PNoImplicits (en t)
965 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
966 en (PProof ts) = PProof (map (fmap en) ts)
967 en (PTactics ts) = PTactics (map (fmap en) ts)
969 en (PQuote (Var n))
970 | n `nselem` ns = PQuote (Var (dec n))
971 en (PApp fc (PInferRef fc' n) as)
972 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
973 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
974 en (PApp fc (PRef fc' n) as)
975 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
976 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
977 | n `nselem` ns = PApp fc (PRef fc' (dec n))
978 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
979 en (PAppBind fc (PRef fc' n) as)
980 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
981 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
982 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
983 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
984 en (PRef fc n)
985 | n `elem` infs = PApp fc (PInferRef fc (dec n))
986 (map (pexp . (PRef fc)) (map fst ps))
987 | n `nselem` ns = PApp fc (PRef fc (dec n))
988 (map (pexp . (PRef fc)) (map fst ps))
989 en (PInferRef fc n)
990 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
991 (map (pexp . (PRef fc)) (map fst ps))
992 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
993 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
994 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
995 en (PRunTactics fc tm) = PRunTactics fc (en tm)
996 en t = t
998 nselem x [] = False
999 nselem x (y : xs) | nseq x y = True
1000 | otherwise = nselem x xs
1002 nseq x y = nsroot x == nsroot y
1004 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1005 enTacImp other = other
1007expandParamsD :: Bool -> -- True = RHS only
1008 IState ->
1009 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1010expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
1011 = if n `elem` ns && (not rhsonly)
1012 then -- trace (show (n, expandParams dec ps ns ty)) $
1013 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
1014 else --trace (show (n, expandParams dec ps ns ty)) $
1015 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
1016expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
1017 = if n `elem` ns && (not rhsonly)
1018 then -- trace (show (n, expandParams dec ps ns ty)) $
1019 PPostulate doc syn fc o (dec n) (piBind ps
1020 (expandParams dec ps ns [] ty))
1021 else --trace (show (n, expandParams dec ps ns ty)) $
1022 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1023expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1024 = let n' = if n `elem` ns then dec n else n in
1025 PClauses fc opts n' (map expandParamsC cs)
1026 where
1027 expandParamsC (PClause fc n lhs ws rhs ds)
1028 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1029 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1030 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1031 n' = if n `elem` ns then dec n else n
1032 -- names bound on the lhs should not be expanded on the rhs
1033 ns' = removeBound lhs ns in
1034 PClause fc n' lhs'
1035 (map (expandParams dec ps'' ns' []) ws)
1036 (expandParams dec ps'' ns' [] rhs)
1037 (map (expandParamsD True ist dec ps'' ns') ds)
1038 expandParamsC (PWith fc n lhs ws wval pn ds)
1039 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1040 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1041 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1042 n' = if n `elem` ns then dec n else n
1043 ns' = removeBound lhs ns in
1044 PWith fc n' lhs'
1045 (map (expandParams dec ps'' ns' []) ws)
1046 (expandParams dec ps'' ns' [] wval)
1047 pn
1048 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1049 updateps yn nm [] = []
1050 updateps yn nm (((a, t), i):as)
1051 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1052 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1054 removeBound lhs ns = ns \\ nub (bnames lhs)
1056 bnames (PRef _ n) = [n]
1057 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1058 bnames (PPair _ _ l r) = bnames l ++ bnames r
1059 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1060 bnames _ = []
1062-- | Expands parameters defined in parameter and where blocks inside of declarations
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 opts cdoc cn cty)
1076 = if tn `elem` ns
1077 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1078 opts cdoc (dec cn) conty
1079 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1080 opts 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 pDocs fds decls)
1089 = PClass doc info f
1090 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1092 (map (mapsnd (expandParams dec ps ns [])) params)
1093 pDocs
1094 fds
1095 (map (expandParamsD rhs ist dec ps ns) decls)
1096expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)
1097 = PInstance doc argDocs info f
1098 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1100 (map (expandParams dec ps ns []) params)
1101 (expandParams dec ps ns [] ty)
1102 cn
1103 (map (expandParamsD rhs ist dec ps ns) decls)
1104expandParamsD rhs ist dec ps ns d = d
1106mapsnd f (x, t) = (x, f t)
1108-- Calculate a priority for a type, for deciding elaboration order
1109-- * if it's just a type variable or concrete type, do it early (0)
1110-- * if there's only type variables and injective constructors, do it next (1)
1111-- * if there's a function type, next (2)
1112-- * finally, everything else (3)
1114getPriority :: IState -> PTerm -> Int
1115getPriority i tm = 1 -- pri tm
1116 where
1117 pri (PRef _ n) =
1118 case lookupP n (tt_ctxt i) of
1119 ((P (DCon _ _ _) _ _):_) -> 1
1120 ((P (TCon _ _) _ _):_) -> 1
1121 ((P Ref _ _):_) -> 1
1122 [] -> 0 -- must be locally bound, if it's not an error...
1123 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1124 pri (PTrue _ _) = 0
1125 pri (PRefl _ _) = 1
1126 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1127 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1128 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1129 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1130 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1131 pri (PTyped l r) = pri l
1132 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1133 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1134 pri (PAlternative a as) = maximum (map pri as)
1135 pri (PConstant _) = 0
1136 pri Placeholder = 1
1137 pri _ = 3
1140addStatics :: Name -> Term -> PTerm -> Idris ()
1141addStatics n tm ptm =
1142 do let (statics, dynamics) = initStatics tm ptm
1143 ist <- getIState
1144 let paramnames
1145 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1146 Just p -> getNamesFrom 0 (fn_params p) tm ++
1147 concatMap (getParamNames ist) (map snd statics)
1148 _ -> concatMap (getParamNames ist) (map snd statics)
1150 let stnames = nub $ concatMap freeArgNames (map snd statics)
1151 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1152 \\ paramnames
1153 -- also get the arguments which are 'uniquely inferrable' from
1154 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1155 -- or parameters to the type of a static
1156 let statics' = nub $ map fst statics ++
1157 filter (\x -> not (elem x dnames)) stnames
1158 let stpos = staticList statics' tm
1159 i <- getIState
1160 when (not (null statics)) $
1161 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1162 ++ showTmImpls ptm ++ "\n"
1163 ++ show statics ++ "\n" ++ show dynamics
1164 ++ "\n" ++ show paramnames
1165 ++ "\n" ++ show stpos
1166 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1167 addIBC (IBCStatic n)
1168 where
1169 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
1170 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1171 (static, (n, ty) : dynamic)
1172 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)
1173 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1174 if pstatic p == Static then ((n, ty) : static, dynamic)
1175 else if (not (searchArg p))
1176 then (static, (n, ty) : dynamic)
1177 else (static, dynamic)
1178 initStatics t pt = ([], [])
1180 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1181 = case lookupCtxtExact n (idris_datatypes ist) of
1182 Just ti -> getNamePos 0 (param_pos ti) args
1183 Nothing -> []
1184 where getNamePos i ps [] = []
1185 getNamePos i ps (P _ n _ : as)
1186 | i `elem` ps = n : getNamePos (i + 1) ps as
1187 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1188 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1189 = n : getParamNames ist sc
1190 getParamNames ist _ = []
1192 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1193 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1194 | otherwise = getNamesFrom (i + 1) ps sc
1195 getNamesFrom i ps sc = []
1197 freeArgNames (Bind n (Pi _ ty _) sc)
1198 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1199 freeArgNames tm = let (_, args) = unApply tm in
1200 concatMap freeNames args
1202 -- if a name appears in a type class or tactic implicit index, it doesn't
1203 -- affect its 'uniquely inferrable' from a static status since these are
1204 -- resolved by searching.
1205 searchArg (Constraint _ _) = True
1206 searchArg (TacImp _ _ _) = True
1207 searchArg _ = False
1209 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1210 staticList _ _ = []
1212-- Dealing with implicit arguments
1214-- Add some bound implicits to the using block if they aren't there already
1216addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1217addToUsing us [] = us
1218addToUsing us ((n, t) : ns)
1219 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1220 | otherwise = addToUsing us ns
1221 where impName (UImplicit n _) = Just n
1222 impName _ = Nothing
1224-- Add constraint bindings from using block
1226addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1227addUsingConstraints syn fc t
1228 = do ist <- get
1229 let ns = namesIn [] ist t
1230 let cs = getConstraints t -- check declared constraints
1231 let addconsts = uconsts \\ cs
1232 return (doAdd addconsts ns t)
1233 where uconsts = filter uconst (using syn)
1234 uconst (UConstraint _ _) = True
1235 uconst _ = False
1237 doAdd [] _ t = t
1238 -- if all of args in ns, then add it
1239 doAdd (UConstraint c args : cs) ns t
1240 | all (\n -> elem n ns) args
1241 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1242 (mkConst c args) (doAdd cs ns t)
1243 | otherwise = doAdd cs ns t
1245 mkConst c args = PApp fc (PRef fc c)
1246 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1248 getConstraints (PPi (Constraint _ _) _ c sc)
1249 = getcapp c ++ getConstraints sc
1250 getConstraints (PPi _ _ c sc) = getConstraints sc
1251 getConstraints _ = []
1253 getcapp (PApp _ (PRef _ c) args)
1254 = do ns <- mapM getName args
1255 return (UConstraint c ns)
1256 getcapp _ = []
1258 getName (PExp _ _ _ (PRef _ n)) = return n
1259 getName _ = []
1261-- Add implicit bindings from using block, and bind any missing names
1262addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1263addUsingImpls syn n fc t
1264 = do ist <- getIState
1265 let ns = implicitNamesIn (map iname uimpls) ist t
1266 let badnames = filter (\n -> not (implicitable n) &&
1267 n `notElem` (map iname uimpls)) ns
1268 when (not (null badnames)) $
1269 throwError (At fc (Elaborating "type of " n
1270 (NoSuchVariable (head badnames))))
1271 let cs = getArgnames t -- get already bound names
1272 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1273 -- if all names in the arguments of addconsts appear in ns,
1274 -- add the constraint implicitly
1275 return (bindFree ns (doAdd addimpls ns t))
1276 where uimpls = filter uimpl (using syn)
1277 uimpl (UImplicit _ _) = True
1278 uimpl _ = False
1280 iname (UImplicit n _) = n
1281 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1283 doAdd [] _ t = t
1284 -- if all of args in ns, then add it
1285 doAdd (UImplicit n ty : cs) ns t
1286 | elem n ns
1287 = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)
1288 | otherwise = doAdd cs ns t
1290 -- bind the free names which weren't in the using block
1291 bindFree [] tm = tm
1292 bindFree (n:ns) tm
1293 | elem n (map iname uimpls) = bindFree ns tm
1294 | otherwise
1295 = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
1297 getArgnames (PPi _ n c sc)
1298 = n : getArgnames sc
1299 getArgnames _ = []
1301-- Given the original type and the elaborated type, return the implicitness
1302-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1304getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1305getUnboundImplicits i t tm = getImps t (collectImps tm)
1306 where collectImps (PPi p n t sc)
1307 = (n, (p, t)) : collectImps sc
1308 collectImps _ = []
1310 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1311 getImps (Bind n (Pi _ t _) sc) imps
1312 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1313 where
1314 argInfo n (Imp opt _ _ _) Placeholder
1315 = (True, PImp 0 True opt n Placeholder)
1316 argInfo n (Imp opt _ _ _) t'
1317 = (False, PImp (getPriority i t') True opt n t')
1318 argInfo n (Exp opt _ _) t'
1319 = (InaccessibleArg `elem` opt,
1320 PExp (getPriority i t') opt n t')
1321 argInfo n (Constraint opt _) t'
1322 = (InaccessibleArg `elem` opt,
1323 PConstraint 10 opt n t')
1324 argInfo n (TacImp opt _ scr) t'
1325 = (InaccessibleArg `elem` opt,
1326 PTacImplicit 10 opt n scr t')
1327 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1328 where impBind n t = (True, PImp 1 True [] n Placeholder)
1329 getImps sc tm = []
1331-- Add implicit Pi bindings for any names in the term which appear in an
1332-- argument position.
1334-- This has become a right mess already. Better redo it some time...
1335-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1336-- a couple of places which use it. Clean them up!
1338-- Issue 1739 in the issue tracker
1339-- https://github.com/idris-lang/Idris-dev/issues/1739
1340implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1341implicit info syn n ptm = implicit' info syn [] n ptm
1343implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1344implicit' info syn ignore n ptm
1345 = do i <- getIState
1346 let (tm', impdata) = implicitise syn ignore i ptm
1347 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1348-- let (tm'', spos) = findStatics i tm'
1349 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1350 addIBC (IBCImp n)
1351 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1352-- i <- get
1353-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1354 return tm'
1355 where
1356 -- Detect unknown names in default arguments and throw error if found.
1357 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1358 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1360 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1361 notFoundInDefault kns (PTacImplicit _ _ n script _)
1362 = do i <- getIState
1363 case notFound kns (namesIn [] i script) of
1364 Nothing -> return (n:kns)
1365 Just name -> throwError (NoSuchVariable name)
1366 notFoundInDefault kns p = return ((pname p):kns)
1368 notFound :: [Name] -> [Name] -> Maybe Name
1369 notFound kns [] = Nothing
1370 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1371 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1373implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1374implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1375 let (declimps, ns') = execState (imps True [] tm) ([], [])
1376 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1377 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1378 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1379 if null ns
1380 then (tm, reverse declimps)
1381 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1382 where
1383 uvars = map ipair (filter uimplicit (using syn))
1384 pvars = syn_params syn
1386 inUsing n = n `elem` map fst uvars
1388 ipair (UImplicit x y) = (x, y)
1389 uimplicit (UImplicit _ _) = True
1390 uimplicit _ = False
1392 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1393 | otherwise = x : dropAll xs ys
1394 dropAll [] ys = []
1396 -- Find names in argument position in a type, suitable for implicit
1397 -- binding
1398 -- Not the function position, but do everything else...
1399 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1400 implNamesIn uv t = namesIn uv ist t
1402 imps top env (PApp _ f as)
1403 = do (decls, ns) <- get
1404 let isn = concatMap (namesIn uvars ist) (map getTm as)
1405 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1406 imps top env (PPi (Imp l _ _ _) n ty sc)
1407 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1408 (decls , ns) <- get
1409 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1410 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1411 imps True (n:env) sc
1412 imps top env (PPi (Exp l _ _) n ty sc)
1413 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1414 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1415 _ -> [])
1416 (decls, ns) <- get -- ignore decls in HO types
1417 put (PExp (getPriority ist ty) l n Placeholder : decls,
1418 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1419 imps True (n:env) sc
1420 imps top env (PPi (Constraint l _) n ty sc)
1421 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1422 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1423 _ -> [])
1424 (decls, ns) <- get -- ignore decls in HO types
1425 put (PConstraint 10 l n Placeholder : decls,
1426 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1427 imps True (n:env) sc
1428 imps top env (PPi (TacImp l _ scr) n ty sc)
1429 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1430 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1431 _ -> [])
1432 (decls, ns) <- get -- ignore decls in HO types
1433 put (PTacImplicit 10 l n scr Placeholder : decls,
1434 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1435 imps True (n:env) sc
1436 imps top env (PEq _ _ _ l r)
1437 = do (decls, ns) <- get
1438 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1439 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1440 imps top env (PRewrite _ l r _)
1441 = do (decls, ns) <- get
1442 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1443 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1444 imps top env (PTyped l r)
1445 = imps top env l
1446 imps top env (PPair _ _ l r)
1447 = do (decls, ns) <- get
1448 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1449 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1450 imps top env (PDPair _ _ (PRef _ n) t r)
1451 = do (decls, ns) <- get
1452 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1453 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1454 imps top env (PDPair _ _ l t r)
1455 = do (decls, ns) <- get
1456 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1457 namesIn uvars ist r
1458 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1459 imps top env (PAlternative a as)
1460 = do (decls, ns) <- get
1461 let isn = concatMap (namesIn uvars ist) as
1462 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1463 imps top env (PLam fc n ty sc)
1464 = do imps False env ty
1465 imps False (n:env) sc
1466 imps top env (PHidden tm) = imps False env tm
1467 imps top env (PUnifyLog tm) = imps False env tm
1468 imps top env (PNoImplicits tm) = imps False env tm
1469 imps top env (PRunTactics fc tm) = imps False env tm
1470 imps top env _ = return ()
1472 pibind using [] sc = sc
1473 pibind using (n:ns) sc
1474 = case lookup n using of
1475 Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1476 Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1477 (pibind using ns sc)
1479-- Add implicit arguments in function calls
1480addImplPat :: IState -> PTerm -> PTerm
1481addImplPat = addImpl' True [] [] []
1483addImplBound :: IState -> [Name] -> PTerm -> PTerm
1484addImplBound ist ns = addImpl' False ns [] [] ist
1486addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1487addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
1489-- | Add the implicit arguments to applications in the term
1490-- [Name] gives the names to always expend, even when under a binder of
1491-- that name (this is to expand methods with implicit arguments in dependent
1492-- type classes).
1493addImpl :: [Name] -> IState -> PTerm -> PTerm
1494addImpl = addImpl' False [] []
1496-- TODO: in patterns, don't add implicits to function names guarded by constructors
1497-- and *not* inside a PHidden
1499addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1500addImpl' inpat env infns imp_meths ist ptm
1501 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1502 where
1503 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1504 ai qq env ds (PRef fc f)
1505 | f `elem` infns = PInferRef fc f
1506 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []
1507 ai qq env ds (PHidden (PRef fc f))
1508 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])
1509 ai qq env ds (PEq fc lt rt l r)
1510 = let lt' = ai qq env ds lt
1511 rt' = ai qq env ds rt
1512 l' = ai qq env ds l
1513 r' = ai qq env ds r in
1514 PEq fc lt' rt' l' r'
1515 ai qq env ds (PRewrite fc l r g)
1516 = let l' = ai qq env ds l
1517 r' = ai qq env ds r
1518 g' = fmap (ai qq env ds) g in
1519 PRewrite fc l' r' g'
1520 ai qq env ds (PTyped l r)
1521 = let l' = ai qq env ds l
1522 r' = ai qq env ds r in
1523 PTyped l' r'
1524 ai qq env ds (PPair fc p l r)
1525 = let l' = ai qq env ds l
1526 r' = ai qq env ds r in
1527 PPair fc p l' r'
1528 ai qq env ds (PDPair fc p l t r)
1529 = let l' = ai qq env ds l
1530 t' = ai qq env ds t
1531 r' = ai qq env ds r in
1532 PDPair fc p l' t' r'
1533 ai qq env ds (PAlternative a as)
1534 = let as' = map (ai qq env ds) as in
1535 PAlternative a as'
1536 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1537 ai qq env ds (PApp fc (PInferRef _ f) as)
1538 = let as' = map (fmap (ai qq env ds)) as in
1539 PApp fc (PInferRef fc f) as'
1540 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1541 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1542 | not (f `elem` map fst env)
1543 = let as' = map (fmap (ai qq env ds)) as in
1544 handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'
1545 | Just (Just ty) <- lookup f env =
1546 let as' = map (fmap (ai qq env ds)) as
1547 arity = getPArity ty in
1548 mkPApp fc arity ftm as'
1549 ai qq env ds (PApp fc f as)
1550 = let f' = ai qq env ds f
1551 as' = map (fmap (ai qq env ds)) as in
1552 mkPApp fc 1 f' as'
1553 ai qq env ds (PCase fc c os)
1554 = let c' = ai qq env ds c in
1555 -- leave os alone, because they get lifted into a new pattern match
1556 -- definition which is passed through addImpl again with more scope
1557 -- information
1558 PCase fc c' os
1559 -- If the name in a lambda is a constructor name, do this as a 'case'
1560 -- instead (it is harmless to do so, especially since the lambda will
1561 -- be lifted anyway!)
1562 ai qq env ds (PLam fc n ty sc)
1563 = case lookupDef n (tt_ctxt ist) of
1564 [] -> let ty' = ai qq env ds ty
1565 sc' = ai qq ((n, Just ty):env) ds sc in
1566 PLam fc n ty' sc'
1567 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1568 (PCase fc (PRef fc (sMN 0 "lamp") )
1569 [(PRef fc n, sc)]))
1570 ai qq env ds (PLet fc n ty val sc)
1571 = case lookupDef n (tt_ctxt ist) of
1572 [] -> let ty' = ai qq env ds ty
1573 val' = ai qq env ds val
1574 sc' = ai qq ((n, Just ty):env) ds sc in
1575 PLet fc n ty' val' sc'
1576 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1577 ai qq env ds (PPi p n ty sc)
1578 = let ty' = ai qq env ds ty
1579 env' = if n `elem` imp_meths then env
1580 else ((n, Just ty) : env)
1581 sc' = ai qq env' ds sc in
1582 PPi p n ty' sc'
1583 ai qq env ds (PGoal fc r n sc)
1584 = let r' = ai qq env ds r
1585 sc' = ai qq ((n, Nothing):env) ds sc in
1586 PGoal fc r' n sc'
1587 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1588 -- Don't do PProof or PTactics since implicits get added when scope is
1589 -- properly known in ElabTerm.runTac
1590 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1591 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1592 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1593 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1594 (fmap (ai True env ds) g)
1595 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1596 ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
1597 ai qq env ds tm = tm
1599 handleErr (Left err) = PElabError err
1600 handleErr (Right x) = x
1602-- if in a pattern, and there are no arguments, and there's no possible
1603-- names with zero explicit arguments, don't add implicits.
1605aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1606aiFn inpat True qq imp_meths ist fc f ds []
1607 = case lookupDef f (tt_ctxt ist) of
1608 [] -> Right $ PPatvar fc f
1609 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1610 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1611 if (not (vname f) || tcname f
1612 || any (conCaf (tt_ctxt ist)) ialts)
1613-- any constructor alts || any allImp ialts))
1614 then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor
1615 else Right $ PPatvar fc f
1616 where imp (PExp _ _ _ _) = False
1617 imp _ = True
1618-- allImp [] = False
1619 allImp xs = all imp xs
1620 constructor (TyDecl (DCon _ _ _) _) = True
1621 constructor _ = False
1623 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1625 vname (UN n) = True -- non qualified
1626 vname _ = False
1628aiFn inpat expat qq imp_meths ist fc f ds as
1629 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1630aiFn inpat expat qq imp_meths ist fc f ds as
1631 -- This is where namespaces get resolved by adding PAlternative
1632 = do let ns = lookupCtxtName f (idris_implicits ist)
1633 let nh = filter (\(n, _) -> notHidden n) ns
1634 let ns' = case trimAlts ds nh of
1635 [] -> nh
1636 x -> x
1637 case ns' of
1638 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)
1639 [] -> if f `elem` (map fst (idris_metavars ist))
1640 then Right $ PApp fc (PRef fc f) as
1641 else Right $ mkPApp fc (length as) (PRef fc f) as
1642 alts -> Right $
1643 PAlternative True $
1644 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))
1645 (insertImpl ns as)) alts
1646 where
1647 -- if the name is in imp_meths, we should actually refer to the bound
1648 -- name rather than the global one after expanding implicits
1649 isImpName f f' | f `elem` imp_meths = f
1650 | otherwise = f'
1652 trimAlts [] alts = alts
1653 trimAlts ns alts
1654 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1656 nspace (NS _ s) = s
1657 nspace _ = []
1659 notHidden n = case getAccessibility n of
1660 Hidden -> False
1661 _ -> True
1663 getAccessibility n
1664 = case lookupDefAccExact n False (tt_ctxt ist) of
1665 Just (n,t) -> t
1666 _ -> Public
1668 insertImpl :: [PArg] -> [PArg] -> [PArg]
1669 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1671 exp (PExp _ _ _ _) = True
1672 exp (PConstraint _ _ _ _) = True
1673 exp _ = False
1675 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1676 -> [PArg] -- parameters
1677 -> [PArg] -- explicit arguments
1678 -> [PArg] -- implicits given
1679 -> [PArg]
1680 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1681 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1682 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1683 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1684 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1685 let rtc = PResolveTC fc in
1686 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1687 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1688 case find n imps [] of
1689 Just (tm, imps') ->
1690 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1691 Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
1692 PImp p True l n ph :
1693 insImpAcc (M.insert n ph pnas) ps given imps
1694 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1695 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1696 case find n imps [] of
1697 Just (tm, imps') ->
1698 PTacImplicit p l n sc tm :
1699 insImpAcc (M.insert n tm pnas) ps given imps'
1700 Nothing ->
1701 if inpat
1702 then PTacImplicit p l n sc Placeholder :
1703 insImpAcc (M.insert n Placeholder pnas) ps given imps
1704 else PTacImplicit p l n sc sc :
1705 insImpAcc (M.insert n sc pnas) ps given imps
1706 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1707 -- TODO: report here, and prune alternatives
1708 -- Issue #1740 in the Issue Tracker
1709-- https://github.com/idris-lang/Idris-dev/issues/1740
1710 insImpAcc _ _ given imps = given ++ imps
1712 find n [] acc = Nothing
1713 find n (PImp _ _ _ n' t : gs) acc
1714 | n == n' = Just (t, reverse acc ++ gs)
1715 find n (PTacImplicit _ _ n' _ t : gs) acc
1716 | n == n' = Just (t, reverse acc ++ gs)
1717 find n (g : gs) acc = find n gs (g : acc)
1719-- replace non-linear occurrences with _
1721stripLinear :: IState -> PTerm -> PTerm
1722stripLinear i tm = evalState (sl tm) [] where
1723 sl :: PTerm -> State [Name] PTerm
1724 sl (PRef fc f)
1725 | (_:_) <- lookupTy f (tt_ctxt i)
1726 = return $ PRef fc f
1727 | otherwise = do ns <- get
1728 if (f `elem` ns)
1729 then return $ PHidden (PRef fc f) -- Placeholder
1730 else do put (f : ns)
1731 return (PRef fc f)
1732 sl (PPatvar fc f)
1733 = do ns <- get
1734 if (f `elem` ns)
1735 then return $ PHidden (PPatvar fc f) -- Placeholder
1736 else do put (f : ns)
1737 return (PPatvar fc f)
1738 -- Assumption is that variables are all the same in each alternative
1739 sl t@(PAlternative b as) = do ns <- get
1740 as' <- slAlts ns as
1741 return (PAlternative b as')
1742 where slAlts ns (a : as) = do put ns
1743 a' <- sl a
1744 as' <- slAlts ns as
1745 return (a' : as')
1746 slAlts ns [] = return []
1747 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1748 sl (PDPair fc p l t r) = do l' <- sl l
1749 t' <- sl t
1750 r' <- sl r
1751 return (PDPair fc p l' t' r')
1752 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1753 args' <- mapM slA args
1754 return $ PApp fc fn args'
1755 where slA (PImp p m l n t) = do t' <- sl t
1756 return $ PImp p m l n t'
1757 slA (PExp p l n t) = do t' <- sl t
1758 return $ PExp p l n t'
1759 slA (PConstraint p l n t)
1760 = do t' <- sl t
1761 return $ PConstraint p l n t'
1762 slA (PTacImplicit p l n sc t)
1763 = do t' <- sl t
1764 return $ PTacImplicit p l n sc t'
1765 sl x = return x
1767-- Remove functions which aren't applied to anything, which must then
1768-- be resolved by unification. Assume names resolved and alternatives
1769-- filled in (so no ambiguity).
1771stripUnmatchable :: IState -> PTerm -> PTerm
1772stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1773 su :: PTerm -> PTerm
1774 su (PRef fc f)
1775 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1776 = Placeholder
1777 su (PApp fc f@(PRef _ fn) args)
1778 -- here we use canBeDConName because the impossible pattern
1779 -- check will not necessarily fully resolve constructor names,
1780 -- and these bare names will otherwise get in the way of
1781 -- impossbility checking.
1782 | canBeDConName fn ctxt
1783 = PApp fc f (fmap (fmap su) args)
1784 su (PApp fc f args)
1785 = PHidden (PApp fc f args)
1786 su (PAlternative b alts)
1787 = let alts' = filter (/= Placeholder) (map su alts) in
1788 if null alts' then Placeholder
1789 else PAlternative b alts'
1790 su (PPair fc p l r) = PPair fc p (su l) (su r)
1791 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1792 su t@(PLam fc _ _ _) = PHidden t
1793 su t@(PPi _ _ _ _) = PHidden t
1794 su t@(PEq _ _ _ _ _) = PHidden t
1795 su t = t
1797 ctxt = tt_ctxt i
1799stripUnmatchable i tm = tm
1801mkPApp fc a f [] = f
1802mkPApp fc a f as = let rest = drop a as in
1803 appRest fc (PApp fc f (take a as)) rest
1804 where
1805 appRest fc f [] = f
1806 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1808-- Find 'static' argument positions
1809-- (the declared ones, plus any names in argument position in the declared
1810-- statics)
1811-- FIXME: It's possible that this really has to happen after elaboration
1813findStatics :: IState -> PTerm -> (PTerm, [Bool])
1814findStatics ist tm = trace (show tm) $
1815 let (ns, ss) = fs tm in
1816 runState (pos ns ss tm) []
1817 where fs (PPi p n t sc)
1818 | Static <- pstatic p
1819 = let (ns, ss) = fs sc in
1820 (namesIn [] ist t : ns, n : ss)
1821 | otherwise = let (ns, ss) = fs sc in
1822 (ns, ss)
1823 fs _ = ([], [])
1825 inOne n ns = length (filter id (map (elem n) ns)) == 1
1827 pos ns ss (PPi p n t sc)
1828 | elem n ss = do sc' <- pos ns ss sc
1829 spos <- get
1830 put (True : spos)
1831 return (PPi (p { pstatic = Static }) n t sc')
1832 | otherwise = do sc' <- pos ns ss sc
1833 spos <- get
1834 put (False : spos)
1835 return (PPi p n t sc')
1836 pos ns ss t = return t
1838-- for 6.12/7 compatibility
1839data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1841instance Applicative (EitherErr a) where
1842 pure = return
1843 (<*>) = ap
1845instance Monad (EitherErr a) where
1846 return = RightOK
1848 (LeftErr e) >>= k = LeftErr e
1849 RightOK v >>= k = k v
1851toEither (LeftErr e) = Left e
1852toEither (RightOK ho) = Right ho
1854-- syntactic match of a against b, returning pair of variables in a
1855-- and what they match. Returns the pair that failed if not a match.
1857matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1858matchClause = matchClause' False
1860matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1861matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1862 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1864 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1865 fullApp x = x
1867 match' x y = match (fullApp x) (fullApp y)
1868 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1869 | fi == txt "fromInteger" && b == txt "builtins",
1870 PConstant (I _) <- getTm x = match (getTm x) x'
1871 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1872 | fi == txt "fromInteger" && b == txt "builtins",
1873 PConstant (I _) <- getTm x = match (getTm x) x'
1874 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1875 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1876 match (PApp _ f args) (PApp _ f' args')
1877 | length args == length args'
1878 = do mf <- match' f f'
1879 ms <- zipWithM matchArg args args'
1880 return (mf ++ concat ms)
1881 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1882 match (PPatvar f n) xr = match (PRef f n) xr
1883 match xr (PPatvar f n) = match xr (PRef f n)
1884 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1885 match (PRef _ n) tm@(PRef _ n')
1886 | n == n' && not names &&
1887 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1888 || tm == Placeholder)
1889 = return [(n, tm)]
1890 -- if one namespace is missing, drop the other
1891 | n == n' || n == dropNS n' || dropNS n == n' = return []
1892 where dropNS (NS n _) = n
1893 dropNS n = n
1894 match (PRef _ n) tm
1895 | not names && (not (isConName n (tt_ctxt i) ||
1896 isFnName n (tt_ctxt i)) || tm == Placeholder)
1897 = return [(n, tm)]
1898 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1899 = do ml <- match' l l'
1900 mr <- match' r r'
1901 return (ml ++ mr)
1902 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1903 = do ml <- match' l l'
1904 mr <- match' r r'
1905 return (ml ++ mr)
1906 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1907 mr <- match r r'
1908 return (ml ++ mr)
1909 match (PTyped l r) x = match l x
1910 match x (PTyped l r) = match x l
1911 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1912 mr <- match' r r'
1913 return (ml ++ mr)
1914 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1915 mt <- match' t t'
1916 mr <- match' r r'
1917 return (ml ++ mt ++ mr)
1918 match (PAlternative a as) (PAlternative a' as')
1919 = do ms <- zipWithM match' as as'
1920 return (concat ms)
1921 match a@(PAlternative _ as) b
1922 = do let ms = zipWith match' as (repeat b)
1923 case (rights (map toEither ms)) of
1924 (x: _) -> return x
1925 _ -> LeftErr (a, b)
1926 match (PCase _ _ _) _ = return [] -- lifted out
1927 match (PMetavar _) _ = return [] -- modified
1928 match (PInferRef _ _) _ = return [] -- modified
1929 match (PQuote _) _ = return []
1930 match (PProof _) _ = return []
1931 match (PTactics _) _ = return []
1932 match (PRefl _ _) (PRefl _ _) = return []
1933 match (PResolveTC _) (PResolveTC _) = return []
1934 match (PTrue _ _) (PTrue _ _) = return []
1935 match (PReturn _) (PReturn _) = return []
1936 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1937 ms <- match' s s'
1938 return (mt ++ ms)
1939 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1940 ms <- match' s s'
1941 return (mt ++ ms)
1942 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1943 mty <- match' ty ty'
1944 ms <- match' s s'
1945 return (mt ++ mty ++ ms)
1946 match (PHidden x) (PHidden y)
1947 | RightOK xs <- match x y = return xs -- to collect variables
1948 | otherwise = return [] -- Otherwise hidden things are unmatchable
1949 match (PHidden x) y
1950 | RightOK xs <- match x y = return xs
1951 | otherwise = return []
1952 match x (PHidden y)
1953 | RightOK xs <- match x y = return xs
1954 | otherwise = return []
1955 match (PUnifyLog x) y = match' x y
1956 match x (PUnifyLog y) = match' x y
1957 match (PNoImplicits x) y = match' x y
1958 match x (PNoImplicits y) = match' x y
1959 match Placeholder _ = return []
1960 match _ Placeholder = return []
1961 match (PResolveTC _) _ = return []
1962 match a b | a == b = return []
1963 | otherwise = LeftErr (a, b)
1965 checkRpts (RightOK ms) = check ms where
1966 check ((n,t):xs)
1967 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1968 then Left (t, t')
1969 else check xs
1970 check (_:xs) = check xs
1971 check [] = Right ms
1972 checkRpts (LeftErr x) = Left x
1974substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1975substMatches ms = substMatchesShadow ms []
1977substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1978substMatchesShadow [] shs t = t
1979substMatchesShadow ((n,tm):ns) shs t
1980 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1982substMatch :: Name -> PTerm -> PTerm -> PTerm
1983substMatch n = substMatchShadow n []
1985substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1986substMatchShadow n shs tm t = sm shs t where
1987 sm xs (PRef _ n') | n == n' = tm
1988 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1989 sm xs (PPi p x t sc)
1990 | x `elem` xs
1991 = let x' = nextName x in
1992 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1993 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1994 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1995 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1996 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1997 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1998 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1999 (fmap (sm xs) tm)
2000 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
2001 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
2002 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
2003 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
2004 sm xs (PHidden x) = PHidden (sm xs x)
2005 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2006 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2007 sm xs x = x
2009 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2010 fullApp x = x
2012shadow :: Name -> Name -> PTerm -> PTerm
2013shadow n n' t = sm t where
2014 sm (PRef fc x) | n == x = PRef fc n'
2015 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
2016 | otherwise = PLam fc x (sm t) sc
2017 sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
2018 | otherwise = PPi p x (sm t) sc
2019 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
2020 | otherwise = PLet fc x (sm t) (sm v) sc
2021 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
2022 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
2023 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
2024 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
2025 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
2026 sm (PTyped x y) = PTyped (sm x) (sm y)
2027 sm (PPair f p x y) = PPair f p (sm x) (sm y)
2028 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
2029 sm (PAlternative a as) = PAlternative a (map sm as)
2030 sm (PTactics ts) = PTactics (map (fmap sm) ts)
2031 sm (PProof ts) = PProof (map (fmap sm) ts)
2032 sm (PHidden x) = PHidden (sm x)
2033 sm (PUnifyLog x) = PUnifyLog (sm x)
2034 sm (PNoImplicits x) = PNoImplicits (sm x)
2035 sm x = x
2037-- Rename any binders which are repeated (so that we don't have to mess
2038-- about with shadowing anywhere else).
2040mkUniqueNames :: [Name] -> PTerm -> PTerm
2041mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2042 inScope :: S.Set Name
2043 inScope = S.fromList $ boundNamesIn tm
2045 mkUniqA arg = do t' <- mkUniq (getTm arg)
2046 return (arg { getTm = t' })
2048 -- Initialise the unique name with the environment length (so we're not
2049 -- looking for too long...)
2050 initN (UN n) l = UN $ txt (str n ++ show l)
2051 initN (MN i s) l = MN (i+l) s
2052 initN n l = n
2054 -- FIXME: Probably ought to do this for completeness! It's fine as
2055 -- long as there are no bindings inside tactics though.
2056 mkUniqT tac = return tac
2058 mkUniq :: PTerm -> State (S.Set Name) PTerm
2059 mkUniq (PLam fc n ty sc)
2060 = do env <- get
2061 (n', sc') <-
2062 if n `S.member` env
2063 then do let n' = uniqueNameSet (initN n (S.size env))
2064 (S.union env inScope)
2065 return (n', shadow n n' sc)
2066 else return (n, sc)
2067 put (S.insert n' env)
2068 ty' <- mkUniq ty
2069 sc'' <- mkUniq sc'
2070 return $! PLam fc n' ty' sc''
2071 mkUniq (PPi p n ty sc)
2072 = do env <- get
2073 (n', sc') <-
2074 if n `S.member` env
2075 then do let n' = uniqueNameSet (initN n (S.size env))
2076 (S.union env inScope)
2077 return (n', shadow n n' sc)
2078 else return (n, sc)
2079 put (S.insert n' env)
2080 ty' <- mkUniq ty
2081 sc'' <- mkUniq sc'
2082 return $! PPi p n' ty' sc''
2083 mkUniq (PLet fc n ty val sc)
2084 = do env <- get
2085 (n', sc') <-
2086 if n `S.member` env
2087 then do let n' = uniqueNameSet (initN n (S.size env))
2088 (S.union env inScope)
2089 return (n', shadow n n' sc)
2090 else return (n, sc)
2091 put (S.insert n' env)
2092 ty' <- mkUniq ty; val' <- mkUniq val
2093 sc'' <- mkUniq sc'
2094 return $! PLet fc n' ty' val' sc''
2095 mkUniq (PApp fc t args)
2096 = do t' <- mkUniq t
2097 args' <- mapM mkUniqA args
2098 return $! PApp fc t' args'
2099 mkUniq (PAppBind fc t args)
2100 = do t' <- mkUniq t
2101 args' <- mapM mkUniqA args
2102 return $! PAppBind fc t' args'
2103 mkUniq (PCase fc t alts)
2104 = do t' <- mkUniq t
2105 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2106 return (x', y')) alts
2107 return $! PCase fc t' alts'
2108 mkUniq (PPair fc p l r)
2109 = do l' <- mkUniq l; r' <- mkUniq r
2110 return $! PPair fc p l' r'
2111 mkUniq (PDPair fc p (PRef fc' n) t sc)
2112 | t /= Placeholder
2113 = do env <- get
2114 (n', sc') <- if n `S.member` env
2115 then do let n' = uniqueNameSet n (S.union env inScope)
2116 return (n', shadow n n' sc)
2117 else return (n, sc)
2118 put (S.insert n' env)
2119 t' <- mkUniq t
2120 sc'' <- mkUniq sc'
2121 return $! PDPair fc p (PRef fc' n') t' sc''
2122 mkUniq (PDPair fc p l t r)
2123 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2124 return $! PDPair fc p l' t' r'
2125 mkUniq (PAlternative b as)
2126 = liftM (PAlternative b) (mapM mkUniq as)
2127 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2128 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2129 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2130 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2131 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2132 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2133 mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
2134 mkUniq t = return t