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