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