git.iko.soy/Idris-dev
on ee8fce0 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2096 lines 88 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 }
132addUsedName :: FC -> Name -> Name -> Idris ()
133addUsedName fc n arg
134 = do ist <- getIState
135 case lookupTyName n (tt_ctxt ist) of
136 [(_, ty)] -> addUsage 0 ty
137 [] -> throwError (At fc (NoSuchVariable n))
138 xs -> throwError (At fc (CantResolveAlts (map fst xs)))
139 where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
140 addErasureUsage n i
141 | otherwise = addUsage (i + 1) sc
142 addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
144getErasureUsage :: Idris [(Name, Int)]
145getErasureUsage = do ist <- getIState;
146 return (idris_erasureUsed ist)
148totcheck :: (FC, Name) -> Idris ()
149totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
151defer_totcheck :: (FC, Name) -> Idris ()
152defer_totcheck n
153 = do i <- getIState;
154 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
156clear_totcheck :: Idris ()
157clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
159setFlags :: Name -> [FnOpt] -> Idris ()
160setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
162setFnInfo :: Name -> FnInfo -> Idris ()
163setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
165setAccessibility :: Name -> Accessibility -> Idris ()
166setAccessibility n a
167 = do i <- getIState
168 let ctxt = setAccess n a (tt_ctxt i)
169 putIState $ i { tt_ctxt = ctxt }
171setTotality :: Name -> Totality -> Idris ()
172setTotality n a
173 = do i <- getIState
174 let ctxt = setTotal n a (tt_ctxt i)
175 putIState $ i { tt_ctxt = ctxt }
177getTotality :: Name -> Idris Totality
178getTotality n
179 = do i <- getIState
180 case lookupTotal n (tt_ctxt i) of
181 [t] -> return t
182 _ -> return (Total [])
184-- Get coercions which might return the required type
185getCoercionsTo :: IState -> Type -> [Name]
186getCoercionsTo i ty =
187 let cs = idris_coercions i
188 (fn,_) = unApply (getRetTy ty) in
189 findCoercions fn cs
190 where findCoercions t [] = []
191 findCoercions t (n : ns) =
192 let ps = case lookupTy n (tt_ctxt i) of
193 [ty'] -> case unApply (getRetTy ty') of
194 (t', _) ->
195 if t == t' then [n] else []
196 _ -> [] in
197 ps ++ findCoercions t ns
199addToCG :: Name -> CGInfo -> Idris ()
200addToCG n cg
201 = do i <- getIState
202 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
204addTyInferred :: Name -> Idris ()
205addTyInferred n
206 = do i <- getIState
207 putIState $ i { idris_tyinfodata =
208 addDef n TIPartial (idris_tyinfodata i) }
210addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
211addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
212 mapM_ addConstraint ts
213 return ()
214 where addConstraint (x, y) = findMVApps x y
216 findMVApps x y
217 = do let (fx, argsx) = unApply x
218 let (fy, argsy) = unApply y
219 if (not (fx == fy))
220 then do
221 tryAddMV fx y
222 tryAddMV fy x
223 else mapM_ addConstraint (zip argsx argsy)
225 tryAddMV (P _ mv _) y =
226 do ist <- get
227 case lookup mv (idris_metavars ist) of
228 Just _ -> addConstraintRule mv y
229 _ -> return ()
230 tryAddMV _ _ = return ()
232 addConstraintRule :: Name -> Term -> Idris ()
233 addConstraintRule n t
234 = do ist <- get
235 logLvl 1 $ "TI constraint: " ++ show (n, t)
236 case lookupCtxt n (idris_tyinfodata ist) of
237 [TISolution ts] ->
238 do mapM_ (checkConsistent t) ts
239 let ti' = addDef n (TISolution (t : ts))
240 (idris_tyinfodata ist)
241 put $ ist { idris_tyinfodata = ti' }
242 _ ->
243 do let ti' = addDef n (TISolution [t])
244 (idris_tyinfodata ist)
245 put $ ist { idris_tyinfodata = ti' }
247 -- Check a solution is consistent with previous solutions
248 -- Meaning: If heads are both data types, they had better be the
249 -- same.
250 checkConsistent :: Term -> Term -> Idris ()
251 checkConsistent x y =
252 do let (fx, _) = unApply x
253 let (fy, _) = unApply y
254 case (fx, fy) of
255 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
256 (P (TCon _ _) n _, Constant _) -> errWhen True
257 (Constant _, P (TCon _ _) n' _) -> errWhen True
258 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
259 _ -> return ()
261 where errWhen True
262 = throwError (At fc
263 (CantUnify False x y (Msg "") [] 0))
264 errWhen False = return ()
266isTyInferred :: Name -> Idris Bool
267isTyInferred n
268 = do i <- getIState
269 case lookupCtxt n (idris_tyinfodata i) of
270 [TIPartial] -> return True
271 _ -> return False
273-- | Adds error handlers for a particular function and argument. If names are
274-- ambiguous, all matching handlers are updated.
275addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
276addFunctionErrorHandlers f arg hs =
277 do i <- getIState
278 let oldHandlers = idris_function_errorhandlers i
279 let newHandlers = flip (addDef f) oldHandlers $
280 case lookupCtxtExact f oldHandlers of
281 Nothing -> M.singleton arg (S.fromList hs)
282 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
283 -- will always be one of those two, thus no extra case
284 putIState $ i { idris_function_errorhandlers = newHandlers }
286getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
287getFunctionErrorHandlers f arg = do i <- getIState
288 return . maybe [] S.toList $
289 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
292-- Trace all the names in a call graph starting at the given name
293getAllNames :: Name -> Idris [Name]
294getAllNames n = allNames [] n
296allNames :: [Name] -> Name -> Idris [Name]
297allNames ns n | n `elem` ns = return []
298allNames ns n = do i <- getIState
299 case lookupCtxtExact n (idris_callgraph i) of
300 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
301 return (nub (n : concat more))
302 _ -> return [n]
304addCoercion :: Name -> Idris ()
305addCoercion n = do i <- getIState
306 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
308addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
309addDocStr n doc args
310 = do i <- getIState
311 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
313addNameHint :: Name -> Name -> Idris ()
314addNameHint ty n
315 = do i <- getIState
316 ty' <- case lookupCtxtName ty (idris_implicits i) of
317 [(tyn, _)] -> return tyn
318 [] -> throwError (NoSuchVariable ty)
319 tyns -> throwError (CantResolveAlts (map fst tyns))
320 let ns' = case lookupCtxt ty' (idris_namehints i) of
321 [ns] -> ns ++ [n]
322 _ -> [n]
323 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
325getNameHints :: IState -> Name -> [Name]
326getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
327getNameHints i n =
328 case lookupCtxt n (idris_namehints i) of
329 [ns] -> ns
330 _ -> []
332-- Issue #1737 in the Issue Tracker.
333-- https://github.com/idris-lang/Idris-dev/issues/1737
334addToCalledG :: Name -> [Name] -> Idris ()
335addToCalledG n ns = return () -- TODO
337push_estack :: Name -> Idris ()
338push_estack n = do i <- getIState
339 putIState (i { elab_stack = n : elab_stack i })
341pop_estack :: Idris ()
342pop_estack = do i <- getIState
343 putIState (i { elab_stack = ptail (elab_stack i) })
344 where ptail [] = []
345 ptail (x : xs) = xs
347-- Add a class instance function. Dodgy hack: Put integer instances first in the
348-- list so they are resolved by default.
349-- Dodgy hack 2: put constraint chasers (@@) last
351addInstance :: Bool -> Name -> Name -> Idris ()
352addInstance int n i
353 = do ist <- getIState
354 case lookupCtxt n (idris_classes ist) of
355 [CI a b c d e ins] ->
356 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
357 putIState $ ist { idris_classes = cs }
358 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
359 putIState $ ist { idris_classes = cs }
360 where addI i ins | int = i : ins
361 | chaser n = ins ++ [i]
362 | otherwise = insI i ins
363 insI i [] = [i]
364 insI i (n : ns) | chaser n = i : n : ns
365 | otherwise = n : insI i ns
367 chaser (UN nm)
368 | ('@':'@':_) <- str nm = True
369 chaser (NS n _) = chaser n
370 chaser _ = False
372addClass :: Name -> ClassInfo -> Idris ()
373addClass n i
374 = do ist <- getIState
375 let i' = case lookupCtxt n (idris_classes ist) of
376 [c] -> c { class_instances = class_instances i }
377 _ -> i
378 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
380addIBC :: IBCWrite -> Idris ()
381addIBC ibc@(IBCDef n)
382 = do i <- getIState
383 when (notDef (ibc_write i)) $
384 putIState $ i { ibc_write = ibc : ibc_write i }
385 where notDef [] = True
386 notDef (IBCDef n': is) | n == n' = False
387 notDef (_ : is) = notDef is
388addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
390clearIBC :: Idris ()
391clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
393resetNameIdx :: Idris ()
394resetNameIdx = do i <- getIState
395 put (i { idris_nameIdx = (0, emptyContext) })
397-- Used to preserve sharing of names
398addNameIdx :: Name -> Idris (Int, Name)
399addNameIdx n = do i <- getIState
400 let (i', x) = addNameIdx' i n
401 putIState i'
402 return x
404addNameIdx' :: IState -> Name -> (IState, (Int, Name))
405addNameIdx' i n
406 = let idxs = snd (idris_nameIdx i) in
407 case lookupCtxt n idxs of
408 [x] -> (i, x)
409 _ -> let i' = fst (idris_nameIdx i) + 1 in
410 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
412getSymbol :: Name -> Idris Name
413getSymbol n = do i <- getIState
414 case M.lookup n (idris_symbols i) of
415 Just n' -> return n'
416 Nothing -> do let sym' = M.insert n n (idris_symbols i)
417 put (i { idris_symbols = sym' })
418 return n
420getHdrs :: Codegen -> Idris [String]
421getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
423getImported :: Idris [(FilePath, Bool)]
424getImported = do i <- getIState; return (idris_imported i)
426setErrSpan :: FC -> Idris ()
427setErrSpan x = do i <- getIState;
428 case (errSpan i) of
429 Nothing -> putIState $ i { errSpan = Just x }
430 Just _ -> return ()
432clearErr :: Idris ()
433clearErr = do i <- getIState
434 putIState $ i { errSpan = Nothing }
436getSO :: Idris (Maybe String)
437getSO = do i <- getIState
438 return (compiled_so i)
440setSO :: Maybe String -> Idris ()
441setSO s = do i <- getIState
442 putIState $ (i { compiled_so = s })
444getIState :: Idris IState
445getIState = get
447putIState :: IState -> Idris ()
448putIState = put
450withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
451withContext ctx name dflt action = do
452 ist <- getIState
453 case lookupCtxt name (ctx ist) of
454 [x] -> action x
455 _ -> return dflt
457withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
458withContext_ ctx name action = withContext ctx name () action
460-- | A version of liftIO that puts errors into the exception type of the Idris monad
461runIO :: IO a -> Idris a
462runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
463-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
464--
465-- Issue #1738 on the issue tracker.
466-- https://github.com/idris-lang/Idris-dev/issues/1738
468getName :: Idris Int
469getName = do i <- getIState;
470 let idx = idris_name i;
471 putIState $ (i { idris_name = idx + 1 })
472 return idx
474-- InternalApp keeps track of the real function application for making case splits from, not the application the
475-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
476addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
477addInternalApp fp l t
478 = do i <- getIState
479 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
481getInternalApp :: FilePath -> Int -> Idris PTerm
482getInternalApp fp l = do i <- getIState
483 case lookup (fp, l) (idris_lineapps i) of
484 Just n' -> return n'
485 Nothing -> return Placeholder
486 -- TODO: What if it's not there?
488-- Pattern definitions are only used for coverage checking, so erase them
489-- when we're done
490clearOrigPats :: Idris ()
491clearOrigPats = do i <- get
492 let ps = idris_patdefs i
493 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
494 put (i { idris_patdefs = ps' })
496-- Erase types from Ps in the context (basically ending up with what's in
497-- the .ibc, which is all we need after all the analysis is done)
498clearPTypes :: Idris ()
499clearPTypes = do i <- get
500 let ctxt = tt_ctxt i
501 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
502 where pErase (CaseOp c t tys orig tot cds)
503 = CaseOp c t tys orig [] (pErase' cds)
504 pErase x = x
505 pErase' (CaseDefs _ (cs, c) _ rs)
506 = let c' = (cs, fmap pEraseType c) in
507 CaseDefs c' c' c' rs
509checkUndefined :: FC -> Name -> Idris ()
510checkUndefined fc n
511 = do i <- getContext
512 case lookupTy n i of
513 (_:_) -> throwError . Msg $ show fc ++ ":" ++
514 show n ++ " already defined"
515 _ -> return ()
517isUndefined :: FC -> Name -> Idris Bool
518isUndefined fc n
519 = do i <- getContext
520 case lookupTyExact n i of
521 Just _ -> return False
522 _ -> return True
524setContext :: Context -> Idris ()
525setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
527updateContext :: (Context -> Context) -> Idris ()
528updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
530addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
531addConstraints fc (v, cs)
532 = do i <- getIState
533 let ctxt = tt_ctxt i
534 let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,
535 next_tvar = v }
536 let ics = zip cs (repeat fc) ++ idris_constraints i
537 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
539addDeferred = addDeferred' Ref
540addDeferredTyCon = addDeferred' (TCon 0 0)
542addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
543addDeferred' nt ns
544 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
545 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
546 i <- getIState
547 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
548 idris_metavars i }
549 where
550 -- 'tidyNames' is to generate user accessible names in case they are
551 -- needed in tactic scripts
552 tidyNames used (Bind (MN i x) b sc)
553 = let n' = uniqueNameSet (UN x) used in
554 Bind n' b $ tidyNames (S.insert n' used) sc
555 tidyNames used (Bind n b sc)
556 = let n' = uniqueNameSet n used in
557 Bind n' b $ tidyNames (S.insert n' used) sc
558 tidyNames used b = b
560solveDeferred :: Name -> Idris ()
561solveDeferred n = do i <- getIState
562 putIState $ i { idris_metavars =
563 filter (\(n', _) -> n/=n')
564 (idris_metavars i),
565 ibc_write =
566 filter (notMV n) (ibc_write i)
567 }
568 where notMV n (IBCMetavar n') = not (n == n')
569 notMV n _ = True
571getUndefined :: Idris [Name]
572getUndefined = do i <- getIState
573 return (map fst (idris_metavars i) \\ primDefs)
575isMetavarName :: Name -> IState -> Bool
576isMetavarName n ist
577 = case lookupNames n (tt_ctxt ist) of
578 (t:_) -> isJust $ lookup t (idris_metavars ist)
579 _ -> False
581getWidth :: Idris ConsoleWidth
582getWidth = fmap idris_consolewidth getIState
584setWidth :: ConsoleWidth -> Idris ()
585setWidth w = do ist <- getIState
586 put ist { idris_consolewidth = w }
588renderWidth :: Idris Int
589renderWidth = do iw <- getWidth
590 case iw of
591 InfinitelyWide -> return 100000000
592 ColsWide n -> return (max n 1)
593 AutomaticWidth -> runIO getScreenWidth
597type1Doc :: Doc OutputAnnotation
598type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
601isetPrompt :: String -> Idris ()
602isetPrompt p = do i <- getIState
603 case idris_outputmode i of
604 IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
606-- | Tell clients how much was parsed and loaded
607isetLoadedRegion :: Idris ()
608isetLoadedRegion = do i <- getIState
609 let span = idris_parsedSpan i
610 case span of
611 Just fc ->
612 case idris_outputmode i of
613 IdeMode n h ->
614 runIO . hPutStrLn h $
615 convSExp "set-loaded-region" fc n
616 Nothing -> return ()
618setLogLevel :: Int -> Idris ()
619setLogLevel l = do i <- getIState
620 let opts = idris_options i
621 let opt' = opts { opt_logLevel = l }
622 putIState $ i { idris_options = opt' }
624setCmdLine :: [Opt] -> Idris ()
625setCmdLine opts = do i <- getIState
626 let iopts = idris_options i
627 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
629getCmdLine :: Idris [Opt]
630getCmdLine = do i <- getIState
631 return (opt_cmdline (idris_options i))
633getDumpDefun :: Idris (Maybe FilePath)
634getDumpDefun = do i <- getIState
635 return $ findC (opt_cmdline (idris_options i))
636 where findC [] = Nothing
637 findC (DumpDefun x : _) = Just x
638 findC (_ : xs) = findC xs
640getDumpCases :: Idris (Maybe FilePath)
641getDumpCases = do i <- getIState
642 return $ findC (opt_cmdline (idris_options i))
643 where findC [] = Nothing
644 findC (DumpCases x : _) = Just x
645 findC (_ : xs) = findC xs
647logLevel :: Idris Int
648logLevel = do i <- getIState
649 return (opt_logLevel (idris_options i))
651setErrContext :: Bool -> Idris ()
652setErrContext t = do i <- getIState
653 let opts = idris_options i
654 let opts' = opts { opt_errContext = t }
655 putIState $ i { idris_options = opts' }
657errContext :: Idris Bool
658errContext = do i <- getIState
659 return (opt_errContext (idris_options i))
661getOptimise :: Idris [Optimisation]
662getOptimise = do i <- getIState
663 return (opt_optimise (idris_options i))
665setOptimise :: [Optimisation] -> Idris ()
666setOptimise newopts = do i <- getIState
667 let opts = idris_options i
668 let opts' = opts { opt_optimise = newopts }
669 putIState $ i { idris_options = opts' }
671addOptimise :: Optimisation -> Idris ()
672addOptimise opt = do opts <- getOptimise
673 setOptimise (nub (opt : opts))
675removeOptimise :: Optimisation -> Idris ()
676removeOptimise opt = do opts <- getOptimise
677 setOptimise ((nub opts) \\ [opt])
679-- Set appropriate optimisation set for the given level. We only have
680-- one optimisation that is configurable at the moment, however!
681setOptLevel :: Int -> Idris ()
682setOptLevel n | n <= 0 = setOptimise []
683setOptLevel 1 = setOptimise []
684setOptLevel 2 = setOptimise [PETransform]
685setOptLevel n | n >= 3 = setOptimise [PETransform]
687useREPL :: Idris Bool
688useREPL = do i <- getIState
689 return (opt_repl (idris_options i))
691setREPL :: Bool -> Idris ()
692setREPL t = do i <- getIState
693 let opts = idris_options i
694 let opt' = opts { opt_repl = t }
695 putIState $ i { idris_options = opt' }
697showOrigErr :: Idris Bool
698showOrigErr = do i <- getIState
699 return (opt_origerr (idris_options i))
701setShowOrigErr :: Bool -> Idris ()
702setShowOrigErr b = do i <- getIState
703 let opts = idris_options i
704 let opt' = opts { opt_origerr = b }
705 putIState $ i { idris_options = opt' }
707setAutoSolve :: Bool -> Idris ()
708setAutoSolve b = do i <- getIState
709 let opts = idris_options i
710 let opt' = opts { opt_autoSolve = b }
711 putIState $ i { idris_options = opt' }
713setNoBanner :: Bool -> Idris ()
714setNoBanner n = do i <- getIState
715 let opts = idris_options i
716 let opt' = opts { opt_nobanner = n }
717 putIState $ i { idris_options = opt' }
719getNoBanner :: Idris Bool
720getNoBanner = do i <- getIState
721 let opts = idris_options i
722 return (opt_nobanner opts)
724setQuiet :: Bool -> Idris ()
725setQuiet q = do i <- getIState
726 let opts = idris_options i
727 let opt' = opts { opt_quiet = q }
728 putIState $ i { idris_options = opt' }
730getQuiet :: Idris Bool
731getQuiet = do i <- getIState
732 let opts = idris_options i
733 return (opt_quiet opts)
735setCodegen :: Codegen -> Idris ()
736setCodegen t = do i <- getIState
737 let opts = idris_options i
738 let opt' = opts { opt_codegen = t }
739 putIState $ i { idris_options = opt' }
741codegen :: Idris Codegen
742codegen = do i <- getIState
743 return (opt_codegen (idris_options i))
745setOutputTy :: OutputType -> Idris ()
746setOutputTy t = do i <- getIState
747 let opts = idris_options i
748 let opt' = opts { opt_outputTy = t }
749 putIState $ i { idris_options = opt' }
751outputTy :: Idris OutputType
752outputTy = do i <- getIState
753 return $ opt_outputTy $ idris_options i
755setIdeMode :: Bool -> Handle -> Idris ()
756setIdeMode True h = do i <- getIState
757 putIState $ i { idris_outputmode = IdeMode 0 h
758 , idris_colourRepl = False
759 }
760setIdeMode False _ = return ()
762setTargetTriple :: String -> Idris ()
763setTargetTriple t = do i <- getIState
764 let opts = idris_options i
765 opt' = opts { opt_triple = t }
766 putIState $ i { idris_options = opt' }
768targetTriple :: Idris String
769targetTriple = do i <- getIState
770 return (opt_triple (idris_options i))
772setTargetCPU :: String -> Idris ()
773setTargetCPU t = do i <- getIState
774 let opts = idris_options i
775 opt' = opts { opt_cpu = t }
776 putIState $ i { idris_options = opt' }
778targetCPU :: Idris String
779targetCPU = do i <- getIState
780 return (opt_cpu (idris_options i))
782verbose :: Idris Bool
783verbose = do i <- getIState
784 return (opt_verbose (idris_options i))
786setVerbose :: Bool -> Idris ()
787setVerbose t = do i <- getIState
788 let opts = idris_options i
789 let opt' = opts { opt_verbose = t }
790 putIState $ i { idris_options = opt' }
792typeInType :: Idris Bool
793typeInType = do i <- getIState
794 return (opt_typeintype (idris_options i))
796setTypeInType :: Bool -> Idris ()
797setTypeInType t = do i <- getIState
798 let opts = idris_options i
799 let opt' = opts { opt_typeintype = t }
800 putIState $ i { idris_options = opt' }
802coverage :: Idris Bool
803coverage = do i <- getIState
804 return (opt_coverage (idris_options i))
806setCoverage :: Bool -> Idris ()
807setCoverage t = do i <- getIState
808 let opts = idris_options i
809 let opt' = opts { opt_coverage = t }
810 putIState $ i { idris_options = opt' }
812setIBCSubDir :: FilePath -> Idris ()
813setIBCSubDir fp = do i <- getIState
814 let opts = idris_options i
815 let opt' = opts { opt_ibcsubdir = fp }
816 putIState $ i { idris_options = opt' }
818valIBCSubDir :: IState -> Idris FilePath
819valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
821addImportDir :: FilePath -> Idris ()
822addImportDir fp = do i <- getIState
823 let opts = idris_options i
824 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
825 putIState $ i { idris_options = opt' }
827setImportDirs :: [FilePath] -> Idris ()
828setImportDirs fps = do i <- getIState
829 let opts = idris_options i
830 let opt' = opts { opt_importdirs = fps }
831 putIState $ i { idris_options = opt' }
833allImportDirs :: Idris [FilePath]
834allImportDirs = do i <- getIState
835 let optdirs = opt_importdirs (idris_options i)
836 return ("." : reverse optdirs)
838colourise :: Idris Bool
839colourise = do i <- getIState
840 return $ idris_colourRepl i
842setColourise :: Bool -> Idris ()
843setColourise b = do i <- getIState
844 putIState $ i { idris_colourRepl = b }
846impShow :: Idris Bool
847impShow = do i <- getIState
848 return (opt_showimp (idris_options i))
850setImpShow :: Bool -> Idris ()
851setImpShow t = do i <- getIState
852 let opts = idris_options i
853 let opt' = opts { opt_showimp = t }
854 putIState $ i { idris_options = opt' }
856setColour :: ColourType -> IdrisColour -> Idris ()
857setColour ct c = do i <- getIState
858 let newTheme = setColour' ct c (idris_colourTheme i)
859 putIState $ i { idris_colourTheme = newTheme }
860 where setColour' KeywordColour c t = t { keywordColour = c }
861 setColour' BoundVarColour c t = t { boundVarColour = c }
862 setColour' ImplicitColour c t = t { implicitColour = c }
863 setColour' FunctionColour c t = t { functionColour = c }
864 setColour' TypeColour c t = t { typeColour = c }
865 setColour' DataColour c t = t { dataColour = c }
866 setColour' PromptColour c t = t { promptColour = c }
867 setColour' PostulateColour c t = t { postulateColour = c }
869logLvl :: Int -> String -> Idris ()
870logLvl l str = do i <- getIState
871 let lvl = opt_logLevel (idris_options i)
872 when (lvl >= l) $
873 case idris_outputmode i of
874 RawOutput h -> do runIO $ hPutStrLn h str
875 IdeMode n h ->
876 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
877 runIO . hPutStrLn h $ convSExp "log" good n
879cmdOptType :: Opt -> Idris Bool
880cmdOptType x = do i <- getIState
881 return $ x `elem` opt_cmdline (idris_options i)
883iLOG :: String -> Idris ()
884iLOG = logLvl 1
886noErrors :: Idris Bool
887noErrors = do i <- getIState
888 case errSpan i of
889 Nothing -> return True
890 _ -> return False
892setTypeCase :: Bool -> Idris ()
893setTypeCase t = do i <- getIState
894 let opts = idris_options i
895 let opt' = opts { opt_typecase = t }
896 putIState $ i { idris_options = opt' }
899-- Dealing with parameters
901expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
902 [Name] -> -- all names
903 [Name] -> -- names with no declaration
904 PTerm -> PTerm
905expandParams dec ps ns infs tm = en tm
906 where
907 -- if we shadow a name (say in a lambda binding) that is used in a call to
908 -- a lifted function, we need access to both names - once in the scope of the
909 -- binding and once to call the lifted functions. So we'll explicitly shadow
910 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
911 -- but we didn't...)
913 mkShadow (UN n) = MN 0 n
914 mkShadow (MN i n) = MN (i+1) n
915 mkShadow (NS x s) = NS (mkShadow x) s
917 en (PLam fc n t s)
918 | n `elem` (map fst ps ++ ns)
919 = let n' = mkShadow n in
920 PLam fc n' (en t) (en (shadow n n' s))
921 | otherwise = PLam fc n (en t) (en s)
922 en (PPi p n t s)
923 | n `elem` (map fst ps ++ ns)
924 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
925 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
926 | otherwise = PPi (enTacImp p) n (en t) (en s)
927 en (PLet fc n ty v s)
928 | n `elem` (map fst ps ++ ns)
929 = let n' = mkShadow n in
930 PLet fc n' (en ty) (en v) (en (shadow n n' s))
931 | otherwise = PLet fc n (en ty) (en v) (en s)
932 -- FIXME: Should only do this in a type signature!
933 en (PDPair f p (PRef f' n) t r)
934 | n `elem` (map fst ps ++ ns) && t /= Placeholder
935 = let n' = mkShadow n in
936 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
937 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
938 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
939 en (PTyped l r) = PTyped (en l) (en r)
940 en (PPair f p l r) = PPair f p (en l) (en r)
941 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
942 en (PAlternative a as) = PAlternative a (map en as)
943 en (PHidden t) = PHidden (en t)
944 en (PUnifyLog t) = PUnifyLog (en t)
945 en (PDisamb ds t) = PDisamb ds (en t)
946 en (PNoImplicits t) = PNoImplicits (en t)
947 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
948 en (PProof ts) = PProof (map (fmap en) ts)
949 en (PTactics ts) = PTactics (map (fmap en) ts)
951 en (PQuote (Var n))
952 | n `nselem` ns = PQuote (Var (dec n))
953 en (PApp fc (PInferRef fc' n) as)
954 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
955 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
956 en (PApp fc (PRef fc' n) as)
957 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
958 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
959 | n `nselem` ns = PApp fc (PRef fc' (dec n))
960 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
961 en (PAppBind fc (PRef fc' n) as)
962 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
963 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
964 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
965 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
966 en (PRef fc n)
967 | n `elem` infs = PApp fc (PInferRef fc (dec n))
968 (map (pexp . (PRef fc)) (map fst ps))
969 | n `nselem` ns = PApp fc (PRef fc (dec n))
970 (map (pexp . (PRef fc)) (map fst ps))
971 en (PInferRef fc n)
972 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
973 (map (pexp . (PRef fc)) (map fst ps))
974 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
975 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
976 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
977 en (PRunTactics fc tm) = PRunTactics fc (en tm)
978 en t = t
980 nselem x [] = False
981 nselem x (y : xs) | nseq x y = True
982 | otherwise = nselem x xs
984 nseq x y = nsroot x == nsroot y
986 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
987 enTacImp other = other
989expandParamsD :: Bool -> -- True = RHS only
990 IState ->
991 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
992expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
993 = if n `elem` ns && (not rhsonly)
994 then -- trace (show (n, expandParams dec ps ns ty)) $
995 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
996 else --trace (show (n, expandParams dec ps ns ty)) $
997 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
998expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
999 = if n `elem` ns && (not rhsonly)
1000 then -- trace (show (n, expandParams dec ps ns ty)) $
1001 PPostulate doc syn fc o (dec n) (piBind ps
1002 (expandParams dec ps ns [] ty))
1003 else --trace (show (n, expandParams dec ps ns ty)) $
1004 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1005expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1006 = let n' = if n `elem` ns then dec n else n in
1007 PClauses fc opts n' (map expandParamsC cs)
1008 where
1009 expandParamsC (PClause fc n lhs ws rhs ds)
1010 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1011 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1012 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1013 n' = if n `elem` ns then dec n else n
1014 -- names bound on the lhs should not be expanded on the rhs
1015 ns' = removeBound lhs ns in
1016 PClause fc n' lhs'
1017 (map (expandParams dec ps'' ns' []) ws)
1018 (expandParams dec ps'' ns' [] rhs)
1019 (map (expandParamsD True ist dec ps'' ns') ds)
1020 expandParamsC (PWith fc n lhs ws wval pn ds)
1021 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1022 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1023 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1024 n' = if n `elem` ns then dec n else n
1025 ns' = removeBound lhs ns in
1026 PWith fc n' lhs'
1027 (map (expandParams dec ps'' ns' []) ws)
1028 (expandParams dec ps'' ns' [] wval)
1029 pn
1030 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1031 updateps yn nm [] = []
1032 updateps yn nm (((a, t), i):as)
1033 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1034 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1036 removeBound lhs ns = ns \\ nub (bnames lhs)
1038 bnames (PRef _ n) = [n]
1039 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1040 bnames (PPair _ _ l r) = bnames l ++ bnames r
1041 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1042 bnames _ = []
1044-- | Expands parameters defined in parameter and where blocks inside of declarations
1045expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1046 = PData doc argDocs syn fc co (expandPData pd)
1047 where
1048 -- just do the type decl, leave constructors alone (parameters will be
1049 -- added implicitly)
1050 expandPData (PDatadecl n ty cons)
1051 = if n `elem` ns
1052 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1053 (map econ cons)
1054 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1055 econ (doc, argDocs, n, t, fc, fs)
1056 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1057expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
1058 = if tn `elem` ns
1059 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1060 opts cdoc (dec cn) conty
1061 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1062 opts cdoc (dec cn) conty
1063 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1064expandParamsD rhs ist dec ps ns (PParams f params pds)
1065 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1066 (map (expandParamsD True ist dec ps ns) pds)
1067-- (map (expandParamsD ist dec ps ns) pds)
1068expandParamsD rhs ist dec ps ns (PMutual f pds)
1069 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1070expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
1071 = PClass doc info f
1072 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1074 (map (mapsnd (expandParams dec ps ns [])) params)
1075 pDocs
1076 (map (expandParamsD rhs ist dec ps ns) decls)
1077expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1078 = PInstance info f
1079 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1081 (map (expandParams dec ps ns []) params)
1082 (expandParams dec ps ns [] ty)
1083 cn
1084 (map (expandParamsD rhs ist dec ps ns) decls)
1085expandParamsD rhs ist dec ps ns d = d
1087mapsnd f (x, t) = (x, f t)
1089-- Calculate a priority for a type, for deciding elaboration order
1090-- * if it's just a type variable or concrete type, do it early (0)
1091-- * if there's only type variables and injective constructors, do it next (1)
1092-- * if there's a function type, next (2)
1093-- * finally, everything else (3)
1095getPriority :: IState -> PTerm -> Int
1096getPriority i tm = 1 -- pri tm
1097 where
1098 pri (PRef _ n) =
1099 case lookupP n (tt_ctxt i) of
1100 ((P (DCon _ _ _) _ _):_) -> 1
1101 ((P (TCon _ _) _ _):_) -> 1
1102 ((P Ref _ _):_) -> 1
1103 [] -> 0 -- must be locally bound, if it's not an error...
1104 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1105 pri (PTrue _ _) = 0
1106 pri (PRefl _ _) = 1
1107 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1108 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1109 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1110 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1111 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1112 pri (PTyped l r) = pri l
1113 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1114 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1115 pri (PAlternative a as) = maximum (map pri as)
1116 pri (PConstant _) = 0
1117 pri Placeholder = 1
1118 pri _ = 3
1121addStatics :: Name -> Term -> PTerm -> Idris ()
1122addStatics n tm ptm =
1123 do let (statics, dynamics) = initStatics tm ptm
1124 ist <- getIState
1125 let paramnames
1126 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1127 Just p -> getNamesFrom 0 (fn_params p) tm ++
1128 concatMap (getParamNames ist) (map snd statics)
1129 _ -> concatMap (getParamNames ist) (map snd statics)
1131 let stnames = nub $ concatMap freeArgNames (map snd statics)
1132 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1133 \\ paramnames
1134 -- also get the arguments which are 'uniquely inferrable' from
1135 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1136 -- or parameters to the type of a static
1137 let statics' = nub $ map fst statics ++
1138 filter (\x -> not (elem x dnames)) stnames
1139 let stpos = staticList statics' tm
1140 i <- getIState
1141 when (not (null statics)) $
1142 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1143 ++ showTmImpls ptm ++ "\n"
1144 ++ show statics ++ "\n" ++ show dynamics
1145 ++ "\n" ++ show paramnames
1146 ++ "\n" ++ show stpos
1147 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1148 addIBC (IBCStatic n)
1149 where
1150 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
1151 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1152 (static, (n, ty) : dynamic)
1153 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)
1154 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1155 if pstatic p == Static then ((n, ty) : static, dynamic)
1156 else if (not (searchArg p))
1157 then (static, (n, ty) : dynamic)
1158 else (static, dynamic)
1159 initStatics t pt = ([], [])
1161 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1162 = case lookupCtxtExact n (idris_datatypes ist) of
1163 Just ti -> getNamePos 0 (param_pos ti) args
1164 Nothing -> []
1165 where getNamePos i ps [] = []
1166 getNamePos i ps (P _ n _ : as)
1167 | i `elem` ps = n : getNamePos (i + 1) ps as
1168 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1169 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1170 = n : getParamNames ist sc
1171 getParamNames ist _ = []
1173 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1174 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1175 | otherwise = getNamesFrom (i + 1) ps sc
1176 getNamesFrom i ps sc = []
1178 freeArgNames (Bind n (Pi _ ty _) sc)
1179 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1180 freeArgNames tm = let (_, args) = unApply tm in
1181 concatMap freeNames args
1183 -- if a name appears in a type class or tactic implicit index, it doesn't
1184 -- affect its 'uniquely inferrable' from a static status since these are
1185 -- resolved by searching.
1186 searchArg (Constraint _ _) = True
1187 searchArg (TacImp _ _ _) = True
1188 searchArg _ = False
1190 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1191 staticList _ _ = []
1193-- Dealing with implicit arguments
1195-- Add some bound implicits to the using block if they aren't there already
1197addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1198addToUsing us [] = us
1199addToUsing us ((n, t) : ns)
1200 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1201 | otherwise = addToUsing us ns
1202 where impName (UImplicit n _) = Just n
1203 impName _ = Nothing
1205-- Add constraint bindings from using block
1207addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1208addUsingConstraints syn fc t
1209 = do ist <- get
1210 let ns = namesIn [] ist t
1211 let cs = getConstraints t -- check declared constraints
1212 let addconsts = uconsts \\ cs
1213 return (doAdd addconsts ns t)
1214 where uconsts = filter uconst (using syn)
1215 uconst (UConstraint _ _) = True
1216 uconst _ = False
1218 doAdd [] _ t = t
1219 -- if all of args in ns, then add it
1220 doAdd (UConstraint c args : cs) ns t
1221 | all (\n -> elem n ns) args
1222 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1223 (mkConst c args) (doAdd cs ns t)
1224 | otherwise = doAdd cs ns t
1226 mkConst c args = PApp fc (PRef fc c)
1227 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1229 getConstraints (PPi (Constraint _ _) _ c sc)
1230 = getcapp c ++ getConstraints sc
1231 getConstraints (PPi _ _ c sc) = getConstraints sc
1232 getConstraints _ = []
1234 getcapp (PApp _ (PRef _ c) args)
1235 = do ns <- mapM getName args
1236 return (UConstraint c ns)
1237 getcapp _ = []
1239 getName (PExp _ _ _ (PRef _ n)) = return n
1240 getName _ = []
1242-- Add implicit bindings from using block, and bind any missing names
1243addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1244addUsingImpls syn n fc t
1245 = do ist <- getIState
1246 let ns = implicitNamesIn (map iname uimpls) ist t
1247 let badnames = filter (\n -> not (implicitable n) &&
1248 n `notElem` (map iname uimpls)) ns
1249 when (not (null badnames)) $
1250 throwError (At fc (Elaborating "type of " n
1251 (NoSuchVariable (head badnames))))
1252 let cs = getArgnames t -- get already bound names
1253 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1254 -- if all names in the arguments of addconsts appear in ns,
1255 -- add the constraint implicitly
1256 return (bindFree ns (doAdd addimpls ns t))
1257 where uimpls = filter uimpl (using syn)
1258 uimpl (UImplicit _ _) = True
1259 uimpl _ = False
1261 iname (UImplicit n _) = n
1262 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1264 doAdd [] _ t = t
1265 -- if all of args in ns, then add it
1266 doAdd (UImplicit n ty : cs) ns t
1267 | elem n ns
1268 = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)
1269 | otherwise = doAdd cs ns t
1271 -- bind the free names which weren't in the using block
1272 bindFree [] tm = tm
1273 bindFree (n:ns) tm
1274 | elem n (map iname uimpls) = bindFree ns tm
1275 | otherwise
1276 = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
1278 getArgnames (PPi _ n c sc)
1279 = n : getArgnames sc
1280 getArgnames _ = []
1282-- Given the original type and the elaborated type, return the implicitness
1283-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1285getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1286getUnboundImplicits i t tm = getImps t (collectImps tm)
1287 where collectImps (PPi p n t sc)
1288 = (n, (p, t)) : collectImps sc
1289 collectImps _ = []
1291 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1292 getImps (Bind n (Pi _ t _) sc) imps
1293 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1294 where
1295 argInfo n (Imp opt _ _ _) t'
1296 = (True, PImp (getPriority i t') True opt n t')
1297 argInfo n (Exp opt _ _) t'
1298 = (InaccessibleArg `elem` opt,
1299 PExp (getPriority i t') opt n t')
1300 argInfo n (Constraint opt _) t'
1301 = (InaccessibleArg `elem` opt,
1302 PConstraint 10 opt n t')
1303 argInfo n (TacImp opt _ scr) t'
1304 = (InaccessibleArg `elem` opt,
1305 PTacImplicit 10 opt n scr t')
1306 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1307 where impBind n t = (True, PImp 1 True [] n Placeholder)
1308 getImps sc tm = []
1310-- Add implicit Pi bindings for any names in the term which appear in an
1311-- argument position.
1313-- This has become a right mess already. Better redo it some time...
1314-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1315-- a couple of places which use it. Clean them up!
1317-- Issue 1739 in the issue tracker
1318-- https://github.com/idris-lang/Idris-dev/issues/1739
1319implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1320implicit info syn n ptm = implicit' info syn [] n ptm
1322implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1323implicit' info syn ignore n ptm
1324 = do i <- getIState
1325 let (tm', impdata) = implicitise syn ignore i ptm
1326 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1327-- let (tm'', spos) = findStatics i tm'
1328 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1329 addIBC (IBCImp n)
1330 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1331-- i <- get
1332-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1333 return tm'
1334 where
1335 -- Detect unknown names in default arguments and throw error if found.
1336 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1337 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1339 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1340 notFoundInDefault kns (PTacImplicit _ _ n script _)
1341 = do i <- getIState
1342 case notFound kns (namesIn [] i script) of
1343 Nothing -> return (n:kns)
1344 Just name -> throwError (NoSuchVariable name)
1345 notFoundInDefault kns p = return ((pname p):kns)
1347 notFound :: [Name] -> [Name] -> Maybe Name
1348 notFound kns [] = Nothing
1349 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1350 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1352implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1353implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1354 let (declimps, ns') = execState (imps True [] tm) ([], [])
1355 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1356 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1357 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1358 if null ns
1359 then (tm, reverse declimps)
1360 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1361 where
1362 uvars = map ipair (filter uimplicit (using syn))
1363 pvars = syn_params syn
1365 inUsing n = n `elem` map fst uvars
1367 ipair (UImplicit x y) = (x, y)
1368 uimplicit (UImplicit _ _) = True
1369 uimplicit _ = False
1371 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1372 | otherwise = x : dropAll xs ys
1373 dropAll [] ys = []
1375 -- Find names in argument position in a type, suitable for implicit
1376 -- binding
1377 -- Not the function position, but do everything else...
1378 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1379 implNamesIn uv t = namesIn uv ist t
1381 imps top env (PApp _ f as)
1382 = do (decls, ns) <- get
1383 let isn = concatMap (namesIn uvars ist) (map getTm as)
1384 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1385 imps top env (PPi (Imp l _ _ _) n ty sc)
1386 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1387 (decls , ns) <- get
1388 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1389 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1390 imps True (n:env) sc
1391 imps top env (PPi (Exp l _ _) n ty sc)
1392 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1393 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1394 _ -> [])
1395 (decls, ns) <- get -- ignore decls in HO types
1396 put (PExp (getPriority ist ty) l n Placeholder : decls,
1397 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1398 imps True (n:env) sc
1399 imps top env (PPi (Constraint l _) n ty sc)
1400 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1401 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1402 _ -> [])
1403 (decls, ns) <- get -- ignore decls in HO types
1404 put (PConstraint 10 l n Placeholder : decls,
1405 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1406 imps True (n:env) sc
1407 imps top env (PPi (TacImp l _ scr) n ty sc)
1408 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1409 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1410 _ -> [])
1411 (decls, ns) <- get -- ignore decls in HO types
1412 put (PTacImplicit 10 l n scr Placeholder : decls,
1413 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1414 imps True (n:env) sc
1415 imps top env (PEq _ _ _ l r)
1416 = do (decls, ns) <- get
1417 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1418 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1419 imps top env (PRewrite _ l r _)
1420 = do (decls, ns) <- get
1421 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1422 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1423 imps top env (PTyped l r)
1424 = imps top env l
1425 imps top env (PPair _ _ l r)
1426 = do (decls, ns) <- get
1427 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1428 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1429 imps top env (PDPair _ _ (PRef _ n) t r)
1430 = do (decls, ns) <- get
1431 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1432 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1433 imps top env (PDPair _ _ l t r)
1434 = do (decls, ns) <- get
1435 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1436 namesIn uvars ist r
1437 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1438 imps top env (PAlternative a as)
1439 = do (decls, ns) <- get
1440 let isn = concatMap (namesIn uvars ist) as
1441 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1442 imps top env (PLam fc n ty sc)
1443 = do imps False env ty
1444 imps False (n:env) sc
1445 imps top env (PHidden tm) = imps False env tm
1446 imps top env (PUnifyLog tm) = imps False env tm
1447 imps top env (PNoImplicits tm) = imps False env tm
1448 imps top env (PRunTactics fc tm) = imps False env tm
1449 imps top env _ = return ()
1451 pibind using [] sc = sc
1452 pibind using (n:ns) sc
1453 = case lookup n using of
1454 Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1455 Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1456 (pibind using ns sc)
1458-- Add implicit arguments in function calls
1459addImplPat :: IState -> PTerm -> PTerm
1460addImplPat = addImpl' True [] []
1462addImplBound :: IState -> [Name] -> PTerm -> PTerm
1463addImplBound ist ns = addImpl' False ns [] ist
1465addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1466addImplBoundInf ist ns inf = addImpl' False ns inf ist
1468-- | Add the implicit arguments to applications in the term
1469addImpl :: IState -> PTerm -> PTerm
1470addImpl = addImpl' False [] []
1472-- TODO: in patterns, don't add implicits to function names guarded by constructors
1473-- and *not* inside a PHidden
1475addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1476addImpl' inpat env infns ist ptm
1477 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1478 where
1479 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1480 ai qq env ds (PRef fc f)
1481 | f `elem` infns = PInferRef fc f
1482 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1483 ai qq env ds (PHidden (PRef fc f))
1484 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
1485 ai qq env ds (PEq fc lt rt l r)
1486 = let lt' = ai qq env ds lt
1487 rt' = ai qq env ds rt
1488 l' = ai qq env ds l
1489 r' = ai qq env ds r in
1490 PEq fc lt' rt' l' r'
1491 ai qq env ds (PRewrite fc l r g)
1492 = let l' = ai qq env ds l
1493 r' = ai qq env ds r
1494 g' = fmap (ai qq env ds) g in
1495 PRewrite fc l' r' g'
1496 ai qq env ds (PTyped l r)
1497 = let l' = ai qq env ds l
1498 r' = ai qq env ds r in
1499 PTyped l' r'
1500 ai qq env ds (PPair fc p l r)
1501 = let l' = ai qq env ds l
1502 r' = ai qq env ds r in
1503 PPair fc p l' r'
1504 ai qq env ds (PDPair fc p l t r)
1505 = let l' = ai qq env ds l
1506 t' = ai qq env ds t
1507 r' = ai qq env ds r in
1508 PDPair fc p l' t' r'
1509 ai qq env ds (PAlternative a as)
1510 = let as' = map (ai qq env ds) as in
1511 PAlternative a as'
1512 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1513 ai qq env ds (PApp fc (PInferRef _ f) as)
1514 = let as' = map (fmap (ai qq env ds)) as in
1515 PApp fc (PInferRef fc f) as'
1516 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1517 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1518 | not (f `elem` map fst env)
1519 = let as' = map (fmap (ai qq env ds)) as in
1520 handleErr $ aiFn inpat False qq ist fc f ds as'
1521 | Just (Just ty) <- lookup f env =
1522 let as' = map (fmap (ai qq env ds)) as
1523 arity = getPArity ty in
1524 mkPApp fc arity ftm as'
1525 ai qq env ds (PApp fc f as)
1526 = let f' = ai qq env ds f
1527 as' = map (fmap (ai qq env ds)) as in
1528 mkPApp fc 1 f' as'
1529 ai qq env ds (PCase fc c os)
1530 = let c' = ai qq env ds c in
1531 -- leave os alone, because they get lifted into a new pattern match
1532 -- definition which is passed through addImpl again with more scope
1533 -- information
1534 PCase fc c' os
1535 -- If the name in a lambda is a constructor name, do this as a 'case'
1536 -- instead (it is harmless to do so, especially since the lambda will
1537 -- be lifted anyway!)
1538 ai qq env ds (PLam fc n ty sc)
1539 = case lookupDef n (tt_ctxt ist) of
1540 [] -> let ty' = ai qq env ds ty
1541 sc' = ai qq ((n, Just ty):env) ds sc in
1542 PLam fc n ty' sc'
1543 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1544 (PCase fc (PRef fc (sMN 0 "lamp") )
1545 [(PRef fc n, sc)]))
1546 ai qq env ds (PLet fc n ty val sc)
1547 = case lookupDef n (tt_ctxt ist) of
1548 [] -> let ty' = ai qq env ds ty
1549 val' = ai qq env ds val
1550 sc' = ai qq ((n, Just ty):env) ds sc in
1551 PLet fc n ty' val' sc'
1552 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1553 ai qq env ds (PPi p n ty sc)
1554 = let ty' = ai qq env ds ty
1555 sc' = ai qq ((n, Just ty):env) ds sc in
1556 PPi p n ty' sc'
1557 ai qq env ds (PGoal fc r n sc)
1558 = let r' = ai qq env ds r
1559 sc' = ai qq ((n, Nothing):env) ds sc in
1560 PGoal fc r' n sc'
1561 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1562 -- Don't do PProof or PTactics since implicits get added when scope is
1563 -- properly known in ElabTerm.runTac
1564 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1565 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1566 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1567 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1568 (fmap (ai True env ds) g)
1569 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1570 ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
1571 ai qq env ds tm = tm
1573 handleErr (Left err) = PElabError err
1574 handleErr (Right x) = x
1576-- if in a pattern, and there are no arguments, and there's no possible
1577-- names with zero explicit arguments, don't add implicits.
1579aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1580aiFn inpat True qq ist fc f ds []
1581 = case lookupDef f (tt_ctxt ist) of
1582 [] -> Right $ PPatvar fc f
1583 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1584 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1585 if (not (vname f) || tcname f
1586 || any (conCaf (tt_ctxt ist)) ialts)
1587-- any constructor alts || any allImp ialts))
1588 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1589 else Right $ PPatvar fc f
1590 where imp (PExp _ _ _ _) = False
1591 imp _ = True
1592-- allImp [] = False
1593 allImp xs = all imp xs
1594 constructor (TyDecl (DCon _ _ _) _) = True
1595 constructor _ = False
1597 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1599 vname (UN n) = True -- non qualified
1600 vname _ = False
1602aiFn inpat expat qq ist fc f ds as
1603 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1604aiFn inpat expat qq ist fc f ds as
1605 -- This is where namespaces get resolved by adding PAlternative
1606 = do let ns = lookupCtxtName f (idris_implicits ist)
1607 let nh = filter (\(n, _) -> notHidden n) ns
1608 let ns' = case trimAlts ds nh of
1609 [] -> nh
1610 x -> x
1611 case ns' of
1612 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1613 [] -> if f `elem` (map fst (idris_metavars ist))
1614 then Right $ PApp fc (PRef fc f) as
1615 else Right $ mkPApp fc (length as) (PRef fc f) as
1616 alts -> Right $
1617 PAlternative True $
1618 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1619 (insertImpl ns as)) alts
1620 where
1621 trimAlts [] alts = alts
1622 trimAlts ns alts
1623 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1625 nspace (NS _ s) = s
1626 nspace _ = []
1628 notHidden n = case getAccessibility n of
1629 Hidden -> False
1630 _ -> True
1632 getAccessibility n
1633 = case lookupDefAccExact n False (tt_ctxt ist) of
1634 Just (n,t) -> t
1635 _ -> Public
1637 insertImpl :: [PArg] -> [PArg] -> [PArg]
1638 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1640 exp (PExp _ _ _ _) = True
1641 exp (PConstraint _ _ _ _) = True
1642 exp _ = False
1644 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1645 -> [PArg] -- parameters
1646 -> [PArg] -- explicit arguments
1647 -> [PArg] -- implicits given
1648 -> [PArg]
1649 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1650 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1651 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1652 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1653 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1654 let rtc = PResolveTC fc in
1655 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1656 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1657 case find n imps [] of
1658 Just (tm, imps') ->
1659 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1660 Nothing ->
1661 PImp p True l n Placeholder :
1662 insImpAcc (M.insert n Placeholder pnas) ps given imps
1663 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1664 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1665 case find n imps [] of
1666 Just (tm, imps') ->
1667 PTacImplicit p l n sc tm :
1668 insImpAcc (M.insert n tm pnas) ps given imps'
1669 Nothing ->
1670 if inpat
1671 then PTacImplicit p l n sc Placeholder :
1672 insImpAcc (M.insert n Placeholder pnas) ps given imps
1673 else PTacImplicit p l n sc sc :
1674 insImpAcc (M.insert n sc pnas) ps given imps
1675 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1676 -- TODO: report here, and prune alternatives
1677 -- Issue #1740 in the Issue Tracker
1678-- https://github.com/idris-lang/Idris-dev/issues/1740
1679 insImpAcc _ _ given imps = given ++ imps
1681 find n [] acc = Nothing
1682 find n (PImp _ _ _ n' t : gs) acc
1683 | n == n' = Just (t, reverse acc ++ gs)
1684 find n (PTacImplicit _ _ n' _ t : gs) acc
1685 | n == n' = Just (t, reverse acc ++ gs)
1686 find n (g : gs) acc = find n gs (g : acc)
1688-- replace non-linear occurrences with _
1690stripLinear :: IState -> PTerm -> PTerm
1691stripLinear i tm = evalState (sl tm) [] where
1692 sl :: PTerm -> State [Name] PTerm
1693 sl (PRef fc f)
1694 | (_:_) <- lookupTy f (tt_ctxt i)
1695 = return $ PRef fc f
1696 | otherwise = do ns <- get
1697 if (f `elem` ns)
1698 then return $ PHidden (PRef fc f) -- Placeholder
1699 else do put (f : ns)
1700 return (PRef fc f)
1701 sl (PPatvar fc f)
1702 = do ns <- get
1703 if (f `elem` ns)
1704 then return $ PHidden (PPatvar fc f) -- Placeholder
1705 else do put (f : ns)
1706 return (PPatvar fc f)
1707 -- Assumption is that variables are all the same in each alternative
1708 sl t@(PAlternative b as) = do ns <- get
1709 as' <- slAlts ns as
1710 return (PAlternative b as')
1711 where slAlts ns (a : as) = do put ns
1712 a' <- sl a
1713 as' <- slAlts ns as
1714 return (a' : as')
1715 slAlts ns [] = return []
1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1717 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1718 args' <- mapM slA args
1719 return $ PApp fc fn args'
1720 where slA (PImp p m l n t) = do t' <- sl t
1721 return $ PImp p m l n t'
1722 slA (PExp p l n t) = do t' <- sl t
1723 return $ PExp p l n t'
1724 slA (PConstraint p l n t)
1725 = do t' <- sl t
1726 return $ PConstraint p l n t'
1727 slA (PTacImplicit p l n sc t)
1728 = do t' <- sl t
1729 return $ PTacImplicit p l n sc t'
1730 sl x = return x
1732-- Remove functions which aren't applied to anything, which must then
1733-- be resolved by unification. Assume names resolved and alternatives
1734-- filled in (so no ambiguity).
1736stripUnmatchable :: IState -> PTerm -> PTerm
1737stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1738 su :: PTerm -> PTerm
1739 su (PRef fc f)
1740 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1741 = Placeholder
1742 su (PApp fc f@(PRef _ fn) args)
1743 -- here we use canBeDConName because the impossible pattern
1744 -- check will not necessarily fully resolve constructor names,
1745 -- and these bare names will otherwise get in the way of
1746 -- impossbility checking.
1747 | canBeDConName fn ctxt
1748 = PApp fc f (fmap (fmap su) args)
1749 su (PApp fc f args)
1750 = PHidden (PApp fc f args)
1751 su (PAlternative b alts)
1752 = let alts' = filter (/= Placeholder) (map su alts) in
1753 if null alts' then Placeholder
1754 else PAlternative b alts'
1755 su (PPair fc p l r) = PPair fc p (su l) (su r)
1756 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1757 su t@(PLam fc _ _ _) = PHidden t
1758 su t@(PPi _ _ _ _) = PHidden t
1759 su t@(PEq _ _ _ _ _) = PHidden t
1760 su t = t
1762 ctxt = tt_ctxt i
1764stripUnmatchable i tm = tm
1766mkPApp fc a f [] = f
1767mkPApp fc a f as = let rest = drop a as in
1768 appRest fc (PApp fc f (take a as)) rest
1769 where
1770 appRest fc f [] = f
1771 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1773-- Find 'static' argument positions
1774-- (the declared ones, plus any names in argument position in the declared
1775-- statics)
1776-- FIXME: It's possible that this really has to happen after elaboration
1778findStatics :: IState -> PTerm -> (PTerm, [Bool])
1779findStatics ist tm = trace (show tm) $
1780 let (ns, ss) = fs tm in
1781 runState (pos ns ss tm) []
1782 where fs (PPi p n t sc)
1783 | Static <- pstatic p
1784 = let (ns, ss) = fs sc in
1785 (namesIn [] ist t : ns, n : ss)
1786 | otherwise = let (ns, ss) = fs sc in
1787 (ns, ss)
1788 fs _ = ([], [])
1790 inOne n ns = length (filter id (map (elem n) ns)) == 1
1792 pos ns ss (PPi p n t sc)
1793 | elem n ss = do sc' <- pos ns ss sc
1794 spos <- get
1795 put (True : spos)
1796 return (PPi (p { pstatic = Static }) n t sc')
1797 | otherwise = do sc' <- pos ns ss sc
1798 spos <- get
1799 put (False : spos)
1800 return (PPi p n t sc')
1801 pos ns ss t = return t
1803-- for 6.12/7 compatibility
1804data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1806instance Applicative (EitherErr a) where
1807 pure = return
1808 (<*>) = ap
1810instance Monad (EitherErr a) where
1811 return = RightOK
1813 (LeftErr e) >>= k = LeftErr e
1814 RightOK v >>= k = k v
1816toEither (LeftErr e) = Left e
1817toEither (RightOK ho) = Right ho
1819-- syntactic match of a against b, returning pair of variables in a
1820-- and what they match. Returns the pair that failed if not a match.
1822matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1823matchClause = matchClause' False
1825matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1826matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1827 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1829 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1830 fullApp x = x
1832 match' x y = match (fullApp x) (fullApp y)
1833 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1834 | fi == txt "fromInteger" && b == txt "builtins",
1835 PConstant (I _) <- getTm x = match (getTm x) x'
1836 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1837 | fi == txt "fromInteger" && b == txt "builtins",
1838 PConstant (I _) <- getTm x = match (getTm x) x'
1839 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1840 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1841 match (PApp _ f args) (PApp _ f' args')
1842 | length args == length args'
1843 = do mf <- match' f f'
1844 ms <- zipWithM matchArg args args'
1845 return (mf ++ concat ms)
1846 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1847 match (PPatvar f n) xr = match (PRef f n) xr
1848 match xr (PPatvar f n) = match xr (PRef f n)
1849 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1850 match (PRef _ n) tm@(PRef _ n')
1851 | n == n' && not names &&
1852 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1853 || tm == Placeholder)
1854 = return [(n, tm)]
1855 -- if one namespace is missing, drop the other
1856 | n == n' || n == dropNS n' || dropNS n == n' = return []
1857 where dropNS (NS n _) = n
1858 dropNS n = n
1859 match (PRef _ n) tm
1860 | not names && (not (isConName n (tt_ctxt i) ||
1861 isFnName n (tt_ctxt i)) || tm == Placeholder)
1862 = return [(n, tm)]
1863 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1864 = do ml <- match' l l'
1865 mr <- match' r r'
1866 return (ml ++ mr)
1867 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1868 = do ml <- match' l l'
1869 mr <- match' r r'
1870 return (ml ++ mr)
1871 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1872 mr <- match r r'
1873 return (ml ++ mr)
1874 match (PTyped l r) x = match l x
1875 match x (PTyped l r) = match x l
1876 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1877 mr <- match' r r'
1878 return (ml ++ mr)
1879 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1880 mt <- match' t t'
1881 mr <- match' r r'
1882 return (ml ++ mt ++ mr)
1883 match (PAlternative a as) (PAlternative a' as')
1884 = do ms <- zipWithM match' as as'
1885 return (concat ms)
1886 match a@(PAlternative _ as) b
1887 = do let ms = zipWith match' as (repeat b)
1888 case (rights (map toEither ms)) of
1889 (x: _) -> return x
1890 _ -> LeftErr (a, b)
1891 match (PCase _ _ _) _ = return [] -- lifted out
1892 match (PMetavar _) _ = return [] -- modified
1893 match (PInferRef _ _) _ = return [] -- modified
1894 match (PQuote _) _ = return []
1895 match (PProof _) _ = return []
1896 match (PTactics _) _ = return []
1897 match (PRefl _ _) (PRefl _ _) = return []
1898 match (PResolveTC _) (PResolveTC _) = return []
1899 match (PTrue _ _) (PTrue _ _) = return []
1900 match (PReturn _) (PReturn _) = return []
1901 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1902 ms <- match' s s'
1903 return (mt ++ ms)
1904 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1905 ms <- match' s s'
1906 return (mt ++ ms)
1907 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1908 mty <- match' ty ty'
1909 ms <- match' s s'
1910 return (mt ++ mty ++ ms)
1911 match (PHidden x) (PHidden y)
1912 | RightOK xs <- match x y = return xs -- to collect variables
1913 | otherwise = return [] -- Otherwise hidden things are unmatchable
1914 match (PHidden x) y
1915 | RightOK xs <- match x y = return xs
1916 | otherwise = return []
1917 match x (PHidden y)
1918 | RightOK xs <- match x y = return xs
1919 | otherwise = return []
1920 match (PUnifyLog x) y = match' x y
1921 match x (PUnifyLog y) = match' x y
1922 match (PNoImplicits x) y = match' x y
1923 match x (PNoImplicits y) = match' x y
1924 match Placeholder _ = return []
1925 match _ Placeholder = return []
1926 match (PResolveTC _) _ = return []
1927 match a b | a == b = return []
1928 | otherwise = LeftErr (a, b)
1930 checkRpts (RightOK ms) = check ms where
1931 check ((n,t):xs)
1932 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1933 then Left (t, t')
1934 else check xs
1935 check (_:xs) = check xs
1936 check [] = Right ms
1937 checkRpts (LeftErr x) = Left x
1939substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1940substMatches ms = substMatchesShadow ms []
1942substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1943substMatchesShadow [] shs t = t
1944substMatchesShadow ((n,tm):ns) shs t
1945 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1947substMatch :: Name -> PTerm -> PTerm -> PTerm
1948substMatch n = substMatchShadow n []
1950substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1951substMatchShadow n shs tm t = sm shs t where
1952 sm xs (PRef _ n') | n == n' = tm
1953 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1954 sm xs (PPi p x t sc)
1955 | x `elem` xs
1956 = let x' = nextName x in
1957 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1958 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1959 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1960 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1961 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1962 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1963 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1964 (fmap (sm xs) tm)
1965 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1966 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1967 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1968 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1969 sm xs (PHidden x) = PHidden (sm xs x)
1970 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1971 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1972 sm xs x = x
1974 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1975 fullApp x = x
1977shadow :: Name -> Name -> PTerm -> PTerm
1978shadow n n' t = sm t where
1979 sm (PRef fc x) | n == x = PRef fc n'
1980 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
1981 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1982 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
1983 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1984 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1985 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1986 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1987 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1988 sm (PTyped x y) = PTyped (sm x) (sm y)
1989 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1990 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1991 sm (PAlternative a as) = PAlternative a (map sm as)
1992 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1993 sm (PProof ts) = PProof (map (fmap sm) ts)
1994 sm (PHidden x) = PHidden (sm x)
1995 sm (PUnifyLog x) = PUnifyLog (sm x)
1996 sm (PNoImplicits x) = PNoImplicits (sm x)
1997 sm x = x
1999-- Rename any binders which are repeated (so that we don't have to mess
2000-- about with shadowing anywhere else).
2002mkUniqueNames :: [Name] -> PTerm -> PTerm
2003mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2004 inScope :: S.Set Name
2005 inScope = S.fromList $ boundNamesIn tm
2007 mkUniqA arg = do t' <- mkUniq (getTm arg)
2008 return (arg { getTm = t' })
2010 -- Initialise the unique name with the environment length (so we're not
2011 -- looking for too long...)
2012 initN (UN n) l = UN $ txt (str n ++ show l)
2013 initN (MN i s) l = MN (i+l) s
2014 initN n l = n
2016 -- FIXME: Probably ought to do this for completeness! It's fine as
2017 -- long as there are no bindings inside tactics though.
2018 mkUniqT tac = return tac
2020 mkUniq :: PTerm -> State (S.Set Name) PTerm
2021 mkUniq (PLam fc n ty sc)
2022 = do env <- get
2023 (n', sc') <-
2024 if n `S.member` env
2025 then do let n' = uniqueNameSet (initN n (S.size env))
2026 (S.union env inScope)
2027 return (n', shadow n n' sc)
2028 else return (n, sc)
2029 put (S.insert n' env)
2030 ty' <- mkUniq ty
2031 sc'' <- mkUniq sc'
2032 return $! PLam fc n' ty' sc''
2033 mkUniq (PPi p n ty sc)
2034 = do env <- get
2035 (n', sc') <-
2036 if n `S.member` env
2037 then do let n' = uniqueNameSet (initN n (S.size env))
2038 (S.union env inScope)
2039 return (n', shadow n n' sc)
2040 else return (n, sc)
2041 put (S.insert n' env)
2042 ty' <- mkUniq ty
2043 sc'' <- mkUniq sc'
2044 return $! PPi p n' ty' sc''
2045 mkUniq (PLet fc n ty val sc)
2046 = do env <- get
2047 (n', sc') <-
2048 if n `S.member` env
2049 then do let n' = uniqueNameSet (initN n (S.size env))
2050 (S.union env inScope)
2051 return (n', shadow n n' sc)
2052 else return (n, sc)
2053 put (S.insert n' env)
2054 ty' <- mkUniq ty; val' <- mkUniq val
2055 sc'' <- mkUniq sc'
2056 return $! PLet fc n' ty' val' sc''
2057 mkUniq (PApp fc t args)
2058 = do t' <- mkUniq t
2059 args' <- mapM mkUniqA args
2060 return $! PApp fc t' args'
2061 mkUniq (PAppBind fc t args)
2062 = do t' <- mkUniq t
2063 args' <- mapM mkUniqA args
2064 return $! PAppBind fc t' args'
2065 mkUniq (PCase fc t alts)
2066 = do t' <- mkUniq t
2067 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2068 return (x', y')) alts
2069 return $! PCase fc t' alts'
2070 mkUniq (PPair fc p l r)
2071 = do l' <- mkUniq l; r' <- mkUniq r
2072 return $! PPair fc p l' r'
2073 mkUniq (PDPair fc p (PRef fc' n) t sc)
2074 | t /= Placeholder
2075 = do env <- get
2076 (n', sc') <- if n `S.member` env
2077 then do let n' = uniqueNameSet n (S.union env inScope)
2078 return (n', shadow n n' sc)
2079 else return (n, sc)
2080 put (S.insert n' env)
2081 t' <- mkUniq t
2082 sc'' <- mkUniq sc'
2083 return $! PDPair fc p (PRef fc' n') t' sc''
2084 mkUniq (PDPair fc p l t r)
2085 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2086 return $! PDPair fc p l' t' r'
2087 mkUniq (PAlternative b as)
2088 = liftM (PAlternative b) (mapM mkUniq as)
2089 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2090 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2091 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2092 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2093 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2094 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2095 mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
2096 mkUniq t = return t