git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1927 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 h -> runIO . hPutStrLn h $ 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 h ->
550 runIO . hPutStrLn h $
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 -> Handle -> Idris ()
666setIdeSlave True h = do i <- getIState
667 putIState $ i { idris_outputmode = (IdeSlave 0 h), 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 }
764impShow :: Idris Bool
765impShow = do i <- getIState
766 return (opt_showimp (idris_options i))
768setImpShow :: Bool -> Idris ()
769setImpShow t = do i <- getIState
770 let opts = idris_options i
771 let opt' = opts { opt_showimp = t }
772 putIState $ i { idris_options = opt' }
774setColour :: ColourType -> IdrisColour -> Idris ()
775setColour ct c = do i <- getIState
776 let newTheme = setColour' ct c (idris_colourTheme i)
777 putIState $ i { idris_colourTheme = newTheme }
778 where setColour' KeywordColour c t = t { keywordColour = c }
779 setColour' BoundVarColour c t = t { boundVarColour = c }
780 setColour' ImplicitColour c t = t { implicitColour = c }
781 setColour' FunctionColour c t = t { functionColour = c }
782 setColour' TypeColour c t = t { typeColour = c }
783 setColour' DataColour c t = t { dataColour = c }
784 setColour' PromptColour c t = t { promptColour = c }
785 setColour' PostulateColour c t = t { postulateColour = c }
787logLvl :: Int -> String -> Idris ()
788logLvl l str = do i <- getIState
789 let lvl = opt_logLevel (idris_options i)
790 when (lvl >= l) $
791 case idris_outputmode i of
792 RawOutput h -> do runIO $ hPutStrLn h str
793 IdeSlave n h ->
794 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
795 runIO . hPutStrLn h $ convSExp "log" good n
797cmdOptType :: Opt -> Idris Bool
798cmdOptType x = do i <- getIState
799 return $ x `elem` opt_cmdline (idris_options i)
801iLOG :: String -> Idris ()
802iLOG = logLvl 1
804noErrors :: Idris Bool
805noErrors = do i <- getIState
806 case errSpan i of
807 Nothing -> return True
808 _ -> return False
810setTypeCase :: Bool -> Idris ()
811setTypeCase t = do i <- getIState
812 let opts = idris_options i
813 let opt' = opts { opt_typecase = t }
814 putIState $ i { idris_options = opt' }
817-- Dealing with parameters
819expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
820 [Name] -> -- all names
821 [Name] -> -- names with no declaration
822 PTerm -> PTerm
823expandParams dec ps ns infs tm = en tm
824 where
825 -- if we shadow a name (say in a lambda binding) that is used in a call to
826 -- a lifted function, we need access to both names - once in the scope of the
827 -- binding and once to call the lifted functions. So we'll explicitly shadow
828 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
829 -- but we didn't...)
831 mkShadow (UN n) = MN 0 n
832 mkShadow (MN i n) = MN (i+1) n
833 mkShadow (NS x s) = NS (mkShadow x) s
835 en (PLam n t s)
836 | n `elem` (map fst ps ++ ns)
837 = let n' = mkShadow n in
838 PLam n' (en t) (en (shadow n n' s))
839 | otherwise = PLam n (en t) (en s)
840 en (PPi p n t s)
841 | n `elem` (map fst ps ++ ns)
842 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
843 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
844 | otherwise = PPi (enTacImp p) n (en t) (en s)
845 en (PLet n ty v s)
846 | n `elem` (map fst ps ++ ns)
847 = let n' = mkShadow n in
848 PLet n' (en ty) (en v) (en (shadow n n' s))
849 | otherwise = PLet n (en ty) (en v) (en s)
850 -- FIXME: Should only do this in a type signature!
851 en (PDPair f p (PRef f' n) t r)
852 | n `elem` (map fst ps ++ ns) && t /= Placeholder
853 = let n' = mkShadow n in
854 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
855 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
856 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
857 en (PTyped l r) = PTyped (en l) (en r)
858 en (PPair f p l r) = PPair f p (en l) (en r)
859 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
860 en (PAlternative a as) = PAlternative a (map en as)
861 en (PHidden t) = PHidden (en t)
862 en (PUnifyLog t) = PUnifyLog (en t)
863 en (PDisamb ds t) = PDisamb ds (en t)
864 en (PNoImplicits t) = PNoImplicits (en t)
865 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
866 en (PProof ts) = PProof (map (fmap en) ts)
867 en (PTactics ts) = PTactics (map (fmap en) ts)
869 en (PQuote (Var n))
870 | n `nselem` ns = PQuote (Var (dec n))
871 en (PApp fc (PInferRef fc' n) as)
872 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
873 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
874 en (PApp fc (PRef fc' n) as)
875 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
876 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
877 | n `nselem` ns = PApp fc (PRef fc' (dec n))
878 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
879 en (PAppBind fc (PRef fc' n) as)
880 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
881 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
882 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
883 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
884 en (PRef fc n)
885 | n `elem` infs = PApp fc (PInferRef fc (dec n))
886 (map (pexp . (PRef fc)) (map fst ps))
887 | n `nselem` ns = PApp fc (PRef fc (dec n))
888 (map (pexp . (PRef fc)) (map fst ps))
889 en (PInferRef fc n)
890 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
891 (map (pexp . (PRef fc)) (map fst ps))
892 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
893 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
894 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
895 en t = t
897 nselem x [] = False
898 nselem x (y : xs) | nseq x y = True
899 | otherwise = nselem x xs
901 nseq x y = nsroot x == nsroot y
903 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
904 enTacImp other = other
906expandParamsD :: Bool -> -- True = RHS only
907 IState ->
908 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
909expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
910 = if n `elem` ns && (not rhsonly)
911 then -- trace (show (n, expandParams dec ps ns ty)) $
912 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
913 else --trace (show (n, expandParams dec ps ns ty)) $
914 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
915expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
916 = if n `elem` ns && (not rhsonly)
917 then -- trace (show (n, expandParams dec ps ns ty)) $
918 PPostulate doc syn fc o (dec n) (piBind ps
919 (expandParams dec ps ns [] ty))
920 else --trace (show (n, expandParams dec ps ns ty)) $
921 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
922expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
923 = let n' = if n `elem` ns then dec n else n in
924 PClauses fc opts n' (map expandParamsC cs)
925 where
926 expandParamsC (PClause fc n lhs ws rhs ds)
927 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
928 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
929 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
930 n' = if n `elem` ns then dec n else n
931 -- names bound on the lhs should not be expanded on the rhs
932 ns' = removeBound lhs ns in
933 PClause fc n' lhs'
934 (map (expandParams dec ps'' ns' []) ws)
935 (expandParams dec ps'' ns' [] rhs)
936 (map (expandParamsD True ist dec ps'' ns') ds)
937 expandParamsC (PWith fc n lhs ws wval ds)
938 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
939 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
940 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
941 n' = if n `elem` ns then dec n else n
942 ns' = removeBound lhs ns in
943 PWith fc n' lhs'
944 (map (expandParams dec ps'' ns' []) ws)
945 (expandParams dec ps'' ns' [] wval)
946 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
947 updateps yn nm [] = []
948 updateps yn nm (((a, t), i):as)
949 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
950 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
952 removeBound lhs ns = ns \\ nub (bnames lhs)
954 bnames (PRef _ n) = [n]
955 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
956 bnames (PPair _ _ l r) = bnames l ++ bnames r
957 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
958 bnames _ = []
960-- | Expands parameters defined in parameter and where blocks inside of declarations
961expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
962 = PData doc argDocs syn fc co (expandPData pd)
963 where
964 -- just do the type decl, leave constructors alone (parameters will be
965 -- added implicitly)
966 expandPData (PDatadecl n ty cons)
967 = if n `elem` ns
968 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
969 (map econ cons)
970 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
971 econ (doc, argDocs, n, t, fc, fs)
972 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
973expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
974 = if tn `elem` ns
975 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
976 opts cdoc (dec cn) conty
977 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
978 opts cdoc (dec cn) conty
979 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
980expandParamsD rhs ist dec ps ns (PParams f params pds)
981 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
982 (map (expandParamsD True ist dec ps ns) pds)
983-- (map (expandParamsD ist dec ps ns) pds)
984expandParamsD rhs ist dec ps ns (PMutual f pds)
985 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
986expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
987 = PClass doc info f
988 (map (expandParams dec ps ns []) cs)
989 n
990 (map (mapsnd (expandParams dec ps ns [])) params)
991 pDocs
992 (map (expandParamsD rhs ist dec ps ns) decls)
993expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
994 = PInstance info f
995 (map (expandParams dec ps ns []) cs)
996 n
997 (map (expandParams dec ps ns []) params)
998 (expandParams dec ps ns [] ty)
999 cn
1000 (map (expandParamsD rhs ist dec ps ns) decls)
1001expandParamsD rhs ist dec ps ns d = d
1003mapsnd f (x, t) = (x, f t)
1005-- Calculate a priority for a type, for deciding elaboration order
1006-- * if it's just a type variable or concrete type, do it early (0)
1007-- * if there's only type variables and injective constructors, do it next (1)
1008-- * if there's a function type, next (2)
1009-- * finally, everything else (3)
1011getPriority :: IState -> PTerm -> Int
1012getPriority i tm = 1 -- pri tm
1013 where
1014 pri (PRef _ n) =
1015 case lookupP n (tt_ctxt i) of
1016 ((P (DCon _ _) _ _):_) -> 1
1017 ((P (TCon _ _) _ _):_) -> 1
1018 ((P Ref _ _):_) -> 1
1019 [] -> 0 -- must be locally bound, if it's not an error...
1020 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1021 pri (PTrue _ _) = 0
1022 pri (PFalse _) = 0
1023 pri (PRefl _ _) = 1
1024 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1025 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1026 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1027 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1028 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1029 pri (PTyped l r) = pri l
1030 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1031 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1032 pri (PAlternative a as) = maximum (map pri as)
1033 pri (PConstant _) = 0
1034 pri Placeholder = 1
1035 pri _ = 3
1038addStatics :: Name -> Term -> PTerm -> Idris ()
1039addStatics n tm ptm =
1040 do let (statics, dynamics) = initStatics tm ptm
1041 let stnames = nub $ concatMap freeArgNames (map snd statics)
1042 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1043 -- also get the arguments which are 'uniquely inferrable' from
1044 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1045 let statics' = nub $ map fst statics ++
1046 filter (\x -> not (elem x dnames)) stnames
1047 let stpos = staticList statics' tm
1048 i <- getIState
1049 when (not (null statics)) $
1050 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1051 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1052 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1053 addIBC (IBCStatic n)
1054 where
1055 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1056 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1057 if pstatic p == Static then ((n, ty) : static, dynamic)
1058 else if (not (searchArg p))
1059 then (static, (n, ty) : dynamic)
1060 else (static, dynamic)
1061 initStatics t pt = ([], [])
1063 freeArgNames (Bind n (Pi ty) sc)
1064 = nub $ freeArgNames ty
1065 freeArgNames tm = let (_, args) = unApply tm in
1066 concatMap freeNames args
1068 -- if a name appears in a type class or tactic implicit index, it doesn't
1069 -- affect its 'uniquely inferrable' from a static status since these are
1070 -- resolved by searching.
1071 searchArg (Constraint _ _) = True
1072 searchArg (TacImp _ _ _) = True
1073 searchArg _ = False
1075 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1076 staticList _ _ = []
1078-- Dealing with implicit arguments
1080-- Add some bound implicits to the using block if they aren't there already
1082addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1083addToUsing us [] = us
1084addToUsing us ((n, t) : ns)
1085 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1086 | otherwise = addToUsing us ns
1087 where impName (UImplicit n _) = Just n
1088 impName _ = Nothing
1090-- Add constraint bindings from using block
1092addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1093addUsingConstraints syn fc t
1094 = do ist <- get
1095 let ns = namesIn [] ist t
1096 let cs = getConstraints t -- check declared constraints
1097 let addconsts = uconsts \\ cs
1098 return (doAdd addconsts ns t)
1099 where uconsts = filter uconst (using syn)
1100 uconst (UConstraint _ _) = True
1101 uconst _ = False
1103 doAdd [] _ t = t
1104 -- if all of args in ns, then add it
1105 doAdd (UConstraint c args : cs) ns t
1106 | all (\n -> elem n ns) args
1107 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1108 (mkConst c args) (doAdd cs ns t)
1109 | otherwise = doAdd cs ns t
1111 mkConst c args = PApp fc (PRef fc c)
1112 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1114 getConstraints (PPi (Constraint _ _) _ c sc)
1115 = getcapp c ++ getConstraints sc
1116 getConstraints (PPi _ _ c sc) = getConstraints sc
1117 getConstraints _ = []
1119 getcapp (PApp _ (PRef _ c) args)
1120 = do ns <- mapM getName args
1121 return (UConstraint c ns)
1122 getcapp _ = []
1124 getName (PExp _ _ _ (PRef _ n)) = return n
1125 getName _ = []
1127-- Add implicit bindings from using block, and bind any missing names
1128addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1129addUsingImpls syn n fc t
1130 = do ist <- getIState
1131 let ns = implicitNamesIn (map iname uimpls) ist t
1132 let badnames = filter (\n -> not (implicitable n) &&
1133 n `notElem` (map iname uimpls)) ns
1134 when (not (null badnames)) $
1135 throwError (At fc (Elaborating "type of " n
1136 (NoSuchVariable (head badnames))))
1137 let cs = getArgnames t -- get already bound names
1138 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1139 -- if all names in the arguments of addconsts appear in ns,
1140 -- add the constraint implicitly
1141 return (bindFree ns (doAdd addimpls ns t))
1142 where uimpls = filter uimpl (using syn)
1143 uimpl (UImplicit _ _) = True
1144 uimpl _ = False
1146 iname (UImplicit n _) = n
1147 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1149 doAdd [] _ t = t
1150 -- if all of args in ns, then add it
1151 doAdd (UImplicit n ty : cs) ns t
1152 | elem n ns
1153 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1154 | otherwise = doAdd cs ns t
1156 -- bind the free names which weren't in the using block
1157 bindFree [] tm = tm
1158 bindFree (n:ns) tm
1159 | elem n (map iname uimpls) = bindFree ns tm
1160 | otherwise
1161 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1163 getArgnames (PPi _ n c sc)
1164 = n : getArgnames sc
1165 getArgnames _ = []
1167-- Given the original type and the elaborated type, return the implicitness
1168-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1170getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1171getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')
1172 | n == n' = argInfo n p : getUnboundImplicits i sc sc'
1173 where
1174 argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')
1175 argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,
1176 PExp (getPriority i t') opt n t')
1177 argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,
1178 PConstraint 10 opt n t')
1179 argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,
1180 PTacImplicit 10 opt n scr t')
1181getUnboundImplicits i (Bind n (Pi t) sc) tm
1182 = impBind n t : getUnboundImplicits i sc tm
1183 where
1184 impBind n t = (True, PImp 1 True [] n Placeholder)
1185getUnboundImplicits i sc tm = []
1187-- Add implicit Pi bindings for any names in the term which appear in an
1188-- argument position.
1190-- This has become a right mess already. Better redo it some time...
1191-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1192-- a couple of places which use it. Clean them up!
1193implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1194implicit info syn n ptm = implicit' info syn [] n ptm
1196implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1197implicit' info syn ignore n ptm
1198 = do i <- getIState
1199 let (tm', impdata) = implicitise syn ignore i ptm
1200 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1201-- let (tm'', spos) = findStatics i tm'
1202 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1203 addIBC (IBCImp n)
1204 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1205-- i <- get
1206-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1207 return tm'
1208 where
1209 -- Detect unknown names in default arguments and throw error if found.
1210 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1211 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1213 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1214 notFoundInDefault kns (PTacImplicit _ _ n script _)
1215 = do i <- getIState
1216 case notFound kns (namesIn [] i script) of
1217 Nothing -> return (n:kns)
1218 Just name -> throwError (NoSuchVariable name)
1219 notFoundInDefault kns p = return ((pname p):kns)
1221 notFound :: [Name] -> [Name] -> Maybe Name
1222 notFound kns [] = Nothing
1223 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1224 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1226implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1227implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1228 let (declimps, ns') = execState (imps True [] tm) ([], [])
1229 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1230 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1231 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1232 if null ns
1233 then (tm, reverse declimps)
1234 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1235 where
1236 uvars = map ipair (filter uimplicit (using syn))
1237 pvars = syn_params syn
1239 inUsing n = n `elem` map fst uvars
1241 ipair (UImplicit x y) = (x, y)
1242 uimplicit (UImplicit _ _) = True
1243 uimplicit _ = False
1245 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1246 | otherwise = x : dropAll xs ys
1247 dropAll [] ys = []
1249 -- Find names in argument position in a type, suitable for implicit
1250 -- binding
1251 -- Not the function position, but do everything else...
1252 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1253 implNamesIn uv t = namesIn uv ist t
1255 imps top env (PApp _ f as)
1256 = do (decls, ns) <- get
1257 let isn = concatMap (namesIn uvars ist) (map getTm as)
1258 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1259 imps top env (PPi (Imp l _ _) n ty sc)
1260 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1261 (decls , ns) <- get
1262 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1263 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1264 imps True (n:env) sc
1265 imps top env (PPi (Exp l _ _) n ty sc)
1266 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1267 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1268 _ -> [])
1269 (decls, ns) <- get -- ignore decls in HO types
1270 put (PExp (getPriority ist ty) l n Placeholder : decls,
1271 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1272 imps True (n:env) sc
1273 imps top env (PPi (Constraint l _) n ty sc)
1274 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1275 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1276 _ -> [])
1277 (decls, ns) <- get -- ignore decls in HO types
1278 put (PConstraint 10 l n Placeholder : decls,
1279 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1280 imps True (n:env) sc
1281 imps top env (PPi (TacImp l _ scr) n ty sc)
1282 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1283 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1284 _ -> [])
1285 (decls, ns) <- get -- ignore decls in HO types
1286 put (PTacImplicit 10 l n scr Placeholder : decls,
1287 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1288 imps True (n:env) sc
1289 imps top env (PEq _ _ _ l r)
1290 = do (decls, ns) <- get
1291 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1292 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1293 imps top env (PRewrite _ 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 (PTyped l r)
1298 = imps top env l
1299 imps top env (PPair _ _ l r)
1300 = do (decls, ns) <- get
1301 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1302 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1303 imps top env (PDPair _ _ (PRef _ n) t r)
1304 = do (decls, ns) <- get
1305 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1306 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1307 imps top env (PDPair _ _ l t r)
1308 = do (decls, ns) <- get
1309 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1310 namesIn uvars ist r
1311 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1312 imps top env (PAlternative a as)
1313 = do (decls, ns) <- get
1314 let isn = concatMap (namesIn uvars ist) as
1315 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1316 imps top env (PLam n ty sc)
1317 = do imps False env ty
1318 imps False (n:env) sc
1319 imps top env (PHidden tm) = imps False env tm
1320 imps top env (PUnifyLog tm) = imps False env tm
1321 imps top env (PNoImplicits tm) = imps False env tm
1322 imps top env _ = return ()
1324 pibind using [] sc = sc
1325 pibind using (n:ns) sc
1326 = case lookup n using of
1327 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1328 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1329 (pibind using ns sc)
1331-- Add implicit arguments in function calls
1332addImplPat :: IState -> PTerm -> PTerm
1333addImplPat = addImpl' True [] []
1335addImplBound :: IState -> [Name] -> PTerm -> PTerm
1336addImplBound ist ns = addImpl' False ns [] ist
1338addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1339addImplBoundInf ist ns inf = addImpl' False ns inf ist
1341-- | Add the implicit arguments to applications in the term
1342addImpl :: IState -> PTerm -> PTerm
1343addImpl = addImpl' False [] []
1345-- TODO: in patterns, don't add implicits to function names guarded by constructors
1346-- and *not* inside a PHidden
1348addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1349addImpl' inpat env infns ist ptm
1350 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1351 where
1352 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1353 ai qq env ds (PRef fc f)
1354 | f `elem` infns = PInferRef fc f
1355 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1356 ai qq env ds (PHidden (PRef fc f))
1357 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1358 ai qq env ds (PEq fc lt rt l r)
1359 = let lt' = ai qq env ds lt
1360 rt' = ai qq env ds rt
1361 l' = ai qq env ds l
1362 r' = ai qq env ds r in
1363 PEq fc lt' rt' l' r'
1364 ai qq env ds (PRewrite fc l r g)
1365 = let l' = ai qq env ds l
1366 r' = ai qq env ds r
1367 g' = fmap (ai qq env ds) g in
1368 PRewrite fc l' r' g'
1369 ai qq env ds (PTyped l r)
1370 = let l' = ai qq env ds l
1371 r' = ai qq env ds r in
1372 PTyped l' r'
1373 ai qq env ds (PPair fc p l r)
1374 = let l' = ai qq env ds l
1375 r' = ai qq env ds r in
1376 PPair fc p l' r'
1377 ai qq env ds (PDPair fc p l t r)
1378 = let l' = ai qq env ds l
1379 t' = ai qq env ds t
1380 r' = ai qq env ds r in
1381 PDPair fc p l' t' r'
1382 ai qq env ds (PAlternative a as)
1383 = let as' = map (ai qq env ds) as in
1384 PAlternative a as'
1385 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1386 ai qq env ds (PApp fc (PInferRef _ f) as)
1387 = let as' = map (fmap (ai qq env ds)) as in
1388 PApp fc (PInferRef fc f) as'
1389 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1390 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1391 | not (f `elem` map fst env)
1392 = let as' = map (fmap (ai qq env ds)) as in
1393 handleErr $ aiFn inpat False qq ist fc f ds as'
1394 | Just (Just ty) <- lookup f env =
1395 let as' = map (fmap (ai qq env ds)) as
1396 arity = getPArity ty in
1397 mkPApp fc arity ftm as'
1398 ai qq env ds (PApp fc f as)
1399 = let f' = ai qq env ds f
1400 as' = map (fmap (ai qq env ds)) as in
1401 mkPApp fc 1 f' as'
1402 ai qq env ds (PCase fc c os)
1403 = let c' = ai qq env ds c in
1404 -- leave os alone, because they get lifted into a new pattern match
1405 -- definition which is passed through addImpl again with more scope
1406 -- information
1407 PCase fc c' os
1408 ai qq env ds (PLam n ty sc)
1409 = let ty' = ai qq env ds ty
1410 sc' = ai qq ((n, Just ty):env) ds sc in
1411 PLam n ty' sc'
1412 ai qq env ds (PLet n ty val sc)
1413 = let ty' = ai qq env ds ty
1414 val' = ai qq env ds val
1415 sc' = ai qq ((n, Just ty):env) ds sc in
1416 PLet n ty' val' sc'
1417 ai qq env ds (PPi p n ty sc)
1418 = let ty' = ai qq env ds ty
1419 sc' = ai qq ((n, Just ty):env) ds sc in
1420 PPi p n ty' sc'
1421 ai qq env ds (PGoal fc r n sc)
1422 = let r' = ai qq env ds r
1423 sc' = ai qq ((n, Nothing):env) ds sc in
1424 PGoal fc r' n sc'
1425 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1426 -- Don't do PProof or PTactics since implicits get added when scope is
1427 -- properly known in ElabTerm.runTac
1428 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1429 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1430 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1431 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1432 (fmap (ai True env ds) g)
1433 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1434 ai qq env ds tm = tm
1436 handleErr (Left err) = PElabError err
1437 handleErr (Right x) = x
1439-- if in a pattern, and there are no arguments, and there's no possible
1440-- names with zero explicit arguments, don't add implicits.
1442aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1443aiFn inpat True qq ist fc f ds []
1444 = case lookupDef f (tt_ctxt ist) of
1445 [] -> Right $ PPatvar fc f
1446 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1447 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1448 if (not (vname f) || tcname f
1449 || any (conCaf (tt_ctxt ist)) ialts)
1450-- any constructor alts || any allImp ialts))
1451 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1452 else Right $ PPatvar fc f
1453 where imp (PExp _ _ _ _) = False
1454 imp _ = True
1455-- allImp [] = False
1456 allImp xs = all imp xs
1457 constructor (TyDecl (DCon _ _) _) = True
1458 constructor _ = False
1460 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1462 vname (UN n) = True -- non qualified
1463 vname _ = False
1465aiFn inpat expat qq ist fc f ds as
1466 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1467aiFn inpat expat qq ist fc f ds as
1468 -- This is where namespaces get resolved by adding PAlternative
1469 = do let ns = lookupCtxtName f (idris_implicits ist)
1470 let nh = filter (\(n, _) -> notHidden n) ns
1471 let ns' = case trimAlts ds nh of
1472 [] -> nh
1473 x -> x
1474 case ns' of
1475 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1476 [] -> if f `elem` (map fst (idris_metavars ist))
1477 then Right $ PApp fc (PRef fc f) as
1478 else Right $ mkPApp fc (length as) (PRef fc f) as
1479 alts -> Right $
1480 PAlternative True $
1481 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1482 (insertImpl ns as)) alts
1483 where
1484 trimAlts [] alts = alts
1485 trimAlts ns alts
1486 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1488 nspace (NS _ s) = s
1489 nspace _ = []
1491 notHidden n = case getAccessibility n of
1492 Hidden -> False
1493 _ -> True
1495 getAccessibility n
1496 = case lookupDefAcc n False (tt_ctxt ist) of
1497 [(n,t)] -> t
1498 _ -> Public
1500 insertImpl :: [PArg] -> [PArg] -> [PArg]
1501 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1503 exp (PExp _ _ _ _) = True
1504 exp (PConstraint _ _ _ _) = True
1505 exp _ = False
1507 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1508 -> [PArg] -- parameters
1509 -> [PArg] -- explicit arguments
1510 -> [PArg] -- implicits given
1511 -> [PArg]
1512 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1513 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1514 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1515 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1516 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1517 let rtc = PResolveTC fc in
1518 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1519 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1520 case find n imps [] of
1521 Just (tm, imps') ->
1522 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1523 Nothing ->
1524 PImp p True l n Placeholder :
1525 insImpAcc (M.insert n Placeholder pnas) ps given imps
1526 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1527 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1528 case find n imps [] of
1529 Just (tm, imps') ->
1530 PTacImplicit p l n sc tm :
1531 insImpAcc (M.insert n tm pnas) ps given imps'
1532 Nothing ->
1533 if inpat
1534 then PTacImplicit p l n sc Placeholder :
1535 insImpAcc (M.insert n Placeholder pnas) ps given imps
1536 else PTacImplicit p l n sc sc :
1537 insImpAcc (M.insert n sc pnas) ps given imps
1538 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1539 -- TODO: report here, and prune alternatives
1540 insImpAcc _ _ given imps = given ++ imps
1542 find n [] acc = Nothing
1543 find n (PImp _ _ _ n' t : gs) acc
1544 | n == n' = Just (t, reverse acc ++ gs)
1545 find n (PTacImplicit _ _ n' _ t : gs) acc
1546 | n == n' = Just (t, reverse acc ++ gs)
1547 find n (g : gs) acc = find n gs (g : acc)
1549-- replace non-linear occurrences with _
1550-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1551-- it is hard to get right!
1553stripLinear :: IState -> PTerm -> PTerm
1554stripLinear i tm = evalState (sl tm) [] where
1555 sl :: PTerm -> State [Name] PTerm
1556 sl (PRef fc f)
1557 | (_:_) <- lookupTy f (tt_ctxt i)
1558 = return $ PRef fc f
1559 | otherwise = do ns <- get
1560 if (f `elem` ns)
1561 then return Placeholder
1562 else do put (f : ns)
1563 return (PRef fc f)
1564 sl (PPatvar fc f)
1565 = do ns <- get
1566 if (f `elem` ns)
1567 then return Placeholder
1568 else do put (f : ns)
1569 return (PPatvar fc f)
1570 sl t@(PAlternative _ (a : as)) = do sl a
1571 return t
1572 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1573 args' <- mapM slA args
1574 return $ PApp fc fn args'
1575 where slA (PImp p m l n t) = do t' <- sl t
1576 return $ PImp p m l n t'
1577 slA (PExp p l n t) = do t' <- sl t
1578 return $ PExp p l n t'
1579 slA (PConstraint p l n t)
1580 = do t' <- sl t
1581 return $ PConstraint p l n t'
1582 slA (PTacImplicit p l n sc t)
1583 = do t' <- sl t
1584 return $ PTacImplicit p l n sc t'
1585 sl x = return x
1587-- Remove functions which aren't applied to anything, which must then
1588-- be resolved by unification. Assume names resolved and alternatives
1589-- filled in (so no ambiguity).
1591stripUnmatchable :: IState -> PTerm -> PTerm
1592stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1593 su :: PTerm -> PTerm
1594 su (PRef fc f)
1595 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1596 = Placeholder
1597 su (PApp fc fn args)
1598 = PApp fc fn (fmap (fmap su) args)
1599 su (PAlternative b alts)
1600 = let alts' = filter (/= Placeholder) (map su alts) in
1601 if null alts' then Placeholder
1602 else PAlternative b alts'
1603 su (PPair fc p l r) = PPair fc p (su l) (su r)
1604 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1605 su t = t
1606stripUnmatchable i tm = tm
1608mkPApp fc a f [] = f
1609mkPApp fc a f as = let rest = drop a as in
1610 appRest fc (PApp fc f (take a as)) rest
1611 where
1612 appRest fc f [] = f
1613 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1615-- Find 'static' argument positions
1616-- (the declared ones, plus any names in argument position in the declared
1617-- statics)
1618-- FIXME: It's possible that this really has to happen after elaboration
1620findStatics :: IState -> PTerm -> (PTerm, [Bool])
1621findStatics ist tm = trace (show tm) $
1622 let (ns, ss) = fs tm in
1623 runState (pos ns ss tm) []
1624 where fs (PPi p n t sc)
1625 | Static <- pstatic p
1626 = let (ns, ss) = fs sc in
1627 (namesIn [] ist t : ns, n : ss)
1628 | otherwise = let (ns, ss) = fs sc in
1629 (ns, ss)
1630 fs _ = ([], [])
1632 inOne n ns = length (filter id (map (elem n) ns)) == 1
1634 pos ns ss (PPi p n t sc)
1635 | elem n ss = do sc' <- pos ns ss sc
1636 spos <- get
1637 put (True : spos)
1638 return (PPi (p { pstatic = Static }) n t sc')
1639 | otherwise = do sc' <- pos ns ss sc
1640 spos <- get
1641 put (False : spos)
1642 return (PPi p n t sc')
1643 pos ns ss t = return t
1645-- for 6.12/7 compatibility
1646data EitherErr a b = LeftErr a | RightOK b
1648instance Monad (EitherErr a) where
1649 return = RightOK
1651 (LeftErr e) >>= k = LeftErr e
1652 RightOK v >>= k = k v
1654toEither (LeftErr e) = Left e
1655toEither (RightOK ho) = Right ho
1657-- syntactic match of a against b, returning pair of variables in a
1658-- and what they match. Returns the pair that failed if not a match.
1660matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1661matchClause = matchClause' False
1663matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1664matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1665 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1667 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1668 fullApp x = x
1670 match' x y = match (fullApp x) (fullApp y)
1671 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1672 | fi == txt "fromInteger" && b == txt "builtins",
1673 PConstant (I _) <- getTm x = match (getTm x) x'
1674 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1675 | fi == txt "fromInteger" && b == txt "builtins",
1676 PConstant (I _) <- getTm x = match (getTm x) x'
1677 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1678 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1679 match (PApp _ f args) (PApp _ f' args')
1680 | length args == length args'
1681 = do mf <- match' f f'
1682 ms <- zipWithM matchArg args args'
1683 return (mf ++ concat ms)
1684 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1685 match (PPatvar f n) xr = match (PRef f n) xr
1686 match xr (PPatvar f n) = match xr (PRef f n)
1687 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1688 match (PRef _ n) tm@(PRef _ n')
1689 | n == n' && not names &&
1690 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1691 || tm == Placeholder)
1692 = return [(n, tm)]
1693 -- if one namespace is missing, drop the other
1694 | n == n' || n == dropNS n' || dropNS n == n' = return []
1695 where dropNS (NS n _) = n
1696 dropNS n = n
1697 match (PRef _ n) tm
1698 | not names && (not (isConName n (tt_ctxt i) ||
1699 isFnName n (tt_ctxt i)) || tm == Placeholder)
1700 = return [(n, tm)]
1701 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1702 = do ml <- match' l l'
1703 mr <- match' r r'
1704 return (ml ++ mr)
1705 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1706 = do ml <- match' l l'
1707 mr <- match' r r'
1708 return (ml ++ mr)
1709 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1710 mr <- match r r'
1711 return (ml ++ mr)
1712 match (PTyped l r) x = match l x
1713 match x (PTyped l r) = match x l
1714 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1715 mr <- match' r r'
1716 return (ml ++ mr)
1717 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1718 mt <- match' t t'
1719 mr <- match' r r'
1720 return (ml ++ mt ++ mr)
1721 match (PAlternative a as) (PAlternative a' as')
1722 = do ms <- zipWithM match' as as'
1723 return (concat ms)
1724 match a@(PAlternative _ as) b
1725 = do let ms = zipWith match' as (repeat b)
1726 case (rights (map toEither ms)) of
1727 (x: _) -> return x
1728 _ -> LeftErr (a, b)
1729 match (PCase _ _ _) _ = return [] -- lifted out
1730 match (PMetavar _) _ = return [] -- modified
1731 match (PInferRef _ _) _ = return [] -- modified
1732 match (PQuote _) _ = return []
1733 match (PProof _) _ = return []
1734 match (PTactics _) _ = return []
1735 match (PRefl _ _) (PRefl _ _) = return []
1736 match (PResolveTC _) (PResolveTC _) = return []
1737 match (PTrue _ _) (PTrue _ _) = return []
1738 match (PFalse _) (PFalse _) = return []
1739 match (PReturn _) (PReturn _) = return []
1740 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1741 ms <- match' s s'
1742 return (mt ++ ms)
1743 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1744 ms <- match' s s'
1745 return (mt ++ ms)
1746 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1747 mty <- match' ty ty'
1748 ms <- match' s s'
1749 return (mt ++ mty ++ ms)
1750 match (PHidden x) (PHidden y) = match' x y
1751 match (PUnifyLog x) y = match' x y
1752 match x (PUnifyLog y) = match' x y
1753 match (PNoImplicits x) y = match' x y
1754 match x (PNoImplicits y) = match' x y
1755 match Placeholder _ = return []
1756 match _ Placeholder = return []
1757 match (PResolveTC _) _ = return []
1758 match a b | a == b = return []
1759 | otherwise = LeftErr (a, b)
1761 checkRpts (RightOK ms) = check ms where
1762 check ((n,t):xs)
1763 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1764 then Left (t, t')
1765 else check xs
1766 check (_:xs) = check xs
1767 check [] = Right ms
1768 checkRpts (LeftErr x) = Left x
1770substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1771substMatches ms = substMatchesShadow ms []
1773substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1774substMatchesShadow [] shs t = t
1775substMatchesShadow ((n,tm):ns) shs t
1776 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1778substMatch :: Name -> PTerm -> PTerm -> PTerm
1779substMatch n = substMatchShadow n []
1781substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1782substMatchShadow n shs tm t = sm shs t where
1783 sm xs (PRef _ n') | n == n' = tm
1784 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1785 sm xs (PPi p x t sc)
1786 | x `elem` xs
1787 = let x' = nextName x in
1788 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1789 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1790 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1791 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1792 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1793 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1794 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1795 (fmap (sm xs) tm)
1796 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1797 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1798 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1799 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1800 sm xs (PHidden x) = PHidden (sm xs x)
1801 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1802 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1803 sm xs x = x
1805 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1806 fullApp x = x
1808shadow :: Name -> Name -> PTerm -> PTerm
1809shadow n n' t = sm t where
1810 sm (PRef fc x) | n == x = PRef fc n'
1811 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1812 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1813 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1814 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1815 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1816 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1817 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1818 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1819 sm (PTyped x y) = PTyped (sm x) (sm y)
1820 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1821 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1822 sm (PAlternative a as) = PAlternative a (map sm as)
1823 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1824 sm (PProof ts) = PProof (map (fmap sm) ts)
1825 sm (PHidden x) = PHidden (sm x)
1826 sm (PUnifyLog x) = PUnifyLog (sm x)
1827 sm (PNoImplicits x) = PNoImplicits (sm x)
1828 sm x = x
1830-- Rename any binders which are repeated (so that we don't have to mess
1831-- about with shadowing anywhere else).
1833mkUniqueNames :: [Name] -> PTerm -> PTerm
1834mkUniqueNames env tm = evalState (mkUniq tm) env where
1835 inScope = boundNamesIn tm
1837 mkUniqA arg = do t' <- mkUniq (getTm arg)
1838 return (arg { getTm = t' })
1840 -- Initialise the unique name with the environment length (so we're not
1841 -- looking for too long...)
1842 initN (UN n) l = UN $ txt (str n ++ show l)
1843 initN (MN i s) l = MN (i+l) s
1844 initN n l = n
1846 -- FIXME: Probably ought to do this for completeness! It's fine as
1847 -- long as there are no bindings inside tactics though.
1848 mkUniqT tac = return tac
1850 mkUniq :: PTerm -> State [Name] PTerm
1851 mkUniq (PLam n ty sc)
1852 = do env <- get
1853 (n', sc') <-
1854 if n `elem` env
1855 then do let n' = uniqueName (initN n (length env))
1856 (env ++ inScope)
1857 return (n', shadow n n' sc)
1858 else return (n, sc)
1859 put (n' : env)
1860 ty' <- mkUniq ty
1861 sc'' <- mkUniq sc'
1862 return $! PLam n' ty' sc''
1863 mkUniq (PPi p n ty sc)
1864 = do env <- get
1865 (n', sc') <-
1866 if n `elem` env
1867 then do let n' = uniqueName (initN n (length env))
1868 (env ++ inScope)
1869 return (n', shadow n n' sc)
1870 else return (n, sc)
1871 put (n' : env)
1872 ty' <- mkUniq ty
1873 sc'' <- mkUniq sc'
1874 return $! PPi p n' ty' sc''
1875 mkUniq (PLet n ty val sc)
1876 = do env <- get
1877 (n', sc') <-
1878 if n `elem` env
1879 then do let n' = uniqueName (initN n (length env))
1880 (env ++ inScope)
1881 return (n', shadow n n' sc)
1882 else return (n, sc)
1883 put (n' : env)
1884 ty' <- mkUniq ty; val' <- mkUniq val
1885 sc'' <- mkUniq sc'
1886 return $! PLet n' ty' val' sc''
1887 mkUniq (PApp fc t args)
1888 = do t' <- mkUniq t
1889 args' <- mapM mkUniqA args
1890 return $! PApp fc t' args'
1891 mkUniq (PAppBind fc t args)
1892 = do t' <- mkUniq t
1893 args' <- mapM mkUniqA args
1894 return $! PAppBind fc t' args'
1895 mkUniq (PCase fc t alts)
1896 = do t' <- mkUniq t
1897 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1898 return (x', y')) alts
1899 return $! PCase fc t' alts'
1900 mkUniq (PPair fc p l r)
1901 = do l' <- mkUniq l; r' <- mkUniq r
1902 return $! PPair fc p l' r'
1903 mkUniq (PDPair fc p (PRef fc' n) t sc)
1904 | t /= Placeholder
1905 = do env <- get
1906 (n', sc') <- if n `elem` env
1907 then do let n' = uniqueName n (env ++ inScope)
1908 return (n', shadow n n' sc)
1909 else return (n, sc)
1910 put (n' : env)
1911 t' <- mkUniq t
1912 sc'' <- mkUniq sc'
1913 return $! PDPair fc p (PRef fc' n') t' sc''
1914 mkUniq (PDPair fc p l t r)
1915 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1916 return $! PDPair fc p l' t' r'
1917 mkUniq (PAlternative b as)
1918 = liftM (PAlternative b) (mapM mkUniq as)
1919 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1920 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1921 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1922 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1923 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1924 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1925 mkUniq t = return t