git.iko.soy/Idris-dev
on 783ddc3 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1944 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 t tm = getImps t (collectImps tm)
1182 where collectImps (PPi p n t sc)
1183 = (n, (p, t)) : collectImps sc
1184 collectImps _ = []
1186 getImps (Bind n (Pi t) sc) imps
1187 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1188 where
1189 argInfo n (Imp opt _ _) t'
1190 = (True, PImp (getPriority i t') True opt n t')
1191 argInfo n (Exp opt _ _) t'
1192 = (InaccessibleArg `elem` opt,
1193 PExp (getPriority i t') opt n t')
1194 argInfo n (Constraint opt _) t'
1195 = (InaccessibleArg `elem` opt,
1196 PConstraint 10 opt n t')
1197 argInfo n (TacImp opt _ scr) t'
1198 = (InaccessibleArg `elem` opt,
1199 PTacImplicit 10 opt n scr t')
1200 getImps (Bind n (Pi t) sc) imps = impBind n t : getImps sc imps
1201 where impBind n t = (True, PImp 1 True [] n Placeholder)
1202 getImps sc tm = []
1204-- Add implicit Pi bindings for any names in the term which appear in an
1205-- argument position.
1207-- This has become a right mess already. Better redo it some time...
1208-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1209-- a couple of places which use it. Clean them up!
1210implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1211implicit info syn n ptm = implicit' info syn [] n ptm
1213implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1214implicit' info syn ignore n ptm
1215 = do i <- getIState
1216 let (tm', impdata) = implicitise syn ignore i ptm
1217 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1218-- let (tm'', spos) = findStatics i tm'
1219 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1220 addIBC (IBCImp n)
1221 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1222-- i <- get
1223-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1224 return tm'
1225 where
1226 -- Detect unknown names in default arguments and throw error if found.
1227 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1228 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1230 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1231 notFoundInDefault kns (PTacImplicit _ _ n script _)
1232 = do i <- getIState
1233 case notFound kns (namesIn [] i script) of
1234 Nothing -> return (n:kns)
1235 Just name -> throwError (NoSuchVariable name)
1236 notFoundInDefault kns p = return ((pname p):kns)
1238 notFound :: [Name] -> [Name] -> Maybe Name
1239 notFound kns [] = Nothing
1240 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1241 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1243implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1244implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1245 let (declimps, ns') = execState (imps True [] tm) ([], [])
1246 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1247 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1248 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1249 if null ns
1250 then (tm, reverse declimps)
1251 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1252 where
1253 uvars = map ipair (filter uimplicit (using syn))
1254 pvars = syn_params syn
1256 inUsing n = n `elem` map fst uvars
1258 ipair (UImplicit x y) = (x, y)
1259 uimplicit (UImplicit _ _) = True
1260 uimplicit _ = False
1262 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1263 | otherwise = x : dropAll xs ys
1264 dropAll [] ys = []
1266 -- Find names in argument position in a type, suitable for implicit
1267 -- binding
1268 -- Not the function position, but do everything else...
1269 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1270 implNamesIn uv t = namesIn uv ist t
1272 imps top env (PApp _ f as)
1273 = do (decls, ns) <- get
1274 let isn = concatMap (namesIn uvars ist) (map getTm as)
1275 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1276 imps top env (PPi (Imp l _ _) n ty sc)
1277 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1278 (decls , ns) <- get
1279 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1280 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1281 imps True (n:env) sc
1282 imps top env (PPi (Exp l _ _) n ty sc)
1283 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1284 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1285 _ -> [])
1286 (decls, ns) <- get -- ignore decls in HO types
1287 put (PExp (getPriority ist ty) l n Placeholder : decls,
1288 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1289 imps True (n:env) sc
1290 imps top env (PPi (Constraint l _) n ty sc)
1291 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1292 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1293 _ -> [])
1294 (decls, ns) <- get -- ignore decls in HO types
1295 put (PConstraint 10 l n Placeholder : decls,
1296 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1297 imps True (n:env) sc
1298 imps top env (PPi (TacImp l _ scr) n ty sc)
1299 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1300 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1301 _ -> [])
1302 (decls, ns) <- get -- ignore decls in HO types
1303 put (PTacImplicit 10 l n scr Placeholder : decls,
1304 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1305 imps True (n:env) sc
1306 imps top env (PEq _ _ _ l r)
1307 = do (decls, ns) <- get
1308 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1309 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1310 imps top env (PRewrite _ l r _)
1311 = do (decls, ns) <- get
1312 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1313 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1314 imps top env (PTyped l r)
1315 = imps top env l
1316 imps top env (PPair _ _ l r)
1317 = do (decls, ns) <- get
1318 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1319 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1320 imps top env (PDPair _ _ (PRef _ n) t r)
1321 = do (decls, ns) <- get
1322 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1323 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1324 imps top env (PDPair _ _ l t r)
1325 = do (decls, ns) <- get
1326 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1327 namesIn uvars ist r
1328 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1329 imps top env (PAlternative a as)
1330 = do (decls, ns) <- get
1331 let isn = concatMap (namesIn uvars ist) as
1332 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1333 imps top env (PLam n ty sc)
1334 = do imps False env ty
1335 imps False (n:env) sc
1336 imps top env (PHidden tm) = imps False env tm
1337 imps top env (PUnifyLog tm) = imps False env tm
1338 imps top env (PNoImplicits tm) = imps False env tm
1339 imps top env _ = return ()
1341 pibind using [] sc = sc
1342 pibind using (n:ns) sc
1343 = case lookup n using of
1344 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1345 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1346 (pibind using ns sc)
1348-- Add implicit arguments in function calls
1349addImplPat :: IState -> PTerm -> PTerm
1350addImplPat = addImpl' True [] []
1352addImplBound :: IState -> [Name] -> PTerm -> PTerm
1353addImplBound ist ns = addImpl' False ns [] ist
1355addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1356addImplBoundInf ist ns inf = addImpl' False ns inf ist
1358-- | Add the implicit arguments to applications in the term
1359addImpl :: IState -> PTerm -> PTerm
1360addImpl = addImpl' False [] []
1362-- TODO: in patterns, don't add implicits to function names guarded by constructors
1363-- and *not* inside a PHidden
1365addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1366addImpl' inpat env infns ist ptm
1367 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1368 where
1369 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1370 ai qq env ds (PRef fc f)
1371 | f `elem` infns = PInferRef fc f
1372 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1373 ai qq env ds (PHidden (PRef fc f))
1374 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1375 ai qq env ds (PEq fc lt rt l r)
1376 = let lt' = ai qq env ds lt
1377 rt' = ai qq env ds rt
1378 l' = ai qq env ds l
1379 r' = ai qq env ds r in
1380 PEq fc lt' rt' l' r'
1381 ai qq env ds (PRewrite fc l r g)
1382 = let l' = ai qq env ds l
1383 r' = ai qq env ds r
1384 g' = fmap (ai qq env ds) g in
1385 PRewrite fc l' r' g'
1386 ai qq env ds (PTyped l r)
1387 = let l' = ai qq env ds l
1388 r' = ai qq env ds r in
1389 PTyped l' r'
1390 ai qq env ds (PPair fc p l r)
1391 = let l' = ai qq env ds l
1392 r' = ai qq env ds r in
1393 PPair fc p l' r'
1394 ai qq env ds (PDPair fc p l t r)
1395 = let l' = ai qq env ds l
1396 t' = ai qq env ds t
1397 r' = ai qq env ds r in
1398 PDPair fc p l' t' r'
1399 ai qq env ds (PAlternative a as)
1400 = let as' = map (ai qq env ds) as in
1401 PAlternative a as'
1402 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1403 ai qq env ds (PApp fc (PInferRef _ f) as)
1404 = let as' = map (fmap (ai qq env ds)) as in
1405 PApp fc (PInferRef fc f) as'
1406 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1407 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1408 | not (f `elem` map fst env)
1409 = let as' = map (fmap (ai qq env ds)) as in
1410 handleErr $ aiFn inpat False qq ist fc f ds as'
1411 | Just (Just ty) <- lookup f env =
1412 let as' = map (fmap (ai qq env ds)) as
1413 arity = getPArity ty in
1414 mkPApp fc arity ftm as'
1415 ai qq env ds (PApp fc f as)
1416 = let f' = ai qq env ds f
1417 as' = map (fmap (ai qq env ds)) as in
1418 mkPApp fc 1 f' as'
1419 ai qq env ds (PCase fc c os)
1420 = let c' = ai qq env ds c in
1421 -- leave os alone, because they get lifted into a new pattern match
1422 -- definition which is passed through addImpl again with more scope
1423 -- information
1424 PCase fc c' os
1425 ai qq env ds (PLam n ty sc)
1426 = let ty' = ai qq env ds ty
1427 sc' = ai qq ((n, Just ty):env) ds sc in
1428 PLam n ty' sc'
1429 ai qq env ds (PLet n ty val sc)
1430 = let ty' = ai qq env ds ty
1431 val' = ai qq env ds val
1432 sc' = ai qq ((n, Just ty):env) ds sc in
1433 PLet n ty' val' sc'
1434 ai qq env ds (PPi p n ty sc)
1435 = let ty' = ai qq env ds ty
1436 sc' = ai qq ((n, Just ty):env) ds sc in
1437 PPi p n ty' sc'
1438 ai qq env ds (PGoal fc r n sc)
1439 = let r' = ai qq env ds r
1440 sc' = ai qq ((n, Nothing):env) ds sc in
1441 PGoal fc r' n sc'
1442 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1443 -- Don't do PProof or PTactics since implicits get added when scope is
1444 -- properly known in ElabTerm.runTac
1445 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1446 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1447 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1448 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1449 (fmap (ai True env ds) g)
1450 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1451 ai qq env ds tm = tm
1453 handleErr (Left err) = PElabError err
1454 handleErr (Right x) = x
1456-- if in a pattern, and there are no arguments, and there's no possible
1457-- names with zero explicit arguments, don't add implicits.
1459aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1460aiFn inpat True qq ist fc f ds []
1461 = case lookupDef f (tt_ctxt ist) of
1462 [] -> Right $ PPatvar fc f
1463 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1464 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1465 if (not (vname f) || tcname f
1466 || any (conCaf (tt_ctxt ist)) ialts)
1467-- any constructor alts || any allImp ialts))
1468 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1469 else Right $ PPatvar fc f
1470 where imp (PExp _ _ _ _) = False
1471 imp _ = True
1472-- allImp [] = False
1473 allImp xs = all imp xs
1474 constructor (TyDecl (DCon _ _) _) = True
1475 constructor _ = False
1477 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1479 vname (UN n) = True -- non qualified
1480 vname _ = False
1482aiFn inpat expat qq ist fc f ds as
1483 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1484aiFn inpat expat qq ist fc f ds as
1485 -- This is where namespaces get resolved by adding PAlternative
1486 = do let ns = lookupCtxtName f (idris_implicits ist)
1487 let nh = filter (\(n, _) -> notHidden n) ns
1488 let ns' = case trimAlts ds nh of
1489 [] -> nh
1490 x -> x
1491 case ns' of
1492 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1493 [] -> if f `elem` (map fst (idris_metavars ist))
1494 then Right $ PApp fc (PRef fc f) as
1495 else Right $ mkPApp fc (length as) (PRef fc f) as
1496 alts -> Right $
1497 PAlternative True $
1498 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1499 (insertImpl ns as)) alts
1500 where
1501 trimAlts [] alts = alts
1502 trimAlts ns alts
1503 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1505 nspace (NS _ s) = s
1506 nspace _ = []
1508 notHidden n = case getAccessibility n of
1509 Hidden -> False
1510 _ -> True
1512 getAccessibility n
1513 = case lookupDefAcc n False (tt_ctxt ist) of
1514 [(n,t)] -> t
1515 _ -> Public
1517 insertImpl :: [PArg] -> [PArg] -> [PArg]
1518 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1520 exp (PExp _ _ _ _) = True
1521 exp (PConstraint _ _ _ _) = True
1522 exp _ = False
1524 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1525 -> [PArg] -- parameters
1526 -> [PArg] -- explicit arguments
1527 -> [PArg] -- implicits given
1528 -> [PArg]
1529 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1530 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1531 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1532 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1533 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1534 let rtc = PResolveTC fc in
1535 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1536 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1537 case find n imps [] of
1538 Just (tm, imps') ->
1539 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1540 Nothing ->
1541 PImp p True l n Placeholder :
1542 insImpAcc (M.insert n Placeholder pnas) ps given imps
1543 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1544 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1545 case find n imps [] of
1546 Just (tm, imps') ->
1547 PTacImplicit p l n sc tm :
1548 insImpAcc (M.insert n tm pnas) ps given imps'
1549 Nothing ->
1550 if inpat
1551 then PTacImplicit p l n sc Placeholder :
1552 insImpAcc (M.insert n Placeholder pnas) ps given imps
1553 else PTacImplicit p l n sc sc :
1554 insImpAcc (M.insert n sc pnas) ps given imps
1555 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1556 -- TODO: report here, and prune alternatives
1557 insImpAcc _ _ given imps = given ++ imps
1559 find n [] acc = Nothing
1560 find n (PImp _ _ _ n' t : gs) acc
1561 | n == n' = Just (t, reverse acc ++ gs)
1562 find n (PTacImplicit _ _ n' _ t : gs) acc
1563 | n == n' = Just (t, reverse acc ++ gs)
1564 find n (g : gs) acc = find n gs (g : acc)
1566-- replace non-linear occurrences with _
1567-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1568-- it is hard to get right!
1570stripLinear :: IState -> PTerm -> PTerm
1571stripLinear i tm = evalState (sl tm) [] where
1572 sl :: PTerm -> State [Name] PTerm
1573 sl (PRef fc f)
1574 | (_:_) <- lookupTy f (tt_ctxt i)
1575 = return $ PRef fc f
1576 | otherwise = do ns <- get
1577 if (f `elem` ns)
1578 then return Placeholder
1579 else do put (f : ns)
1580 return (PRef fc f)
1581 sl (PPatvar fc f)
1582 = do ns <- get
1583 if (f `elem` ns)
1584 then return Placeholder
1585 else do put (f : ns)
1586 return (PPatvar fc f)
1587 sl t@(PAlternative _ (a : as)) = do sl a
1588 return t
1589 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1590 args' <- mapM slA args
1591 return $ PApp fc fn args'
1592 where slA (PImp p m l n t) = do t' <- sl t
1593 return $ PImp p m l n t'
1594 slA (PExp p l n t) = do t' <- sl t
1595 return $ PExp p l n t'
1596 slA (PConstraint p l n t)
1597 = do t' <- sl t
1598 return $ PConstraint p l n t'
1599 slA (PTacImplicit p l n sc t)
1600 = do t' <- sl t
1601 return $ PTacImplicit p l n sc t'
1602 sl x = return x
1604-- Remove functions which aren't applied to anything, which must then
1605-- be resolved by unification. Assume names resolved and alternatives
1606-- filled in (so no ambiguity).
1608stripUnmatchable :: IState -> PTerm -> PTerm
1609stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1610 su :: PTerm -> PTerm
1611 su (PRef fc f)
1612 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1613 = Placeholder
1614 su (PApp fc fn args)
1615 = PApp fc fn (fmap (fmap su) args)
1616 su (PAlternative b alts)
1617 = let alts' = filter (/= Placeholder) (map su alts) in
1618 if null alts' then Placeholder
1619 else PAlternative b alts'
1620 su (PPair fc p l r) = PPair fc p (su l) (su r)
1621 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1622 su t = t
1623stripUnmatchable i tm = tm
1625mkPApp fc a f [] = f
1626mkPApp fc a f as = let rest = drop a as in
1627 appRest fc (PApp fc f (take a as)) rest
1628 where
1629 appRest fc f [] = f
1630 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1632-- Find 'static' argument positions
1633-- (the declared ones, plus any names in argument position in the declared
1634-- statics)
1635-- FIXME: It's possible that this really has to happen after elaboration
1637findStatics :: IState -> PTerm -> (PTerm, [Bool])
1638findStatics ist tm = trace (show tm) $
1639 let (ns, ss) = fs tm in
1640 runState (pos ns ss tm) []
1641 where fs (PPi p n t sc)
1642 | Static <- pstatic p
1643 = let (ns, ss) = fs sc in
1644 (namesIn [] ist t : ns, n : ss)
1645 | otherwise = let (ns, ss) = fs sc in
1646 (ns, ss)
1647 fs _ = ([], [])
1649 inOne n ns = length (filter id (map (elem n) ns)) == 1
1651 pos ns ss (PPi p n t sc)
1652 | elem n ss = do sc' <- pos ns ss sc
1653 spos <- get
1654 put (True : spos)
1655 return (PPi (p { pstatic = Static }) n t sc')
1656 | otherwise = do sc' <- pos ns ss sc
1657 spos <- get
1658 put (False : spos)
1659 return (PPi p n t sc')
1660 pos ns ss t = return t
1662-- for 6.12/7 compatibility
1663data EitherErr a b = LeftErr a | RightOK b
1665instance Monad (EitherErr a) where
1666 return = RightOK
1668 (LeftErr e) >>= k = LeftErr e
1669 RightOK v >>= k = k v
1671toEither (LeftErr e) = Left e
1672toEither (RightOK ho) = Right ho
1674-- syntactic match of a against b, returning pair of variables in a
1675-- and what they match. Returns the pair that failed if not a match.
1677matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1678matchClause = matchClause' False
1680matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1681matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1682 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1684 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1685 fullApp x = x
1687 match' x y = match (fullApp x) (fullApp y)
1688 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1689 | fi == txt "fromInteger" && b == txt "builtins",
1690 PConstant (I _) <- getTm x = match (getTm x) x'
1691 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1692 | fi == txt "fromInteger" && b == txt "builtins",
1693 PConstant (I _) <- getTm x = match (getTm x) x'
1694 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1695 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1696 match (PApp _ f args) (PApp _ f' args')
1697 | length args == length args'
1698 = do mf <- match' f f'
1699 ms <- zipWithM matchArg args args'
1700 return (mf ++ concat ms)
1701 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1702 match (PPatvar f n) xr = match (PRef f n) xr
1703 match xr (PPatvar f n) = match xr (PRef f n)
1704 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1705 match (PRef _ n) tm@(PRef _ n')
1706 | n == n' && not names &&
1707 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1708 || tm == Placeholder)
1709 = return [(n, tm)]
1710 -- if one namespace is missing, drop the other
1711 | n == n' || n == dropNS n' || dropNS n == n' = return []
1712 where dropNS (NS n _) = n
1713 dropNS n = n
1714 match (PRef _ n) tm
1715 | not names && (not (isConName n (tt_ctxt i) ||
1716 isFnName n (tt_ctxt i)) || tm == Placeholder)
1717 = return [(n, tm)]
1718 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1719 = do ml <- match' l l'
1720 mr <- match' r r'
1721 return (ml ++ mr)
1722 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1723 = do ml <- match' l l'
1724 mr <- match' r r'
1725 return (ml ++ mr)
1726 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1727 mr <- match r r'
1728 return (ml ++ mr)
1729 match (PTyped l r) x = match l x
1730 match x (PTyped l r) = match x l
1731 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1732 mr <- match' r r'
1733 return (ml ++ mr)
1734 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1735 mt <- match' t t'
1736 mr <- match' r r'
1737 return (ml ++ mt ++ mr)
1738 match (PAlternative a as) (PAlternative a' as')
1739 = do ms <- zipWithM match' as as'
1740 return (concat ms)
1741 match a@(PAlternative _ as) b
1742 = do let ms = zipWith match' as (repeat b)
1743 case (rights (map toEither ms)) of
1744 (x: _) -> return x
1745 _ -> LeftErr (a, b)
1746 match (PCase _ _ _) _ = return [] -- lifted out
1747 match (PMetavar _) _ = return [] -- modified
1748 match (PInferRef _ _) _ = return [] -- modified
1749 match (PQuote _) _ = return []
1750 match (PProof _) _ = return []
1751 match (PTactics _) _ = return []
1752 match (PRefl _ _) (PRefl _ _) = return []
1753 match (PResolveTC _) (PResolveTC _) = return []
1754 match (PTrue _ _) (PTrue _ _) = return []
1755 match (PFalse _) (PFalse _) = return []
1756 match (PReturn _) (PReturn _) = return []
1757 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1758 ms <- match' s s'
1759 return (mt ++ ms)
1760 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1761 ms <- match' s s'
1762 return (mt ++ ms)
1763 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1764 mty <- match' ty ty'
1765 ms <- match' s s'
1766 return (mt ++ mty ++ ms)
1767 match (PHidden x) (PHidden y) = match' x y
1768 match (PUnifyLog x) y = match' x y
1769 match x (PUnifyLog y) = match' x y
1770 match (PNoImplicits x) y = match' x y
1771 match x (PNoImplicits y) = match' x y
1772 match Placeholder _ = return []
1773 match _ Placeholder = return []
1774 match (PResolveTC _) _ = return []
1775 match a b | a == b = return []
1776 | otherwise = LeftErr (a, b)
1778 checkRpts (RightOK ms) = check ms where
1779 check ((n,t):xs)
1780 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1781 then Left (t, t')
1782 else check xs
1783 check (_:xs) = check xs
1784 check [] = Right ms
1785 checkRpts (LeftErr x) = Left x
1787substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1788substMatches ms = substMatchesShadow ms []
1790substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1791substMatchesShadow [] shs t = t
1792substMatchesShadow ((n,tm):ns) shs t
1793 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1795substMatch :: Name -> PTerm -> PTerm -> PTerm
1796substMatch n = substMatchShadow n []
1798substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1799substMatchShadow n shs tm t = sm shs t where
1800 sm xs (PRef _ n') | n == n' = tm
1801 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1802 sm xs (PPi p x t sc)
1803 | x `elem` xs
1804 = let x' = nextName x in
1805 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1806 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1807 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1808 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1809 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1810 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1811 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1812 (fmap (sm xs) tm)
1813 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1814 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1815 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1816 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1817 sm xs (PHidden x) = PHidden (sm xs x)
1818 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1819 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1820 sm xs x = x
1822 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1823 fullApp x = x
1825shadow :: Name -> Name -> PTerm -> PTerm
1826shadow n n' t = sm t where
1827 sm (PRef fc x) | n == x = PRef fc n'
1828 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1829 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1830 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1831 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1832 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1833 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1834 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1835 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1836 sm (PTyped x y) = PTyped (sm x) (sm y)
1837 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1838 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1839 sm (PAlternative a as) = PAlternative a (map sm as)
1840 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1841 sm (PProof ts) = PProof (map (fmap sm) ts)
1842 sm (PHidden x) = PHidden (sm x)
1843 sm (PUnifyLog x) = PUnifyLog (sm x)
1844 sm (PNoImplicits x) = PNoImplicits (sm x)
1845 sm x = x
1847-- Rename any binders which are repeated (so that we don't have to mess
1848-- about with shadowing anywhere else).
1850mkUniqueNames :: [Name] -> PTerm -> PTerm
1851mkUniqueNames env tm = evalState (mkUniq tm) env where
1852 inScope = boundNamesIn tm
1854 mkUniqA arg = do t' <- mkUniq (getTm arg)
1855 return (arg { getTm = t' })
1857 -- Initialise the unique name with the environment length (so we're not
1858 -- looking for too long...)
1859 initN (UN n) l = UN $ txt (str n ++ show l)
1860 initN (MN i s) l = MN (i+l) s
1861 initN n l = n
1863 -- FIXME: Probably ought to do this for completeness! It's fine as
1864 -- long as there are no bindings inside tactics though.
1865 mkUniqT tac = return tac
1867 mkUniq :: PTerm -> State [Name] PTerm
1868 mkUniq (PLam n ty sc)
1869 = do env <- get
1870 (n', sc') <-
1871 if n `elem` env
1872 then do let n' = uniqueName (initN n (length env))
1873 (env ++ inScope)
1874 return (n', shadow n n' sc)
1875 else return (n, sc)
1876 put (n' : env)
1877 ty' <- mkUniq ty
1878 sc'' <- mkUniq sc'
1879 return $! PLam n' ty' sc''
1880 mkUniq (PPi p n ty sc)
1881 = do env <- get
1882 (n', sc') <-
1883 if n `elem` env
1884 then do let n' = uniqueName (initN n (length env))
1885 (env ++ inScope)
1886 return (n', shadow n n' sc)
1887 else return (n, sc)
1888 put (n' : env)
1889 ty' <- mkUniq ty
1890 sc'' <- mkUniq sc'
1891 return $! PPi p n' ty' sc''
1892 mkUniq (PLet n ty val sc)
1893 = do env <- get
1894 (n', sc') <-
1895 if n `elem` env
1896 then do let n' = uniqueName (initN n (length env))
1897 (env ++ inScope)
1898 return (n', shadow n n' sc)
1899 else return (n, sc)
1900 put (n' : env)
1901 ty' <- mkUniq ty; val' <- mkUniq val
1902 sc'' <- mkUniq sc'
1903 return $! PLet n' ty' val' sc''
1904 mkUniq (PApp fc t args)
1905 = do t' <- mkUniq t
1906 args' <- mapM mkUniqA args
1907 return $! PApp fc t' args'
1908 mkUniq (PAppBind fc t args)
1909 = do t' <- mkUniq t
1910 args' <- mapM mkUniqA args
1911 return $! PAppBind fc t' args'
1912 mkUniq (PCase fc t alts)
1913 = do t' <- mkUniq t
1914 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1915 return (x', y')) alts
1916 return $! PCase fc t' alts'
1917 mkUniq (PPair fc p l r)
1918 = do l' <- mkUniq l; r' <- mkUniq r
1919 return $! PPair fc p l' r'
1920 mkUniq (PDPair fc p (PRef fc' n) t sc)
1921 | t /= Placeholder
1922 = do env <- get
1923 (n', sc') <- if n `elem` env
1924 then do let n' = uniqueName n (env ++ inScope)
1925 return (n', shadow n n' sc)
1926 else return (n, sc)
1927 put (n' : env)
1928 t' <- mkUniq t
1929 sc'' <- mkUniq sc'
1930 return $! PDPair fc p (PRef fc' n') t' sc''
1931 mkUniq (PDPair fc p l t r)
1932 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1933 return $! PDPair fc p l' t' r'
1934 mkUniq (PAlternative b as)
1935 = liftM (PAlternative b) (mapM mkUniq as)
1936 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1937 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1938 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1939 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1940 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1941 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1942 mkUniq t = return t