git.iko.soy/Idris-dev
on 2fcd41c help sign in
Idris-dev/src/Idris/AbsSyntax.hs
2006 lines 84 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.Error(throwError)
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 Control.Monad.Error (throwError, catchError)
36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
38import Util.Pretty
39import Util.ScreenSize
40import Util.System
42getContext :: Idris Context
43getContext = do i <- getIState; return (tt_ctxt i)
45forCodegen :: Codegen -> [(Codegen, a)] -> [a]
46forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
48getObjectFiles :: Codegen -> Idris [FilePath]
49getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
51addObjectFile :: Codegen -> FilePath -> Idris ()
52addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
54getLibs :: Codegen -> Idris [String]
55getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
57addLib :: Codegen -> String -> Idris ()
58addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
60getFlags :: Codegen -> Idris [String]
61getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
63addFlag :: Codegen -> String -> Idris ()
64addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
66addDyLib :: [String] -> Idris (Either DynamicLib String)
67addDyLib libs = do i <- getIState
68 let ls = idris_dynamic_libs i
69 let importdirs = opt_importdirs (idris_options i)
70 case mapMaybe (findDyLib ls) libs of
71 x:_ -> return (Left x)
72 [] -> do
73 handle <- lift . lift .
74 mapM (\l -> catchIO (tryLoadLib importdirs l)
75 (\_ -> return Nothing)) $ libs
76 case msum handle of
77 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
78 concat (intersperse "," libs) ++ "\"")
79 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
80 return (Left x)
81 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
82 findDyLib [] l = Nothing
83 findDyLib (lib:libs) l | l == lib_name lib = Just lib
84 | otherwise = findDyLib libs l
86getAutoImports :: Idris [FilePath]
87getAutoImports = do i <- getIState
88 return (opt_autoImport (idris_options i))
90addAutoImport :: FilePath -> Idris ()
91addAutoImport fp = do i <- getIState
92 let opts = idris_options i
93 let autoimps = opt_autoImport opts
94 put (i { idris_options = opts { opt_autoImport =
95 fp : opt_autoImport opts } } )
97addHdr :: Codegen -> String -> Idris ()
98addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
100addImported :: FilePath -> Idris ()
101addImported f = do i <- getIState
102 putIState $ i { idris_imported = nub $ f : 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 _ -> []
313addToCalledG :: Name -> [Name] -> Idris ()
314addToCalledG n ns = return () -- TODO
316-- Add a class instance function. Dodgy hack: Put integer instances first in the
317-- list so they are resolved by default.
318-- Dodgy hack 2: put constraint chasers (@@) last
320addInstance :: Bool -> Name -> Name -> Idris ()
321addInstance int n i
322 = do ist <- getIState
323 case lookupCtxt n (idris_classes ist) of
324 [CI a b c d e ins] ->
325 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
326 putIState $ ist { idris_classes = cs }
327 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
328 putIState $ ist { idris_classes = cs }
329 where addI i ins | int = i : ins
330 | chaser n = ins ++ [i]
331 | otherwise = insI i ins
332 insI i [] = [i]
333 insI i (n : ns) | chaser n = i : n : ns
334 | otherwise = n : insI i ns
336 chaser (UN nm)
337 | ('@':'@':_) <- str nm = True
338 chaser (NS n _) = chaser n
339 chaser _ = False
341addClass :: Name -> ClassInfo -> Idris ()
342addClass n i
343 = do ist <- getIState
344 let i' = case lookupCtxt n (idris_classes ist) of
345 [c] -> c { class_instances = class_instances i }
346 _ -> i
347 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
349addIBC :: IBCWrite -> Idris ()
350addIBC ibc@(IBCDef n)
351 = do i <- getIState
352 when (notDef (ibc_write i)) $
353 putIState $ i { ibc_write = ibc : ibc_write i }
354 where notDef [] = True
355 notDef (IBCDef n': is) | n == n' = False
356 notDef (_ : is) = notDef is
357addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
359clearIBC :: Idris ()
360clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
362resetNameIdx :: Idris ()
363resetNameIdx = do i <- getIState
364 put (i { idris_nameIdx = (0, emptyContext) })
366-- Used to preserve sharing of names
367addNameIdx :: Name -> Idris (Int, Name)
368addNameIdx n = do i <- getIState
369 let (i', x) = addNameIdx' i n
370 return x
372addNameIdx' :: IState -> Name -> (IState, (Int, Name))
373addNameIdx' i n
374 = let idxs = snd (idris_nameIdx i) in
375 case lookupCtxt n idxs of
376 [x] -> (i, x)
377 _ -> let i' = fst (idris_nameIdx i) + 1 in
378 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
380getHdrs :: Codegen -> Idris [String]
381getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
383getImported :: Idris [FilePath]
384getImported = do i <- getIState; return (idris_imported i)
386setErrSpan :: FC -> Idris ()
387setErrSpan x = do i <- getIState;
388 case (errSpan i) of
389 Nothing -> putIState $ i { errSpan = Just x }
390 Just _ -> return ()
392clearErr :: Idris ()
393clearErr = do i <- getIState
394 putIState $ i { errSpan = Nothing }
396getSO :: Idris (Maybe String)
397getSO = do i <- getIState
398 return (compiled_so i)
400setSO :: Maybe String -> Idris ()
401setSO s = do i <- getIState
402 putIState $ (i { compiled_so = s })
404getIState :: Idris IState
405getIState = get
407putIState :: IState -> Idris ()
408putIState = put
410withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
411withContext ctx name dflt action = do
412 ist <- getIState
413 case lookupCtxt name (ctx ist) of
414 [x] -> action x
415 _ -> return dflt
417withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
418withContext_ ctx name action = withContext ctx name () action
420-- | A version of liftIO that puts errors into the exception type of the Idris monad
421runIO :: IO a -> Idris a
422runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
423-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
425getName :: Idris Int
426getName = do i <- getIState;
427 let idx = idris_name i;
428 putIState $ (i { idris_name = idx + 1 })
429 return idx
431-- InternalApp keeps track of the real function application for making case splits from, not the application the
432-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
433addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
434addInternalApp fp l t
435 = do i <- getIState
436 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
438getInternalApp :: FilePath -> Int -> Idris PTerm
439getInternalApp fp l = do i <- getIState
440 case lookup (fp, l) (idris_lineapps i) of
441 Just n' -> return n'
442 Nothing -> return Placeholder
443 -- TODO: What if it's not there?
445-- Pattern definitions are only used for coverage checking, so erase them
446-- when we're done
447clearOrigPats :: Idris ()
448clearOrigPats = do i <- get
449 let ps = idris_patdefs i
450 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
451 put (i { idris_patdefs = ps' })
453-- Erase types from Ps in the context (basically ending up with what's in
454-- the .ibc, which is all we need after all the analysis is done)
455clearPTypes :: Idris ()
456clearPTypes = do i <- get
457 let ctxt = tt_ctxt i
458 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
459 where pErase (CaseOp c t tys orig tot cds)
460 = CaseOp c t tys orig [] (pErase' cds)
461 pErase x = x
462 pErase' (CaseDefs _ (cs, c) _ rs)
463 = let c' = (cs, fmap pEraseType c) in
464 CaseDefs c' c' c' rs
466checkUndefined :: FC -> Name -> Idris ()
467checkUndefined fc n
468 = do i <- getContext
469 case lookupTy n i of
470 (_:_) -> throwError . Msg $ show fc ++ ":" ++
471 show n ++ " already defined"
472 _ -> return ()
474isUndefined :: FC -> Name -> Idris Bool
475isUndefined fc n
476 = do i <- getContext
477 case lookupTy n i of
478 (_:_) -> return False
479 _ -> return True
481setContext :: Context -> Idris ()
482setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
484updateContext :: (Context -> Context) -> Idris ()
485updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
487addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
488addConstraints fc (v, cs)
489 = do i <- getIState
490 let ctxt = tt_ctxt i
491 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
492 next_tvar = v }
493 let ics = zip cs (repeat fc) ++ idris_constraints i
494 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
496addDeferred = addDeferred' Ref
497addDeferredTyCon = addDeferred' (TCon 0 0)
499addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
500addDeferred' nt ns
501 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
502 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
503 i <- getIState
504 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
505 idris_metavars i }
506 where
507 -- 'tidyNames' is to generate user accessible names in case they are
508 -- needed in tactic scripts
509 tidyNames used (Bind (MN i x) b sc)
510 = let n' = uniqueNameSet (UN x) used in
511 Bind n' b $ tidyNames (S.insert n' used) sc
512 tidyNames used (Bind n b sc)
513 = let n' = uniqueNameSet n used in
514 Bind n' b $ tidyNames (S.insert n' used) sc
515 tidyNames used b = b
517solveDeferred :: Name -> Idris ()
518solveDeferred n = do i <- getIState
519 putIState $ i { idris_metavars =
520 filter (\(n', _) -> n/=n')
521 (idris_metavars i),
522 ibc_write =
523 filter (notMV n) (ibc_write i)
524 }
525 where notMV n (IBCMetavar n') = not (n == n')
526 notMV n _ = True
528getUndefined :: Idris [Name]
529getUndefined = do i <- getIState
530 return (map fst (idris_metavars i) \\ primDefs)
532isMetavarName :: Name -> IState -> Bool
533isMetavarName n ist
534 = case lookupNames n (tt_ctxt ist) of
535 (t:_) -> isJust $ lookup t (idris_metavars ist)
536 _ -> False
538getWidth :: Idris ConsoleWidth
539getWidth = fmap idris_consolewidth getIState
541setWidth :: ConsoleWidth -> Idris ()
542setWidth w = do ist <- getIState
543 put ist { idris_consolewidth = w }
545renderWidth :: Idris Int
546renderWidth = do iw <- getWidth
547 case iw of
548 InfinitelyWide -> return 100000000
549 ColsWide n -> return (max n 1)
550 AutomaticWidth -> runIO getScreenWidth
554type1Doc :: Doc OutputAnnotation
555type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
558isetPrompt :: String -> Idris ()
559isetPrompt p = do i <- getIState
560 case idris_outputmode i of
561 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
563-- | Tell clients how much was parsed and loaded
564isetLoadedRegion :: Idris ()
565isetLoadedRegion = do i <- getIState
566 let span = idris_parsedSpan i
567 case span of
568 Just fc ->
569 case idris_outputmode i of
570 IdeSlave n h ->
571 runIO . hPutStrLn h $
572 convSExp "set-loaded-region" fc n
573 Nothing -> return ()
575setLogLevel :: Int -> Idris ()
576setLogLevel l = do i <- getIState
577 let opts = idris_options i
578 let opt' = opts { opt_logLevel = l }
579 putIState $ i { idris_options = opt' }
581setCmdLine :: [Opt] -> Idris ()
582setCmdLine opts = do i <- getIState
583 let iopts = idris_options i
584 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
586getCmdLine :: Idris [Opt]
587getCmdLine = do i <- getIState
588 return (opt_cmdline (idris_options i))
590getDumpDefun :: Idris (Maybe FilePath)
591getDumpDefun = do i <- getIState
592 return $ findC (opt_cmdline (idris_options i))
593 where findC [] = Nothing
594 findC (DumpDefun x : _) = Just x
595 findC (_ : xs) = findC xs
597getDumpCases :: Idris (Maybe FilePath)
598getDumpCases = do i <- getIState
599 return $ findC (opt_cmdline (idris_options i))
600 where findC [] = Nothing
601 findC (DumpCases x : _) = Just x
602 findC (_ : xs) = findC xs
604logLevel :: Idris Int
605logLevel = do i <- getIState
606 return (opt_logLevel (idris_options i))
608setErrContext :: Bool -> Idris ()
609setErrContext t = do i <- getIState
610 let opts = idris_options i
611 let opts' = opts { opt_errContext = t }
612 putIState $ i { idris_options = opts' }
614errContext :: Idris Bool
615errContext = do i <- getIState
616 return (opt_errContext (idris_options i))
618getOptimise :: Idris [Optimisation]
619getOptimise = do i <- getIState
620 return (opt_optimise (idris_options i))
622setOptimise :: [Optimisation] -> Idris ()
623setOptimise newopts = do i <- getIState
624 let opts = idris_options i
625 let opts' = opts { opt_optimise = newopts }
626 putIState $ i { idris_options = opts' }
628addOptimise :: Optimisation -> Idris ()
629addOptimise opt = do opts <- getOptimise
630 setOptimise (nub (opt : opts))
632removeOptimise :: Optimisation -> Idris ()
633removeOptimise opt = do opts <- getOptimise
634 setOptimise ((nub opts) \\ [opt])
636-- Set appropriate optimisation set for the given level. We only have
637-- one optimisation that is configurable at the moment, however!
638setOptLevel :: Int -> Idris ()
639setOptLevel n | n <= 0 = setOptimise []
640setOptLevel 1 = setOptimise []
641setOptLevel 2 = setOptimise [PETransform]
642setOptLevel n | n >= 3 = setOptimise [PETransform]
644useREPL :: Idris Bool
645useREPL = do i <- getIState
646 return (opt_repl (idris_options i))
648setREPL :: Bool -> Idris ()
649setREPL t = do i <- getIState
650 let opts = idris_options i
651 let opt' = opts { opt_repl = t }
652 putIState $ i { idris_options = opt' }
654showOrigErr :: Idris Bool
655showOrigErr = do i <- getIState
656 return (opt_origerr (idris_options i))
658setShowOrigErr :: Bool -> Idris ()
659setShowOrigErr b = do i <- getIState
660 let opts = idris_options i
661 let opt' = opts { opt_origerr = b }
662 putIState $ i { idris_options = opt' }
664setAutoSolve :: Bool -> Idris ()
665setAutoSolve b = do i <- getIState
666 let opts = idris_options i
667 let opt' = opts { opt_autoSolve = b }
668 putIState $ i { idris_options = opt' }
670setNoBanner :: Bool -> Idris ()
671setNoBanner n = do i <- getIState
672 let opts = idris_options i
673 let opt' = opts { opt_nobanner = n }
674 putIState $ i { idris_options = opt' }
676getNoBanner :: Idris Bool
677getNoBanner = do i <- getIState
678 let opts = idris_options i
679 return (opt_nobanner opts)
681setQuiet :: Bool -> Idris ()
682setQuiet q = do i <- getIState
683 let opts = idris_options i
684 let opt' = opts { opt_quiet = q }
685 putIState $ i { idris_options = opt' }
687getQuiet :: Idris Bool
688getQuiet = do i <- getIState
689 let opts = idris_options i
690 return (opt_quiet opts)
692setCodegen :: Codegen -> Idris ()
693setCodegen t = do i <- getIState
694 let opts = idris_options i
695 let opt' = opts { opt_codegen = t }
696 putIState $ i { idris_options = opt' }
698codegen :: Idris Codegen
699codegen = do i <- getIState
700 return (opt_codegen (idris_options i))
702setOutputTy :: OutputType -> Idris ()
703setOutputTy t = do i <- getIState
704 let opts = idris_options i
705 let opt' = opts { opt_outputTy = t }
706 putIState $ i { idris_options = opt' }
708outputTy :: Idris OutputType
709outputTy = do i <- getIState
710 return $ opt_outputTy $ idris_options i
712setIdeSlave :: Bool -> Handle -> Idris ()
713setIdeSlave True h = do i <- getIState
714 putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }
715setIdeSlave False _ = return ()
717setTargetTriple :: String -> Idris ()
718setTargetTriple t = do i <- getIState
719 let opts = idris_options i
720 opt' = opts { opt_triple = t }
721 putIState $ i { idris_options = opt' }
723targetTriple :: Idris String
724targetTriple = do i <- getIState
725 return (opt_triple (idris_options i))
727setTargetCPU :: String -> Idris ()
728setTargetCPU t = do i <- getIState
729 let opts = idris_options i
730 opt' = opts { opt_cpu = t }
731 putIState $ i { idris_options = opt' }
733targetCPU :: Idris String
734targetCPU = do i <- getIState
735 return (opt_cpu (idris_options i))
737verbose :: Idris Bool
738verbose = do i <- getIState
739 return (opt_verbose (idris_options i))
741setVerbose :: Bool -> Idris ()
742setVerbose t = do i <- getIState
743 let opts = idris_options i
744 let opt' = opts { opt_verbose = t }
745 putIState $ i { idris_options = opt' }
747typeInType :: Idris Bool
748typeInType = do i <- getIState
749 return (opt_typeintype (idris_options i))
751setTypeInType :: Bool -> Idris ()
752setTypeInType t = do i <- getIState
753 let opts = idris_options i
754 let opt' = opts { opt_typeintype = t }
755 putIState $ i { idris_options = opt' }
757coverage :: Idris Bool
758coverage = do i <- getIState
759 return (opt_coverage (idris_options i))
761setCoverage :: Bool -> Idris ()
762setCoverage t = do i <- getIState
763 let opts = idris_options i
764 let opt' = opts { opt_coverage = t }
765 putIState $ i { idris_options = opt' }
767setIBCSubDir :: FilePath -> Idris ()
768setIBCSubDir fp = do i <- getIState
769 let opts = idris_options i
770 let opt' = opts { opt_ibcsubdir = fp }
771 putIState $ i { idris_options = opt' }
773valIBCSubDir :: IState -> Idris FilePath
774valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
776addImportDir :: FilePath -> Idris ()
777addImportDir fp = do i <- getIState
778 let opts = idris_options i
779 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
780 putIState $ i { idris_options = opt' }
782setImportDirs :: [FilePath] -> Idris ()
783setImportDirs fps = do i <- getIState
784 let opts = idris_options i
785 let opt' = opts { opt_importdirs = fps }
786 putIState $ i { idris_options = opt' }
788allImportDirs :: Idris [FilePath]
789allImportDirs = do i <- getIState
790 let optdirs = opt_importdirs (idris_options i)
791 return ("." : reverse optdirs)
793colourise :: Idris Bool
794colourise = do i <- getIState
795 return $ idris_colourRepl i
797setColourise :: Bool -> Idris ()
798setColourise b = do i <- getIState
799 putIState $ i { idris_colourRepl = b }
801impShow :: Idris Bool
802impShow = do i <- getIState
803 return (opt_showimp (idris_options i))
805setImpShow :: Bool -> Idris ()
806setImpShow t = do i <- getIState
807 let opts = idris_options i
808 let opt' = opts { opt_showimp = t }
809 putIState $ i { idris_options = opt' }
811setColour :: ColourType -> IdrisColour -> Idris ()
812setColour ct c = do i <- getIState
813 let newTheme = setColour' ct c (idris_colourTheme i)
814 putIState $ i { idris_colourTheme = newTheme }
815 where setColour' KeywordColour c t = t { keywordColour = c }
816 setColour' BoundVarColour c t = t { boundVarColour = c }
817 setColour' ImplicitColour c t = t { implicitColour = c }
818 setColour' FunctionColour c t = t { functionColour = c }
819 setColour' TypeColour c t = t { typeColour = c }
820 setColour' DataColour c t = t { dataColour = c }
821 setColour' PromptColour c t = t { promptColour = c }
822 setColour' PostulateColour c t = t { postulateColour = c }
824logLvl :: Int -> String -> Idris ()
825logLvl l str = do i <- getIState
826 let lvl = opt_logLevel (idris_options i)
827 when (lvl >= l) $
828 case idris_outputmode i of
829 RawOutput h -> do runIO $ hPutStrLn h str
830 IdeSlave n h ->
831 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
832 runIO . hPutStrLn h $ convSExp "log" good n
834cmdOptType :: Opt -> Idris Bool
835cmdOptType x = do i <- getIState
836 return $ x `elem` opt_cmdline (idris_options i)
838iLOG :: String -> Idris ()
839iLOG = logLvl 1
841noErrors :: Idris Bool
842noErrors = do i <- getIState
843 case errSpan i of
844 Nothing -> return True
845 _ -> return False
847setTypeCase :: Bool -> Idris ()
848setTypeCase t = do i <- getIState
849 let opts = idris_options i
850 let opt' = opts { opt_typecase = t }
851 putIState $ i { idris_options = opt' }
854-- Dealing with parameters
856expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
857 [Name] -> -- all names
858 [Name] -> -- names with no declaration
859 PTerm -> PTerm
860expandParams dec ps ns infs tm = en tm
861 where
862 -- if we shadow a name (say in a lambda binding) that is used in a call to
863 -- a lifted function, we need access to both names - once in the scope of the
864 -- binding and once to call the lifted functions. So we'll explicitly shadow
865 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
866 -- but we didn't...)
868 mkShadow (UN n) = MN 0 n
869 mkShadow (MN i n) = MN (i+1) n
870 mkShadow (NS x s) = NS (mkShadow x) s
872 en (PLam n t s)
873 | n `elem` (map fst ps ++ ns)
874 = let n' = mkShadow n in
875 PLam n' (en t) (en (shadow n n' s))
876 | otherwise = PLam n (en t) (en s)
877 en (PPi p n t s)
878 | n `elem` (map fst ps ++ ns)
879 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
880 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
881 | otherwise = PPi (enTacImp p) n (en t) (en s)
882 en (PLet n ty v s)
883 | n `elem` (map fst ps ++ ns)
884 = let n' = mkShadow n in
885 PLet n' (en ty) (en v) (en (shadow n n' s))
886 | otherwise = PLet n (en ty) (en v) (en s)
887 -- FIXME: Should only do this in a type signature!
888 en (PDPair f p (PRef f' n) t r)
889 | n `elem` (map fst ps ++ ns) && t /= Placeholder
890 = let n' = mkShadow n in
891 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
892 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
893 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
894 en (PTyped l r) = PTyped (en l) (en r)
895 en (PPair f p l r) = PPair f p (en l) (en r)
896 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
897 en (PAlternative a as) = PAlternative a (map en as)
898 en (PHidden t) = PHidden (en t)
899 en (PUnifyLog t) = PUnifyLog (en t)
900 en (PDisamb ds t) = PDisamb ds (en t)
901 en (PNoImplicits t) = PNoImplicits (en t)
902 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
903 en (PProof ts) = PProof (map (fmap en) ts)
904 en (PTactics ts) = PTactics (map (fmap en) ts)
906 en (PQuote (Var n))
907 | n `nselem` ns = PQuote (Var (dec n))
908 en (PApp fc (PInferRef fc' n) as)
909 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
910 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
911 en (PApp fc (PRef fc' n) as)
912 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
913 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
914 | n `nselem` ns = PApp fc (PRef fc' (dec n))
915 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
916 en (PAppBind fc (PRef fc' n) as)
917 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
918 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
919 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
920 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
921 en (PRef fc n)
922 | n `elem` infs = PApp fc (PInferRef fc (dec n))
923 (map (pexp . (PRef fc)) (map fst ps))
924 | n `nselem` ns = PApp fc (PRef fc (dec n))
925 (map (pexp . (PRef fc)) (map fst ps))
926 en (PInferRef fc n)
927 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
928 (map (pexp . (PRef fc)) (map fst ps))
929 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
930 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
931 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
932 en t = t
934 nselem x [] = False
935 nselem x (y : xs) | nseq x y = True
936 | otherwise = nselem x xs
938 nseq x y = nsroot x == nsroot y
940 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
941 enTacImp other = other
943expandParamsD :: Bool -> -- True = RHS only
944 IState ->
945 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
946expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
947 = if n `elem` ns && (not rhsonly)
948 then -- trace (show (n, expandParams dec ps ns ty)) $
949 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
950 else --trace (show (n, expandParams dec ps ns ty)) $
951 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
952expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
953 = if n `elem` ns && (not rhsonly)
954 then -- trace (show (n, expandParams dec ps ns ty)) $
955 PPostulate doc syn fc o (dec n) (piBind ps
956 (expandParams dec ps ns [] ty))
957 else --trace (show (n, expandParams dec ps ns ty)) $
958 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
959expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
960 = let n' = if n `elem` ns then dec n else n in
961 PClauses fc opts n' (map expandParamsC cs)
962 where
963 expandParamsC (PClause fc n lhs ws rhs ds)
964 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
965 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
966 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
967 n' = if n `elem` ns then dec n else n
968 -- names bound on the lhs should not be expanded on the rhs
969 ns' = removeBound lhs ns in
970 PClause fc n' lhs'
971 (map (expandParams dec ps'' ns' []) ws)
972 (expandParams dec ps'' ns' [] rhs)
973 (map (expandParamsD True ist dec ps'' ns') ds)
974 expandParamsC (PWith fc n lhs ws wval ds)
975 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
976 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
977 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
978 n' = if n `elem` ns then dec n else n
979 ns' = removeBound lhs ns in
980 PWith fc n' lhs'
981 (map (expandParams dec ps'' ns' []) ws)
982 (expandParams dec ps'' ns' [] wval)
983 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
984 updateps yn nm [] = []
985 updateps yn nm (((a, t), i):as)
986 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
987 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
989 removeBound lhs ns = ns \\ nub (bnames lhs)
991 bnames (PRef _ n) = [n]
992 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
993 bnames (PPair _ _ l r) = bnames l ++ bnames r
994 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
995 bnames _ = []
997-- | Expands parameters defined in parameter and where blocks inside of declarations
998expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
999 = PData doc argDocs syn fc co (expandPData pd)
1000 where
1001 -- just do the type decl, leave constructors alone (parameters will be
1002 -- added implicitly)
1003 expandPData (PDatadecl n ty cons)
1004 = if n `elem` ns
1005 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1006 (map econ cons)
1007 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1008 econ (doc, argDocs, n, t, fc, fs)
1009 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1010expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
1011 = if tn `elem` ns
1012 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1013 opts cdoc (dec cn) conty
1014 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1015 opts cdoc (dec cn) conty
1016 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1017expandParamsD rhs ist dec ps ns (PParams f params pds)
1018 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1019 (map (expandParamsD True ist dec ps ns) pds)
1020-- (map (expandParamsD ist dec ps ns) pds)
1021expandParamsD rhs ist dec ps ns (PMutual f pds)
1022 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1023expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
1024 = PClass doc info f
1025 (map (expandParams dec ps ns []) cs)
1027 (map (mapsnd (expandParams dec ps ns [])) params)
1028 pDocs
1029 (map (expandParamsD rhs ist dec ps ns) decls)
1030expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1031 = PInstance info f
1032 (map (expandParams dec ps ns []) cs)
1034 (map (expandParams dec ps ns []) params)
1035 (expandParams dec ps ns [] ty)
1036 cn
1037 (map (expandParamsD rhs ist dec ps ns) decls)
1038expandParamsD rhs ist dec ps ns d = d
1040mapsnd f (x, t) = (x, f t)
1042-- Calculate a priority for a type, for deciding elaboration order
1043-- * if it's just a type variable or concrete type, do it early (0)
1044-- * if there's only type variables and injective constructors, do it next (1)
1045-- * if there's a function type, next (2)
1046-- * finally, everything else (3)
1048getPriority :: IState -> PTerm -> Int
1049getPriority i tm = 1 -- pri tm
1050 where
1051 pri (PRef _ n) =
1052 case lookupP n (tt_ctxt i) of
1053 ((P (DCon _ _ _) _ _):_) -> 1
1054 ((P (TCon _ _) _ _):_) -> 1
1055 ((P Ref _ _):_) -> 1
1056 [] -> 0 -- must be locally bound, if it's not an error...
1057 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1058 pri (PTrue _ _) = 0
1059 pri (PRefl _ _) = 1
1060 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1061 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1062 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1063 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1064 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1065 pri (PTyped l r) = pri l
1066 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1067 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1068 pri (PAlternative a as) = maximum (map pri as)
1069 pri (PConstant _) = 0
1070 pri Placeholder = 1
1071 pri _ = 3
1074addStatics :: Name -> Term -> PTerm -> Idris ()
1075addStatics n tm ptm =
1076 do let (statics, dynamics) = initStatics tm ptm
1077 ist <- getIState
1078 let paramnames
1079 = nub $ case lookupCtxtExact n (idris_fninfo ist) of
1080 Just p -> getNamesFrom 0 (fn_params p) tm ++
1081 concatMap (getParamNames ist) (map snd statics)
1082 _ -> concatMap (getParamNames ist) (map snd statics)
1084 let stnames = nub $ concatMap freeArgNames (map snd statics)
1085 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
1086 \\ paramnames
1087 -- also get the arguments which are 'uniquely inferrable' from
1088 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1089 -- or parameters to the type of a static
1090 let statics' = nub $ map fst statics ++
1091 filter (\x -> not (elem x dnames)) stnames
1092 let stpos = staticList statics' tm
1093 i <- getIState
1094 when (not (null statics)) $
1095 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
1096 ++ showTmImpls ptm ++ "\n"
1097 ++ show statics ++ "\n" ++ show dynamics
1098 ++ "\n" ++ show paramnames
1099 ++ "\n" ++ show stpos
1100 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1101 addIBC (IBCStatic n)
1102 where
1103 initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)
1104 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1105 (static, (n, ty) : dynamic)
1106 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)
1107 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1108 if pstatic p == Static then ((n, ty) : static, dynamic)
1109 else if (not (searchArg p))
1110 then (static, (n, ty) : dynamic)
1111 else (static, dynamic)
1112 initStatics t pt = ([], [])
1114 getParamNames ist tm | (P _ n _ , args) <- unApply tm
1115 = case lookupCtxtExact n (idris_datatypes ist) of
1116 Just ti -> getNamePos 0 (param_pos ti) args
1117 Nothing -> []
1118 where getNamePos i ps [] = []
1119 getNamePos i ps (P _ n _ : as)
1120 | i `elem` ps = n : getNamePos (i + 1) ps as
1121 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
1122 getParamNames ist (Bind t (Pi (P _ n _) _) sc)
1123 = n : getParamNames ist sc
1124 getParamNames ist _ = []
1126 getNamesFrom i ps (Bind n (Pi _ _) sc)
1127 | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1128 | otherwise = getNamesFrom (i + 1) ps sc
1129 getNamesFrom i ps sc = []
1131 freeArgNames (Bind n (Pi ty _) sc)
1132 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1133 freeArgNames tm = let (_, args) = unApply tm in
1134 concatMap freeNames args
1136 -- if a name appears in a type class or tactic implicit index, it doesn't
1137 -- affect its 'uniquely inferrable' from a static status since these are
1138 -- resolved by searching.
1139 searchArg (Constraint _ _) = True
1140 searchArg (TacImp _ _ _) = True
1141 searchArg _ = False
1143 staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc
1144 staticList _ _ = []
1146-- Dealing with implicit arguments
1148-- Add some bound implicits to the using block if they aren't there already
1150addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1151addToUsing us [] = us
1152addToUsing us ((n, t) : ns)
1153 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1154 | otherwise = addToUsing us ns
1155 where impName (UImplicit n _) = Just n
1156 impName _ = Nothing
1158-- Add constraint bindings from using block
1160addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1161addUsingConstraints syn fc t
1162 = do ist <- get
1163 let ns = namesIn [] ist t
1164 let cs = getConstraints t -- check declared constraints
1165 let addconsts = uconsts \\ cs
1166 return (doAdd addconsts ns t)
1167 where uconsts = filter uconst (using syn)
1168 uconst (UConstraint _ _) = True
1169 uconst _ = False
1171 doAdd [] _ t = t
1172 -- if all of args in ns, then add it
1173 doAdd (UConstraint c args : cs) ns t
1174 | all (\n -> elem n ns) args
1175 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1176 (mkConst c args) (doAdd cs ns t)
1177 | otherwise = doAdd cs ns t
1179 mkConst c args = PApp fc (PRef fc c)
1180 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1182 getConstraints (PPi (Constraint _ _) _ c sc)
1183 = getcapp c ++ getConstraints sc
1184 getConstraints (PPi _ _ c sc) = getConstraints sc
1185 getConstraints _ = []
1187 getcapp (PApp _ (PRef _ c) args)
1188 = do ns <- mapM getName args
1189 return (UConstraint c ns)
1190 getcapp _ = []
1192 getName (PExp _ _ _ (PRef _ n)) = return n
1193 getName _ = []
1195-- Add implicit bindings from using block, and bind any missing names
1196addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1197addUsingImpls syn n fc t
1198 = do ist <- getIState
1199 let ns = implicitNamesIn (map iname uimpls) ist t
1200 let badnames = filter (\n -> not (implicitable n) &&
1201 n `notElem` (map iname uimpls)) ns
1202 when (not (null badnames)) $
1203 throwError (At fc (Elaborating "type of " n
1204 (NoSuchVariable (head badnames))))
1205 let cs = getArgnames t -- get already bound names
1206 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1207 -- if all names in the arguments of addconsts appear in ns,
1208 -- add the constraint implicitly
1209 return (bindFree ns (doAdd addimpls ns t))
1210 where uimpls = filter uimpl (using syn)
1211 uimpl (UImplicit _ _) = True
1212 uimpl _ = False
1214 iname (UImplicit n _) = n
1215 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1217 doAdd [] _ t = t
1218 -- if all of args in ns, then add it
1219 doAdd (UImplicit n ty : cs) ns t
1220 | elem n ns
1221 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1222 | otherwise = doAdd cs ns t
1224 -- bind the free names which weren't in the using block
1225 bindFree [] tm = tm
1226 bindFree (n:ns) tm
1227 | elem n (map iname uimpls) = bindFree ns tm
1228 | otherwise
1229 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1231 getArgnames (PPi _ n c sc)
1232 = n : getArgnames sc
1233 getArgnames _ = []
1235-- Given the original type and the elaborated type, return the implicitness
1236-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1238getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1239getUnboundImplicits i t tm = getImps t (collectImps tm)
1240 where collectImps (PPi p n t sc)
1241 = (n, (p, t)) : collectImps sc
1242 collectImps _ = []
1244 getImps (Bind n (Pi t _) sc) imps
1245 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1246 where
1247 argInfo n (Imp opt _ _) t'
1248 = (True, PImp (getPriority i t') True opt n t')
1249 argInfo n (Exp opt _ _) t'
1250 = (InaccessibleArg `elem` opt,
1251 PExp (getPriority i t') opt n t')
1252 argInfo n (Constraint opt _) t'
1253 = (InaccessibleArg `elem` opt,
1254 PConstraint 10 opt n t')
1255 argInfo n (TacImp opt _ scr) t'
1256 = (InaccessibleArg `elem` opt,
1257 PTacImplicit 10 opt n scr t')
1258 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps
1259 where impBind n t = (True, PImp 1 True [] n Placeholder)
1260 getImps sc tm = []
1262-- Add implicit Pi bindings for any names in the term which appear in an
1263-- argument position.
1265-- This has become a right mess already. Better redo it some time...
1266-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1267-- a couple of places which use it. Clean them up!
1268implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1269implicit info syn n ptm = implicit' info syn [] n ptm
1271implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1272implicit' info syn ignore n ptm
1273 = do i <- getIState
1274 let (tm', impdata) = implicitise syn ignore i ptm
1275 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1276-- let (tm'', spos) = findStatics i tm'
1277 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1278 addIBC (IBCImp n)
1279 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1280-- i <- get
1281-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1282 return tm'
1283 where
1284 -- Detect unknown names in default arguments and throw error if found.
1285 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1286 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1288 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1289 notFoundInDefault kns (PTacImplicit _ _ n script _)
1290 = do i <- getIState
1291 case notFound kns (namesIn [] i script) of
1292 Nothing -> return (n:kns)
1293 Just name -> throwError (NoSuchVariable name)
1294 notFoundInDefault kns p = return ((pname p):kns)
1296 notFound :: [Name] -> [Name] -> Maybe Name
1297 notFound kns [] = Nothing
1298 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1299 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1301implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1302implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1303 let (declimps, ns') = execState (imps True [] tm) ([], [])
1304 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1305 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1306 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1307 if null ns
1308 then (tm, reverse declimps)
1309 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1310 where
1311 uvars = map ipair (filter uimplicit (using syn))
1312 pvars = syn_params syn
1314 inUsing n = n `elem` map fst uvars
1316 ipair (UImplicit x y) = (x, y)
1317 uimplicit (UImplicit _ _) = True
1318 uimplicit _ = False
1320 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1321 | otherwise = x : dropAll xs ys
1322 dropAll [] ys = []
1324 -- Find names in argument position in a type, suitable for implicit
1325 -- binding
1326 -- Not the function position, but do everything else...
1327 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1328 implNamesIn uv t = namesIn uv ist t
1330 imps top env (PApp _ f as)
1331 = do (decls, ns) <- get
1332 let isn = concatMap (namesIn uvars ist) (map getTm as)
1333 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1334 imps top env (PPi (Imp l _ _) n ty sc)
1335 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1336 (decls , ns) <- get
1337 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1338 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1339 imps True (n:env) sc
1340 imps top env (PPi (Exp l _ _) n ty sc)
1341 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1342 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1343 _ -> [])
1344 (decls, ns) <- get -- ignore decls in HO types
1345 put (PExp (getPriority ist ty) l n Placeholder : decls,
1346 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1347 imps True (n:env) sc
1348 imps top env (PPi (Constraint l _) n ty sc)
1349 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1350 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1351 _ -> [])
1352 (decls, ns) <- get -- ignore decls in HO types
1353 put (PConstraint 10 l n Placeholder : decls,
1354 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1355 imps True (n:env) sc
1356 imps top env (PPi (TacImp l _ scr) n ty sc)
1357 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1358 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1359 _ -> [])
1360 (decls, ns) <- get -- ignore decls in HO types
1361 put (PTacImplicit 10 l n scr Placeholder : decls,
1362 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1363 imps True (n:env) sc
1364 imps top env (PEq _ _ _ l r)
1365 = do (decls, ns) <- get
1366 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1367 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1368 imps top env (PRewrite _ l r _)
1369 = do (decls, ns) <- get
1370 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1371 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1372 imps top env (PTyped l r)
1373 = imps top env l
1374 imps top env (PPair _ _ l r)
1375 = do (decls, ns) <- get
1376 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1377 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1378 imps top env (PDPair _ _ (PRef _ n) t r)
1379 = do (decls, ns) <- get
1380 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1381 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1382 imps top env (PDPair _ _ l t r)
1383 = do (decls, ns) <- get
1384 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1385 namesIn uvars ist r
1386 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1387 imps top env (PAlternative a as)
1388 = do (decls, ns) <- get
1389 let isn = concatMap (namesIn uvars ist) as
1390 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1391 imps top env (PLam n ty sc)
1392 = do imps False env ty
1393 imps False (n:env) sc
1394 imps top env (PHidden tm) = imps False env tm
1395 imps top env (PUnifyLog tm) = imps False env tm
1396 imps top env (PNoImplicits tm) = imps False env tm
1397 imps top env _ = return ()
1399 pibind using [] sc = sc
1400 pibind using (n:ns) sc
1401 = case lookup n using of
1402 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1403 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1404 (pibind using ns sc)
1406-- Add implicit arguments in function calls
1407addImplPat :: IState -> PTerm -> PTerm
1408addImplPat = addImpl' True [] []
1410addImplBound :: IState -> [Name] -> PTerm -> PTerm
1411addImplBound ist ns = addImpl' False ns [] ist
1413addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1414addImplBoundInf ist ns inf = addImpl' False ns inf ist
1416-- | Add the implicit arguments to applications in the term
1417addImpl :: IState -> PTerm -> PTerm
1418addImpl = addImpl' False [] []
1420-- TODO: in patterns, don't add implicits to function names guarded by constructors
1421-- and *not* inside a PHidden
1423addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1424addImpl' inpat env infns ist ptm
1425 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1426 where
1427 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1428 ai qq env ds (PRef fc f)
1429 | f `elem` infns = PInferRef fc f
1430 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1431 ai qq env ds (PHidden (PRef fc f))
1432 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1433 ai qq env ds (PEq fc lt rt l r)
1434 = let lt' = ai qq env ds lt
1435 rt' = ai qq env ds rt
1436 l' = ai qq env ds l
1437 r' = ai qq env ds r in
1438 PEq fc lt' rt' l' r'
1439 ai qq env ds (PRewrite fc l r g)
1440 = let l' = ai qq env ds l
1441 r' = ai qq env ds r
1442 g' = fmap (ai qq env ds) g in
1443 PRewrite fc l' r' g'
1444 ai qq env ds (PTyped l r)
1445 = let l' = ai qq env ds l
1446 r' = ai qq env ds r in
1447 PTyped l' r'
1448 ai qq env ds (PPair fc p l r)
1449 = let l' = ai qq env ds l
1450 r' = ai qq env ds r in
1451 PPair fc p l' r'
1452 ai qq env ds (PDPair fc p l t r)
1453 = let l' = ai qq env ds l
1454 t' = ai qq env ds t
1455 r' = ai qq env ds r in
1456 PDPair fc p l' t' r'
1457 ai qq env ds (PAlternative a as)
1458 = let as' = map (ai qq env ds) as in
1459 PAlternative a as'
1460 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1461 ai qq env ds (PApp fc (PInferRef _ f) as)
1462 = let as' = map (fmap (ai qq env ds)) as in
1463 PApp fc (PInferRef fc f) as'
1464 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1465 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1466 | not (f `elem` map fst env)
1467 = let as' = map (fmap (ai qq env ds)) as in
1468 handleErr $ aiFn inpat False qq ist fc f ds as'
1469 | Just (Just ty) <- lookup f env =
1470 let as' = map (fmap (ai qq env ds)) as
1471 arity = getPArity ty in
1472 mkPApp fc arity ftm as'
1473 ai qq env ds (PApp fc f as)
1474 = let f' = ai qq env ds f
1475 as' = map (fmap (ai qq env ds)) as in
1476 mkPApp fc 1 f' as'
1477 ai qq env ds (PCase fc c os)
1478 = let c' = ai qq env ds c in
1479 -- leave os alone, because they get lifted into a new pattern match
1480 -- definition which is passed through addImpl again with more scope
1481 -- information
1482 PCase fc c' os
1483 ai qq env ds (PLam n ty sc)
1484 = let ty' = ai qq env ds ty
1485 sc' = ai qq ((n, Just ty):env) ds sc in
1486 PLam n ty' sc'
1487 ai qq env ds (PLet n ty val sc)
1488 = let ty' = ai qq env ds ty
1489 val' = ai qq env ds val
1490 sc' = ai qq ((n, Just ty):env) ds sc in
1491 PLet n ty' val' sc'
1492 ai qq env ds (PPi p n ty sc)
1493 = let ty' = ai qq env ds ty
1494 sc' = ai qq ((n, Just ty):env) ds sc in
1495 PPi p n ty' sc'
1496 ai qq env ds (PGoal fc r n sc)
1497 = let r' = ai qq env ds r
1498 sc' = ai qq ((n, Nothing):env) ds sc in
1499 PGoal fc r' n sc'
1500 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1501 -- Don't do PProof or PTactics since implicits get added when scope is
1502 -- properly known in ElabTerm.runTac
1503 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1504 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1505 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1506 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1507 (fmap (ai True env ds) g)
1508 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1509 ai qq env ds tm = tm
1511 handleErr (Left err) = PElabError err
1512 handleErr (Right x) = x
1514-- if in a pattern, and there are no arguments, and there's no possible
1515-- names with zero explicit arguments, don't add implicits.
1517aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1518aiFn inpat True qq ist fc f ds []
1519 = case lookupDef f (tt_ctxt ist) of
1520 [] -> Right $ PPatvar fc f
1521 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1522 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1523 if (not (vname f) || tcname f
1524 || any (conCaf (tt_ctxt ist)) ialts)
1525-- any constructor alts || any allImp ialts))
1526 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1527 else Right $ PPatvar fc f
1528 where imp (PExp _ _ _ _) = False
1529 imp _ = True
1530-- allImp [] = False
1531 allImp xs = all imp xs
1532 constructor (TyDecl (DCon _ _ _) _) = True
1533 constructor _ = False
1535 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1537 vname (UN n) = True -- non qualified
1538 vname _ = False
1540aiFn inpat expat qq ist fc f ds as
1541 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1542aiFn inpat expat qq ist fc f ds as
1543 -- This is where namespaces get resolved by adding PAlternative
1544 = do let ns = lookupCtxtName f (idris_implicits ist)
1545 let nh = filter (\(n, _) -> notHidden n) ns
1546 let ns' = case trimAlts ds nh of
1547 [] -> nh
1548 x -> x
1549 case ns' of
1550 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1551 [] -> if f `elem` (map fst (idris_metavars ist))
1552 then Right $ PApp fc (PRef fc f) as
1553 else Right $ mkPApp fc (length as) (PRef fc f) as
1554 alts -> Right $
1555 PAlternative True $
1556 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1557 (insertImpl ns as)) alts
1558 where
1559 trimAlts [] alts = alts
1560 trimAlts ns alts
1561 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1563 nspace (NS _ s) = s
1564 nspace _ = []
1566 notHidden n = case getAccessibility n of
1567 Hidden -> False
1568 _ -> True
1570 getAccessibility n
1571 = case lookupDefAcc n False (tt_ctxt ist) of
1572 [(n,t)] -> t
1573 _ -> Public
1575 insertImpl :: [PArg] -> [PArg] -> [PArg]
1576 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1578 exp (PExp _ _ _ _) = True
1579 exp (PConstraint _ _ _ _) = True
1580 exp _ = False
1582 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1583 -> [PArg] -- parameters
1584 -> [PArg] -- explicit arguments
1585 -> [PArg] -- implicits given
1586 -> [PArg]
1587 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1588 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1589 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1590 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1591 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1592 let rtc = PResolveTC fc in
1593 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1594 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1595 case find n imps [] of
1596 Just (tm, imps') ->
1597 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1598 Nothing ->
1599 PImp p True l n Placeholder :
1600 insImpAcc (M.insert n Placeholder pnas) ps given imps
1601 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1602 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1603 case find n imps [] of
1604 Just (tm, imps') ->
1605 PTacImplicit p l n sc tm :
1606 insImpAcc (M.insert n tm pnas) ps given imps'
1607 Nothing ->
1608 if inpat
1609 then PTacImplicit p l n sc Placeholder :
1610 insImpAcc (M.insert n Placeholder pnas) ps given imps
1611 else PTacImplicit p l n sc sc :
1612 insImpAcc (M.insert n sc pnas) ps given imps
1613 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1614 -- TODO: report here, and prune alternatives
1615 insImpAcc _ _ given imps = given ++ imps
1617 find n [] acc = Nothing
1618 find n (PImp _ _ _ n' t : gs) acc
1619 | n == n' = Just (t, reverse acc ++ gs)
1620 find n (PTacImplicit _ _ n' _ t : gs) acc
1621 | n == n' = Just (t, reverse acc ++ gs)
1622 find n (g : gs) acc = find n gs (g : acc)
1624-- replace non-linear occurrences with _
1625-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1626-- it is hard to get right!
1628stripLinear :: IState -> PTerm -> PTerm
1629stripLinear i tm = evalState (sl tm) [] where
1630 sl :: PTerm -> State [Name] PTerm
1631 sl (PRef fc f)
1632 | (_:_) <- lookupTy f (tt_ctxt i)
1633 = return $ PRef fc f
1634 | otherwise = do ns <- get
1635 if (f `elem` ns)
1636 then return Placeholder
1637 else do put (f : ns)
1638 return (PRef fc f)
1639 sl (PPatvar fc f)
1640 = do ns <- get
1641 if (f `elem` ns)
1642 then return Placeholder
1643 else do put (f : ns)
1644 return (PPatvar fc f)
1645 sl t@(PAlternative _ (a : as)) = do sl a
1646 return t
1647 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1648 args' <- mapM slA args
1649 return $ PApp fc fn args'
1650 where slA (PImp p m l n t) = do t' <- sl t
1651 return $ PImp p m l n t'
1652 slA (PExp p l n t) = do t' <- sl t
1653 return $ PExp p l n t'
1654 slA (PConstraint p l n t)
1655 = do t' <- sl t
1656 return $ PConstraint p l n t'
1657 slA (PTacImplicit p l n sc t)
1658 = do t' <- sl t
1659 return $ PTacImplicit p l n sc t'
1660 sl x = return x
1662-- Remove functions which aren't applied to anything, which must then
1663-- be resolved by unification. Assume names resolved and alternatives
1664-- filled in (so no ambiguity).
1666stripUnmatchable :: IState -> PTerm -> PTerm
1667stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1668 su :: PTerm -> PTerm
1669 su (PRef fc f)
1670 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)
1671 = Placeholder
1672 su (PApp fc fn args)
1673 = PApp fc fn (fmap (fmap su) args)
1674 su (PAlternative b alts)
1675 = let alts' = filter (/= Placeholder) (map su alts) in
1676 if null alts' then Placeholder
1677 else PAlternative b alts'
1678 su (PPair fc p l r) = PPair fc p (su l) (su r)
1679 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1680 su t = t
1681stripUnmatchable i tm = tm
1683mkPApp fc a f [] = f
1684mkPApp fc a f as = let rest = drop a as in
1685 appRest fc (PApp fc f (take a as)) rest
1686 where
1687 appRest fc f [] = f
1688 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1690-- Find 'static' argument positions
1691-- (the declared ones, plus any names in argument position in the declared
1692-- statics)
1693-- FIXME: It's possible that this really has to happen after elaboration
1695findStatics :: IState -> PTerm -> (PTerm, [Bool])
1696findStatics ist tm = trace (show tm) $
1697 let (ns, ss) = fs tm in
1698 runState (pos ns ss tm) []
1699 where fs (PPi p n t sc)
1700 | Static <- pstatic p
1701 = let (ns, ss) = fs sc in
1702 (namesIn [] ist t : ns, n : ss)
1703 | otherwise = let (ns, ss) = fs sc in
1704 (ns, ss)
1705 fs _ = ([], [])
1707 inOne n ns = length (filter id (map (elem n) ns)) == 1
1709 pos ns ss (PPi p n t sc)
1710 | elem n ss = do sc' <- pos ns ss sc
1711 spos <- get
1712 put (True : spos)
1713 return (PPi (p { pstatic = Static }) n t sc')
1714 | otherwise = do sc' <- pos ns ss sc
1715 spos <- get
1716 put (False : spos)
1717 return (PPi p n t sc')
1718 pos ns ss t = return t
1720-- for 6.12/7 compatibility
1721data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1723instance Applicative (EitherErr a) where
1724 pure = return
1725 (<*>) = ap
1727instance Monad (EitherErr a) where
1728 return = RightOK
1730 (LeftErr e) >>= k = LeftErr e
1731 RightOK v >>= k = k v
1733toEither (LeftErr e) = Left e
1734toEither (RightOK ho) = Right ho
1736-- syntactic match of a against b, returning pair of variables in a
1737-- and what they match. Returns the pair that failed if not a match.
1739matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1740matchClause = matchClause' False
1742matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1743matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1744 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1746 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1747 fullApp x = x
1749 match' x y = match (fullApp x) (fullApp y)
1750 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1751 | fi == txt "fromInteger" && b == txt "builtins",
1752 PConstant (I _) <- getTm x = match (getTm x) x'
1753 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1754 | fi == txt "fromInteger" && b == txt "builtins",
1755 PConstant (I _) <- getTm x = match (getTm x) x'
1756 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1757 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1758 match (PApp _ f args) (PApp _ f' args')
1759 | length args == length args'
1760 = do mf <- match' f f'
1761 ms <- zipWithM matchArg args args'
1762 return (mf ++ concat ms)
1763 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1764 match (PPatvar f n) xr = match (PRef f n) xr
1765 match xr (PPatvar f n) = match xr (PRef f n)
1766 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1767 match (PRef _ n) tm@(PRef _ n')
1768 | n == n' && not names &&
1769 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1770 || tm == Placeholder)
1771 = return [(n, tm)]
1772 -- if one namespace is missing, drop the other
1773 | n == n' || n == dropNS n' || dropNS n == n' = return []
1774 where dropNS (NS n _) = n
1775 dropNS n = n
1776 match (PRef _ n) tm
1777 | not names && (not (isConName n (tt_ctxt i) ||
1778 isFnName n (tt_ctxt i)) || tm == Placeholder)
1779 = return [(n, tm)]
1780 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1781 = do ml <- match' l l'
1782 mr <- match' r r'
1783 return (ml ++ mr)
1784 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1785 = do ml <- match' l l'
1786 mr <- match' r r'
1787 return (ml ++ mr)
1788 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1789 mr <- match r r'
1790 return (ml ++ mr)
1791 match (PTyped l r) x = match l x
1792 match x (PTyped l r) = match x l
1793 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1794 mr <- match' r r'
1795 return (ml ++ mr)
1796 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1797 mt <- match' t t'
1798 mr <- match' r r'
1799 return (ml ++ mt ++ mr)
1800 match (PAlternative a as) (PAlternative a' as')
1801 = do ms <- zipWithM match' as as'
1802 return (concat ms)
1803 match a@(PAlternative _ as) b
1804 = do let ms = zipWith match' as (repeat b)
1805 case (rights (map toEither ms)) of
1806 (x: _) -> return x
1807 _ -> LeftErr (a, b)
1808 match (PCase _ _ _) _ = return [] -- lifted out
1809 match (PMetavar _) _ = return [] -- modified
1810 match (PInferRef _ _) _ = return [] -- modified
1811 match (PQuote _) _ = return []
1812 match (PProof _) _ = return []
1813 match (PTactics _) _ = return []
1814 match (PRefl _ _) (PRefl _ _) = return []
1815 match (PResolveTC _) (PResolveTC _) = return []
1816 match (PTrue _ _) (PTrue _ _) = return []
1817 match (PReturn _) (PReturn _) = return []
1818 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1819 ms <- match' s s'
1820 return (mt ++ ms)
1821 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1822 ms <- match' s s'
1823 return (mt ++ ms)
1824 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1825 mty <- match' ty ty'
1826 ms <- match' s s'
1827 return (mt ++ mty ++ ms)
1828 match (PHidden x) (PHidden y) = match' x y
1829 match (PUnifyLog x) y = match' x y
1830 match x (PUnifyLog y) = match' x y
1831 match (PNoImplicits x) y = match' x y
1832 match x (PNoImplicits y) = match' x y
1833 match Placeholder _ = return []
1834 match _ Placeholder = return []
1835 match (PResolveTC _) _ = return []
1836 match a b | a == b = return []
1837 | otherwise = LeftErr (a, b)
1839 checkRpts (RightOK ms) = check ms where
1840 check ((n,t):xs)
1841 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1842 then Left (t, t')
1843 else check xs
1844 check (_:xs) = check xs
1845 check [] = Right ms
1846 checkRpts (LeftErr x) = Left x
1848substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1849substMatches ms = substMatchesShadow ms []
1851substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1852substMatchesShadow [] shs t = t
1853substMatchesShadow ((n,tm):ns) shs t
1854 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1856substMatch :: Name -> PTerm -> PTerm -> PTerm
1857substMatch n = substMatchShadow n []
1859substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1860substMatchShadow n shs tm t = sm shs t where
1861 sm xs (PRef _ n') | n == n' = tm
1862 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1863 sm xs (PPi p x t sc)
1864 | x `elem` xs
1865 = let x' = nextName x in
1866 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1867 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1868 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1869 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1870 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1871 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1872 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1873 (fmap (sm xs) tm)
1874 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1875 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1876 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1877 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1878 sm xs (PHidden x) = PHidden (sm xs x)
1879 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1880 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1881 sm xs x = x
1883 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1884 fullApp x = x
1886shadow :: Name -> Name -> PTerm -> PTerm
1887shadow n n' t = sm t where
1888 sm (PRef fc x) | n == x = PRef fc n'
1889 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1890 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1891 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1892 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1893 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1894 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1895 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1896 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1897 sm (PTyped x y) = PTyped (sm x) (sm y)
1898 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1899 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1900 sm (PAlternative a as) = PAlternative a (map sm as)
1901 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1902 sm (PProof ts) = PProof (map (fmap sm) ts)
1903 sm (PHidden x) = PHidden (sm x)
1904 sm (PUnifyLog x) = PUnifyLog (sm x)
1905 sm (PNoImplicits x) = PNoImplicits (sm x)
1906 sm x = x
1908-- Rename any binders which are repeated (so that we don't have to mess
1909-- about with shadowing anywhere else).
1911mkUniqueNames :: [Name] -> PTerm -> PTerm
1912mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
1913 inScope :: S.Set Name
1914 inScope = S.fromList $ boundNamesIn tm
1916 mkUniqA arg = do t' <- mkUniq (getTm arg)
1917 return (arg { getTm = t' })
1919 -- Initialise the unique name with the environment length (so we're not
1920 -- looking for too long...)
1921 initN (UN n) l = UN $ txt (str n ++ show l)
1922 initN (MN i s) l = MN (i+l) s
1923 initN n l = n
1925 -- FIXME: Probably ought to do this for completeness! It's fine as
1926 -- long as there are no bindings inside tactics though.
1927 mkUniqT tac = return tac
1929 mkUniq :: PTerm -> State (S.Set Name) PTerm
1930 mkUniq (PLam n ty sc)
1931 = do env <- get
1932 (n', sc') <-
1933 if n `S.member` env
1934 then do let n' = uniqueNameSet (initN n (S.size env))
1935 (S.union env inScope)
1936 return (n', shadow n n' sc)
1937 else return (n, sc)
1938 put (S.insert n' env)
1939 ty' <- mkUniq ty
1940 sc'' <- mkUniq sc'
1941 return $! PLam n' ty' sc''
1942 mkUniq (PPi p n ty sc)
1943 = do env <- get
1944 (n', sc') <-
1945 if n `S.member` env
1946 then do let n' = uniqueNameSet (initN n (S.size env))
1947 (S.union env inScope)
1948 return (n', shadow n n' sc)
1949 else return (n, sc)
1950 put (S.insert n' env)
1951 ty' <- mkUniq ty
1952 sc'' <- mkUniq sc'
1953 return $! PPi p n' ty' sc''
1954 mkUniq (PLet n ty val sc)
1955 = do env <- get
1956 (n', sc') <-
1957 if n `S.member` env
1958 then do let n' = uniqueNameSet (initN n (S.size env))
1959 (S.union env inScope)
1960 return (n', shadow n n' sc)
1961 else return (n, sc)
1962 put (S.insert n' env)
1963 ty' <- mkUniq ty; val' <- mkUniq val
1964 sc'' <- mkUniq sc'
1965 return $! PLet n' ty' val' sc''
1966 mkUniq (PApp fc t args)
1967 = do t' <- mkUniq t
1968 args' <- mapM mkUniqA args
1969 return $! PApp fc t' args'
1970 mkUniq (PAppBind fc t args)
1971 = do t' <- mkUniq t
1972 args' <- mapM mkUniqA args
1973 return $! PAppBind fc t' args'
1974 mkUniq (PCase fc t alts)
1975 = do t' <- mkUniq t
1976 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1977 return (x', y')) alts
1978 return $! PCase fc t' alts'
1979 mkUniq (PPair fc p l r)
1980 = do l' <- mkUniq l; r' <- mkUniq r
1981 return $! PPair fc p l' r'
1982 mkUniq (PDPair fc p (PRef fc' n) t sc)
1983 | t /= Placeholder
1984 = do env <- get
1985 (n', sc') <- if n `S.member` env
1986 then do let n' = uniqueNameSet n (S.union env inScope)
1987 return (n', shadow n n' sc)
1988 else return (n, sc)
1989 put (S.insert n' env)
1990 t' <- mkUniq t
1991 sc'' <- mkUniq sc'
1992 return $! PDPair fc p (PRef fc' n') t' sc''
1993 mkUniq (PDPair fc p l t r)
1994 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1995 return $! PDPair fc p l' t' r'
1996 mkUniq (PAlternative b as)
1997 = liftM (PAlternative b) (mapM mkUniq as)
1998 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1999 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
2000 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
2001 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2002 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2003 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2004 mkUniq t = return t