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