git.iko.soy/Idris-dev
on aef8dc1 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2066 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 Nothing) 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 Nothing) 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 (Just _) _ _) sc) imps = getImps sc imps
1269 getImps (Bind n (Pi _ t _) sc) imps
1270 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1271 where
1272 argInfo n (Imp opt _ _ _) t'
1273 = (True, PImp (getPriority i t') True opt n t')
1274 argInfo n (Exp opt _ _) t'
1275 = (InaccessibleArg `elem` opt,
1276 PExp (getPriority i t') opt n t')
1277 argInfo n (Constraint opt _) t'
1278 = (InaccessibleArg `elem` opt,
1279 PConstraint 10 opt n t')
1280 argInfo n (TacImp opt _ scr) t'
1281 = (InaccessibleArg `elem` opt,
1282 PTacImplicit 10 opt n scr t')
1283 getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
1284 where impBind n t = (True, PImp 1 True [] n Placeholder)
1285 getImps sc tm = []
1287-- Add implicit Pi bindings for any names in the term which appear in an
1288-- argument position.
1290-- This has become a right mess already. Better redo it some time...
1291-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1292-- a couple of places which use it. Clean them up!
1294-- Issue 1739 in the issue tracker
1295-- https://github.com/idris-lang/Idris-dev/issues/1739
1296implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1297implicit info syn n ptm = implicit' info syn [] n ptm
1299implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1300implicit' info syn ignore n ptm
1301 = do i <- getIState
1302 let (tm', impdata) = implicitise syn ignore i ptm
1303 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1304-- let (tm'', spos) = findStatics i tm'
1305 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1306 addIBC (IBCImp n)
1307 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1308-- i <- get
1309-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1310 return tm'
1311 where
1312 -- Detect unknown names in default arguments and throw error if found.
1313 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1314 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1316 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1317 notFoundInDefault kns (PTacImplicit _ _ n script _)
1318 = do i <- getIState
1319 case notFound kns (namesIn [] i script) of
1320 Nothing -> return (n:kns)
1321 Just name -> throwError (NoSuchVariable name)
1322 notFoundInDefault kns p = return ((pname p):kns)
1324 notFound :: [Name] -> [Name] -> Maybe Name
1325 notFound kns [] = Nothing
1326 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1327 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1329implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1330implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1331 let (declimps, ns') = execState (imps True [] tm) ([], [])
1332 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1333 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1334 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1335 if null ns
1336 then (tm, reverse declimps)
1337 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1338 where
1339 uvars = map ipair (filter uimplicit (using syn))
1340 pvars = syn_params syn
1342 inUsing n = n `elem` map fst uvars
1344 ipair (UImplicit x y) = (x, y)
1345 uimplicit (UImplicit _ _) = True
1346 uimplicit _ = False
1348 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1349 | otherwise = x : dropAll xs ys
1350 dropAll [] ys = []
1352 -- Find names in argument position in a type, suitable for implicit
1353 -- binding
1354 -- Not the function position, but do everything else...
1355 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1356 implNamesIn uv t = namesIn uv ist t
1358 imps top env (PApp _ f as)
1359 = do (decls, ns) <- get
1360 let isn = concatMap (namesIn uvars ist) (map getTm as)
1361 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1362 imps top env (PPi (Imp l _ _ _) n ty sc)
1363 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1364 (decls , ns) <- get
1365 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1366 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1367 imps True (n:env) sc
1368 imps top env (PPi (Exp l _ _) n ty sc)
1369 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1370 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1371 _ -> [])
1372 (decls, ns) <- get -- ignore decls in HO types
1373 put (PExp (getPriority ist ty) l n Placeholder : decls,
1374 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1375 imps True (n:env) sc
1376 imps top env (PPi (Constraint l _) n ty sc)
1377 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1378 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1379 _ -> [])
1380 (decls, ns) <- get -- ignore decls in HO types
1381 put (PConstraint 10 l n Placeholder : decls,
1382 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1383 imps True (n:env) sc
1384 imps top env (PPi (TacImp l _ scr) n ty sc)
1385 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1386 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1387 _ -> [])
1388 (decls, ns) <- get -- ignore decls in HO types
1389 put (PTacImplicit 10 l n scr Placeholder : decls,
1390 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1391 imps True (n:env) sc
1392 imps top env (PEq _ _ _ l r)
1393 = do (decls, ns) <- get
1394 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1395 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1396 imps top env (PRewrite _ l r _)
1397 = do (decls, ns) <- get
1398 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1399 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1400 imps top env (PTyped l r)
1401 = imps top env l
1402 imps top env (PPair _ _ l r)
1403 = do (decls, ns) <- get
1404 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1405 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1406 imps top env (PDPair _ _ (PRef _ n) t r)
1407 = do (decls, ns) <- get
1408 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1409 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1410 imps top env (PDPair _ _ l t r)
1411 = do (decls, ns) <- get
1412 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1413 namesIn uvars ist r
1414 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1415 imps top env (PAlternative a as)
1416 = do (decls, ns) <- get
1417 let isn = concatMap (namesIn uvars ist) as
1418 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1419 imps top env (PLam fc n ty sc)
1420 = do imps False env ty
1421 imps False (n:env) sc
1422 imps top env (PHidden tm) = imps False env tm
1423 imps top env (PUnifyLog tm) = imps False env tm
1424 imps top env (PNoImplicits tm) = imps False env tm
1425 imps top env _ = return ()
1427 pibind using [] sc = sc
1428 pibind using (n:ns) sc
1429 = case lookup n using of
1430 Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1431 Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1432 (pibind using ns sc)
1434-- Add implicit arguments in function calls
1435addImplPat :: IState -> PTerm -> PTerm
1436addImplPat = addImpl' True [] []
1438addImplBound :: IState -> [Name] -> PTerm -> PTerm
1439addImplBound ist ns = addImpl' False ns [] ist
1441addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1442addImplBoundInf ist ns inf = addImpl' False ns inf ist
1444-- | Add the implicit arguments to applications in the term
1445addImpl :: IState -> PTerm -> PTerm
1446addImpl = addImpl' False [] []
1448-- TODO: in patterns, don't add implicits to function names guarded by constructors
1449-- and *not* inside a PHidden
1451addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1452addImpl' inpat env infns ist ptm
1453 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1454 where
1455 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1456 ai qq env ds (PRef fc f)
1457 | f `elem` infns = PInferRef fc f
1458 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1459 ai qq env ds (PHidden (PRef fc f))
1460 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
1461 ai qq env ds (PEq fc lt rt l r)
1462 = let lt' = ai qq env ds lt
1463 rt' = ai qq env ds rt
1464 l' = ai qq env ds l
1465 r' = ai qq env ds r in
1466 PEq fc lt' rt' l' r'
1467 ai qq env ds (PRewrite fc l r g)
1468 = let l' = ai qq env ds l
1469 r' = ai qq env ds r
1470 g' = fmap (ai qq env ds) g in
1471 PRewrite fc l' r' g'
1472 ai qq env ds (PTyped l r)
1473 = let l' = ai qq env ds l
1474 r' = ai qq env ds r in
1475 PTyped l' r'
1476 ai qq env ds (PPair fc p l r)
1477 = let l' = ai qq env ds l
1478 r' = ai qq env ds r in
1479 PPair fc p l' r'
1480 ai qq env ds (PDPair fc p l t r)
1481 = let l' = ai qq env ds l
1482 t' = ai qq env ds t
1483 r' = ai qq env ds r in
1484 PDPair fc p l' t' r'
1485 ai qq env ds (PAlternative a as)
1486 = let as' = map (ai qq env ds) as in
1487 PAlternative a as'
1488 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1489 ai qq env ds (PApp fc (PInferRef _ f) as)
1490 = let as' = map (fmap (ai qq env ds)) as in
1491 PApp fc (PInferRef fc f) as'
1492 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1493 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1494 | not (f `elem` map fst env)
1495 = let as' = map (fmap (ai qq env ds)) as in
1496 handleErr $ aiFn inpat False qq ist fc f ds as'
1497 | Just (Just ty) <- lookup f env =
1498 let as' = map (fmap (ai qq env ds)) as
1499 arity = getPArity ty in
1500 mkPApp fc arity ftm as'
1501 ai qq env ds (PApp fc f as)
1502 = let f' = ai qq env ds f
1503 as' = map (fmap (ai qq env ds)) as in
1504 mkPApp fc 1 f' as'
1505 ai qq env ds (PCase fc c os)
1506 = let c' = ai qq env ds c in
1507 -- leave os alone, because they get lifted into a new pattern match
1508 -- definition which is passed through addImpl again with more scope
1509 -- information
1510 PCase fc c' os
1511 -- If the name in a lambda is a constructor name, do this as a 'case'
1512 -- instead (it is harmless to do so, especially since the lambda will
1513 -- be lifted anyway!)
1514 ai qq env ds (PLam fc n ty sc)
1515 = case lookupDef n (tt_ctxt ist) of
1516 [] -> let ty' = ai qq env ds ty
1517 sc' = ai qq ((n, Just ty):env) ds sc in
1518 PLam fc n ty' sc'
1519 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1520 (PCase fc (PRef fc (sMN 0 "lamp") )
1521 [(PRef fc n, sc)]))
1522 ai qq env ds (PLet fc n ty val sc)
1523 = case lookupDef n (tt_ctxt ist) of
1524 [] -> let ty' = ai qq env ds ty
1525 val' = ai qq env ds val
1526 sc' = ai qq ((n, Just ty):env) ds sc in
1527 PLet fc n ty' val' sc'
1528 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1529 ai qq env ds (PPi p n ty sc)
1530 = let ty' = ai qq env ds ty
1531 sc' = ai qq ((n, Just ty):env) ds sc in
1532 PPi p n ty' sc'
1533 ai qq env ds (PGoal fc r n sc)
1534 = let r' = ai qq env ds r
1535 sc' = ai qq ((n, Nothing):env) ds sc in
1536 PGoal fc r' n sc'
1537 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1538 -- Don't do PProof or PTactics since implicits get added when scope is
1539 -- properly known in ElabTerm.runTac
1540 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1541 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1542 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1543 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1544 (fmap (ai True env ds) g)
1545 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1546 ai qq env ds tm = tm
1548 handleErr (Left err) = PElabError err
1549 handleErr (Right x) = x
1551-- if in a pattern, and there are no arguments, and there's no possible
1552-- names with zero explicit arguments, don't add implicits.
1554aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1555aiFn inpat True qq ist fc f ds []
1556 = case lookupDef f (tt_ctxt ist) of
1557 [] -> Right $ PPatvar fc f
1558 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1559 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1560 if (not (vname f) || tcname f
1561 || any (conCaf (tt_ctxt ist)) ialts)
1562-- any constructor alts || any allImp ialts))
1563 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1564 else Right $ PPatvar fc f
1565 where imp (PExp _ _ _ _) = False
1566 imp _ = True
1567-- allImp [] = False
1568 allImp xs = all imp xs
1569 constructor (TyDecl (DCon _ _ _) _) = True
1570 constructor _ = False
1572 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1574 vname (UN n) = True -- non qualified
1575 vname _ = False
1577aiFn inpat expat qq ist fc f ds as
1578 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1579aiFn inpat expat qq ist fc f ds as
1580 -- This is where namespaces get resolved by adding PAlternative
1581 = do let ns = lookupCtxtName f (idris_implicits ist)
1582 let nh = filter (\(n, _) -> notHidden n) ns
1583 let ns' = case trimAlts ds nh of
1584 [] -> nh
1585 x -> x
1586 case ns' of
1587 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1588 [] -> if f `elem` (map fst (idris_metavars ist))
1589 then Right $ PApp fc (PRef fc f) as
1590 else Right $ mkPApp fc (length as) (PRef fc f) as
1591 alts -> Right $
1592 PAlternative True $
1593 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1594 (insertImpl ns as)) alts
1595 where
1596 trimAlts [] alts = alts
1597 trimAlts ns alts
1598 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1600 nspace (NS _ s) = s
1601 nspace _ = []
1603 notHidden n = case getAccessibility n of
1604 Hidden -> False
1605 _ -> True
1607 getAccessibility n
1608 = case lookupDefAccExact n False (tt_ctxt ist) of
1609 Just (n,t) -> t
1610 _ -> Public
1612 insertImpl :: [PArg] -> [PArg] -> [PArg]
1613 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1615 exp (PExp _ _ _ _) = True
1616 exp (PConstraint _ _ _ _) = True
1617 exp _ = False
1619 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1620 -> [PArg] -- parameters
1621 -> [PArg] -- explicit arguments
1622 -> [PArg] -- implicits given
1623 -> [PArg]
1624 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1625 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1626 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1627 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1628 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1629 let rtc = PResolveTC fc in
1630 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1631 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1632 case find n imps [] of
1633 Just (tm, imps') ->
1634 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1635 Nothing ->
1636 PImp p True l n Placeholder :
1637 insImpAcc (M.insert n Placeholder pnas) ps given imps
1638 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1639 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1640 case find n imps [] of
1641 Just (tm, imps') ->
1642 PTacImplicit p l n sc tm :
1643 insImpAcc (M.insert n tm pnas) ps given imps'
1644 Nothing ->
1645 if inpat
1646 then PTacImplicit p l n sc Placeholder :
1647 insImpAcc (M.insert n Placeholder pnas) ps given imps
1648 else PTacImplicit p l n sc sc :
1649 insImpAcc (M.insert n sc pnas) ps given imps
1650 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1651 -- TODO: report here, and prune alternatives
1652 -- Issue #1740 in the Issue Tracker
1653-- https://github.com/idris-lang/Idris-dev/issues/1740
1654 insImpAcc _ _ given imps = given ++ imps
1656 find n [] acc = Nothing
1657 find n (PImp _ _ _ n' t : gs) acc
1658 | n == n' = Just (t, reverse acc ++ gs)
1659 find n (PTacImplicit _ _ n' _ t : gs) acc
1660 | n == n' = Just (t, reverse acc ++ gs)
1661 find n (g : gs) acc = find n gs (g : acc)
1663-- replace non-linear occurrences with _
1665stripLinear :: IState -> PTerm -> PTerm
1666stripLinear i tm = evalState (sl tm) [] where
1667 sl :: PTerm -> State [Name] PTerm
1668 sl (PRef fc f)
1669 | (_:_) <- lookupTy f (tt_ctxt i)
1670 = return $ PRef fc f
1671 | otherwise = do ns <- get
1672 if (f `elem` ns)
1673 then return $ PHidden (PRef fc f) -- Placeholder
1674 else do put (f : ns)
1675 return (PRef fc f)
1676 sl (PPatvar fc f)
1677 = do ns <- get
1678 if (f `elem` ns)
1679 then return $ PHidden (PPatvar fc f) -- Placeholder
1680 else do put (f : ns)
1681 return (PPatvar fc f)
1682 -- Assumption is that variables are all the same in each alternative
1683 sl t@(PAlternative b as) = do ns <- get
1684 as' <- slAlts ns as
1685 return (PAlternative b as')
1686 where slAlts ns (a : as) = do put ns
1687 a' <- sl a
1688 as' <- slAlts ns as
1689 return (a' : as')
1690 slAlts ns [] = return []
1691 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1692 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1693 args' <- mapM slA args
1694 return $ PApp fc fn args'
1695 where slA (PImp p m l n t) = do t' <- sl t
1696 return $ PImp p m l n t'
1697 slA (PExp p l n t) = do t' <- sl t
1698 return $ PExp p l n t'
1699 slA (PConstraint p l n t)
1700 = do t' <- sl t
1701 return $ PConstraint p l n t'
1702 slA (PTacImplicit p l n sc t)
1703 = do t' <- sl t
1704 return $ PTacImplicit p l n sc t'
1705 sl x = return x
1707-- Remove functions which aren't applied to anything, which must then
1708-- be resolved by unification. Assume names resolved and alternatives
1709-- filled in (so no ambiguity).
1711stripUnmatchable :: IState -> PTerm -> PTerm
1712stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1713 su :: PTerm -> PTerm
1714 su (PRef fc f)
1715 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1716 = Placeholder
1717 su (PApp fc f@(PRef _ fn) args)
1718 | isDConName fn ctxt
1719 = PApp fc f (fmap (fmap su) args)
1720 su (PApp fc f args)
1721 = PHidden (PApp fc f args)
1722 su (PAlternative b alts)
1723 = let alts' = filter (/= Placeholder) (map su alts) in
1724 if null alts' then Placeholder
1725 else PAlternative b alts'
1726 su (PPair fc p l r) = PPair fc p (su l) (su r)
1727 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1728 su t@(PLam fc _ _ _) = PHidden t
1729 su t@(PPi _ _ _ _) = PHidden t
1730 su t@(PEq _ _ _ _ _) = PHidden t
1731 su t = t
1733 ctxt = tt_ctxt i
1735stripUnmatchable i tm = tm
1737mkPApp fc a f [] = f
1738mkPApp fc a f as = let rest = drop a as in
1739 appRest fc (PApp fc f (take a as)) rest
1740 where
1741 appRest fc f [] = f
1742 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1744-- Find 'static' argument positions
1745-- (the declared ones, plus any names in argument position in the declared
1746-- statics)
1747-- FIXME: It's possible that this really has to happen after elaboration
1749findStatics :: IState -> PTerm -> (PTerm, [Bool])
1750findStatics ist tm = trace (show tm) $
1751 let (ns, ss) = fs tm in
1752 runState (pos ns ss tm) []
1753 where fs (PPi p n t sc)
1754 | Static <- pstatic p
1755 = let (ns, ss) = fs sc in
1756 (namesIn [] ist t : ns, n : ss)
1757 | otherwise = let (ns, ss) = fs sc in
1758 (ns, ss)
1759 fs _ = ([], [])
1761 inOne n ns = length (filter id (map (elem n) ns)) == 1
1763 pos ns ss (PPi p n t sc)
1764 | elem n ss = do sc' <- pos ns ss sc
1765 spos <- get
1766 put (True : spos)
1767 return (PPi (p { pstatic = Static }) n t sc')
1768 | otherwise = do sc' <- pos ns ss sc
1769 spos <- get
1770 put (False : spos)
1771 return (PPi p n t sc')
1772 pos ns ss t = return t
1774-- for 6.12/7 compatibility
1775data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1777instance Applicative (EitherErr a) where
1778 pure = return
1779 (<*>) = ap
1781instance Monad (EitherErr a) where
1782 return = RightOK
1784 (LeftErr e) >>= k = LeftErr e
1785 RightOK v >>= k = k v
1787toEither (LeftErr e) = Left e
1788toEither (RightOK ho) = Right ho
1790-- syntactic match of a against b, returning pair of variables in a
1791-- and what they match. Returns the pair that failed if not a match.
1793matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1794matchClause = matchClause' False
1796matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1797matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1798 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1800 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1801 fullApp x = x
1803 match' x y = match (fullApp x) (fullApp y)
1804 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1805 | fi == txt "fromInteger" && b == txt "builtins",
1806 PConstant (I _) <- getTm x = match (getTm x) x'
1807 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1808 | fi == txt "fromInteger" && b == txt "builtins",
1809 PConstant (I _) <- getTm x = match (getTm x) x'
1810 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1811 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1812 match (PApp _ f args) (PApp _ f' args')
1813 | length args == length args'
1814 = do mf <- match' f f'
1815 ms <- zipWithM matchArg args args'
1816 return (mf ++ concat ms)
1817 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1818 match (PPatvar f n) xr = match (PRef f n) xr
1819 match xr (PPatvar f n) = match xr (PRef f n)
1820 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1821 match (PRef _ n) tm@(PRef _ n')
1822 | n == n' && not names &&
1823 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1824 || tm == Placeholder)
1825 = return [(n, tm)]
1826 -- if one namespace is missing, drop the other
1827 | n == n' || n == dropNS n' || dropNS n == n' = return []
1828 where dropNS (NS n _) = n
1829 dropNS n = n
1830 match (PRef _ n) tm
1831 | not names && (not (isConName n (tt_ctxt i) ||
1832 isFnName n (tt_ctxt i)) || tm == Placeholder)
1833 = return [(n, tm)]
1834 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1835 = do ml <- match' l l'
1836 mr <- match' r r'
1837 return (ml ++ mr)
1838 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1839 = do ml <- match' l l'
1840 mr <- match' r r'
1841 return (ml ++ mr)
1842 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1843 mr <- match r r'
1844 return (ml ++ mr)
1845 match (PTyped l r) x = match l x
1846 match x (PTyped l r) = match x l
1847 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1848 mr <- match' r r'
1849 return (ml ++ mr)
1850 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1851 mt <- match' t t'
1852 mr <- match' r r'
1853 return (ml ++ mt ++ mr)
1854 match (PAlternative a as) (PAlternative a' as')
1855 = do ms <- zipWithM match' as as'
1856 return (concat ms)
1857 match a@(PAlternative _ as) b
1858 = do let ms = zipWith match' as (repeat b)
1859 case (rights (map toEither ms)) of
1860 (x: _) -> return x
1861 _ -> LeftErr (a, b)
1862 match (PCase _ _ _) _ = return [] -- lifted out
1863 match (PMetavar _) _ = return [] -- modified
1864 match (PInferRef _ _) _ = return [] -- modified
1865 match (PQuote _) _ = return []
1866 match (PProof _) _ = return []
1867 match (PTactics _) _ = return []
1868 match (PRefl _ _) (PRefl _ _) = return []
1869 match (PResolveTC _) (PResolveTC _) = return []
1870 match (PTrue _ _) (PTrue _ _) = return []
1871 match (PReturn _) (PReturn _) = return []
1872 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1873 ms <- match' s s'
1874 return (mt ++ ms)
1875 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1876 ms <- match' s s'
1877 return (mt ++ ms)
1878 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1879 mty <- match' ty ty'
1880 ms <- match' s s'
1881 return (mt ++ mty ++ ms)
1882 match (PHidden x) (PHidden y)
1883 | RightOK xs <- match x y = return xs -- to collect variables
1884 | otherwise = return [] -- Otherwise hidden things are unmatchable
1885 match (PHidden x) y
1886 | RightOK xs <- match x y = return xs
1887 | otherwise = return []
1888 match x (PHidden y)
1889 | RightOK xs <- match x y = return xs
1890 | otherwise = return []
1891 match (PUnifyLog x) y = match' x y
1892 match x (PUnifyLog y) = match' x y
1893 match (PNoImplicits x) y = match' x y
1894 match x (PNoImplicits y) = match' x y
1895 match Placeholder _ = return []
1896 match _ Placeholder = return []
1897 match (PResolveTC _) _ = return []
1898 match a b | a == b = return []
1899 | otherwise = LeftErr (a, b)
1901 checkRpts (RightOK ms) = check ms where
1902 check ((n,t):xs)
1903 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1904 then Left (t, t')
1905 else check xs
1906 check (_:xs) = check xs
1907 check [] = Right ms
1908 checkRpts (LeftErr x) = Left x
1910substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1911substMatches ms = substMatchesShadow ms []
1913substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1914substMatchesShadow [] shs t = t
1915substMatchesShadow ((n,tm):ns) shs t
1916 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1918substMatch :: Name -> PTerm -> PTerm -> PTerm
1919substMatch n = substMatchShadow n []
1921substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1922substMatchShadow n shs tm t = sm shs t where
1923 sm xs (PRef _ n') | n == n' = tm
1924 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1925 sm xs (PPi p x t sc)
1926 | x `elem` xs
1927 = let x' = nextName x in
1928 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1929 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1930 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1931 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1932 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1933 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1934 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1935 (fmap (sm xs) tm)
1936 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1937 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1938 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1939 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1940 sm xs (PHidden x) = PHidden (sm xs x)
1941 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1942 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1943 sm xs x = x
1945 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1946 fullApp x = x
1948shadow :: Name -> Name -> PTerm -> PTerm
1949shadow n n' t = sm t where
1950 sm (PRef fc x) | n == x = PRef fc n'
1951 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
1952 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1953 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
1954 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1955 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1956 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1957 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1958 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1959 sm (PTyped x y) = PTyped (sm x) (sm y)
1960 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1961 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1962 sm (PAlternative a as) = PAlternative a (map sm as)
1963 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1964 sm (PProof ts) = PProof (map (fmap sm) ts)
1965 sm (PHidden x) = PHidden (sm x)
1966 sm (PUnifyLog x) = PUnifyLog (sm x)
1967 sm (PNoImplicits x) = PNoImplicits (sm x)
1968 sm x = x
1970-- Rename any binders which are repeated (so that we don't have to mess
1971-- about with shadowing anywhere else).
1973mkUniqueNames :: [Name] -> PTerm -> PTerm
1974mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
1975 inScope :: S.Set Name
1976 inScope = S.fromList $ boundNamesIn tm
1978 mkUniqA arg = do t' <- mkUniq (getTm arg)
1979 return (arg { getTm = t' })
1981 -- Initialise the unique name with the environment length (so we're not
1982 -- looking for too long...)
1983 initN (UN n) l = UN $ txt (str n ++ show l)
1984 initN (MN i s) l = MN (i+l) s
1985 initN n l = n
1987 -- FIXME: Probably ought to do this for completeness! It's fine as
1988 -- long as there are no bindings inside tactics though.
1989 mkUniqT tac = return tac
1991 mkUniq :: PTerm -> State (S.Set Name) PTerm
1992 mkUniq (PLam fc n ty sc)
1993 = do env <- get
1994 (n', sc') <-
1995 if n `S.member` env
1996 then do let n' = uniqueNameSet (initN n (S.size env))
1997 (S.union env inScope)
1998 return (n', shadow n n' sc)
1999 else return (n, sc)
2000 put (S.insert n' env)
2001 ty' <- mkUniq ty
2002 sc'' <- mkUniq sc'
2003 return $! PLam fc n' ty' sc''
2004 mkUniq (PPi p n ty sc)
2005 = do env <- get
2006 (n', sc') <-
2007 if n `S.member` env
2008 then do let n' = uniqueNameSet (initN n (S.size env))
2009 (S.union env inScope)
2010 return (n', shadow n n' sc)
2011 else return (n, sc)
2012 put (S.insert n' env)
2013 ty' <- mkUniq ty
2014 sc'' <- mkUniq sc'
2015 return $! PPi p n' ty' sc''
2016 mkUniq (PLet fc n ty val sc)
2017 = do env <- get
2018 (n', sc') <-
2019 if n `S.member` env
2020 then do let n' = uniqueNameSet (initN n (S.size env))
2021 (S.union env inScope)
2022 return (n', shadow n n' sc)
2023 else return (n, sc)
2024 put (S.insert n' env)
2025 ty' <- mkUniq ty; val' <- mkUniq val
2026 sc'' <- mkUniq sc'
2027 return $! PLet fc n' ty' val' sc''
2028 mkUniq (PApp fc t args)
2029 = do t' <- mkUniq t
2030 args' <- mapM mkUniqA args
2031 return $! PApp fc t' args'
2032 mkUniq (PAppBind fc t args)
2033 = do t' <- mkUniq t
2034 args' <- mapM mkUniqA args
2035 return $! PAppBind fc t' args'
2036 mkUniq (PCase fc t alts)
2037 = do t' <- mkUniq t
2038 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2039 return (x', y')) alts
2040 return $! PCase fc t' alts'
2041 mkUniq (PPair fc p l r)
2042 = do l' <- mkUniq l; r' <- mkUniq r
2043 return $! PPair fc p l' r'
2044 mkUniq (PDPair fc p (PRef fc' n) t sc)
2045 | t /= Placeholder
2046 = do env <- get
2047 (n', sc') <- if n `S.member` env
2048 then do let n' = uniqueNameSet n (S.union env inScope)
2049 return (n', shadow n n' sc)
2050 else return (n, sc)
2051 put (S.insert n' env)
2052 t' <- mkUniq t
2053 sc'' <- mkUniq sc'
2054 return $! PDPair fc p (PRef fc' n') t' sc''
2055 mkUniq (PDPair fc p l t r)
2056 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2057 return $! PDPair fc p l' t' r'
2058 mkUniq (PAlternative b as)
2059 = liftM (PAlternative b) (mapM mkUniq as)
2060 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2061 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2062 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2063 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2064 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2065 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2066 mkUniq t = return t