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