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