git.iko.soy/Idris-dev
on a87f69e help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2085 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.IdeSlave 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 IdeSlave 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 IdeSlave 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
755setIdeSlave :: Bool -> Handle -> Idris ()
756setIdeSlave True h = do i <- getIState
757 putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }
758setIdeSlave False _ = return ()
760setTargetTriple :: String -> Idris ()
761setTargetTriple t = do i <- getIState
762 let opts = idris_options i
763 opt' = opts { opt_triple = t }
764 putIState $ i { idris_options = opt' }
766targetTriple :: Idris String
767targetTriple = do i <- getIState
768 return (opt_triple (idris_options i))
770setTargetCPU :: String -> Idris ()
771setTargetCPU t = do i <- getIState
772 let opts = idris_options i
773 opt' = opts { opt_cpu = t }
774 putIState $ i { idris_options = opt' }
776targetCPU :: Idris String
777targetCPU = do i <- getIState
778 return (opt_cpu (idris_options i))
780verbose :: Idris Bool
781verbose = do i <- getIState
782 return (opt_verbose (idris_options i))
784setVerbose :: Bool -> Idris ()
785setVerbose t = do i <- getIState
786 let opts = idris_options i
787 let opt' = opts { opt_verbose = t }
788 putIState $ i { idris_options = opt' }
790typeInType :: Idris Bool
791typeInType = do i <- getIState
792 return (opt_typeintype (idris_options i))
794setTypeInType :: Bool -> Idris ()
795setTypeInType t = do i <- getIState
796 let opts = idris_options i
797 let opt' = opts { opt_typeintype = t }
798 putIState $ i { idris_options = opt' }
800coverage :: Idris Bool
801coverage = do i <- getIState
802 return (opt_coverage (idris_options i))
804setCoverage :: Bool -> Idris ()
805setCoverage t = do i <- getIState
806 let opts = idris_options i
807 let opt' = opts { opt_coverage = t }
808 putIState $ i { idris_options = opt' }
810setIBCSubDir :: FilePath -> Idris ()
811setIBCSubDir fp = do i <- getIState
812 let opts = idris_options i
813 let opt' = opts { opt_ibcsubdir = fp }
814 putIState $ i { idris_options = opt' }
816valIBCSubDir :: IState -> Idris FilePath
817valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
819addImportDir :: FilePath -> Idris ()
820addImportDir fp = do i <- getIState
821 let opts = idris_options i
822 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
823 putIState $ i { idris_options = opt' }
825setImportDirs :: [FilePath] -> Idris ()
826setImportDirs fps = do i <- getIState
827 let opts = idris_options i
828 let opt' = opts { opt_importdirs = fps }
829 putIState $ i { idris_options = opt' }
831allImportDirs :: Idris [FilePath]
832allImportDirs = do i <- getIState
833 let optdirs = opt_importdirs (idris_options i)
834 return ("." : reverse optdirs)
836colourise :: Idris Bool
837colourise = do i <- getIState
838 return $ idris_colourRepl i
840setColourise :: Bool -> Idris ()
841setColourise b = do i <- getIState
842 putIState $ i { idris_colourRepl = b }
844impShow :: Idris Bool
845impShow = do i <- getIState
846 return (opt_showimp (idris_options i))
848setImpShow :: Bool -> Idris ()
849setImpShow t = do i <- getIState
850 let opts = idris_options i
851 let opt' = opts { opt_showimp = t }
852 putIState $ i { idris_options = opt' }
854setColour :: ColourType -> IdrisColour -> Idris ()
855setColour ct c = do i <- getIState
856 let newTheme = setColour' ct c (idris_colourTheme i)
857 putIState $ i { idris_colourTheme = newTheme }
858 where setColour' KeywordColour c t = t { keywordColour = c }
859 setColour' BoundVarColour c t = t { boundVarColour = c }
860 setColour' ImplicitColour c t = t { implicitColour = c }
861 setColour' FunctionColour c t = t { functionColour = c }
862 setColour' TypeColour c t = t { typeColour = c }
863 setColour' DataColour c t = t { dataColour = c }
864 setColour' PromptColour c t = t { promptColour = c }
865 setColour' PostulateColour c t = t { postulateColour = c }
867logLvl :: Int -> String -> Idris ()
868logLvl l str = do i <- getIState
869 let lvl = opt_logLevel (idris_options i)
870 when (lvl >= l) $
871 case idris_outputmode i of
872 RawOutput h -> do runIO $ hPutStrLn h str
873 IdeSlave n h ->
874 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
875 runIO . hPutStrLn h $ convSExp "log" good n
877cmdOptType :: Opt -> Idris Bool
878cmdOptType x = do i <- getIState
879 return $ x `elem` opt_cmdline (idris_options i)
881iLOG :: String -> Idris ()
882iLOG = logLvl 1
884noErrors :: Idris Bool
885noErrors = do i <- getIState
886 case errSpan i of
887 Nothing -> return True
888 _ -> return False
890setTypeCase :: Bool -> Idris ()
891setTypeCase t = do i <- getIState
892 let opts = idris_options i
893 let opt' = opts { opt_typecase = t }
894 putIState $ i { idris_options = opt' }
897-- Dealing with parameters
899expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
900 [Name] -> -- all names
901 [Name] -> -- names with no declaration
902 PTerm -> PTerm
903expandParams dec ps ns infs tm = en tm
904 where
905 -- if we shadow a name (say in a lambda binding) that is used in a call to
906 -- a lifted function, we need access to both names - once in the scope of the
907 -- binding and once to call the lifted functions. So we'll explicitly shadow
908 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
909 -- but we didn't...)
911 mkShadow (UN n) = MN 0 n
912 mkShadow (MN i n) = MN (i+1) n
913 mkShadow (NS x s) = NS (mkShadow x) s
915 en (PLam fc n t s)
916 | n `elem` (map fst ps ++ ns)
917 = let n' = mkShadow n in
918 PLam fc n' (en t) (en (shadow n n' s))
919 | otherwise = PLam fc n (en t) (en s)
920 en (PPi p n t s)
921 | n `elem` (map fst ps ++ ns)
922 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
923 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
924 | otherwise = PPi (enTacImp p) n (en t) (en s)
925 en (PLet fc n ty v s)
926 | n `elem` (map fst ps ++ ns)
927 = let n' = mkShadow n in
928 PLet fc n' (en ty) (en v) (en (shadow n n' s))
929 | otherwise = PLet fc n (en ty) (en v) (en s)
930 -- FIXME: Should only do this in a type signature!
931 en (PDPair f p (PRef f' n) t r)
932 | n `elem` (map fst ps ++ ns) && t /= Placeholder
933 = let n' = mkShadow n in
934 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
935 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
936 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
937 en (PTyped l r) = PTyped (en l) (en r)
938 en (PPair f p l r) = PPair f p (en l) (en r)
939 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
940 en (PAlternative a as) = PAlternative a (map en as)
941 en (PHidden t) = PHidden (en t)
942 en (PUnifyLog t) = PUnifyLog (en t)
943 en (PDisamb ds t) = PDisamb ds (en t)
944 en (PNoImplicits t) = PNoImplicits (en t)
945 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
946 en (PProof ts) = PProof (map (fmap en) ts)
947 en (PTactics ts) = PTactics (map (fmap en) ts)
949 en (PQuote (Var n))
950 | n `nselem` ns = PQuote (Var (dec n))
951 en (PApp fc (PInferRef fc' n) as)
952 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
953 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
954 en (PApp fc (PRef fc' n) as)
955 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
956 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
957 | n `nselem` ns = PApp fc (PRef fc' (dec n))
958 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
959 en (PAppBind fc (PRef fc' n) as)
960 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
961 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
962 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
963 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
964 en (PRef fc n)
965 | n `elem` infs = PApp fc (PInferRef fc (dec n))
966 (map (pexp . (PRef fc)) (map fst ps))
967 | n `nselem` ns = PApp fc (PRef fc (dec n))
968 (map (pexp . (PRef fc)) (map fst ps))
969 en (PInferRef fc n)
970 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
971 (map (pexp . (PRef fc)) (map fst ps))
972 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
973 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
974 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
975 en t = t
977 nselem x [] = False
978 nselem x (y : xs) | nseq x y = True
979 | otherwise = nselem x xs
981 nseq x y = nsroot x == nsroot y
983 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
984 enTacImp other = other
986expandParamsD :: Bool -> -- True = RHS only
987 IState ->
988 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
989expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
990 = if n `elem` ns && (not rhsonly)
991 then -- trace (show (n, expandParams dec ps ns ty)) $
992 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
993 else --trace (show (n, expandParams dec ps ns ty)) $
994 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
995expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
996 = if n `elem` ns && (not rhsonly)
997 then -- trace (show (n, expandParams dec ps ns ty)) $
998 PPostulate doc syn fc o (dec n) (piBind ps
999 (expandParams dec ps ns [] ty))
1000 else --trace (show (n, expandParams dec ps ns ty)) $
1001 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1002expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1003 = let n' = if n `elem` ns then dec n else n in
1004 PClauses fc opts n' (map expandParamsC cs)
1005 where
1006 expandParamsC (PClause fc n lhs ws rhs ds)
1007 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1008 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1009 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1010 n' = if n `elem` ns then dec n else n
1011 -- names bound on the lhs should not be expanded on the rhs
1012 ns' = removeBound lhs ns in
1013 PClause fc n' lhs'
1014 (map (expandParams dec ps'' ns' []) ws)
1015 (expandParams dec ps'' ns' [] rhs)
1016 (map (expandParamsD True ist dec ps'' ns') ds)
1017 expandParamsC (PWith fc n lhs ws wval ds)
1018 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1019 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1020 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1021 n' = if n `elem` ns then dec n else n
1022 ns' = removeBound lhs ns in
1023 PWith fc n' lhs'
1024 (map (expandParams dec ps'' ns' []) ws)
1025 (expandParams dec ps'' ns' [] wval)
1026 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1027 updateps yn nm [] = []
1028 updateps yn nm (((a, t), i):as)
1029 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1030 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1032 removeBound lhs ns = ns \\ nub (bnames lhs)
1034 bnames (PRef _ n) = [n]
1035 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1036 bnames (PPair _ _ l r) = bnames l ++ bnames r
1037 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1038 bnames _ = []
1040-- | Expands parameters defined in parameter and where blocks inside of declarations
1041expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1042 = PData doc argDocs syn fc co (expandPData pd)
1043 where
1044 -- just do the type decl, leave constructors alone (parameters will be
1045 -- added implicitly)
1046 expandPData (PDatadecl n ty cons)
1047 = if n `elem` ns
1048 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1049 (map econ cons)
1050 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1051 econ (doc, argDocs, n, t, fc, fs)
1052 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1053expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
1054 = if tn `elem` ns
1055 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1056 opts cdoc (dec cn) conty
1057 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1058 opts cdoc (dec cn) conty
1059 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1060expandParamsD rhs ist dec ps ns (PParams f params pds)
1061 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1062 (map (expandParamsD True ist dec ps ns) pds)
1063-- (map (expandParamsD ist dec ps ns) pds)
1064expandParamsD rhs ist dec ps ns (PMutual f pds)
1065 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1066expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
1067 = PClass doc info f
1068 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1070 (map (mapsnd (expandParams dec ps ns [])) params)
1071 pDocs
1072 (map (expandParamsD rhs ist dec ps ns) decls)
1073expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1074 = PInstance info f
1075 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1077 (map (expandParams dec ps ns []) params)
1078 (expandParams dec ps ns [] ty)
1079 cn
1080 (map (expandParamsD rhs ist dec ps ns) decls)
1081expandParamsD rhs ist dec ps ns d = d
1083mapsnd f (x, t) = (x, f t)
1085-- Calculate a priority for a type, for deciding elaboration order
1086-- * if it's just a type variable or concrete type, do it early (0)
1087-- * if there's only type variables and injective constructors, do it next (1)
1088-- * if there's a function type, next (2)
1089-- * finally, everything else (3)
1091getPriority :: IState -> PTerm -> Int
1092getPriority i tm = 1 -- pri tm
1093 where
1094 pri (PRef _ n) =
1095 case lookupP n (tt_ctxt i) of
1096 ((P (DCon _ _ _) _ _):_) -> 1
1097 ((P (TCon _ _) _ _):_) -> 1
1098 ((P Ref _ _):_) -> 1
1099 [] -> 0 -- must be locally bound, if it's not an error...
1100 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1101 pri (PTrue _ _) = 0
1102 pri (PRefl _ _) = 1
1103 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1104 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1105 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1106 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1107 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1108 pri (PTyped l r) = pri l
1109 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1110 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1111 pri (PAlternative a as) = maximum (map pri as)
1112 pri (PConstant _) = 0
1113 pri Placeholder = 1
1114 pri _ = 3
1117addStatics :: Name -> Term -> PTerm -> Idris ()
1118addStatics n tm ptm =
1119 do let (statics, dynamics) = initStatics tm ptm
1120 ist <- getIState
1121 let paramnames
1122 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1123 Just p -> getNamesFrom 0 (fn_params p) tm ++
1124 concatMap (getParamNames ist) (map snd statics)
1125 _ -> concatMap (getParamNames ist) (map snd statics)
1127 let stnames = nub $ concatMap freeArgNames (map snd statics)
1128 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1129 \\ paramnames
1130 -- also get the arguments which are 'uniquely inferrable' from
1131 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1132 -- or parameters to the type of a static
1133 let statics' = nub $ map fst statics ++
1134 filter (\x -> not (elem x dnames)) stnames
1135 let stpos = staticList statics' tm
1136 i <- getIState
1137 when (not (null statics)) $
1138 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1139 ++ showTmImpls ptm ++ "\n"
1140 ++ show statics ++ "\n" ++ show dynamics
1141 ++ "\n" ++ show paramnames
1142 ++ "\n" ++ show stpos
1143 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1144 addIBC (IBCStatic n)
1145 where
1146 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
1147 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1148 (static, (n, ty) : dynamic)
1149 initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)
1150 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1151 if pstatic p == Static then ((n, ty) : static, dynamic)
1152 else if (not (searchArg p))
1153 then (static, (n, ty) : dynamic)
1154 else (static, dynamic)
1155 initStatics t pt = ([], [])
1157 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1158 = case lookupCtxtExact n (idris_datatypes ist) of
1159 Just ti -> getNamePos 0 (param_pos ti) args
1160 Nothing -> []
1161 where getNamePos i ps [] = []
1162 getNamePos i ps (P _ n _ : as)
1163 | i `elem` ps = n : getNamePos (i + 1) ps as
1164 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1165 getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
1166 = n : getParamNames ist sc
1167 getParamNames ist _ = []
1169 getNamesFrom i ps (Bind n (Pi _ _ _) sc)
1170 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1171 | otherwise = getNamesFrom (i + 1) ps sc
1172 getNamesFrom i ps sc = []
1174 freeArgNames (Bind n (Pi _ ty _) sc)
1175 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1176 freeArgNames tm = let (_, args) = unApply tm in
1177 concatMap freeNames args
1179 -- if a name appears in a type class or tactic implicit index, it doesn't
1180 -- affect its 'uniquely inferrable' from a static status since these are
1181 -- resolved by searching.
1182 searchArg (Constraint _ _) = True
1183 searchArg (TacImp _ _ _) = True
1184 searchArg _ = False
1186 staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc
1187 staticList _ _ = []
1189-- Dealing with implicit arguments
1191-- Add some bound implicits to the using block if they aren't there already
1193addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1194addToUsing us [] = us
1195addToUsing us ((n, t) : ns)
1196 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1197 | otherwise = addToUsing us ns
1198 where impName (UImplicit n _) = Just n
1199 impName _ = Nothing
1201-- Add constraint bindings from using block
1203addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1204addUsingConstraints syn fc t
1205 = do ist <- get
1206 let ns = namesIn [] ist t
1207 let cs = getConstraints t -- check declared constraints
1208 let addconsts = uconsts \\ cs
1209 return (doAdd addconsts ns t)
1210 where uconsts = filter uconst (using syn)
1211 uconst (UConstraint _ _) = True
1212 uconst _ = False
1214 doAdd [] _ t = t
1215 -- if all of args in ns, then add it
1216 doAdd (UConstraint c args : cs) ns t
1217 | all (\n -> elem n ns) args
1218 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1219 (mkConst c args) (doAdd cs ns t)
1220 | otherwise = doAdd cs ns t
1222 mkConst c args = PApp fc (PRef fc c)
1223 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1225 getConstraints (PPi (Constraint _ _) _ c sc)
1226 = getcapp c ++ getConstraints sc
1227 getConstraints (PPi _ _ c sc) = getConstraints sc
1228 getConstraints _ = []
1230 getcapp (PApp _ (PRef _ c) args)
1231 = do ns <- mapM getName args
1232 return (UConstraint c ns)
1233 getcapp _ = []
1235 getName (PExp _ _ _ (PRef _ n)) = return n
1236 getName _ = []
1238-- Add implicit bindings from using block, and bind any missing names
1239addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1240addUsingImpls syn n fc t
1241 = do ist <- getIState
1242 let ns = implicitNamesIn (map iname uimpls) ist t
1243 let badnames = filter (\n -> not (implicitable n) &&
1244 n `notElem` (map iname uimpls)) ns
1245 when (not (null badnames)) $
1246 throwError (At fc (Elaborating "type of " n
1247 (NoSuchVariable (head badnames))))
1248 let cs = getArgnames t -- get already bound names
1249 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1250 -- if all names in the arguments of addconsts appear in ns,
1251 -- add the constraint implicitly
1252 return (bindFree ns (doAdd addimpls ns t))
1253 where uimpls = filter uimpl (using syn)
1254 uimpl (UImplicit _ _) = True
1255 uimpl _ = False
1257 iname (UImplicit n _) = n
1258 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1260 doAdd [] _ t = t
1261 -- if all of args in ns, then add it
1262 doAdd (UImplicit n ty : cs) ns t
1263 | elem n ns
1264 = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)
1265 | otherwise = doAdd cs ns t
1267 -- bind the free names which weren't in the using block
1268 bindFree [] tm = tm
1269 bindFree (n:ns) tm
1270 | elem n (map iname uimpls) = bindFree ns tm
1271 | otherwise
1272 = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
1274 getArgnames (PPi _ n c sc)
1275 = n : getArgnames sc
1276 getArgnames _ = []
1278-- Given the original type and the elaborated type, return the implicitness
1279-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1281getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1282getUnboundImplicits i t tm = getImps t (collectImps tm)
1283 where collectImps (PPi p n t sc)
1284 = (n, (p, t)) : collectImps sc
1285 collectImps _ = []
1287 getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
1288 getImps (Bind n (Pi _ t _) sc) imps
1289 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1290 where
1291 argInfo n (Imp opt _ _ _) t'
1292 = (True, PImp (getPriority i t') True opt n t')
1293 argInfo n (Exp opt _ _) t'
1294 = (InaccessibleArg `elem` opt,
1295 PExp (getPriority i t') opt n t')
1296 argInfo n (Constraint opt _) t'
1297 = (InaccessibleArg `elem` opt,
1298 PConstraint 10 opt n t')
1299 argInfo n (TacImp opt _ scr) t'
1300 = (InaccessibleArg `elem` opt,
1301 PTacImplicit 10 opt n scr t')
1302 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1303 where impBind n t = (True, PImp 1 True [] n Placeholder)
1304 getImps sc tm = []
1306-- Add implicit Pi bindings for any names in the term which appear in an
1307-- argument position.
1309-- This has become a right mess already. Better redo it some time...
1310-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1311-- a couple of places which use it. Clean them up!
1313-- Issue 1739 in the issue tracker
1314-- https://github.com/idris-lang/Idris-dev/issues/1739
1315implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1316implicit info syn n ptm = implicit' info syn [] n ptm
1318implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1319implicit' info syn ignore n ptm
1320 = do i <- getIState
1321 let (tm', impdata) = implicitise syn ignore i ptm
1322 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1323-- let (tm'', spos) = findStatics i tm'
1324 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1325 addIBC (IBCImp n)
1326 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1327-- i <- get
1328-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1329 return tm'
1330 where
1331 -- Detect unknown names in default arguments and throw error if found.
1332 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1333 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1335 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1336 notFoundInDefault kns (PTacImplicit _ _ n script _)
1337 = do i <- getIState
1338 case notFound kns (namesIn [] i script) of
1339 Nothing -> return (n:kns)
1340 Just name -> throwError (NoSuchVariable name)
1341 notFoundInDefault kns p = return ((pname p):kns)
1343 notFound :: [Name] -> [Name] -> Maybe Name
1344 notFound kns [] = Nothing
1345 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1346 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1348implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1349implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1350 let (declimps, ns') = execState (imps True [] tm) ([], [])
1351 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1352 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1353 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1354 if null ns
1355 then (tm, reverse declimps)
1356 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1357 where
1358 uvars = map ipair (filter uimplicit (using syn))
1359 pvars = syn_params syn
1361 inUsing n = n `elem` map fst uvars
1363 ipair (UImplicit x y) = (x, y)
1364 uimplicit (UImplicit _ _) = True
1365 uimplicit _ = False
1367 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1368 | otherwise = x : dropAll xs ys
1369 dropAll [] ys = []
1371 -- Find names in argument position in a type, suitable for implicit
1372 -- binding
1373 -- Not the function position, but do everything else...
1374 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1375 implNamesIn uv t = namesIn uv ist t
1377 imps top env (PApp _ f as)
1378 = do (decls, ns) <- get
1379 let isn = concatMap (namesIn uvars ist) (map getTm as)
1380 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1381 imps top env (PPi (Imp l _ _ _) n ty sc)
1382 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1383 (decls , ns) <- get
1384 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1385 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1386 imps True (n:env) sc
1387 imps top env (PPi (Exp l _ _) n ty sc)
1388 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1389 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1390 _ -> [])
1391 (decls, ns) <- get -- ignore decls in HO types
1392 put (PExp (getPriority ist ty) l n Placeholder : decls,
1393 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1394 imps True (n:env) sc
1395 imps top env (PPi (Constraint l _) n ty sc)
1396 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1397 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1398 _ -> [])
1399 (decls, ns) <- get -- ignore decls in HO types
1400 put (PConstraint 10 l n Placeholder : decls,
1401 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1402 imps True (n:env) sc
1403 imps top env (PPi (TacImp l _ scr) n ty sc)
1404 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1405 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1406 _ -> [])
1407 (decls, ns) <- get -- ignore decls in HO types
1408 put (PTacImplicit 10 l n scr Placeholder : decls,
1409 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1410 imps True (n:env) sc
1411 imps top env (PEq _ _ _ l r)
1412 = do (decls, ns) <- get
1413 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1414 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1415 imps top env (PRewrite _ 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 (PTyped l r)
1420 = imps top env l
1421 imps top env (PPair _ _ l r)
1422 = do (decls, ns) <- get
1423 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1424 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1425 imps top env (PDPair _ _ (PRef _ n) t r)
1426 = do (decls, ns) <- get
1427 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1428 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1429 imps top env (PDPair _ _ l t r)
1430 = do (decls, ns) <- get
1431 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1432 namesIn uvars ist r
1433 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1434 imps top env (PAlternative a as)
1435 = do (decls, ns) <- get
1436 let isn = concatMap (namesIn uvars ist) as
1437 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1438 imps top env (PLam fc n ty sc)
1439 = do imps False env ty
1440 imps False (n:env) sc
1441 imps top env (PHidden tm) = imps False env tm
1442 imps top env (PUnifyLog tm) = imps False env tm
1443 imps top env (PNoImplicits tm) = imps False env tm
1444 imps top env _ = return ()
1446 pibind using [] sc = sc
1447 pibind using (n:ns) sc
1448 = case lookup n using of
1449 Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1450 Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1451 (pibind using ns sc)
1453-- Add implicit arguments in function calls
1454addImplPat :: IState -> PTerm -> PTerm
1455addImplPat = addImpl' True [] []
1457addImplBound :: IState -> [Name] -> PTerm -> PTerm
1458addImplBound ist ns = addImpl' False ns [] ist
1460addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1461addImplBoundInf ist ns inf = addImpl' False ns inf ist
1463-- | Add the implicit arguments to applications in the term
1464addImpl :: IState -> PTerm -> PTerm
1465addImpl = addImpl' False [] []
1467-- TODO: in patterns, don't add implicits to function names guarded by constructors
1468-- and *not* inside a PHidden
1470addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1471addImpl' inpat env infns ist ptm
1472 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1473 where
1474 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1475 ai qq env ds (PRef fc f)
1476 | f `elem` infns = PInferRef fc f
1477 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1478 ai qq env ds (PHidden (PRef fc f))
1479 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
1480 ai qq env ds (PEq fc lt rt l r)
1481 = let lt' = ai qq env ds lt
1482 rt' = ai qq env ds rt
1483 l' = ai qq env ds l
1484 r' = ai qq env ds r in
1485 PEq fc lt' rt' l' r'
1486 ai qq env ds (PRewrite fc l r g)
1487 = let l' = ai qq env ds l
1488 r' = ai qq env ds r
1489 g' = fmap (ai qq env ds) g in
1490 PRewrite fc l' r' g'
1491 ai qq env ds (PTyped l r)
1492 = let l' = ai qq env ds l
1493 r' = ai qq env ds r in
1494 PTyped l' r'
1495 ai qq env ds (PPair fc p l r)
1496 = let l' = ai qq env ds l
1497 r' = ai qq env ds r in
1498 PPair fc p l' r'
1499 ai qq env ds (PDPair fc p l t r)
1500 = let l' = ai qq env ds l
1501 t' = ai qq env ds t
1502 r' = ai qq env ds r in
1503 PDPair fc p l' t' r'
1504 ai qq env ds (PAlternative a as)
1505 = let as' = map (ai qq env ds) as in
1506 PAlternative a as'
1507 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1508 ai qq env ds (PApp fc (PInferRef _ f) as)
1509 = let as' = map (fmap (ai qq env ds)) as in
1510 PApp fc (PInferRef fc f) as'
1511 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1512 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1513 | not (f `elem` map fst env)
1514 = let as' = map (fmap (ai qq env ds)) as in
1515 handleErr $ aiFn inpat False qq ist fc f ds as'
1516 | Just (Just ty) <- lookup f env =
1517 let as' = map (fmap (ai qq env ds)) as
1518 arity = getPArity ty in
1519 mkPApp fc arity ftm as'
1520 ai qq env ds (PApp fc f as)
1521 = let f' = ai qq env ds f
1522 as' = map (fmap (ai qq env ds)) as in
1523 mkPApp fc 1 f' as'
1524 ai qq env ds (PCase fc c os)
1525 = let c' = ai qq env ds c in
1526 -- leave os alone, because they get lifted into a new pattern match
1527 -- definition which is passed through addImpl again with more scope
1528 -- information
1529 PCase fc c' os
1530 -- If the name in a lambda is a constructor name, do this as a 'case'
1531 -- instead (it is harmless to do so, especially since the lambda will
1532 -- be lifted anyway!)
1533 ai qq env ds (PLam fc n ty sc)
1534 = case lookupDef n (tt_ctxt ist) of
1535 [] -> let ty' = ai qq env ds ty
1536 sc' = ai qq ((n, Just ty):env) ds sc in
1537 PLam fc n ty' sc'
1538 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1539 (PCase fc (PRef fc (sMN 0 "lamp") )
1540 [(PRef fc n, sc)]))
1541 ai qq env ds (PLet fc n ty val sc)
1542 = case lookupDef n (tt_ctxt ist) of
1543 [] -> let ty' = ai qq env ds ty
1544 val' = ai qq env ds val
1545 sc' = ai qq ((n, Just ty):env) ds sc in
1546 PLet fc n ty' val' sc'
1547 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1548 ai qq env ds (PPi p n ty sc)
1549 = let ty' = ai qq env ds ty
1550 sc' = ai qq ((n, Just ty):env) ds sc in
1551 PPi p n ty' sc'
1552 ai qq env ds (PGoal fc r n sc)
1553 = let r' = ai qq env ds r
1554 sc' = ai qq ((n, Nothing):env) ds sc in
1555 PGoal fc r' n sc'
1556 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1557 -- Don't do PProof or PTactics since implicits get added when scope is
1558 -- properly known in ElabTerm.runTac
1559 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1560 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1561 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1562 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1563 (fmap (ai True env ds) g)
1564 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1565 ai qq env ds tm = tm
1567 handleErr (Left err) = PElabError err
1568 handleErr (Right x) = x
1570-- if in a pattern, and there are no arguments, and there's no possible
1571-- names with zero explicit arguments, don't add implicits.
1573aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1574aiFn inpat True qq ist fc f ds []
1575 = case lookupDef f (tt_ctxt ist) of
1576 [] -> Right $ PPatvar fc f
1577 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1578 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1579 if (not (vname f) || tcname f
1580 || any (conCaf (tt_ctxt ist)) ialts)
1581-- any constructor alts || any allImp ialts))
1582 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1583 else Right $ PPatvar fc f
1584 where imp (PExp _ _ _ _) = False
1585 imp _ = True
1586-- allImp [] = False
1587 allImp xs = all imp xs
1588 constructor (TyDecl (DCon _ _ _) _) = True
1589 constructor _ = False
1591 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1593 vname (UN n) = True -- non qualified
1594 vname _ = False
1596aiFn inpat expat qq ist fc f ds as
1597 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1598aiFn inpat expat qq ist fc f ds as
1599 -- This is where namespaces get resolved by adding PAlternative
1600 = do let ns = lookupCtxtName f (idris_implicits ist)
1601 let nh = filter (\(n, _) -> notHidden n) ns
1602 let ns' = case trimAlts ds nh of
1603 [] -> nh
1604 x -> x
1605 case ns' of
1606 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1607 [] -> if f `elem` (map fst (idris_metavars ist))
1608 then Right $ PApp fc (PRef fc f) as
1609 else Right $ mkPApp fc (length as) (PRef fc f) as
1610 alts -> Right $
1611 PAlternative True $
1612 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1613 (insertImpl ns as)) alts
1614 where
1615 trimAlts [] alts = alts
1616 trimAlts ns alts
1617 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1619 nspace (NS _ s) = s
1620 nspace _ = []
1622 notHidden n = case getAccessibility n of
1623 Hidden -> False
1624 _ -> True
1626 getAccessibility n
1627 = case lookupDefAccExact n False (tt_ctxt ist) of
1628 Just (n,t) -> t
1629 _ -> Public
1631 insertImpl :: [PArg] -> [PArg] -> [PArg]
1632 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1634 exp (PExp _ _ _ _) = True
1635 exp (PConstraint _ _ _ _) = True
1636 exp _ = False
1638 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1639 -> [PArg] -- parameters
1640 -> [PArg] -- explicit arguments
1641 -> [PArg] -- implicits given
1642 -> [PArg]
1643 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1644 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1645 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1646 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1647 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1648 let rtc = PResolveTC fc in
1649 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1650 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1651 case find n imps [] of
1652 Just (tm, imps') ->
1653 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1654 Nothing ->
1655 PImp p True l n Placeholder :
1656 insImpAcc (M.insert n Placeholder pnas) ps given imps
1657 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1658 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1659 case find n imps [] of
1660 Just (tm, imps') ->
1661 PTacImplicit p l n sc tm :
1662 insImpAcc (M.insert n tm pnas) ps given imps'
1663 Nothing ->
1664 if inpat
1665 then PTacImplicit p l n sc Placeholder :
1666 insImpAcc (M.insert n Placeholder pnas) ps given imps
1667 else PTacImplicit p l n sc sc :
1668 insImpAcc (M.insert n sc pnas) ps given imps
1669 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1670 -- TODO: report here, and prune alternatives
1671 -- Issue #1740 in the Issue Tracker
1672-- https://github.com/idris-lang/Idris-dev/issues/1740
1673 insImpAcc _ _ given imps = given ++ imps
1675 find n [] acc = Nothing
1676 find n (PImp _ _ _ n' t : gs) acc
1677 | n == n' = Just (t, reverse acc ++ gs)
1678 find n (PTacImplicit _ _ n' _ t : gs) acc
1679 | n == n' = Just (t, reverse acc ++ gs)
1680 find n (g : gs) acc = find n gs (g : acc)
1682-- replace non-linear occurrences with _
1684stripLinear :: IState -> PTerm -> PTerm
1685stripLinear i tm = evalState (sl tm) [] where
1686 sl :: PTerm -> State [Name] PTerm
1687 sl (PRef fc f)
1688 | (_:_) <- lookupTy f (tt_ctxt i)
1689 = return $ PRef fc f
1690 | otherwise = do ns <- get
1691 if (f `elem` ns)
1692 then return $ PHidden (PRef fc f) -- Placeholder
1693 else do put (f : ns)
1694 return (PRef fc f)
1695 sl (PPatvar fc f)
1696 = do ns <- get
1697 if (f `elem` ns)
1698 then return $ PHidden (PPatvar fc f) -- Placeholder
1699 else do put (f : ns)
1700 return (PPatvar fc f)
1701 -- Assumption is that variables are all the same in each alternative
1702 sl t@(PAlternative b as) = do ns <- get
1703 as' <- slAlts ns as
1704 return (PAlternative b as')
1705 where slAlts ns (a : as) = do put ns
1706 a' <- sl a
1707 as' <- slAlts ns as
1708 return (a' : as')
1709 slAlts ns [] = return []
1710 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1711 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1712 args' <- mapM slA args
1713 return $ PApp fc fn args'
1714 where slA (PImp p m l n t) = do t' <- sl t
1715 return $ PImp p m l n t'
1716 slA (PExp p l n t) = do t' <- sl t
1717 return $ PExp p l n t'
1718 slA (PConstraint p l n t)
1719 = do t' <- sl t
1720 return $ PConstraint p l n t'
1721 slA (PTacImplicit p l n sc t)
1722 = do t' <- sl t
1723 return $ PTacImplicit p l n sc t'
1724 sl x = return x
1726-- Remove functions which aren't applied to anything, which must then
1727-- be resolved by unification. Assume names resolved and alternatives
1728-- filled in (so no ambiguity).
1730stripUnmatchable :: IState -> PTerm -> PTerm
1731stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1732 su :: PTerm -> PTerm
1733 su (PRef fc f)
1734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1735 = Placeholder
1736 su (PApp fc f@(PRef _ fn) args)
1737 | isDConName fn ctxt
1738 = PApp fc f (fmap (fmap su) args)
1739 su (PApp fc f args)
1740 = PHidden (PApp fc f args)
1741 su (PAlternative b alts)
1742 = let alts' = filter (/= Placeholder) (map su alts) in
1743 if null alts' then Placeholder
1744 else PAlternative b alts'
1745 su (PPair fc p l r) = PPair fc p (su l) (su r)
1746 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1747 su t@(PLam fc _ _ _) = PHidden t
1748 su t@(PPi _ _ _ _) = PHidden t
1749 su t@(PEq _ _ _ _ _) = PHidden t
1750 su t = t
1752 ctxt = tt_ctxt i
1754stripUnmatchable i tm = tm
1756mkPApp fc a f [] = f
1757mkPApp fc a f as = let rest = drop a as in
1758 appRest fc (PApp fc f (take a as)) rest
1759 where
1760 appRest fc f [] = f
1761 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1763-- Find 'static' argument positions
1764-- (the declared ones, plus any names in argument position in the declared
1765-- statics)
1766-- FIXME: It's possible that this really has to happen after elaboration
1768findStatics :: IState -> PTerm -> (PTerm, [Bool])
1769findStatics ist tm = trace (show tm) $
1770 let (ns, ss) = fs tm in
1771 runState (pos ns ss tm) []
1772 where fs (PPi p n t sc)
1773 | Static <- pstatic p
1774 = let (ns, ss) = fs sc in
1775 (namesIn [] ist t : ns, n : ss)
1776 | otherwise = let (ns, ss) = fs sc in
1777 (ns, ss)
1778 fs _ = ([], [])
1780 inOne n ns = length (filter id (map (elem n) ns)) == 1
1782 pos ns ss (PPi p n t sc)
1783 | elem n ss = do sc' <- pos ns ss sc
1784 spos <- get
1785 put (True : spos)
1786 return (PPi (p { pstatic = Static }) n t sc')
1787 | otherwise = do sc' <- pos ns ss sc
1788 spos <- get
1789 put (False : spos)
1790 return (PPi p n t sc')
1791 pos ns ss t = return t
1793-- for 6.12/7 compatibility
1794data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1796instance Applicative (EitherErr a) where
1797 pure = return
1798 (<*>) = ap
1800instance Monad (EitherErr a) where
1801 return = RightOK
1803 (LeftErr e) >>= k = LeftErr e
1804 RightOK v >>= k = k v
1806toEither (LeftErr e) = Left e
1807toEither (RightOK ho) = Right ho
1809-- syntactic match of a against b, returning pair of variables in a
1810-- and what they match. Returns the pair that failed if not a match.
1812matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1813matchClause = matchClause' False
1815matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1816matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1817 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1819 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1820 fullApp x = x
1822 match' x y = match (fullApp x) (fullApp y)
1823 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1824 | fi == txt "fromInteger" && b == txt "builtins",
1825 PConstant (I _) <- getTm x = match (getTm x) x'
1826 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1827 | fi == txt "fromInteger" && b == txt "builtins",
1828 PConstant (I _) <- getTm x = match (getTm x) x'
1829 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1830 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1831 match (PApp _ f args) (PApp _ f' args')
1832 | length args == length args'
1833 = do mf <- match' f f'
1834 ms <- zipWithM matchArg args args'
1835 return (mf ++ concat ms)
1836 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1837 match (PPatvar f n) xr = match (PRef f n) xr
1838 match xr (PPatvar f n) = match xr (PRef f n)
1839 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1840 match (PRef _ n) tm@(PRef _ n')
1841 | n == n' && not names &&
1842 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1843 || tm == Placeholder)
1844 = return [(n, tm)]
1845 -- if one namespace is missing, drop the other
1846 | n == n' || n == dropNS n' || dropNS n == n' = return []
1847 where dropNS (NS n _) = n
1848 dropNS n = n
1849 match (PRef _ n) tm
1850 | not names && (not (isConName n (tt_ctxt i) ||
1851 isFnName n (tt_ctxt i)) || tm == Placeholder)
1852 = return [(n, tm)]
1853 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1854 = do ml <- match' l l'
1855 mr <- match' r r'
1856 return (ml ++ mr)
1857 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1858 = do ml <- match' l l'
1859 mr <- match' r r'
1860 return (ml ++ mr)
1861 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1862 mr <- match r r'
1863 return (ml ++ mr)
1864 match (PTyped l r) x = match l x
1865 match x (PTyped l r) = match x l
1866 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1867 mr <- match' r r'
1868 return (ml ++ mr)
1869 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1870 mt <- match' t t'
1871 mr <- match' r r'
1872 return (ml ++ mt ++ mr)
1873 match (PAlternative a as) (PAlternative a' as')
1874 = do ms <- zipWithM match' as as'
1875 return (concat ms)
1876 match a@(PAlternative _ as) b
1877 = do let ms = zipWith match' as (repeat b)
1878 case (rights (map toEither ms)) of
1879 (x: _) -> return x
1880 _ -> LeftErr (a, b)
1881 match (PCase _ _ _) _ = return [] -- lifted out
1882 match (PMetavar _) _ = return [] -- modified
1883 match (PInferRef _ _) _ = return [] -- modified
1884 match (PQuote _) _ = return []
1885 match (PProof _) _ = return []
1886 match (PTactics _) _ = return []
1887 match (PRefl _ _) (PRefl _ _) = return []
1888 match (PResolveTC _) (PResolveTC _) = return []
1889 match (PTrue _ _) (PTrue _ _) = return []
1890 match (PReturn _) (PReturn _) = return []
1891 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1892 ms <- match' s s'
1893 return (mt ++ ms)
1894 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1895 ms <- match' s s'
1896 return (mt ++ ms)
1897 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1898 mty <- match' ty ty'
1899 ms <- match' s s'
1900 return (mt ++ mty ++ ms)
1901 match (PHidden x) (PHidden y)
1902 | RightOK xs <- match x y = return xs -- to collect variables
1903 | otherwise = return [] -- Otherwise hidden things are unmatchable
1904 match (PHidden x) y
1905 | RightOK xs <- match x y = return xs
1906 | otherwise = return []
1907 match x (PHidden y)
1908 | RightOK xs <- match x y = return xs
1909 | otherwise = return []
1910 match (PUnifyLog x) y = match' x y
1911 match x (PUnifyLog y) = match' x y
1912 match (PNoImplicits x) y = match' x y
1913 match x (PNoImplicits y) = match' x y
1914 match Placeholder _ = return []
1915 match _ Placeholder = return []
1916 match (PResolveTC _) _ = return []
1917 match a b | a == b = return []
1918 | otherwise = LeftErr (a, b)
1920 checkRpts (RightOK ms) = check ms where
1921 check ((n,t):xs)
1922 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1923 then Left (t, t')
1924 else check xs
1925 check (_:xs) = check xs
1926 check [] = Right ms
1927 checkRpts (LeftErr x) = Left x
1929substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1930substMatches ms = substMatchesShadow ms []
1932substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1933substMatchesShadow [] shs t = t
1934substMatchesShadow ((n,tm):ns) shs t
1935 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1937substMatch :: Name -> PTerm -> PTerm -> PTerm
1938substMatch n = substMatchShadow n []
1940substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1941substMatchShadow n shs tm t = sm shs t where
1942 sm xs (PRef _ n') | n == n' = tm
1943 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1944 sm xs (PPi p x t sc)
1945 | x `elem` xs
1946 = let x' = nextName x in
1947 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1948 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1949 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1950 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1951 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1952 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1953 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1954 (fmap (sm xs) tm)
1955 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1956 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1957 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1958 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1959 sm xs (PHidden x) = PHidden (sm xs x)
1960 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1961 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1962 sm xs x = x
1964 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1965 fullApp x = x
1967shadow :: Name -> Name -> PTerm -> PTerm
1968shadow n n' t = sm t where
1969 sm (PRef fc x) | n == x = PRef fc n'
1970 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
1971 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1972 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
1973 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1974 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1975 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1976 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1977 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1978 sm (PTyped x y) = PTyped (sm x) (sm y)
1979 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1980 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1981 sm (PAlternative a as) = PAlternative a (map sm as)
1982 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1983 sm (PProof ts) = PProof (map (fmap sm) ts)
1984 sm (PHidden x) = PHidden (sm x)
1985 sm (PUnifyLog x) = PUnifyLog (sm x)
1986 sm (PNoImplicits x) = PNoImplicits (sm x)
1987 sm x = x
1989-- Rename any binders which are repeated (so that we don't have to mess
1990-- about with shadowing anywhere else).
1992mkUniqueNames :: [Name] -> PTerm -> PTerm
1993mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
1994 inScope :: S.Set Name
1995 inScope = S.fromList $ boundNamesIn tm
1997 mkUniqA arg = do t' <- mkUniq (getTm arg)
1998 return (arg { getTm = t' })
2000 -- Initialise the unique name with the environment length (so we're not
2001 -- looking for too long...)
2002 initN (UN n) l = UN $ txt (str n ++ show l)
2003 initN (MN i s) l = MN (i+l) s
2004 initN n l = n
2006 -- FIXME: Probably ought to do this for completeness! It's fine as
2007 -- long as there are no bindings inside tactics though.
2008 mkUniqT tac = return tac
2010 mkUniq :: PTerm -> State (S.Set Name) PTerm
2011 mkUniq (PLam fc n ty sc)
2012 = do env <- get
2013 (n', sc') <-
2014 if n `S.member` env
2015 then do let n' = uniqueNameSet (initN n (S.size env))
2016 (S.union env inScope)
2017 return (n', shadow n n' sc)
2018 else return (n, sc)
2019 put (S.insert n' env)
2020 ty' <- mkUniq ty
2021 sc'' <- mkUniq sc'
2022 return $! PLam fc n' ty' sc''
2023 mkUniq (PPi p n ty sc)
2024 = do env <- get
2025 (n', sc') <-
2026 if n `S.member` env
2027 then do let n' = uniqueNameSet (initN n (S.size env))
2028 (S.union env inScope)
2029 return (n', shadow n n' sc)
2030 else return (n, sc)
2031 put (S.insert n' env)
2032 ty' <- mkUniq ty
2033 sc'' <- mkUniq sc'
2034 return $! PPi p n' ty' sc''
2035 mkUniq (PLet fc n ty val sc)
2036 = do env <- get
2037 (n', sc') <-
2038 if n `S.member` env
2039 then do let n' = uniqueNameSet (initN n (S.size env))
2040 (S.union env inScope)
2041 return (n', shadow n n' sc)
2042 else return (n, sc)
2043 put (S.insert n' env)
2044 ty' <- mkUniq ty; val' <- mkUniq val
2045 sc'' <- mkUniq sc'
2046 return $! PLet fc n' ty' val' sc''
2047 mkUniq (PApp fc t args)
2048 = do t' <- mkUniq t
2049 args' <- mapM mkUniqA args
2050 return $! PApp fc t' args'
2051 mkUniq (PAppBind fc t args)
2052 = do t' <- mkUniq t
2053 args' <- mapM mkUniqA args
2054 return $! PAppBind fc t' args'
2055 mkUniq (PCase fc t alts)
2056 = do t' <- mkUniq t
2057 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2058 return (x', y')) alts
2059 return $! PCase fc t' alts'
2060 mkUniq (PPair fc p l r)
2061 = do l' <- mkUniq l; r' <- mkUniq r
2062 return $! PPair fc p l' r'
2063 mkUniq (PDPair fc p (PRef fc' n) t sc)
2064 | t /= Placeholder
2065 = do env <- get
2066 (n', sc') <- if n `S.member` env
2067 then do let n' = uniqueNameSet n (S.union env inScope)
2068 return (n', shadow n n' sc)
2069 else return (n, sc)
2070 put (S.insert n' env)
2071 t' <- mkUniq t
2072 sc'' <- mkUniq sc'
2073 return $! PDPair fc p (PRef fc' n') t' sc''
2074 mkUniq (PDPair fc p l t r)
2075 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2076 return $! PDPair fc p l' t' r'
2077 mkUniq (PAlternative b as)
2078 = liftM (PAlternative b) (mapM mkUniq as)
2079 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2080 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2081 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2082 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2083 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2084 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2085 mkUniq t = return t