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