git.iko.soy/Idris-dev
on 8fe8bb9 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2057 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))
393getHdrs :: Codegen -> Idris [String]
394getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
396getImported :: Idris [(FilePath, Bool)]
397getImported = do i <- getIState; return (idris_imported i)
399setErrSpan :: FC -> Idris ()
400setErrSpan x = do i <- getIState;
401 case (errSpan i) of
402 Nothing -> putIState $ i { errSpan = Just x }
403 Just _ -> return ()
405clearErr :: Idris ()
406clearErr = do i <- getIState
407 putIState $ i { errSpan = Nothing }
409getSO :: Idris (Maybe String)
410getSO = do i <- getIState
411 return (compiled_so i)
413setSO :: Maybe String -> Idris ()
414setSO s = do i <- getIState
415 putIState $ (i { compiled_so = s })
417getIState :: Idris IState
418getIState = get
420putIState :: IState -> Idris ()
421putIState = put
423withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
424withContext ctx name dflt action = do
425 ist <- getIState
426 case lookupCtxt name (ctx ist) of
427 [x] -> action x
428 _ -> return dflt
430withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
431withContext_ ctx name action = withContext ctx name () action
433-- | A version of liftIO that puts errors into the exception type of the Idris monad
434runIO :: IO a -> Idris a
435runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
436-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
437--
438-- Issue #1738 on the issue tracker.
439-- https://github.com/idris-lang/Idris-dev/issues/1738
441getName :: Idris Int
442getName = do i <- getIState;
443 let idx = idris_name i;
444 putIState $ (i { idris_name = idx + 1 })
445 return idx
447-- InternalApp keeps track of the real function application for making case splits from, not the application the
448-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
449addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
450addInternalApp fp l t
451 = do i <- getIState
452 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
454getInternalApp :: FilePath -> Int -> Idris PTerm
455getInternalApp fp l = do i <- getIState
456 case lookup (fp, l) (idris_lineapps i) of
457 Just n' -> return n'
458 Nothing -> return Placeholder
459 -- TODO: What if it's not there?
461-- Pattern definitions are only used for coverage checking, so erase them
462-- when we're done
463clearOrigPats :: Idris ()
464clearOrigPats = do i <- get
465 let ps = idris_patdefs i
466 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
467 put (i { idris_patdefs = ps' })
469-- Erase types from Ps in the context (basically ending up with what's in
470-- the .ibc, which is all we need after all the analysis is done)
471clearPTypes :: Idris ()
472clearPTypes = do i <- get
473 let ctxt = tt_ctxt i
474 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
475 where pErase (CaseOp c t tys orig tot cds)
476 = CaseOp c t tys orig [] (pErase' cds)
477 pErase x = x
478 pErase' (CaseDefs _ (cs, c) _ rs)
479 = let c' = (cs, fmap pEraseType c) in
480 CaseDefs c' c' c' rs
482checkUndefined :: FC -> Name -> Idris ()
483checkUndefined fc n
484 = do i <- getContext
485 case lookupTy n i of
486 (_:_) -> throwError . Msg $ show fc ++ ":" ++
487 show n ++ " already defined"
488 _ -> return ()
490isUndefined :: FC -> Name -> Idris Bool
491isUndefined fc n
492 = do i <- getContext
493 case lookupTyExact n i of
494 Just _ -> return False
495 _ -> return True
497setContext :: Context -> Idris ()
498setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
500updateContext :: (Context -> Context) -> Idris ()
501updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
503addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
504addConstraints fc (v, cs)
505 = do i <- getIState
506 let ctxt = tt_ctxt i
507 let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,
508 next_tvar = v }
509 let ics = zip cs (repeat fc) ++ idris_constraints i
510 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
512addDeferred = addDeferred' Ref
513addDeferredTyCon = addDeferred' (TCon 0 0)
515addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
516addDeferred' nt ns
517 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
518 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
519 i <- getIState
520 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
521 idris_metavars i }
522 where
523 -- 'tidyNames' is to generate user accessible names in case they are
524 -- needed in tactic scripts
525 tidyNames used (Bind (MN i x) b sc)
526 = let n' = uniqueNameSet (UN x) used in
527 Bind n' b $ tidyNames (S.insert n' used) sc
528 tidyNames used (Bind n b sc)
529 = let n' = uniqueNameSet n used in
530 Bind n' b $ tidyNames (S.insert n' used) sc
531 tidyNames used b = b
533solveDeferred :: Name -> Idris ()
534solveDeferred n = do i <- getIState
535 putIState $ i { idris_metavars =
536 filter (\(n', _) -> n/=n')
537 (idris_metavars i),
538 ibc_write =
539 filter (notMV n) (ibc_write i)
540 }
541 where notMV n (IBCMetavar n') = not (n == n')
542 notMV n _ = True
544getUndefined :: Idris [Name]
545getUndefined = do i <- getIState
546 return (map fst (idris_metavars i) \\ primDefs)
548isMetavarName :: Name -> IState -> Bool
549isMetavarName n ist
550 = case lookupNames n (tt_ctxt ist) of
551 (t:_) -> isJust $ lookup t (idris_metavars ist)
552 _ -> False
554getWidth :: Idris ConsoleWidth
555getWidth = fmap idris_consolewidth getIState
557setWidth :: ConsoleWidth -> Idris ()
558setWidth w = do ist <- getIState
559 put ist { idris_consolewidth = w }
561renderWidth :: Idris Int
562renderWidth = do iw <- getWidth
563 case iw of
564 InfinitelyWide -> return 100000000
565 ColsWide n -> return (max n 1)
566 AutomaticWidth -> runIO getScreenWidth
570type1Doc :: Doc OutputAnnotation
571type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
574isetPrompt :: String -> Idris ()
575isetPrompt p = do i <- getIState
576 case idris_outputmode i of
577 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
579-- | Tell clients how much was parsed and loaded
580isetLoadedRegion :: Idris ()
581isetLoadedRegion = do i <- getIState
582 let span = idris_parsedSpan i
583 case span of
584 Just fc ->
585 case idris_outputmode i of
586 IdeSlave n h ->
587 runIO . hPutStrLn h $
588 convSExp "set-loaded-region" fc n
589 Nothing -> return ()
591setLogLevel :: Int -> Idris ()
592setLogLevel l = do i <- getIState
593 let opts = idris_options i
594 let opt' = opts { opt_logLevel = l }
595 putIState $ i { idris_options = opt' }
597setCmdLine :: [Opt] -> Idris ()
598setCmdLine opts = do i <- getIState
599 let iopts = idris_options i
600 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
602getCmdLine :: Idris [Opt]
603getCmdLine = do i <- getIState
604 return (opt_cmdline (idris_options i))
606getDumpDefun :: Idris (Maybe FilePath)
607getDumpDefun = do i <- getIState
608 return $ findC (opt_cmdline (idris_options i))
609 where findC [] = Nothing
610 findC (DumpDefun x : _) = Just x
611 findC (_ : xs) = findC xs
613getDumpCases :: Idris (Maybe FilePath)
614getDumpCases = do i <- getIState
615 return $ findC (opt_cmdline (idris_options i))
616 where findC [] = Nothing
617 findC (DumpCases x : _) = Just x
618 findC (_ : xs) = findC xs
620logLevel :: Idris Int
621logLevel = do i <- getIState
622 return (opt_logLevel (idris_options i))
624setErrContext :: Bool -> Idris ()
625setErrContext t = do i <- getIState
626 let opts = idris_options i
627 let opts' = opts { opt_errContext = t }
628 putIState $ i { idris_options = opts' }
630errContext :: Idris Bool
631errContext = do i <- getIState
632 return (opt_errContext (idris_options i))
634getOptimise :: Idris [Optimisation]
635getOptimise = do i <- getIState
636 return (opt_optimise (idris_options i))
638setOptimise :: [Optimisation] -> Idris ()
639setOptimise newopts = do i <- getIState
640 let opts = idris_options i
641 let opts' = opts { opt_optimise = newopts }
642 putIState $ i { idris_options = opts' }
644addOptimise :: Optimisation -> Idris ()
645addOptimise opt = do opts <- getOptimise
646 setOptimise (nub (opt : opts))
648removeOptimise :: Optimisation -> Idris ()
649removeOptimise opt = do opts <- getOptimise
650 setOptimise ((nub opts) \\ [opt])
652-- Set appropriate optimisation set for the given level. We only have
653-- one optimisation that is configurable at the moment, however!
654setOptLevel :: Int -> Idris ()
655setOptLevel n | n <= 0 = setOptimise []
656setOptLevel 1 = setOptimise []
657setOptLevel 2 = setOptimise [PETransform]
658setOptLevel n | n >= 3 = setOptimise [PETransform]
660useREPL :: Idris Bool
661useREPL = do i <- getIState
662 return (opt_repl (idris_options i))
664setREPL :: Bool -> Idris ()
665setREPL t = do i <- getIState
666 let opts = idris_options i
667 let opt' = opts { opt_repl = t }
668 putIState $ i { idris_options = opt' }
670showOrigErr :: Idris Bool
671showOrigErr = do i <- getIState
672 return (opt_origerr (idris_options i))
674setShowOrigErr :: Bool -> Idris ()
675setShowOrigErr b = do i <- getIState
676 let opts = idris_options i
677 let opt' = opts { opt_origerr = b }
678 putIState $ i { idris_options = opt' }
680setAutoSolve :: Bool -> Idris ()
681setAutoSolve b = do i <- getIState
682 let opts = idris_options i
683 let opt' = opts { opt_autoSolve = b }
684 putIState $ i { idris_options = opt' }
686setNoBanner :: Bool -> Idris ()
687setNoBanner n = do i <- getIState
688 let opts = idris_options i
689 let opt' = opts { opt_nobanner = n }
690 putIState $ i { idris_options = opt' }
692getNoBanner :: Idris Bool
693getNoBanner = do i <- getIState
694 let opts = idris_options i
695 return (opt_nobanner opts)
697setQuiet :: Bool -> Idris ()
698setQuiet q = do i <- getIState
699 let opts = idris_options i
700 let opt' = opts { opt_quiet = q }
701 putIState $ i { idris_options = opt' }
703getQuiet :: Idris Bool
704getQuiet = do i <- getIState
705 let opts = idris_options i
706 return (opt_quiet opts)
708setCodegen :: Codegen -> Idris ()
709setCodegen t = do i <- getIState
710 let opts = idris_options i
711 let opt' = opts { opt_codegen = t }
712 putIState $ i { idris_options = opt' }
714codegen :: Idris Codegen
715codegen = do i <- getIState
716 return (opt_codegen (idris_options i))
718setOutputTy :: OutputType -> Idris ()
719setOutputTy t = do i <- getIState
720 let opts = idris_options i
721 let opt' = opts { opt_outputTy = t }
722 putIState $ i { idris_options = opt' }
724outputTy :: Idris OutputType
725outputTy = do i <- getIState
726 return $ opt_outputTy $ idris_options i
728setIdeSlave :: Bool -> Handle -> Idris ()
729setIdeSlave True h = do i <- getIState
730 putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }
731setIdeSlave False _ = return ()
733setTargetTriple :: String -> Idris ()
734setTargetTriple t = do i <- getIState
735 let opts = idris_options i
736 opt' = opts { opt_triple = t }
737 putIState $ i { idris_options = opt' }
739targetTriple :: Idris String
740targetTriple = do i <- getIState
741 return (opt_triple (idris_options i))
743setTargetCPU :: String -> Idris ()
744setTargetCPU t = do i <- getIState
745 let opts = idris_options i
746 opt' = opts { opt_cpu = t }
747 putIState $ i { idris_options = opt' }
749targetCPU :: Idris String
750targetCPU = do i <- getIState
751 return (opt_cpu (idris_options i))
753verbose :: Idris Bool
754verbose = do i <- getIState
755 return (opt_verbose (idris_options i))
757setVerbose :: Bool -> Idris ()
758setVerbose t = do i <- getIState
759 let opts = idris_options i
760 let opt' = opts { opt_verbose = t }
761 putIState $ i { idris_options = opt' }
763typeInType :: Idris Bool
764typeInType = do i <- getIState
765 return (opt_typeintype (idris_options i))
767setTypeInType :: Bool -> Idris ()
768setTypeInType t = do i <- getIState
769 let opts = idris_options i
770 let opt' = opts { opt_typeintype = t }
771 putIState $ i { idris_options = opt' }
773coverage :: Idris Bool
774coverage = do i <- getIState
775 return (opt_coverage (idris_options i))
777setCoverage :: Bool -> Idris ()
778setCoverage t = do i <- getIState
779 let opts = idris_options i
780 let opt' = opts { opt_coverage = t }
781 putIState $ i { idris_options = opt' }
783setIBCSubDir :: FilePath -> Idris ()
784setIBCSubDir fp = do i <- getIState
785 let opts = idris_options i
786 let opt' = opts { opt_ibcsubdir = fp }
787 putIState $ i { idris_options = opt' }
789valIBCSubDir :: IState -> Idris FilePath
790valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
792addImportDir :: FilePath -> Idris ()
793addImportDir fp = do i <- getIState
794 let opts = idris_options i
795 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
796 putIState $ i { idris_options = opt' }
798setImportDirs :: [FilePath] -> Idris ()
799setImportDirs fps = do i <- getIState
800 let opts = idris_options i
801 let opt' = opts { opt_importdirs = fps }
802 putIState $ i { idris_options = opt' }
804allImportDirs :: Idris [FilePath]
805allImportDirs = do i <- getIState
806 let optdirs = opt_importdirs (idris_options i)
807 return ("." : reverse optdirs)
809colourise :: Idris Bool
810colourise = do i <- getIState
811 return $ idris_colourRepl i
813setColourise :: Bool -> Idris ()
814setColourise b = do i <- getIState
815 putIState $ i { idris_colourRepl = b }
817impShow :: Idris Bool
818impShow = do i <- getIState
819 return (opt_showimp (idris_options i))
821setImpShow :: Bool -> Idris ()
822setImpShow t = do i <- getIState
823 let opts = idris_options i
824 let opt' = opts { opt_showimp = t }
825 putIState $ i { idris_options = opt' }
827setColour :: ColourType -> IdrisColour -> Idris ()
828setColour ct c = do i <- getIState
829 let newTheme = setColour' ct c (idris_colourTheme i)
830 putIState $ i { idris_colourTheme = newTheme }
831 where setColour' KeywordColour c t = t { keywordColour = c }
832 setColour' BoundVarColour c t = t { boundVarColour = c }
833 setColour' ImplicitColour c t = t { implicitColour = c }
834 setColour' FunctionColour c t = t { functionColour = c }
835 setColour' TypeColour c t = t { typeColour = c }
836 setColour' DataColour c t = t { dataColour = c }
837 setColour' PromptColour c t = t { promptColour = c }
838 setColour' PostulateColour c t = t { postulateColour = c }
840logLvl :: Int -> String -> Idris ()
841logLvl l str = do i <- getIState
842 let lvl = opt_logLevel (idris_options i)
843 when (lvl >= l) $
844 case idris_outputmode i of
845 RawOutput h -> do runIO $ hPutStrLn h str
846 IdeSlave n h ->
847 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
848 runIO . hPutStrLn h $ convSExp "log" good n
850cmdOptType :: Opt -> Idris Bool
851cmdOptType x = do i <- getIState
852 return $ x `elem` opt_cmdline (idris_options i)
854iLOG :: String -> Idris ()
855iLOG = logLvl 1
857noErrors :: Idris Bool
858noErrors = do i <- getIState
859 case errSpan i of
860 Nothing -> return True
861 _ -> return False
863setTypeCase :: Bool -> Idris ()
864setTypeCase t = do i <- getIState
865 let opts = idris_options i
866 let opt' = opts { opt_typecase = t }
867 putIState $ i { idris_options = opt' }
870-- Dealing with parameters
872expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
873 [Name] -> -- all names
874 [Name] -> -- names with no declaration
875 PTerm -> PTerm
876expandParams dec ps ns infs tm = en tm
877 where
878 -- if we shadow a name (say in a lambda binding) that is used in a call to
879 -- a lifted function, we need access to both names - once in the scope of the
880 -- binding and once to call the lifted functions. So we'll explicitly shadow
881 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
882 -- but we didn't...)
884 mkShadow (UN n) = MN 0 n
885 mkShadow (MN i n) = MN (i+1) n
886 mkShadow (NS x s) = NS (mkShadow x) s
888 en (PLam fc n t s)
889 | n `elem` (map fst ps ++ ns)
890 = let n' = mkShadow n in
891 PLam fc n' (en t) (en (shadow n n' s))
892 | otherwise = PLam fc n (en t) (en s)
893 en (PPi p n t s)
894 | n `elem` (map fst ps ++ ns)
895 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
896 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
897 | otherwise = PPi (enTacImp p) n (en t) (en s)
898 en (PLet fc n ty v s)
899 | n `elem` (map fst ps ++ ns)
900 = let n' = mkShadow n in
901 PLet fc n' (en ty) (en v) (en (shadow n n' s))
902 | otherwise = PLet fc n (en ty) (en v) (en s)
903 -- FIXME: Should only do this in a type signature!
904 en (PDPair f p (PRef f' n) t r)
905 | n `elem` (map fst ps ++ ns) && t /= Placeholder
906 = let n' = mkShadow n in
907 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
908 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
909 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
910 en (PTyped l r) = PTyped (en l) (en r)
911 en (PPair f p l r) = PPair f p (en l) (en r)
912 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
913 en (PAlternative a as) = PAlternative a (map en as)
914 en (PHidden t) = PHidden (en t)
915 en (PUnifyLog t) = PUnifyLog (en t)
916 en (PDisamb ds t) = PDisamb ds (en t)
917 en (PNoImplicits t) = PNoImplicits (en t)
918 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
919 en (PProof ts) = PProof (map (fmap en) ts)
920 en (PTactics ts) = PTactics (map (fmap en) ts)
922 en (PQuote (Var n))
923 | n `nselem` ns = PQuote (Var (dec n))
924 en (PApp fc (PInferRef fc' n) as)
925 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
926 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
927 en (PApp fc (PRef fc' n) as)
928 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
929 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
930 | n `nselem` ns = PApp fc (PRef fc' (dec n))
931 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
932 en (PAppBind fc (PRef fc' n) as)
933 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
934 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
935 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
936 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
937 en (PRef fc n)
938 | n `elem` infs = PApp fc (PInferRef fc (dec n))
939 (map (pexp . (PRef fc)) (map fst ps))
940 | n `nselem` ns = PApp fc (PRef fc (dec n))
941 (map (pexp . (PRef fc)) (map fst ps))
942 en (PInferRef fc n)
943 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
944 (map (pexp . (PRef fc)) (map fst ps))
945 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
946 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
947 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
948 en t = t
950 nselem x [] = False
951 nselem x (y : xs) | nseq x y = True
952 | otherwise = nselem x xs
954 nseq x y = nsroot x == nsroot y
956 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
957 enTacImp other = other
959expandParamsD :: Bool -> -- True = RHS only
960 IState ->
961 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
962expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
963 = if n `elem` ns && (not rhsonly)
964 then -- trace (show (n, expandParams dec ps ns ty)) $
965 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
966 else --trace (show (n, expandParams dec ps ns ty)) $
967 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
968expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
969 = if n `elem` ns && (not rhsonly)
970 then -- trace (show (n, expandParams dec ps ns ty)) $
971 PPostulate doc syn fc o (dec n) (piBind ps
972 (expandParams dec ps ns [] ty))
973 else --trace (show (n, expandParams dec ps ns ty)) $
974 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
975expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
976 = let n' = if n `elem` ns then dec n else n in
977 PClauses fc opts n' (map expandParamsC cs)
978 where
979 expandParamsC (PClause fc n lhs ws rhs ds)
980 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
981 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
982 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
983 n' = if n `elem` ns then dec n else n
984 -- names bound on the lhs should not be expanded on the rhs
985 ns' = removeBound lhs ns in
986 PClause fc n' lhs'
987 (map (expandParams dec ps'' ns' []) ws)
988 (expandParams dec ps'' ns' [] rhs)
989 (map (expandParamsD True ist dec ps'' ns') ds)
990 expandParamsC (PWith fc n lhs ws wval ds)
991 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
992 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
993 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
994 n' = if n `elem` ns then dec n else n
995 ns' = removeBound lhs ns in
996 PWith fc n' lhs'
997 (map (expandParams dec ps'' ns' []) ws)
998 (expandParams dec ps'' ns' [] wval)
999 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1000 updateps yn nm [] = []
1001 updateps yn nm (((a, t), i):as)
1002 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1003 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
1005 removeBound lhs ns = ns \\ nub (bnames lhs)
1007 bnames (PRef _ n) = [n]
1008 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1009 bnames (PPair _ _ l r) = bnames l ++ bnames r
1010 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1011 bnames _ = []
1013-- | Expands parameters defined in parameter and where blocks inside of declarations
1014expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1015 = PData doc argDocs syn fc co (expandPData pd)
1016 where
1017 -- just do the type decl, leave constructors alone (parameters will be
1018 -- added implicitly)
1019 expandPData (PDatadecl n ty cons)
1020 = if n `elem` ns
1021 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1022 (map econ cons)
1023 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1024 econ (doc, argDocs, n, t, fc, fs)
1025 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1026expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
1027 = if tn `elem` ns
1028 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1029 opts cdoc (dec cn) conty
1030 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1031 opts cdoc (dec cn) conty
1032 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1033expandParamsD rhs ist dec ps ns (PParams f params pds)
1034 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1035 (map (expandParamsD True ist dec ps ns) pds)
1036-- (map (expandParamsD ist dec ps ns) pds)
1037expandParamsD rhs ist dec ps ns (PMutual f pds)
1038 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1039expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
1040 = PClass doc info f
1041 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1043 (map (mapsnd (expandParams dec ps ns [])) params)
1044 pDocs
1045 (map (expandParamsD rhs ist dec ps ns) decls)
1046expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1047 = PInstance info f
1048 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
1050 (map (expandParams dec ps ns []) params)
1051 (expandParams dec ps ns [] ty)
1052 cn
1053 (map (expandParamsD rhs ist dec ps ns) decls)
1054expandParamsD rhs ist dec ps ns d = d
1056mapsnd f (x, t) = (x, f t)
1058-- Calculate a priority for a type, for deciding elaboration order
1059-- * if it's just a type variable or concrete type, do it early (0)
1060-- * if there's only type variables and injective constructors, do it next (1)
1061-- * if there's a function type, next (2)
1062-- * finally, everything else (3)
1064getPriority :: IState -> PTerm -> Int
1065getPriority i tm = 1 -- pri tm
1066 where
1067 pri (PRef _ n) =
1068 case lookupP n (tt_ctxt i) of
1069 ((P (DCon _ _ _) _ _):_) -> 1
1070 ((P (TCon _ _) _ _):_) -> 1
1071 ((P Ref _ _):_) -> 1
1072 [] -> 0 -- must be locally bound, if it's not an error...
1073 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1074 pri (PTrue _ _) = 0
1075 pri (PRefl _ _) = 1
1076 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1077 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1078 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1079 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1080 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1081 pri (PTyped l r) = pri l
1082 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1083 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1084 pri (PAlternative a as) = maximum (map pri as)
1085 pri (PConstant _) = 0
1086 pri Placeholder = 1
1087 pri _ = 3
1090addStatics :: Name -> Term -> PTerm -> Idris ()
1091addStatics n tm ptm =
1092 do let (statics, dynamics) = initStatics tm ptm
1093 ist <- getIState
1094 let paramnames
1095 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1096 Just p -> getNamesFrom 0 (fn_params p) tm ++
1097 concatMap (getParamNames ist) (map snd statics)
1098 _ -> concatMap (getParamNames ist) (map snd statics)
1100 let stnames = nub $ concatMap freeArgNames (map snd statics)
1101 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1102 \\ paramnames
1103 -- also get the arguments which are 'uniquely inferrable' from
1104 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1105 -- or parameters to the type of a static
1106 let statics' = nub $ map fst statics ++
1107 filter (\x -> not (elem x dnames)) stnames
1108 let stpos = staticList statics' tm
1109 i <- getIState
1110 when (not (null statics)) $
1111 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1112 ++ showTmImpls ptm ++ "\n"
1113 ++ show statics ++ "\n" ++ show dynamics
1114 ++ "\n" ++ show paramnames
1115 ++ "\n" ++ show stpos
1116 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1117 addIBC (IBCStatic n)
1118 where
1119 initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)
1120 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1121 (static, (n, ty) : dynamic)
1122 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)
1123 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1124 if pstatic p == Static then ((n, ty) : static, dynamic)
1125 else if (not (searchArg p))
1126 then (static, (n, ty) : dynamic)
1127 else (static, dynamic)
1128 initStatics t pt = ([], [])
1130 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1131 = case lookupCtxtExact n (idris_datatypes ist) of
1132 Just ti -> getNamePos 0 (param_pos ti) args
1133 Nothing -> []
1134 where getNamePos i ps [] = []
1135 getNamePos i ps (P _ n _ : as)
1136 | i `elem` ps = n : getNamePos (i + 1) ps as
1137 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1138 getParamNames ist (Bind t (Pi (P _ n _) _) sc)
1139 = n : getParamNames ist sc
1140 getParamNames ist _ = []
1142 getNamesFrom i ps (Bind n (Pi _ _) sc)
1143 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1144 | otherwise = getNamesFrom (i + 1) ps sc
1145 getNamesFrom i ps sc = []
1147 freeArgNames (Bind n (Pi ty _) sc)
1148 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1149 freeArgNames tm = let (_, args) = unApply tm in
1150 concatMap freeNames args
1152 -- if a name appears in a type class or tactic implicit index, it doesn't
1153 -- affect its 'uniquely inferrable' from a static status since these are
1154 -- resolved by searching.
1155 searchArg (Constraint _ _) = True
1156 searchArg (TacImp _ _ _) = True
1157 searchArg _ = False
1159 staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc
1160 staticList _ _ = []
1162-- Dealing with implicit arguments
1164-- Add some bound implicits to the using block if they aren't there already
1166addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1167addToUsing us [] = us
1168addToUsing us ((n, t) : ns)
1169 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1170 | otherwise = addToUsing us ns
1171 where impName (UImplicit n _) = Just n
1172 impName _ = Nothing
1174-- Add constraint bindings from using block
1176addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1177addUsingConstraints syn fc t
1178 = do ist <- get
1179 let ns = namesIn [] ist t
1180 let cs = getConstraints t -- check declared constraints
1181 let addconsts = uconsts \\ cs
1182 return (doAdd addconsts ns t)
1183 where uconsts = filter uconst (using syn)
1184 uconst (UConstraint _ _) = True
1185 uconst _ = False
1187 doAdd [] _ t = t
1188 -- if all of args in ns, then add it
1189 doAdd (UConstraint c args : cs) ns t
1190 | all (\n -> elem n ns) args
1191 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1192 (mkConst c args) (doAdd cs ns t)
1193 | otherwise = doAdd cs ns t
1195 mkConst c args = PApp fc (PRef fc c)
1196 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1198 getConstraints (PPi (Constraint _ _) _ c sc)
1199 = getcapp c ++ getConstraints sc
1200 getConstraints (PPi _ _ c sc) = getConstraints sc
1201 getConstraints _ = []
1203 getcapp (PApp _ (PRef _ c) args)
1204 = do ns <- mapM getName args
1205 return (UConstraint c ns)
1206 getcapp _ = []
1208 getName (PExp _ _ _ (PRef _ n)) = return n
1209 getName _ = []
1211-- Add implicit bindings from using block, and bind any missing names
1212addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1213addUsingImpls syn n fc t
1214 = do ist <- getIState
1215 let ns = implicitNamesIn (map iname uimpls) ist t
1216 let badnames = filter (\n -> not (implicitable n) &&
1217 n `notElem` (map iname uimpls)) ns
1218 when (not (null badnames)) $
1219 throwError (At fc (Elaborating "type of " n
1220 (NoSuchVariable (head badnames))))
1221 let cs = getArgnames t -- get already bound names
1222 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1223 -- if all names in the arguments of addconsts appear in ns,
1224 -- add the constraint implicitly
1225 return (bindFree ns (doAdd addimpls ns t))
1226 where uimpls = filter uimpl (using syn)
1227 uimpl (UImplicit _ _) = True
1228 uimpl _ = False
1230 iname (UImplicit n _) = n
1231 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1233 doAdd [] _ t = t
1234 -- if all of args in ns, then add it
1235 doAdd (UImplicit n ty : cs) ns t
1236 | elem n ns
1237 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1238 | otherwise = doAdd cs ns t
1240 -- bind the free names which weren't in the using block
1241 bindFree [] tm = tm
1242 bindFree (n:ns) tm
1243 | elem n (map iname uimpls) = bindFree ns tm
1244 | otherwise
1245 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1247 getArgnames (PPi _ n c sc)
1248 = n : getArgnames sc
1249 getArgnames _ = []
1251-- Given the original type and the elaborated type, return the implicitness
1252-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1254getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1255getUnboundImplicits i t tm = getImps t (collectImps tm)
1256 where collectImps (PPi p n t sc)
1257 = (n, (p, t)) : collectImps sc
1258 collectImps _ = []
1260 getImps (Bind n (Pi t _) sc) imps
1261 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1262 where
1263 argInfo n (Imp opt _ _) t'
1264 = (True, PImp (getPriority i t') True opt n t')
1265 argInfo n (Exp opt _ _) t'
1266 = (InaccessibleArg `elem` opt,
1267 PExp (getPriority i t') opt n t')
1268 argInfo n (Constraint opt _) t'
1269 = (InaccessibleArg `elem` opt,
1270 PConstraint 10 opt n t')
1271 argInfo n (TacImp opt _ scr) t'
1272 = (InaccessibleArg `elem` opt,
1273 PTacImplicit 10 opt n scr t')
1274 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps
1275 where impBind n t = (True, PImp 1 True [] n Placeholder)
1276 getImps sc tm = []
1278-- Add implicit Pi bindings for any names in the term which appear in an
1279-- argument position.
1281-- This has become a right mess already. Better redo it some time...
1282-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1283-- a couple of places which use it. Clean them up!
1285-- Issue 1739 in the issue tracker
1286-- https://github.com/idris-lang/Idris-dev/issues/1739
1287implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1288implicit info syn n ptm = implicit' info syn [] n ptm
1290implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1291implicit' info syn ignore n ptm
1292 = do i <- getIState
1293 let (tm', impdata) = implicitise syn ignore i ptm
1294 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1295-- let (tm'', spos) = findStatics i tm'
1296 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1297 addIBC (IBCImp n)
1298 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1299-- i <- get
1300-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1301 return tm'
1302 where
1303 -- Detect unknown names in default arguments and throw error if found.
1304 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1305 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1307 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1308 notFoundInDefault kns (PTacImplicit _ _ n script _)
1309 = do i <- getIState
1310 case notFound kns (namesIn [] i script) of
1311 Nothing -> return (n:kns)
1312 Just name -> throwError (NoSuchVariable name)
1313 notFoundInDefault kns p = return ((pname p):kns)
1315 notFound :: [Name] -> [Name] -> Maybe Name
1316 notFound kns [] = Nothing
1317 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1318 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1320implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1321implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1322 let (declimps, ns') = execState (imps True [] tm) ([], [])
1323 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1324 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1325 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1326 if null ns
1327 then (tm, reverse declimps)
1328 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1329 where
1330 uvars = map ipair (filter uimplicit (using syn))
1331 pvars = syn_params syn
1333 inUsing n = n `elem` map fst uvars
1335 ipair (UImplicit x y) = (x, y)
1336 uimplicit (UImplicit _ _) = True
1337 uimplicit _ = False
1339 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1340 | otherwise = x : dropAll xs ys
1341 dropAll [] ys = []
1343 -- Find names in argument position in a type, suitable for implicit
1344 -- binding
1345 -- Not the function position, but do everything else...
1346 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1347 implNamesIn uv t = namesIn uv ist t
1349 imps top env (PApp _ f as)
1350 = do (decls, ns) <- get
1351 let isn = concatMap (namesIn uvars ist) (map getTm as)
1352 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1353 imps top env (PPi (Imp l _ _) n ty sc)
1354 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1355 (decls , ns) <- get
1356 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1357 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1358 imps True (n:env) sc
1359 imps top env (PPi (Exp l _ _) n ty sc)
1360 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1361 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1362 _ -> [])
1363 (decls, ns) <- get -- ignore decls in HO types
1364 put (PExp (getPriority ist ty) 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 (Constraint 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 (PConstraint 10 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 (TacImp l _ scr) 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 (PTacImplicit 10 l n scr Placeholder : decls,
1381 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1382 imps True (n:env) sc
1383 imps top env (PEq _ _ _ l r)
1384 = do (decls, ns) <- get
1385 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1386 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1387 imps top env (PRewrite _ l r _)
1388 = do (decls, ns) <- get
1389 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1390 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1391 imps top env (PTyped l r)
1392 = imps top env l
1393 imps top env (PPair _ _ l r)
1394 = do (decls, ns) <- get
1395 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1396 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1397 imps top env (PDPair _ _ (PRef _ n) t r)
1398 = do (decls, ns) <- get
1399 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1400 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1401 imps top env (PDPair _ _ l t r)
1402 = do (decls, ns) <- get
1403 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1404 namesIn uvars ist r
1405 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1406 imps top env (PAlternative a as)
1407 = do (decls, ns) <- get
1408 let isn = concatMap (namesIn uvars ist) as
1409 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1410 imps top env (PLam fc n ty sc)
1411 = do imps False env ty
1412 imps False (n:env) sc
1413 imps top env (PHidden tm) = imps False env tm
1414 imps top env (PUnifyLog tm) = imps False env tm
1415 imps top env (PNoImplicits tm) = imps False env tm
1416 imps top env _ = return ()
1418 pibind using [] sc = sc
1419 pibind using (n:ns) sc
1420 = case lookup n using of
1421 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1422 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1423 (pibind using ns sc)
1425-- Add implicit arguments in function calls
1426addImplPat :: IState -> PTerm -> PTerm
1427addImplPat = addImpl' True [] []
1429addImplBound :: IState -> [Name] -> PTerm -> PTerm
1430addImplBound ist ns = addImpl' False ns [] ist
1432addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1433addImplBoundInf ist ns inf = addImpl' False ns inf ist
1435-- | Add the implicit arguments to applications in the term
1436addImpl :: IState -> PTerm -> PTerm
1437addImpl = addImpl' False [] []
1439-- TODO: in patterns, don't add implicits to function names guarded by constructors
1440-- and *not* inside a PHidden
1442addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1443addImpl' inpat env infns ist ptm
1444 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1445 where
1446 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1447 ai qq env ds (PRef fc f)
1448 | f `elem` infns = PInferRef fc f
1449 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1450 ai qq env ds (PHidden (PRef fc f))
1451 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
1452 ai qq env ds (PEq fc lt rt l r)
1453 = let lt' = ai qq env ds lt
1454 rt' = ai qq env ds rt
1455 l' = ai qq env ds l
1456 r' = ai qq env ds r in
1457 PEq fc lt' rt' l' r'
1458 ai qq env ds (PRewrite fc l r g)
1459 = let l' = ai qq env ds l
1460 r' = ai qq env ds r
1461 g' = fmap (ai qq env ds) g in
1462 PRewrite fc l' r' g'
1463 ai qq env ds (PTyped l r)
1464 = let l' = ai qq env ds l
1465 r' = ai qq env ds r in
1466 PTyped l' r'
1467 ai qq env ds (PPair fc p l r)
1468 = let l' = ai qq env ds l
1469 r' = ai qq env ds r in
1470 PPair fc p l' r'
1471 ai qq env ds (PDPair fc p l t r)
1472 = let l' = ai qq env ds l
1473 t' = ai qq env ds t
1474 r' = ai qq env ds r in
1475 PDPair fc p l' t' r'
1476 ai qq env ds (PAlternative a as)
1477 = let as' = map (ai qq env ds) as in
1478 PAlternative a as'
1479 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1480 ai qq env ds (PApp fc (PInferRef _ f) as)
1481 = let as' = map (fmap (ai qq env ds)) as in
1482 PApp fc (PInferRef fc f) as'
1483 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1484 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1485 | not (f `elem` map fst env)
1486 = let as' = map (fmap (ai qq env ds)) as in
1487 handleErr $ aiFn inpat False qq ist fc f ds as'
1488 | Just (Just ty) <- lookup f env =
1489 let as' = map (fmap (ai qq env ds)) as
1490 arity = getPArity ty in
1491 mkPApp fc arity ftm as'
1492 ai qq env ds (PApp fc f as)
1493 = let f' = ai qq env ds f
1494 as' = map (fmap (ai qq env ds)) as in
1495 mkPApp fc 1 f' as'
1496 ai qq env ds (PCase fc c os)
1497 = let c' = ai qq env ds c in
1498 -- leave os alone, because they get lifted into a new pattern match
1499 -- definition which is passed through addImpl again with more scope
1500 -- information
1501 PCase fc c' os
1502 -- If the name in a lambda is a constructor name, do this as a 'case'
1503 -- instead (it is harmless to do so, especially since the lambda will
1504 -- be lifted anyway!)
1505 ai qq env ds (PLam fc n ty sc)
1506 = case lookupDef n (tt_ctxt ist) of
1507 [] -> let ty' = ai qq env ds ty
1508 sc' = ai qq ((n, Just ty):env) ds sc in
1509 PLam fc n ty' sc'
1510 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1511 (PCase fc (PRef fc (sMN 0 "lamp") )
1512 [(PRef fc n, sc)]))
1513 ai qq env ds (PLet fc n ty val sc)
1514 = case lookupDef n (tt_ctxt ist) of
1515 [] -> let ty' = ai qq env ds ty
1516 val' = ai qq env ds val
1517 sc' = ai qq ((n, Just ty):env) ds sc in
1518 PLet fc n ty' val' sc'
1519 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
1520 ai qq env ds (PPi p n ty sc)
1521 = let ty' = ai qq env ds ty
1522 sc' = ai qq ((n, Just ty):env) ds sc in
1523 PPi p n ty' sc'
1524 ai qq env ds (PGoal fc r n sc)
1525 = let r' = ai qq env ds r
1526 sc' = ai qq ((n, Nothing):env) ds sc in
1527 PGoal fc r' n sc'
1528 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1529 -- Don't do PProof or PTactics since implicits get added when scope is
1530 -- properly known in ElabTerm.runTac
1531 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1532 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1533 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1534 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1535 (fmap (ai True env ds) g)
1536 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1537 ai qq env ds tm = tm
1539 handleErr (Left err) = PElabError err
1540 handleErr (Right x) = x
1542-- if in a pattern, and there are no arguments, and there's no possible
1543-- names with zero explicit arguments, don't add implicits.
1545aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1546aiFn inpat True qq ist fc f ds []
1547 = case lookupDef f (tt_ctxt ist) of
1548 [] -> Right $ PPatvar fc f
1549 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1550 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1551 if (not (vname f) || tcname f
1552 || any (conCaf (tt_ctxt ist)) ialts)
1553-- any constructor alts || any allImp ialts))
1554 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1555 else Right $ PPatvar fc f
1556 where imp (PExp _ _ _ _) = False
1557 imp _ = True
1558-- allImp [] = False
1559 allImp xs = all imp xs
1560 constructor (TyDecl (DCon _ _ _) _) = True
1561 constructor _ = False
1563 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1565 vname (UN n) = True -- non qualified
1566 vname _ = False
1568aiFn inpat expat qq ist fc f ds as
1569 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1570aiFn inpat expat qq ist fc f ds as
1571 -- This is where namespaces get resolved by adding PAlternative
1572 = do let ns = lookupCtxtName f (idris_implicits ist)
1573 let nh = filter (\(n, _) -> notHidden n) ns
1574 let ns' = case trimAlts ds nh of
1575 [] -> nh
1576 x -> x
1577 case ns' of
1578 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1579 [] -> if f `elem` (map fst (idris_metavars ist))
1580 then Right $ PApp fc (PRef fc f) as
1581 else Right $ mkPApp fc (length as) (PRef fc f) as
1582 alts -> Right $
1583 PAlternative True $
1584 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1585 (insertImpl ns as)) alts
1586 where
1587 trimAlts [] alts = alts
1588 trimAlts ns alts
1589 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1591 nspace (NS _ s) = s
1592 nspace _ = []
1594 notHidden n = case getAccessibility n of
1595 Hidden -> False
1596 _ -> True
1598 getAccessibility n
1599 = case lookupDefAccExact n False (tt_ctxt ist) of
1600 Just (n,t) -> t
1601 _ -> Public
1603 insertImpl :: [PArg] -> [PArg] -> [PArg]
1604 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1606 exp (PExp _ _ _ _) = True
1607 exp (PConstraint _ _ _ _) = True
1608 exp _ = False
1610 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1611 -> [PArg] -- parameters
1612 -> [PArg] -- explicit arguments
1613 -> [PArg] -- implicits given
1614 -> [PArg]
1615 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1616 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1617 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1618 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1619 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1620 let rtc = PResolveTC fc in
1621 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1622 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1623 case find n imps [] of
1624 Just (tm, imps') ->
1625 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1626 Nothing ->
1627 PImp p True l n Placeholder :
1628 insImpAcc (M.insert n Placeholder pnas) ps given imps
1629 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1630 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1631 case find n imps [] of
1632 Just (tm, imps') ->
1633 PTacImplicit p l n sc tm :
1634 insImpAcc (M.insert n tm pnas) ps given imps'
1635 Nothing ->
1636 if inpat
1637 then PTacImplicit p l n sc Placeholder :
1638 insImpAcc (M.insert n Placeholder pnas) ps given imps
1639 else PTacImplicit p l n sc sc :
1640 insImpAcc (M.insert n sc pnas) ps given imps
1641 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1642 -- TODO: report here, and prune alternatives
1643 -- Issue #1740 in the Issue Tracker
1644-- https://github.com/idris-lang/Idris-dev/issues/1740
1645 insImpAcc _ _ given imps = given ++ imps
1647 find n [] acc = Nothing
1648 find n (PImp _ _ _ n' t : gs) acc
1649 | n == n' = Just (t, reverse acc ++ gs)
1650 find n (PTacImplicit _ _ n' _ t : gs) acc
1651 | n == n' = Just (t, reverse acc ++ gs)
1652 find n (g : gs) acc = find n gs (g : acc)
1654-- replace non-linear occurrences with _
1656stripLinear :: IState -> PTerm -> PTerm
1657stripLinear i tm = evalState (sl tm) [] where
1658 sl :: PTerm -> State [Name] PTerm
1659 sl (PRef fc f)
1660 | (_:_) <- lookupTy f (tt_ctxt i)
1661 = return $ PRef fc f
1662 | otherwise = do ns <- get
1663 if (f `elem` ns)
1664 then return $ PHidden (PRef fc f) -- Placeholder
1665 else do put (f : ns)
1666 return (PRef fc f)
1667 sl (PPatvar fc f)
1668 = do ns <- get
1669 if (f `elem` ns)
1670 then return $ PHidden (PPatvar fc f) -- Placeholder
1671 else do put (f : ns)
1672 return (PPatvar fc f)
1673 -- Assumption is that variables are all the same in each alternative
1674 sl t@(PAlternative b as) = do ns <- get
1675 as' <- slAlts ns as
1676 return (PAlternative b as')
1677 where slAlts ns (a : as) = do put ns
1678 a' <- sl a
1679 as' <- slAlts ns as
1680 return (a' : as')
1681 slAlts ns [] = return []
1682 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1683 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1684 args' <- mapM slA args
1685 return $ PApp fc fn args'
1686 where slA (PImp p m l n t) = do t' <- sl t
1687 return $ PImp p m l n t'
1688 slA (PExp p l n t) = do t' <- sl t
1689 return $ PExp p l n t'
1690 slA (PConstraint p l n t)
1691 = do t' <- sl t
1692 return $ PConstraint p l n t'
1693 slA (PTacImplicit p l n sc t)
1694 = do t' <- sl t
1695 return $ PTacImplicit p l n sc t'
1696 sl x = return x
1698-- Remove functions which aren't applied to anything, which must then
1699-- be resolved by unification. Assume names resolved and alternatives
1700-- filled in (so no ambiguity).
1702stripUnmatchable :: IState -> PTerm -> PTerm
1703stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1704 su :: PTerm -> PTerm
1705 su (PRef fc f)
1706 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)
1707 = Placeholder
1708 su (PApp fc f@(PRef _ fn) args)
1709 | isDConName fn ctxt
1710 = PApp fc f (fmap (fmap su) args)
1711 su (PApp fc f args)
1712 = PHidden (PApp fc f args)
1713 su (PAlternative b alts)
1714 = let alts' = filter (/= Placeholder) (map su alts) in
1715 if null alts' then Placeholder
1716 else PAlternative b alts'
1717 su (PPair fc p l r) = PPair fc p (su l) (su r)
1718 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1719 su t@(PLam fc _ _ _) = PHidden t
1720 su t@(PPi _ _ _ _) = PHidden t
1721 su t@(PEq _ _ _ _ _) = PHidden t
1722 su t = t
1724 ctxt = tt_ctxt i
1726stripUnmatchable i tm = tm
1728mkPApp fc a f [] = f
1729mkPApp fc a f as = let rest = drop a as in
1730 appRest fc (PApp fc f (take a as)) rest
1731 where
1732 appRest fc f [] = f
1733 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1735-- Find 'static' argument positions
1736-- (the declared ones, plus any names in argument position in the declared
1737-- statics)
1738-- FIXME: It's possible that this really has to happen after elaboration
1740findStatics :: IState -> PTerm -> (PTerm, [Bool])
1741findStatics ist tm = trace (show tm) $
1742 let (ns, ss) = fs tm in
1743 runState (pos ns ss tm) []
1744 where fs (PPi p n t sc)
1745 | Static <- pstatic p
1746 = let (ns, ss) = fs sc in
1747 (namesIn [] ist t : ns, n : ss)
1748 | otherwise = let (ns, ss) = fs sc in
1749 (ns, ss)
1750 fs _ = ([], [])
1752 inOne n ns = length (filter id (map (elem n) ns)) == 1
1754 pos ns ss (PPi p n t sc)
1755 | elem n ss = do sc' <- pos ns ss sc
1756 spos <- get
1757 put (True : spos)
1758 return (PPi (p { pstatic = Static }) n t sc')
1759 | otherwise = do sc' <- pos ns ss sc
1760 spos <- get
1761 put (False : spos)
1762 return (PPi p n t sc')
1763 pos ns ss t = return t
1765-- for 6.12/7 compatibility
1766data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1768instance Applicative (EitherErr a) where
1769 pure = return
1770 (<*>) = ap
1772instance Monad (EitherErr a) where
1773 return = RightOK
1775 (LeftErr e) >>= k = LeftErr e
1776 RightOK v >>= k = k v
1778toEither (LeftErr e) = Left e
1779toEither (RightOK ho) = Right ho
1781-- syntactic match of a against b, returning pair of variables in a
1782-- and what they match. Returns the pair that failed if not a match.
1784matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1785matchClause = matchClause' False
1787matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1788matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1789 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1791 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1792 fullApp x = x
1794 match' x y = match (fullApp x) (fullApp y)
1795 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1796 | fi == txt "fromInteger" && b == txt "builtins",
1797 PConstant (I _) <- getTm x = match (getTm x) x'
1798 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1799 | fi == txt "fromInteger" && b == txt "builtins",
1800 PConstant (I _) <- getTm x = match (getTm x) x'
1801 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1802 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1803 match (PApp _ f args) (PApp _ f' args')
1804 | length args == length args'
1805 = do mf <- match' f f'
1806 ms <- zipWithM matchArg args args'
1807 return (mf ++ concat ms)
1808 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1809 match (PPatvar f n) xr = match (PRef f n) xr
1810 match xr (PPatvar f n) = match xr (PRef f n)
1811 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1812 match (PRef _ n) tm@(PRef _ n')
1813 | n == n' && not names &&
1814 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1815 || tm == Placeholder)
1816 = return [(n, tm)]
1817 -- if one namespace is missing, drop the other
1818 | n == n' || n == dropNS n' || dropNS n == n' = return []
1819 where dropNS (NS n _) = n
1820 dropNS n = n
1821 match (PRef _ n) tm
1822 | not names && (not (isConName n (tt_ctxt i) ||
1823 isFnName n (tt_ctxt i)) || tm == Placeholder)
1824 = return [(n, tm)]
1825 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1826 = do ml <- match' l l'
1827 mr <- match' r r'
1828 return (ml ++ mr)
1829 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1830 = do ml <- match' l l'
1831 mr <- match' r r'
1832 return (ml ++ mr)
1833 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1834 mr <- match r r'
1835 return (ml ++ mr)
1836 match (PTyped l r) x = match l x
1837 match x (PTyped l r) = match x l
1838 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1839 mr <- match' r r'
1840 return (ml ++ mr)
1841 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1842 mt <- match' t t'
1843 mr <- match' r r'
1844 return (ml ++ mt ++ mr)
1845 match (PAlternative a as) (PAlternative a' as')
1846 = do ms <- zipWithM match' as as'
1847 return (concat ms)
1848 match a@(PAlternative _ as) b
1849 = do let ms = zipWith match' as (repeat b)
1850 case (rights (map toEither ms)) of
1851 (x: _) -> return x
1852 _ -> LeftErr (a, b)
1853 match (PCase _ _ _) _ = return [] -- lifted out
1854 match (PMetavar _) _ = return [] -- modified
1855 match (PInferRef _ _) _ = return [] -- modified
1856 match (PQuote _) _ = return []
1857 match (PProof _) _ = return []
1858 match (PTactics _) _ = return []
1859 match (PRefl _ _) (PRefl _ _) = return []
1860 match (PResolveTC _) (PResolveTC _) = return []
1861 match (PTrue _ _) (PTrue _ _) = return []
1862 match (PReturn _) (PReturn _) = return []
1863 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1864 ms <- match' s s'
1865 return (mt ++ ms)
1866 match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1867 ms <- match' s s'
1868 return (mt ++ ms)
1869 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
1870 mty <- match' ty ty'
1871 ms <- match' s s'
1872 return (mt ++ mty ++ ms)
1873 match (PHidden x) (PHidden y)
1874 | RightOK xs <- match x y = return xs -- to collect variables
1875 | otherwise = return [] -- Otherwise hidden things are unmatchable
1876 match (PHidden x) y
1877 | RightOK xs <- match x y = return xs
1878 | otherwise = return []
1879 match x (PHidden y)
1880 | RightOK xs <- match x y = return xs
1881 | otherwise = return []
1882 match (PUnifyLog x) y = match' x y
1883 match x (PUnifyLog y) = match' x y
1884 match (PNoImplicits x) y = match' x y
1885 match x (PNoImplicits y) = match' x y
1886 match Placeholder _ = return []
1887 match _ Placeholder = return []
1888 match (PResolveTC _) _ = return []
1889 match a b | a == b = return []
1890 | otherwise = LeftErr (a, b)
1892 checkRpts (RightOK ms) = check ms where
1893 check ((n,t):xs)
1894 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1895 then Left (t, t')
1896 else check xs
1897 check (_:xs) = check xs
1898 check [] = Right ms
1899 checkRpts (LeftErr x) = Left x
1901substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1902substMatches ms = substMatchesShadow ms []
1904substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1905substMatchesShadow [] shs t = t
1906substMatchesShadow ((n,tm):ns) shs t
1907 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1909substMatch :: Name -> PTerm -> PTerm -> PTerm
1910substMatch n = substMatchShadow n []
1912substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1913substMatchShadow n shs tm t = sm shs t where
1914 sm xs (PRef _ n') | n == n' = tm
1915 sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
1916 sm xs (PPi p x t sc)
1917 | x `elem` xs
1918 = let x' = nextName x in
1919 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1920 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1921 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1922 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1923 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1924 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1925 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1926 (fmap (sm xs) tm)
1927 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1928 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1929 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1930 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1931 sm xs (PHidden x) = PHidden (sm xs x)
1932 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1933 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1934 sm xs x = x
1936 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1937 fullApp x = x
1939shadow :: Name -> Name -> PTerm -> PTerm
1940shadow n n' t = sm t where
1941 sm (PRef fc x) | n == x = PRef fc n'
1942 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
1943 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1944 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
1945 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1946 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1947 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1948 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1949 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1950 sm (PTyped x y) = PTyped (sm x) (sm y)
1951 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1952 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1953 sm (PAlternative a as) = PAlternative a (map sm as)
1954 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1955 sm (PProof ts) = PProof (map (fmap sm) ts)
1956 sm (PHidden x) = PHidden (sm x)
1957 sm (PUnifyLog x) = PUnifyLog (sm x)
1958 sm (PNoImplicits x) = PNoImplicits (sm x)
1959 sm x = x
1961-- Rename any binders which are repeated (so that we don't have to mess
1962-- about with shadowing anywhere else).
1964mkUniqueNames :: [Name] -> PTerm -> PTerm
1965mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
1966 inScope :: S.Set Name
1967 inScope = S.fromList $ boundNamesIn tm
1969 mkUniqA arg = do t' <- mkUniq (getTm arg)
1970 return (arg { getTm = t' })
1972 -- Initialise the unique name with the environment length (so we're not
1973 -- looking for too long...)
1974 initN (UN n) l = UN $ txt (str n ++ show l)
1975 initN (MN i s) l = MN (i+l) s
1976 initN n l = n
1978 -- FIXME: Probably ought to do this for completeness! It's fine as
1979 -- long as there are no bindings inside tactics though.
1980 mkUniqT tac = return tac
1982 mkUniq :: PTerm -> State (S.Set Name) PTerm
1983 mkUniq (PLam fc n ty sc)
1984 = do env <- get
1985 (n', sc') <-
1986 if n `S.member` env
1987 then do let n' = uniqueNameSet (initN n (S.size env))
1988 (S.union env inScope)
1989 return (n', shadow n n' sc)
1990 else return (n, sc)
1991 put (S.insert n' env)
1992 ty' <- mkUniq ty
1993 sc'' <- mkUniq sc'
1994 return $! PLam fc n' ty' sc''
1995 mkUniq (PPi p n ty sc)
1996 = do env <- get
1997 (n', sc') <-
1998 if n `S.member` env
1999 then do let n' = uniqueNameSet (initN n (S.size env))
2000 (S.union env inScope)
2001 return (n', shadow n n' sc)
2002 else return (n, sc)
2003 put (S.insert n' env)
2004 ty' <- mkUniq ty
2005 sc'' <- mkUniq sc'
2006 return $! PPi p n' ty' sc''
2007 mkUniq (PLet fc n ty val sc)
2008 = do env <- get
2009 (n', sc') <-
2010 if n `S.member` env
2011 then do let n' = uniqueNameSet (initN n (S.size env))
2012 (S.union env inScope)
2013 return (n', shadow n n' sc)
2014 else return (n, sc)
2015 put (S.insert n' env)
2016 ty' <- mkUniq ty; val' <- mkUniq val
2017 sc'' <- mkUniq sc'
2018 return $! PLet fc n' ty' val' sc''
2019 mkUniq (PApp fc t args)
2020 = do t' <- mkUniq t
2021 args' <- mapM mkUniqA args
2022 return $! PApp fc t' args'
2023 mkUniq (PAppBind fc t args)
2024 = do t' <- mkUniq t
2025 args' <- mapM mkUniqA args
2026 return $! PAppBind fc t' args'
2027 mkUniq (PCase fc t alts)
2028 = do t' <- mkUniq t
2029 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
2030 return (x', y')) alts
2031 return $! PCase fc t' alts'
2032 mkUniq (PPair fc p l r)
2033 = do l' <- mkUniq l; r' <- mkUniq r
2034 return $! PPair fc p l' r'
2035 mkUniq (PDPair fc p (PRef fc' n) t sc)
2036 | t /= Placeholder
2037 = do env <- get
2038 (n', sc') <- if n `S.member` env
2039 then do let n' = uniqueNameSet n (S.union env inScope)
2040 return (n', shadow n n' sc)
2041 else return (n, sc)
2042 put (S.insert n' env)
2043 t' <- mkUniq t
2044 sc'' <- mkUniq sc'
2045 return $! PDPair fc p (PRef fc' n') t' sc''
2046 mkUniq (PDPair fc p l t r)
2047 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
2048 return $! PDPair fc p l' t' r'
2049 mkUniq (PAlternative b as)
2050 = liftM (PAlternative b) (mapM mkUniq as)
2051 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
2052 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2053 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2054 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2055 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2056 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2057 mkUniq t = return t