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