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