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