git.iko.soy/Idris-dev
on 5ffef89 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1926 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 tidyNames used (Bind (MN i x) b sc)
486 = let n' = uniqueName (UN x) used in
487 Bind n' b $ tidyNames (n':used) sc
488 tidyNames used (Bind n b sc)
489 = let n' = uniqueName n used in
490 Bind n' b $ tidyNames (n':used) sc
491 tidyNames used b = b
493solveDeferred :: Name -> Idris ()
494solveDeferred n = do i <- getIState
495 putIState $ i { idris_metavars =
496 filter (\(n', _) -> n/=n')
497 (idris_metavars i),
498 ibc_write =
499 filter (notMV n) (ibc_write i)
500 }
501 where notMV n (IBCMetavar n') = not (n == n')
502 notMV n _ = True
504getUndefined :: Idris [Name]
505getUndefined = do i <- getIState
506 return (map fst (idris_metavars i) \\ primDefs)
508isMetavarName :: Name -> IState -> Bool
509isMetavarName n ist
510 = case lookupNames n (tt_ctxt ist) of
511 (t:_) -> isJust $ lookup t (idris_metavars ist)
512 _ -> False
514getWidth :: Idris ConsoleWidth
515getWidth = fmap idris_consolewidth getIState
517setWidth :: ConsoleWidth -> Idris ()
518setWidth w = do ist <- getIState
519 put ist { idris_consolewidth = w }
521renderWidth :: Idris Int
522renderWidth = do iw <- getWidth
523 case iw of
524 InfinitelyWide -> return 100000000
525 ColsWide n -> return (max n 1)
526 AutomaticWidth -> runIO getScreenWidth
530type1Doc :: Doc OutputAnnotation
531type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
534isetPrompt :: String -> Idris ()
535isetPrompt p = do i <- getIState
536 case idris_outputmode i of
537 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
539-- | Tell clients how much was parsed and loaded
540isetLoadedRegion :: Idris ()
541isetLoadedRegion = do i <- getIState
542 let span = idris_parsedSpan i
543 case span of
544 Just fc ->
545 case idris_outputmode i of
546 IdeSlave n ->
547 runIO . putStrLn $
548 convSExp "set-loaded-region" fc n
549 Nothing -> return ()
551setLogLevel :: Int -> Idris ()
552setLogLevel l = do i <- getIState
553 let opts = idris_options i
554 let opt' = opts { opt_logLevel = l }
555 putIState $ i { idris_options = opt' }
557setCmdLine :: [Opt] -> Idris ()
558setCmdLine opts = do i <- getIState
559 let iopts = idris_options i
560 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
562getCmdLine :: Idris [Opt]
563getCmdLine = do i <- getIState
564 return (opt_cmdline (idris_options i))
566getDumpDefun :: Idris (Maybe FilePath)
567getDumpDefun = do i <- getIState
568 return $ findC (opt_cmdline (idris_options i))
569 where findC [] = Nothing
570 findC (DumpDefun x : _) = Just x
571 findC (_ : xs) = findC xs
573getDumpCases :: Idris (Maybe FilePath)
574getDumpCases = do i <- getIState
575 return $ findC (opt_cmdline (idris_options i))
576 where findC [] = Nothing
577 findC (DumpCases x : _) = Just x
578 findC (_ : xs) = findC xs
580logLevel :: Idris Int
581logLevel = do i <- getIState
582 return (opt_logLevel (idris_options i))
584setErrContext :: Bool -> Idris ()
585setErrContext t = do i <- getIState
586 let opts = idris_options i
587 let opt' = opts { opt_errContext = t }
588 putIState $ i { idris_options = opt' }
590errContext :: Idris Bool
591errContext = do i <- getIState
592 return (opt_errContext (idris_options i))
594useREPL :: Idris Bool
595useREPL = do i <- getIState
596 return (opt_repl (idris_options i))
598setREPL :: Bool -> Idris ()
599setREPL t = do i <- getIState
600 let opts = idris_options i
601 let opt' = opts { opt_repl = t }
602 putIState $ i { idris_options = opt' }
604showOrigErr :: Idris Bool
605showOrigErr = do i <- getIState
606 return (opt_origerr (idris_options i))
608setShowOrigErr :: Bool -> Idris ()
609setShowOrigErr b = do i <- getIState
610 let opts = idris_options i
611 let opt' = opts { opt_origerr = b }
612 putIState $ i { idris_options = opt' }
614setAutoSolve :: Bool -> Idris ()
615setAutoSolve b = do i <- getIState
616 let opts = idris_options i
617 let opt' = opts { opt_autoSolve = b }
618 putIState $ i { idris_options = opt' }
620setNoBanner :: Bool -> Idris ()
621setNoBanner n = do i <- getIState
622 let opts = idris_options i
623 let opt' = opts { opt_nobanner = n }
624 putIState $ i { idris_options = opt' }
626getNoBanner :: Idris Bool
627getNoBanner = do i <- getIState
628 let opts = idris_options i
629 return (opt_nobanner opts)
631setQuiet :: Bool -> Idris ()
632setQuiet q = do i <- getIState
633 let opts = idris_options i
634 let opt' = opts { opt_quiet = q }
635 putIState $ i { idris_options = opt' }
637getQuiet :: Idris Bool
638getQuiet = do i <- getIState
639 let opts = idris_options i
640 return (opt_quiet opts)
642setCodegen :: Codegen -> Idris ()
643setCodegen t = do i <- getIState
644 let opts = idris_options i
645 let opt' = opts { opt_codegen = t }
646 putIState $ i { idris_options = opt' }
648codegen :: Idris Codegen
649codegen = do i <- getIState
650 return (opt_codegen (idris_options i))
652setOutputTy :: OutputType -> Idris ()
653setOutputTy t = do i <- getIState
654 let opts = idris_options i
655 let opt' = opts { opt_outputTy = t }
656 putIState $ i { idris_options = opt' }
658outputTy :: Idris OutputType
659outputTy = do i <- getIState
660 return $ opt_outputTy $ idris_options i
662setIdeSlave :: Bool -> Idris ()
663setIdeSlave True = do i <- getIState
664 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
665setIdeSlave False = return ()
667setTargetTriple :: String -> Idris ()
668setTargetTriple t = do i <- getIState
669 let opts = idris_options i
670 opt' = opts { opt_triple = t }
671 putIState $ i { idris_options = opt' }
673targetTriple :: Idris String
674targetTriple = do i <- getIState
675 return (opt_triple (idris_options i))
677setTargetCPU :: String -> Idris ()
678setTargetCPU t = do i <- getIState
679 let opts = idris_options i
680 opt' = opts { opt_cpu = t }
681 putIState $ i { idris_options = opt' }
683targetCPU :: Idris String
684targetCPU = do i <- getIState
685 return (opt_cpu (idris_options i))
687setOptLevel :: Word -> Idris ()
688setOptLevel t = do i <- getIState
689 let opts = idris_options i
690 opt' = opts { opt_optLevel = t }
691 putIState $ i { idris_options = opt' }
693optLevel :: Idris Word
694optLevel = do i <- getIState
695 return (opt_optLevel (idris_options i))
697verbose :: Idris Bool
698verbose = do i <- getIState
699 return (opt_verbose (idris_options i))
701setVerbose :: Bool -> Idris ()
702setVerbose t = do i <- getIState
703 let opts = idris_options i
704 let opt' = opts { opt_verbose = t }
705 putIState $ i { idris_options = opt' }
707typeInType :: Idris Bool
708typeInType = do i <- getIState
709 return (opt_typeintype (idris_options i))
711setTypeInType :: Bool -> Idris ()
712setTypeInType t = do i <- getIState
713 let opts = idris_options i
714 let opt' = opts { opt_typeintype = t }
715 putIState $ i { idris_options = opt' }
717coverage :: Idris Bool
718coverage = do i <- getIState
719 return (opt_coverage (idris_options i))
721setCoverage :: Bool -> Idris ()
722setCoverage t = do i <- getIState
723 let opts = idris_options i
724 let opt' = opts { opt_coverage = t }
725 putIState $ i { idris_options = opt' }
727setIBCSubDir :: FilePath -> Idris ()
728setIBCSubDir fp = do i <- getIState
729 let opts = idris_options i
730 let opt' = opts { opt_ibcsubdir = fp }
731 putIState $ i { idris_options = opt' }
733valIBCSubDir :: IState -> Idris FilePath
734valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
736addImportDir :: FilePath -> Idris ()
737addImportDir fp = do i <- getIState
738 let opts = idris_options i
739 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
740 putIState $ i { idris_options = opt' }
742setImportDirs :: [FilePath] -> Idris ()
743setImportDirs fps = do i <- getIState
744 let opts = idris_options i
745 let opt' = opts { opt_importdirs = fps }
746 putIState $ i { idris_options = opt' }
748allImportDirs :: Idris [FilePath]
749allImportDirs = do i <- getIState
750 let optdirs = opt_importdirs (idris_options i)
751 return ("." : reverse optdirs)
753colourise :: Idris Bool
754colourise = do i <- getIState
755 return $ idris_colourRepl i
757setColourise :: Bool -> Idris ()
758setColourise b = do i <- getIState
759 putIState $ i { idris_colourRepl = b }
761setOutH :: Handle -> Idris ()
762setOutH h = do i <- getIState
763 putIState $ i { idris_outh = h }
765impShow :: Idris Bool
766impShow = do i <- getIState
767 return (opt_showimp (idris_options i))
769setImpShow :: Bool -> Idris ()
770setImpShow t = do i <- getIState
771 let opts = idris_options i
772 let opt' = opts { opt_showimp = t }
773 putIState $ i { idris_options = opt' }
775setColour :: ColourType -> IdrisColour -> Idris ()
776setColour ct c = do i <- getIState
777 let newTheme = setColour' ct c (idris_colourTheme i)
778 putIState $ i { idris_colourTheme = newTheme }
779 where setColour' KeywordColour c t = t { keywordColour = c }
780 setColour' BoundVarColour c t = t { boundVarColour = c }
781 setColour' ImplicitColour c t = t { implicitColour = c }
782 setColour' FunctionColour c t = t { functionColour = c }
783 setColour' TypeColour c t = t { typeColour = c }
784 setColour' DataColour c t = t { dataColour = c }
785 setColour' PromptColour c t = t { promptColour = c }
786 setColour' PostulateColour c t = t { postulateColour = c }
788logLvl :: Int -> String -> Idris ()
789logLvl l str = do i <- getIState
790 let lvl = opt_logLevel (idris_options i)
791 when (lvl >= l) $
792 case idris_outputmode i of
793 RawOutput -> do runIO $ putStrLn str
794 IdeSlave n ->
795 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
796 runIO $ putStrLn $ convSExp "log" good n
798cmdOptType :: Opt -> Idris Bool
799cmdOptType x = do i <- getIState
800 return $ x `elem` opt_cmdline (idris_options i)
802iLOG :: String -> Idris ()
803iLOG = logLvl 1
805noErrors :: Idris Bool
806noErrors = do i <- getIState
807 case errSpan i of
808 Nothing -> return True
809 _ -> return False
811setTypeCase :: Bool -> Idris ()
812setTypeCase t = do i <- getIState
813 let opts = idris_options i
814 let opt' = opts { opt_typecase = t }
815 putIState $ i { idris_options = opt' }
818-- Dealing with parameters
820expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
821 [Name] -> -- all names
822 [Name] -> -- names with no declaration
823 PTerm -> PTerm
824expandParams dec ps ns infs tm = en tm
825 where
826 -- if we shadow a name (say in a lambda binding) that is used in a call to
827 -- a lifted function, we need access to both names - once in the scope of the
828 -- binding and once to call the lifted functions. So we'll explicitly shadow
829 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
830 -- but we didn't...)
832 mkShadow (UN n) = MN 0 n
833 mkShadow (MN i n) = MN (i+1) n
834 mkShadow (NS x s) = NS (mkShadow x) s
836 en (PLam n t s)
837 | n `elem` (map fst ps ++ ns)
838 = let n' = mkShadow n in
839 PLam n' (en t) (en (shadow n n' s))
840 | otherwise = PLam n (en t) (en s)
841 en (PPi p n t s)
842 | n `elem` (map fst ps ++ ns)
843 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
844 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
845 | otherwise = PPi (enTacImp p) n (en t) (en s)
846 en (PLet n ty v s)
847 | n `elem` (map fst ps ++ ns)
848 = let n' = mkShadow n in
849 PLet n' (en ty) (en v) (en (shadow n n' s))
850 | otherwise = PLet n (en ty) (en v) (en s)
851 -- FIXME: Should only do this in a type signature!
852 en (PDPair f p (PRef f' n) t r)
853 | n `elem` (map fst ps ++ ns) && t /= Placeholder
854 = let n' = mkShadow n in
855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
856 en (PEq f l r) = PEq f (en l) (en r)
857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
858 en (PTyped l r) = PTyped (en l) (en r)
859 en (PPair f p l r) = PPair f p (en l) (en r)
860 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
861 en (PAlternative a as) = PAlternative a (map en as)
862 en (PHidden t) = PHidden (en t)
863 en (PUnifyLog t) = PUnifyLog (en t)
864 en (PDisamb ds t) = PDisamb ds (en t)
865 en (PNoImplicits t) = PNoImplicits (en t)
866 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
867 en (PProof ts) = PProof (map (fmap en) ts)
868 en (PTactics ts) = PTactics (map (fmap en) ts)
870 en (PQuote (Var n))
871 | n `nselem` ns = PQuote (Var (dec n))
872 en (PApp fc (PInferRef fc' n) as)
873 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
874 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
875 en (PApp fc (PRef fc' n) as)
876 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
877 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
878 | n `nselem` ns = PApp fc (PRef fc' (dec n))
879 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
880 en (PAppBind fc (PRef fc' n) as)
881 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
882 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
883 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
884 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
885 en (PRef fc n)
886 | n `elem` infs = PApp fc (PInferRef fc (dec n))
887 (map (pexp . (PRef fc)) (map fst ps))
888 | n `nselem` ns = PApp fc (PRef fc (dec n))
889 (map (pexp . (PRef fc)) (map fst ps))
890 en (PInferRef fc n)
891 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
892 (map (pexp . (PRef fc)) (map fst ps))
893 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
894 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
895 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
896 en t = t
898 nselem x [] = False
899 nselem x (y : xs) | nseq x y = True
900 | otherwise = nselem x xs
902 nseq x y = nsroot x == nsroot y
904 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
905 enTacImp other = other
907expandParamsD :: Bool -> -- True = RHS only
908 IState ->
909 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
910expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
911 = if n `elem` ns && (not rhsonly)
912 then -- trace (show (n, expandParams dec ps ns ty)) $
913 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
914 else --trace (show (n, expandParams dec ps ns ty)) $
915 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
916expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
917 = if n `elem` ns && (not rhsonly)
918 then -- trace (show (n, expandParams dec ps ns ty)) $
919 PPostulate doc syn fc o (dec n) (piBind ps
920 (expandParams dec ps ns [] ty))
921 else --trace (show (n, expandParams dec ps ns ty)) $
922 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
923expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
924 = let n' = if n `elem` ns then dec n else n in
925 PClauses fc opts n' (map expandParamsC cs)
926 where
927 expandParamsC (PClause fc n lhs ws rhs ds)
928 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
929 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
930 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
931 n' = if n `elem` ns then dec n else n
932 -- names bound on the lhs should not be expanded on the rhs
933 ns' = removeBound lhs ns in
934 PClause fc n' lhs'
935 (map (expandParams dec ps'' ns' []) ws)
936 (expandParams dec ps'' ns' [] rhs)
937 (map (expandParamsD True ist dec ps'' ns') ds)
938 expandParamsC (PWith fc n lhs ws wval ds)
939 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
940 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
941 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
942 n' = if n `elem` ns then dec n else n
943 ns' = removeBound lhs ns in
944 PWith fc n' lhs'
945 (map (expandParams dec ps'' ns' []) ws)
946 (expandParams dec ps'' ns' [] wval)
947 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
948 updateps yn nm [] = []
949 updateps yn nm (((a, t), i):as)
950 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
951 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
953 removeBound lhs ns = ns \\ nub (bnames lhs)
955 bnames (PRef _ n) = [n]
956 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
957 bnames (PPair _ _ l r) = bnames l ++ bnames r
958 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
959 bnames _ = []
961-- | Expands parameters defined in parameter and where blocks inside of declarations
962expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
963 = PData doc argDocs syn fc co (expandPData pd)
964 where
965 -- just do the type decl, leave constructors alone (parameters will be
966 -- added implicitly)
967 expandPData (PDatadecl n ty cons)
968 = if n `elem` ns
969 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
970 (map econ cons)
971 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
972 econ (doc, argDocs, n, t, fc, fs)
973 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
974expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
975 = if tn `elem` ns
976 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
977 opts cdoc (dec cn) conty
978 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
979 opts cdoc (dec cn) conty
980 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
981expandParamsD rhs ist dec ps ns (PParams f params pds)
982 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
983 (map (expandParamsD True ist dec ps ns) pds)
984-- (map (expandParamsD ist dec ps ns) pds)
985expandParamsD rhs ist dec ps ns (PMutual f pds)
986 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
987expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
988 = PClass doc info f
989 (map (expandParams dec ps ns []) cs)
990 n
991 (map (mapsnd (expandParams dec ps ns [])) params)
992 pDocs
993 (map (expandParamsD rhs ist dec ps ns) decls)
994expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
995 = PInstance info f
996 (map (expandParams dec ps ns []) cs)
997 n
998 (map (expandParams dec ps ns []) params)
999 (expandParams dec ps ns [] ty)
1000 cn
1001 (map (expandParamsD rhs ist dec ps ns) decls)
1002expandParamsD rhs ist dec ps ns d = d
1004mapsnd f (x, t) = (x, f t)
1006-- Calculate a priority for a type, for deciding elaboration order
1007-- * if it's just a type variable or concrete type, do it early (0)
1008-- * if there's only type variables and injective constructors, do it next (1)
1009-- * if there's a function type, next (2)
1010-- * finally, everything else (3)
1012getPriority :: IState -> PTerm -> Int
1013getPriority i tm = 1 -- pri tm
1014 where
1015 pri (PRef _ n) =
1016 case lookupP n (tt_ctxt i) of
1017 ((P (DCon _ _) _ _):_) -> 1
1018 ((P (TCon _ _) _ _):_) -> 1
1019 ((P Ref _ _):_) -> 1
1020 [] -> 0 -- must be locally bound, if it's not an error...
1021 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1022 pri (PTrue _ _) = 0
1023 pri (PFalse _) = 0
1024 pri (PRefl _ _) = 1
1025 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1026 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1027 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1028 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1029 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1030 pri (PTyped l r) = pri l
1031 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1032 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1033 pri (PAlternative a as) = maximum (map pri as)
1034 pri (PConstant _) = 0
1035 pri Placeholder = 1
1036 pri _ = 3
1039addStatics :: Name -> Term -> PTerm -> Idris ()
1040addStatics n tm ptm =
1041 do let (statics, dynamics) = initStatics tm ptm
1042 let stnames = nub $ concatMap freeArgNames (map snd statics)
1043 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1044 -- also get the arguments which are 'uniquely inferrable' from
1045 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1046 let statics' = nub $ map fst statics ++
1047 filter (\x -> not (elem x dnames)) stnames
1048 let stpos = staticList statics' tm
1049 i <- getIState
1050 when (not (null statics)) $
1051 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1052 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1053 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1054 addIBC (IBCStatic n)
1055 where
1056 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1057 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1058 if pstatic p == Static then ((n, ty) : static, dynamic)
1059 else if (not (searchArg p))
1060 then (static, (n, ty) : dynamic)
1061 else (static, dynamic)
1062 initStatics t pt = ([], [])
1064 freeArgNames (Bind n (Pi ty) sc)
1065 = nub $ freeArgNames ty
1066 freeArgNames tm = let (_, args) = unApply tm in
1067 concatMap freeNames args
1069 -- if a name appears in a type class or tactic implicit index, it doesn't
1070 -- affect its 'uniquely inferrable' from a static status since these are
1071 -- resolved by searching.
1072 searchArg (Constraint _ _) = True
1073 searchArg (TacImp _ _ _) = True
1074 searchArg _ = False
1076 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1077 staticList _ _ = []
1079-- Dealing with implicit arguments
1081-- Add some bound implicits to the using block if they aren't there already
1083addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1084addToUsing us [] = us
1085addToUsing us ((n, t) : ns)
1086 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1087 | otherwise = addToUsing us ns
1088 where impName (UImplicit n _) = Just n
1089 impName _ = Nothing
1091-- Add constraint bindings from using block
1093addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1094addUsingConstraints syn fc t
1095 = do ist <- get
1096 let ns = namesIn [] ist t
1097 let cs = getConstraints t -- check declared constraints
1098 let addconsts = uconsts \\ cs
1099 -- if all names in the arguments of addconsts appear in ns,
1100 -- add the constraint implicitly
1101 return (doAdd addconsts ns t)
1102 where uconsts = filter uconst (using syn)
1103 uconst (UConstraint _ _) = True
1104 uconst _ = False
1106 doAdd [] _ t = t
1107 -- if all of args in ns, then add it
1108 doAdd (UConstraint c args : cs) ns t
1109 | all (\n -> elem n ns) args
1110 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1111 (mkConst c args) (doAdd cs ns t)
1112 | otherwise = doAdd cs ns t
1114 mkConst c args = PApp fc (PRef fc c)
1115 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1117 getConstraints (PPi (Constraint _ _) _ c sc)
1118 = getcapp c ++ getConstraints sc
1119 getConstraints (PPi _ _ c sc) = getConstraints sc
1120 getConstraints _ = []
1122 getcapp (PApp _ (PRef _ c) args)
1123 = do ns <- mapM getName args
1124 return (UConstraint c ns)
1125 getcapp _ = []
1127 getName (PExp _ _ _ (PRef _ n)) = return n
1128 getName _ = []
1130-- Add implicit bindings from using block, and bind any missing names
1131addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1132addUsingImpls syn n fc t
1133 = do ist <- getIState
1134 let ns = implicitNamesIn (map iname uimpls) ist t
1135 let badnames = filter (\n -> not (implicitable n) &&
1136 n `notElem` (map iname uimpls)) ns
1137 when (not (null badnames)) $
1138 throwError (At fc (Elaborating "type of " n
1139 (NoSuchVariable (head badnames))))
1140 let cs = getArgnames t -- get already bound names
1141 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1142 -- if all names in the arguments of addconsts appear in ns,
1143 -- add the constraint implicitly
1144 return (bindFree ns (doAdd addimpls ns t))
1145 where uimpls = filter uimpl (using syn)
1146 uimpl (UImplicit _ _) = True
1147 uimpl _ = False
1149 iname (UImplicit n _) = n
1150 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1152 doAdd [] _ t = t
1153 -- if all of args in ns, then add it
1154 doAdd (UImplicit n ty : cs) ns t
1155 | elem n ns
1156 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1157 | otherwise = doAdd cs ns t
1159 -- bind the free names which weren't in the using block
1160 bindFree [] tm = tm
1161 bindFree (n:ns) tm
1162 | elem n (map iname uimpls) = bindFree ns tm
1163 | otherwise
1164 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1166 getArgnames (PPi _ n c sc)
1167 = n : getArgnames sc
1168 getArgnames _ = []
1170-- Given the original type and the elaborated type, return the implicitness
1171-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1173getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1174getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')
1175 | n == n' = argInfo n p : getUnboundImplicits i sc sc'
1176 where
1177 argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')
1178 argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,
1179 PExp (getPriority i t') opt n t')
1180 argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,
1181 PConstraint 10 opt n t')
1182 argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,
1183 PTacImplicit 10 opt n scr t')
1184getUnboundImplicits i (Bind n (Pi t) sc) tm
1185 = impBind n t : getUnboundImplicits i sc tm
1186 where
1187 impBind n t = (True, PImp 1 True [] n Placeholder)
1188getUnboundImplicits i sc tm = []
1190-- Add implicit Pi bindings for any names in the term which appear in an
1191-- argument position.
1193-- This has become a right mess already. Better redo it some time...
1195implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1196implicit info syn n ptm = implicit' info syn [] n ptm
1198implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1199implicit' info syn ignore n ptm
1200 = do i <- getIState
1201 let (tm', impdata) = implicitise syn ignore i ptm
1202 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1203-- let (tm'', spos) = findStatics i tm'
1204 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1205 addIBC (IBCImp n)
1206 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1207-- i <- get
1208-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1209 return tm'
1210 where
1211 -- Detect unknown names in default arguments and throw error if found.
1212 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1213 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1215 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1216 notFoundInDefault kns (PTacImplicit _ _ n script _)
1217 = do i <- getIState
1218 case notFound kns (namesIn [] i script) of
1219 Nothing -> return (n:kns)
1220 Just name -> throwError (NoSuchVariable name)
1221 notFoundInDefault kns p = return ((pname p):kns)
1223 notFound :: [Name] -> [Name] -> Maybe Name
1224 notFound kns [] = Nothing
1225 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1226 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1228implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1229implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1230 let (declimps, ns') = execState (imps True [] tm) ([], [])
1231 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1232 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1233 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1234 if null ns
1235 then (tm, reverse declimps)
1236 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1237 where
1238 uvars = map ipair (filter uimplicit (using syn))
1239 pvars = syn_params syn
1241 inUsing n = n `elem` map fst uvars
1243 ipair (UImplicit x y) = (x, y)
1244 uimplicit (UImplicit _ _) = True
1245 uimplicit _ = False
1247 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1248 | otherwise = x : dropAll xs ys
1249 dropAll [] ys = []
1251 -- Find names in argument position in a type, suitable for implicit
1252 -- binding
1253 -- Not the function position, but do everything else...
1254 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1255 implNamesIn uv t = namesIn uv ist t
1257 imps top env (PApp _ f as)
1258 = do (decls, ns) <- get
1259 let isn = concatMap (namesIn uvars ist) (map getTm as)
1260 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1261 imps top env (PPi (Imp l _ _) n ty sc)
1262 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1263 (decls , ns) <- get
1264 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1265 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1266 imps True (n:env) sc
1267 imps top env (PPi (Exp l _ _) n ty sc)
1268 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1269 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1270 _ -> [])
1271 (decls, ns) <- get -- ignore decls in HO types
1272 put (PExp (getPriority ist ty) l n Placeholder : decls,
1273 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1274 imps True (n:env) sc
1275 imps top env (PPi (Constraint l _) n ty sc)
1276 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1277 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1278 _ -> [])
1279 (decls, ns) <- get -- ignore decls in HO types
1280 put (PConstraint 10 l n Placeholder : decls,
1281 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1282 imps True (n:env) sc
1283 imps top env (PPi (TacImp l _ scr) n ty sc)
1284 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1285 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1286 _ -> [])
1287 (decls, ns) <- get -- ignore decls in HO types
1288 put (PTacImplicit 10 l n scr Placeholder : decls,
1289 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1290 imps True (n:env) sc
1291 imps top env (PEq _ l r)
1292 = do (decls, ns) <- get
1293 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1294 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1295 imps top env (PRewrite _ l r _)
1296 = do (decls, ns) <- get
1297 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1298 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1299 imps top env (PTyped l r)
1300 = imps top env l
1301 imps top env (PPair _ _ l r)
1302 = do (decls, ns) <- get
1303 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1304 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1305 imps top env (PDPair _ _ (PRef _ n) t r)
1306 = do (decls, ns) <- get
1307 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1308 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1309 imps top env (PDPair _ _ l t r)
1310 = do (decls, ns) <- get
1311 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1312 namesIn uvars ist r
1313 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1314 imps top env (PAlternative a as)
1315 = do (decls, ns) <- get
1316 let isn = concatMap (namesIn uvars ist) as
1317 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1318 imps top env (PLam n ty sc)
1319 = do imps False env ty
1320 imps False (n:env) sc
1321 imps top env (PHidden tm) = imps False env tm
1322 imps top env (PUnifyLog tm) = imps False env tm
1323 imps top env (PNoImplicits tm) = imps False env tm
1324 imps top env _ = return ()
1326 pibind using [] sc = sc
1327 pibind using (n:ns) sc
1328 = case lookup n using of
1329 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1330 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1331 (pibind using ns sc)
1333-- Add implicit arguments in function calls
1334addImplPat :: IState -> PTerm -> PTerm
1335addImplPat = addImpl' True [] []
1337addImplBound :: IState -> [Name] -> PTerm -> PTerm
1338addImplBound ist ns = addImpl' False ns [] ist
1340addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1341addImplBoundInf ist ns inf = addImpl' False ns inf ist
1343-- | Add the implicit arguments to applications in the term
1344addImpl :: IState -> PTerm -> PTerm
1345addImpl = addImpl' False [] []
1347-- TODO: in patterns, don't add implicits to function names guarded by constructors
1348-- and *not* inside a PHidden
1350addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1351addImpl' inpat env infns ist ptm
1352 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1353 where
1354 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1355 ai qq env ds (PRef fc f)
1356 | f `elem` infns = PInferRef fc f
1357 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1358 ai qq env ds (PHidden (PRef fc f))
1359 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1360 ai qq env ds (PEq fc l r)
1361 = let l' = ai qq env ds l
1362 r' = ai qq env ds r in
1363 PEq fc 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 ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)
1427 ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)
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') = do ml <- match' l l'
1702 mr <- match' r r'
1703 return (ml ++ mr)
1704 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1705 = do ml <- match' l l'
1706 mr <- match' r r'
1707 return (ml ++ mr)
1708 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1709 mr <- match r r'
1710 return (ml ++ mr)
1711 match (PTyped l r) x = match l x
1712 match x (PTyped l r) = match x l
1713 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1714 mr <- match' r r'
1715 return (ml ++ mr)
1716 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1717 mt <- match' t t'
1718 mr <- match' r r'
1719 return (ml ++ mt ++ mr)
1720 match (PAlternative a as) (PAlternative a' as')
1721 = do ms <- zipWithM match' as as'
1722 return (concat ms)
1723 match a@(PAlternative _ as) b
1724 = do let ms = zipWith match' as (repeat b)
1725 case (rights (map toEither ms)) of
1726 (x: _) -> return x
1727 _ -> LeftErr (a, b)
1728 match (PCase _ _ _) _ = return [] -- lifted out
1729 match (PMetavar _) _ = return [] -- modified
1730 match (PInferRef _ _) _ = return [] -- modified
1731 match (PQuote _) _ = return []
1732 match (PProof _) _ = return []
1733 match (PTactics _) _ = return []
1734 match (PRefl _ _) (PRefl _ _) = return []
1735 match (PResolveTC _) (PResolveTC _) = return []
1736 match (PTrue _ _) (PTrue _ _) = return []
1737 match (PFalse _) (PFalse _) = return []
1738 match (PReturn _) (PReturn _) = return []
1739 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1740 ms <- match' s s'
1741 return (mt ++ ms)
1742 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1743 ms <- match' s s'
1744 return (mt ++ ms)
1745 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1746 mty <- match' ty ty'
1747 ms <- match' s s'
1748 return (mt ++ mty ++ ms)
1749 match (PHidden x) (PHidden y) = match' x y
1750 match (PUnifyLog x) y = match' x y
1751 match x (PUnifyLog y) = match' x y
1752 match (PNoImplicits x) y = match' x y
1753 match x (PNoImplicits y) = match' x y
1754 match Placeholder _ = return []
1755 match _ Placeholder = return []
1756 match (PResolveTC _) _ = return []
1757 match a b | a == b = return []
1758 | otherwise = LeftErr (a, b)
1760 checkRpts (RightOK ms) = check ms where
1761 check ((n,t):xs)
1762 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1763 then Left (t, t')
1764 else check xs
1765 check (_:xs) = check xs
1766 check [] = Right ms
1767 checkRpts (LeftErr x) = Left x
1769substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1770substMatches ms = substMatchesShadow ms []
1772substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1773substMatchesShadow [] shs t = t
1774substMatchesShadow ((n,tm):ns) shs t
1775 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1777substMatch :: Name -> PTerm -> PTerm -> PTerm
1778substMatch n = substMatchShadow n []
1780substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1781substMatchShadow n shs tm t = sm shs t where
1782 sm xs (PRef _ n') | n == n' = tm
1783 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1784 sm xs (PPi p x t sc)
1785 | x `elem` xs
1786 = let x' = nextName x in
1787 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1788 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1789 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1790 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1791 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1792 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1793 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1794 (fmap (sm xs) tm)
1795 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1796 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1797 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1798 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1799 sm xs (PHidden x) = PHidden (sm xs x)
1800 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1801 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1802 sm xs x = x
1804 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1805 fullApp x = x
1807shadow :: Name -> Name -> PTerm -> PTerm
1808shadow n n' t = sm t where
1809 sm (PRef fc x) | n == x = PRef fc n'
1810 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1811 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1812 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1813 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1814 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1815 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1816 sm (PEq f x y) = PEq f (sm x) (sm y)
1817 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1818 sm (PTyped x y) = PTyped (sm x) (sm y)
1819 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1820 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1821 sm (PAlternative a as) = PAlternative a (map sm as)
1822 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1823 sm (PProof ts) = PProof (map (fmap sm) ts)
1824 sm (PHidden x) = PHidden (sm x)
1825 sm (PUnifyLog x) = PUnifyLog (sm x)
1826 sm (PNoImplicits x) = PNoImplicits (sm x)
1827 sm x = x
1829-- Rename any binders which are repeated (so that we don't have to mess
1830-- about with shadowing anywhere else).
1832mkUniqueNames :: [Name] -> PTerm -> PTerm
1833mkUniqueNames env tm = evalState (mkUniq tm) env where
1834 inScope = boundNamesIn tm
1836 mkUniqA arg = do t' <- mkUniq (getTm arg)
1837 return (arg { getTm = t' })
1839 -- Initialise the unique name with the environment length (so we're not
1840 -- looking for too long...)
1841 initN (UN n) l = UN $ txt (str n ++ show l)
1842 initN (MN i s) l = MN (i+l) s
1843 initN n l = n
1845 -- FIXME: Probably ought to do this for completeness! It's fine as
1846 -- long as there are no bindings inside tactics though.
1847 mkUniqT tac = return tac
1849 mkUniq :: PTerm -> State [Name] PTerm
1850 mkUniq (PLam n ty sc)
1851 = do env <- get
1852 (n', sc') <-
1853 if n `elem` env
1854 then do let n' = uniqueName (initN n (length env))
1855 (env ++ inScope)
1856 return (n', shadow n n' sc)
1857 else return (n, sc)
1858 put (n' : env)
1859 ty' <- mkUniq ty
1860 sc'' <- mkUniq sc'
1861 return $! PLam n' ty' sc''
1862 mkUniq (PPi p n ty sc)
1863 = do env <- get
1864 (n', sc') <-
1865 if n `elem` env
1866 then do let n' = uniqueName (initN n (length env))
1867 (env ++ inScope)
1868 return (n', shadow n n' sc)
1869 else return (n, sc)
1870 put (n' : env)
1871 ty' <- mkUniq ty
1872 sc'' <- mkUniq sc'
1873 return $! PPi p n' ty' sc''
1874 mkUniq (PLet n ty val sc)
1875 = do env <- get
1876 (n', sc') <-
1877 if n `elem` env
1878 then do let n' = uniqueName (initN n (length env))
1879 (env ++ inScope)
1880 return (n', shadow n n' sc)
1881 else return (n, sc)
1882 put (n' : env)
1883 ty' <- mkUniq ty; val' <- mkUniq val
1884 sc'' <- mkUniq sc'
1885 return $! PLet n' ty' val' sc''
1886 mkUniq (PApp fc t args)
1887 = do t' <- mkUniq t
1888 args' <- mapM mkUniqA args
1889 return $! PApp fc t' args'
1890 mkUniq (PAppBind fc t args)
1891 = do t' <- mkUniq t
1892 args' <- mapM mkUniqA args
1893 return $! PAppBind fc t' args'
1894 mkUniq (PCase fc t alts)
1895 = do t' <- mkUniq t
1896 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1897 return (x', y')) alts
1898 return $! PCase fc t' alts'
1899 mkUniq (PPair fc p l r)
1900 = do l' <- mkUniq l; r' <- mkUniq r
1901 return $! PPair fc p l' r'
1902 mkUniq (PDPair fc p (PRef fc' n) t sc)
1903 | t /= Placeholder
1904 = do env <- get
1905 (n', sc') <- if n `elem` env
1906 then do let n' = uniqueName n (env ++ inScope)
1907 return (n', shadow n n' sc)
1908 else return (n, sc)
1909 put (n' : env)
1910 t' <- mkUniq t
1911 sc'' <- mkUniq sc'
1912 return $! PDPair fc p (PRef fc' n') t' sc''
1913 mkUniq (PDPair fc p l t r)
1914 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1915 return $! PDPair fc p l' t' r'
1916 mkUniq (PAlternative b as)
1917 = liftM (PAlternative b) (mapM mkUniq as)
1918 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1919 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1920 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1921 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1922 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1923 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1924 mkUniq t = return t