git.iko.soy/Idris-dev
on ef45cdc help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1832 lines 75 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 Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.State
23import Control.Monad.Error(throwError)
25import Data.List
26import Data.Char
27import qualified Data.Text as T
28import Data.Either
29import qualified Data.Map as M
30import Data.Maybe
31import qualified Data.Set as S
32import Data.Word (Word)
34import Debug.Trace
36import Control.Monad.Error (throwError, catchError)
37import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
39import Util.Pretty
40import Util.ScreenSize
41import Util.System
43getContext :: Idris Context
44getContext = do i <- getIState; return (tt_ctxt i)
46forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
49getObjectFiles :: Codegen -> Idris [FilePath]
50getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
52addObjectFile :: Codegen -> FilePath -> Idris ()
53addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
55getLibs :: Codegen -> Idris [String]
56getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
58addLib :: Codegen -> String -> Idris ()
59addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
61getFlags :: Codegen -> Idris [String]
62getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
64addFlag :: Codegen -> String -> Idris ()
65addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
67addDyLib :: [String] -> Idris (Either DynamicLib String)
68addDyLib libs = do i <- getIState
69 let ls = idris_dynamic_libs i
70 let importdirs = opt_importdirs (idris_options i)
71 case mapMaybe (findDyLib ls) libs of
72 x:_ -> return (Left x)
73 [] -> do
74 handle <- lift . lift .
75 mapM (\l -> catchIO (tryLoadLib importdirs l)
76 (\_ -> return Nothing)) $ libs
77 case msum handle of
78 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
79 concat (intersperse "," libs) ++ "\"")
80 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
81 return (Left x)
82 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
83 findDyLib [] l = Nothing
84 findDyLib (lib:libs) l | l == lib_name lib = Just lib
85 | otherwise = findDyLib libs l
88addHdr :: Codegen -> String -> Idris ()
89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
91addImported :: FilePath -> Idris ()
92addImported f = do i <- getIState
93 putIState $ i { idris_imported = nub $ f : idris_imported i }
95addLangExt :: LanguageExt -> Idris ()
96addLangExt TypeProviders = do i <- getIState
97 putIState $ i {
98 idris_language_extensions = TypeProviders : idris_language_extensions i
99 }
100addLangExt ErrorReflection = do i <- getIState
101 putIState $ i {
102 idris_language_extensions = ErrorReflection : idris_language_extensions i
103 }
105addTrans :: (Term, Term) -> Idris ()
106addTrans t = do i <- getIState
107 putIState $ i { idris_transforms = t : idris_transforms i }
109addErrRev :: (Term, Term) -> Idris ()
110addErrRev t = do i <- getIState
111 putIState $ i { idris_errRev = t : idris_errRev i }
113totcheck :: (FC, Name) -> Idris ()
114totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
116defer_totcheck :: (FC, Name) -> Idris ()
117defer_totcheck n
118 = do i <- getIState;
119 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
121clear_totcheck :: Idris ()
122clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
124setFlags :: Name -> [FnOpt] -> Idris ()
125setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
127setAccessibility :: Name -> Accessibility -> Idris ()
128setAccessibility n a
129 = do i <- getIState
130 let ctxt = setAccess n a (tt_ctxt i)
131 putIState $ i { tt_ctxt = ctxt }
133setTotality :: Name -> Totality -> Idris ()
134setTotality n a
135 = do i <- getIState
136 let ctxt = setTotal n a (tt_ctxt i)
137 putIState $ i { tt_ctxt = ctxt }
139getTotality :: Name -> Idris Totality
140getTotality n
141 = do i <- getIState
142 case lookupTotal n (tt_ctxt i) of
143 [t] -> return t
144 _ -> return (Total [])
146-- Get coercions which might return the required type
147getCoercionsTo :: IState -> Type -> [Name]
148getCoercionsTo i ty =
149 let cs = idris_coercions i
150 (fn,_) = unApply (getRetTy ty) in
151 findCoercions fn cs
152 where findCoercions t [] = []
153 findCoercions t (n : ns) =
154 let ps = case lookupTy n (tt_ctxt i) of
155 [ty'] -> case unApply (getRetTy ty') of
156 (t', _) ->
157 if t == t' then [n] else []
158 _ -> [] in
159 ps ++ findCoercions t ns
161addToCG :: Name -> CGInfo -> Idris ()
162addToCG n cg
163 = do i <- getIState
164 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
166addTyInferred :: Name -> Idris ()
167addTyInferred n
168 = do i <- getIState
169 putIState $ i { idris_tyinfodata =
170 addDef n TIPartial (idris_tyinfodata i) }
172addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
173addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
174 mapM_ addConstraint ts
175 return ()
176 where addConstraint (x, y) = findMVApps x y
178 findMVApps x y
179 = do let (fx, argsx) = unApply x
180 let (fy, argsy) = unApply y
181 if (not (fx == fy))
182 then do
183 tryAddMV fx y
184 tryAddMV fy x
185 else mapM_ addConstraint (zip argsx argsy)
187 tryAddMV (P _ mv _) y =
188 do ist <- get
189 case lookup mv (idris_metavars ist) of
190 Just _ -> addConstraintRule mv y
191 _ -> return ()
192 tryAddMV _ _ = return ()
194 addConstraintRule :: Name -> Term -> Idris ()
195 addConstraintRule n t
196 = do ist <- get
197 logLvl 1 $ "TI constraint: " ++ show (n, t)
198 case lookupCtxt n (idris_tyinfodata ist) of
199 [TISolution ts] ->
200 do mapM_ (checkConsistent t) ts
201 let ti' = addDef n (TISolution (t : ts))
202 (idris_tyinfodata ist)
203 put $ ist { idris_tyinfodata = ti' }
204 _ ->
205 do let ti' = addDef n (TISolution [t])
206 (idris_tyinfodata ist)
207 put $ ist { idris_tyinfodata = ti' }
209 -- Check a solution is consistent with previous solutions
210 -- Meaning: If heads are both data types, they had better be the
211 -- same.
212 checkConsistent :: Term -> Term -> Idris ()
213 checkConsistent x y =
214 do let (fx, _) = unApply x
215 let (fy, _) = unApply y
216 case (fx, fy) of
217 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
218 (P (TCon _ _) n _, Constant _) -> errWhen True
219 (Constant _, P (TCon _ _) n' _) -> errWhen True
220 (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)
221 _ -> return ()
223 where errWhen True
224 = throwError (At fc
225 (CantUnify False x y (Msg "") [] 0))
226 errWhen False = return ()
228isTyInferred :: Name -> Idris Bool
229isTyInferred n
230 = do i <- getIState
231 case lookupCtxt n (idris_tyinfodata i) of
232 [TIPartial] -> return True
233 _ -> return False
235-- | Adds error handlers for a particular function and argument. If names are
236-- ambiguous, all matching handlers are updated.
237addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
238addFunctionErrorHandlers f arg hs =
239 do i <- getIState
240 let oldHandlers = idris_function_errorhandlers i
241 let newHandlers = flip (addDef f) oldHandlers $
242 case lookupCtxtExact f oldHandlers of
243 Nothing -> M.singleton arg (S.fromList hs)
244 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
245 -- will always be one of those two, thus no extra case
246 putIState $ i { idris_function_errorhandlers = newHandlers }
248getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
249getFunctionErrorHandlers f arg = do i <- getIState
250 return . maybe [] S.toList $
251 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
254-- Trace all the names in a call graph starting at the given name
255getAllNames :: Name -> Idris [Name]
256getAllNames n = allNames [] n
258allNames :: [Name] -> Name -> Idris [Name]
259allNames ns n | n `elem` ns = return []
260allNames ns n = do i <- getIState
261 case lookupCtxtExact n (idris_callgraph i) of
262 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
263 return (nub (n : concat more))
264 _ -> return [n]
266addCoercion :: Name -> Idris ()
267addCoercion n = do i <- getIState
268 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
270addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
271addDocStr n doc args
272 = do i <- getIState
273 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
275addNameHint :: Name -> Name -> Idris ()
276addNameHint ty n
277 = do i <- getIState
278 ty' <- case lookupCtxtName ty (idris_implicits i) of
279 [(tyn, _)] -> return tyn
280 [] -> throwError (NoSuchVariable ty)
281 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
282 let ns' = case lookupCtxt ty' (idris_namehints i) of
283 [ns] -> ns ++ [n]
284 _ -> [n]
285 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
287getNameHints :: IState -> Name -> [Name]
288getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
289getNameHints i n =
290 case lookupCtxt n (idris_namehints i) of
291 [ns] -> ns
292 _ -> []
294addToCalledG :: Name -> [Name] -> Idris ()
295addToCalledG n ns = return () -- TODO
297-- Add a class instance function. Dodgy hack: Put integer instances first in the
298-- list so they are resolved by default.
299-- Dodgy hack 2: put constraint chasers (@@) last
301addInstance :: Bool -> Name -> Name -> Idris ()
302addInstance int n i
303 = do ist <- getIState
304 case lookupCtxt n (idris_classes ist) of
305 [CI a b c d e ins] ->
306 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
307 putIState $ ist { idris_classes = cs }
308 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
309 putIState $ ist { idris_classes = cs }
310 where addI i ins | int = i : ins
311 | chaser n = ins ++ [i]
312 | otherwise = insI i ins
313 insI i [] = [i]
314 insI i (n : ns) | chaser n = i : n : ns
315 | otherwise = n : insI i ns
317 chaser (UN nm)
318 | ('@':'@':_) <- str nm = True
319 chaser (NS n _) = chaser n
320 chaser _ = False
322addClass :: Name -> ClassInfo -> Idris ()
323addClass n i
324 = do ist <- getIState
325 let i' = case lookupCtxt n (idris_classes ist) of
326 [c] -> c { class_instances = class_instances i }
327 _ -> i
328 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
330addIBC :: IBCWrite -> Idris ()
331addIBC ibc@(IBCDef n)
332 = do i <- getIState
333 when (notDef (ibc_write i)) $
334 putIState $ i { ibc_write = ibc : ibc_write i }
335 where notDef [] = True
336 notDef (IBCDef n': is) | n == n' = False
337 notDef (_ : is) = notDef is
338addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
340clearIBC :: Idris ()
341clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
343resetNameIdx :: Idris ()
344resetNameIdx = do i <- getIState
345 put (i { idris_nameIdx = (0, emptyContext) })
347-- Used to preserve sharing of names
348addNameIdx :: Name -> Idris (Int, Name)
349addNameIdx n = do i <- getIState
350 let (i', x) = addNameIdx' i n
351 return x
353addNameIdx' :: IState -> Name -> (IState, (Int, Name))
354addNameIdx' i n
355 = let idxs = snd (idris_nameIdx i) in
356 case lookupCtxt n idxs of
357 [x] -> (i, x)
358 _ -> let i' = fst (idris_nameIdx i) + 1 in
359 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
361getHdrs :: Codegen -> Idris [String]
362getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
364getImported :: Idris [FilePath]
365getImported = do i <- getIState; return (idris_imported i)
367setErrSpan :: FC -> Idris ()
368setErrSpan x = do i <- getIState;
369 case (errSpan i) of
370 Nothing -> putIState $ i { errSpan = Just x }
371 Just _ -> return ()
373clearErr :: Idris ()
374clearErr = do i <- getIState
375 putIState $ i { errSpan = Nothing }
377getSO :: Idris (Maybe String)
378getSO = do i <- getIState
379 return (compiled_so i)
381setSO :: Maybe String -> Idris ()
382setSO s = do i <- getIState
383 putIState $ (i { compiled_so = s })
385getIState :: Idris IState
386getIState = get
388putIState :: IState -> Idris ()
389putIState = put
391withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
392withContext ctx name dflt action = do
393 ist <- getIState
394 case lookupCtxt name (ctx ist) of
395 [x] -> action x
396 _ -> return dflt
398withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
399withContext_ ctx name action = withContext ctx name () action
401-- | A version of liftIO that puts errors into the exception type of the Idris monad
402runIO :: IO a -> Idris a
403runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
404-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
406getName :: Idris Int
407getName = do i <- getIState;
408 let idx = idris_name i;
409 putIState $ (i { idris_name = idx + 1 })
410 return idx
412-- InternalApp keeps track of the real function application for making case splits from, not the application the
413-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
414addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
415addInternalApp fp l t
416 = do i <- getIState
417 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
419getInternalApp :: FilePath -> Int -> Idris PTerm
420getInternalApp fp l = do i <- getIState
421 case lookup (fp, l) (idris_lineapps i) of
422 Just n' -> return n'
423 Nothing -> return Placeholder
424 -- TODO: What if it's not there?
426-- Pattern definitions are only used for coverage checking, so erase them
427-- when we're done
428clearOrigPats :: Idris ()
429clearOrigPats = do i <- get
430 let ps = idris_patdefs i
431 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
432 put (i { idris_patdefs = ps' })
434-- Erase types from Ps in the context (basically ending up with what's in
435-- the .ibc, which is all we need after all the analysis is done)
436clearPTypes :: Idris ()
437clearPTypes = do i <- get
438 let ctxt = tt_ctxt i
439 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
440 where pErase (CaseOp c t tys orig tot cds)
441 = CaseOp c t tys orig [] (pErase' cds)
442 pErase x = x
443 pErase' (CaseDefs _ (cs, c) _ rs)
444 = let c' = (cs, fmap pEraseType c) in
445 CaseDefs c' c' c' rs
447checkUndefined :: FC -> Name -> Idris ()
448checkUndefined fc n
449 = do i <- getContext
450 case lookupTy n i of
451 (_:_) -> throwError . Msg $ show fc ++ ":" ++
452 show n ++ " already defined"
453 _ -> return ()
455isUndefined :: FC -> Name -> Idris Bool
456isUndefined fc n
457 = do i <- getContext
458 case lookupTy n i of
459 (_:_) -> return False
460 _ -> return True
462setContext :: Context -> Idris ()
463setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
465updateContext :: (Context -> Context) -> Idris ()
466updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
468addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
469addConstraints fc (v, cs)
470 = do i <- getIState
471 let ctxt = tt_ctxt i
472 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
473 next_tvar = v }
474 let ics = zip cs (repeat fc) ++ idris_constraints i
475 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
477addDeferred = addDeferred' Ref
478addDeferredTyCon = addDeferred' (TCon 0 0)
480addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
481addDeferred' nt ns
482 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
483 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
484 i <- getIState
485 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
486 idris_metavars i }
487 where tidyNames used (Bind (MN i x) b sc)
488 = let n' = uniqueName (UN x) used in
489 Bind n' b $ tidyNames (n':used) sc
490 tidyNames used (Bind n b sc)
491 = let n' = uniqueName n used in
492 Bind n' b $ tidyNames (n':used) sc
493 tidyNames used b = b
495solveDeferred :: Name -> Idris ()
496solveDeferred n = do i <- getIState
497 putIState $ i { idris_metavars =
498 filter (\(n', _) -> n/=n')
499 (idris_metavars i),
500 ibc_write =
501 filter (notMV n) (ibc_write i)
502 }
503 where notMV n (IBCMetavar n') = not (n == n')
504 notMV n _ = True
506getUndefined :: Idris [Name]
507getUndefined = do i <- getIState
508 return (map fst (idris_metavars i) \\ primDefs)
510isMetavarName :: Name -> IState -> Bool
511isMetavarName n ist
512 = case lookupNames n (tt_ctxt ist) of
513 (t:_) -> isJust $ lookup t (idris_metavars ist)
514 _ -> False
516getWidth :: Idris ConsoleWidth
517getWidth = fmap idris_consolewidth getIState
519setWidth :: ConsoleWidth -> Idris ()
520setWidth w = do ist <- getIState
521 put ist { idris_consolewidth = w }
523renderWidth :: Idris Int
524renderWidth = do iw <- getWidth
525 case iw of
526 InfinitelyWide -> return 100000000
527 ColsWide n -> return (max n 1)
528 AutomaticWidth -> runIO getScreenWidth
532type1Doc :: Doc OutputAnnotation
533type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
536isetPrompt :: String -> Idris ()
537isetPrompt p = do i <- getIState
538 case idris_outputmode i of
539 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
541setLogLevel :: Int -> Idris ()
542setLogLevel l = do i <- getIState
543 let opts = idris_options i
544 let opt' = opts { opt_logLevel = l }
545 putIState $ i { idris_options = opt' }
547setCmdLine :: [Opt] -> Idris ()
548setCmdLine opts = do i <- getIState
549 let iopts = idris_options i
550 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
552getCmdLine :: Idris [Opt]
553getCmdLine = do i <- getIState
554 return (opt_cmdline (idris_options i))
556getDumpDefun :: Idris (Maybe FilePath)
557getDumpDefun = do i <- getIState
558 return $ findC (opt_cmdline (idris_options i))
559 where findC [] = Nothing
560 findC (DumpDefun x : _) = Just x
561 findC (_ : xs) = findC xs
563getDumpCases :: Idris (Maybe FilePath)
564getDumpCases = do i <- getIState
565 return $ findC (opt_cmdline (idris_options i))
566 where findC [] = Nothing
567 findC (DumpCases x : _) = Just x
568 findC (_ : xs) = findC xs
570logLevel :: Idris Int
571logLevel = do i <- getIState
572 return (opt_logLevel (idris_options i))
574setErrContext :: Bool -> Idris ()
575setErrContext t = do i <- getIState
576 let opts = idris_options i
577 let opt' = opts { opt_errContext = t }
578 putIState $ i { idris_options = opt' }
580errContext :: Idris Bool
581errContext = do i <- getIState
582 return (opt_errContext (idris_options i))
584useREPL :: Idris Bool
585useREPL = do i <- getIState
586 return (opt_repl (idris_options i))
588setREPL :: Bool -> Idris ()
589setREPL t = do i <- getIState
590 let opts = idris_options i
591 let opt' = opts { opt_repl = t }
592 putIState $ i { idris_options = opt' }
594showOrigErr :: Idris Bool
595showOrigErr = do i <- getIState
596 return (opt_origerr (idris_options i))
598setShowOrigErr :: Bool -> Idris ()
599setShowOrigErr b = do i <- getIState
600 let opts = idris_options i
601 let opt' = opts { opt_origerr = b }
602 putIState $ i { idris_options = opt' }
604setAutoSolve :: Bool -> Idris ()
605setAutoSolve b = do i <- getIState
606 let opts = idris_options i
607 let opt' = opts { opt_autoSolve = b }
608 putIState $ i { idris_options = opt' }
610setNoBanner :: Bool -> Idris ()
611setNoBanner n = do i <- getIState
612 let opts = idris_options i
613 let opt' = opts { opt_nobanner = n }
614 putIState $ i { idris_options = opt' }
616getNoBanner :: Idris Bool
617getNoBanner = do i <- getIState
618 let opts = idris_options i
619 return (opt_nobanner opts)
621setQuiet :: Bool -> Idris ()
622setQuiet q = do i <- getIState
623 let opts = idris_options i
624 let opt' = opts { opt_quiet = q }
625 putIState $ i { idris_options = opt' }
627getQuiet :: Idris Bool
628getQuiet = do i <- getIState
629 let opts = idris_options i
630 return (opt_quiet opts)
632setCodegen :: Codegen -> Idris ()
633setCodegen t = do i <- getIState
634 let opts = idris_options i
635 let opt' = opts { opt_codegen = t }
636 putIState $ i { idris_options = opt' }
638codegen :: Idris Codegen
639codegen = do i <- getIState
640 return (opt_codegen (idris_options i))
642setOutputTy :: OutputType -> Idris ()
643setOutputTy t = do i <- getIState
644 let opts = idris_options i
645 let opt' = opts { opt_outputTy = t }
646 putIState $ i { idris_options = opt' }
648outputTy :: Idris OutputType
649outputTy = do i <- getIState
650 return $ opt_outputTy $ idris_options i
652setIdeSlave :: Bool -> Idris ()
653setIdeSlave True = do i <- getIState
654 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
655setIdeSlave False = return ()
657setTargetTriple :: String -> Idris ()
658setTargetTriple t = do i <- getIState
659 let opts = idris_options i
660 opt' = opts { opt_triple = t }
661 putIState $ i { idris_options = opt' }
663targetTriple :: Idris String
664targetTriple = do i <- getIState
665 return (opt_triple (idris_options i))
667setTargetCPU :: String -> Idris ()
668setTargetCPU t = do i <- getIState
669 let opts = idris_options i
670 opt' = opts { opt_cpu = t }
671 putIState $ i { idris_options = opt' }
673targetCPU :: Idris String
674targetCPU = do i <- getIState
675 return (opt_cpu (idris_options i))
677setOptLevel :: Word -> Idris ()
678setOptLevel t = do i <- getIState
679 let opts = idris_options i
680 opt' = opts { opt_optLevel = t }
681 putIState $ i { idris_options = opt' }
683optLevel :: Idris Word
684optLevel = do i <- getIState
685 return (opt_optLevel (idris_options i))
687verbose :: Idris Bool
688verbose = do i <- getIState
689 return (opt_verbose (idris_options i))
691setVerbose :: Bool -> Idris ()
692setVerbose t = do i <- getIState
693 let opts = idris_options i
694 let opt' = opts { opt_verbose = t }
695 putIState $ i { idris_options = opt' }
697typeInType :: Idris Bool
698typeInType = do i <- getIState
699 return (opt_typeintype (idris_options i))
701setTypeInType :: Bool -> Idris ()
702setTypeInType t = do i <- getIState
703 let opts = idris_options i
704 let opt' = opts { opt_typeintype = t }
705 putIState $ i { idris_options = opt' }
707coverage :: Idris Bool
708coverage = do i <- getIState
709 return (opt_coverage (idris_options i))
711setCoverage :: Bool -> Idris ()
712setCoverage t = do i <- getIState
713 let opts = idris_options i
714 let opt' = opts { opt_coverage = t }
715 putIState $ i { idris_options = opt' }
717setIBCSubDir :: FilePath -> Idris ()
718setIBCSubDir fp = do i <- getIState
719 let opts = idris_options i
720 let opt' = opts { opt_ibcsubdir = fp }
721 putIState $ i { idris_options = opt' }
723valIBCSubDir :: IState -> Idris FilePath
724valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
726addImportDir :: FilePath -> Idris ()
727addImportDir fp = do i <- getIState
728 let opts = idris_options i
729 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
730 putIState $ i { idris_options = opt' }
732setImportDirs :: [FilePath] -> Idris ()
733setImportDirs fps = do i <- getIState
734 let opts = idris_options i
735 let opt' = opts { opt_importdirs = fps }
736 putIState $ i { idris_options = opt' }
738allImportDirs :: Idris [FilePath]
739allImportDirs = do i <- getIState
740 let optdirs = opt_importdirs (idris_options i)
741 return ("." : reverse optdirs)
743colourise :: Idris Bool
744colourise = do i <- getIState
745 return $ idris_colourRepl i
747setColourise :: Bool -> Idris ()
748setColourise b = do i <- getIState
749 putIState $ i { idris_colourRepl = b }
751setOutH :: Handle -> Idris ()
752setOutH h = do i <- getIState
753 putIState $ i { idris_outh = h }
755impShow :: Idris Bool
756impShow = do i <- getIState
757 return (opt_showimp (idris_options i))
759setImpShow :: Bool -> Idris ()
760setImpShow t = do i <- getIState
761 let opts = idris_options i
762 let opt' = opts { opt_showimp = t }
763 putIState $ i { idris_options = opt' }
765setColour :: ColourType -> IdrisColour -> Idris ()
766setColour ct c = do i <- getIState
767 let newTheme = setColour' ct c (idris_colourTheme i)
768 putIState $ i { idris_colourTheme = newTheme }
769 where setColour' KeywordColour c t = t { keywordColour = c }
770 setColour' BoundVarColour c t = t { boundVarColour = c }
771 setColour' ImplicitColour c t = t { implicitColour = c }
772 setColour' FunctionColour c t = t { functionColour = c }
773 setColour' TypeColour c t = t { typeColour = c }
774 setColour' DataColour c t = t { dataColour = c }
775 setColour' PromptColour c t = t { promptColour = c }
777logLvl :: Int -> String -> Idris ()
778logLvl l str = do i <- getIState
779 let lvl = opt_logLevel (idris_options i)
780 when (lvl >= l) $
781 case idris_outputmode i of
782 RawOutput -> do runIO $ putStrLn str
783 IdeSlave n ->
784 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
785 runIO $ putStrLn $ convSExp "log" good n
787cmdOptType :: Opt -> Idris Bool
788cmdOptType x = do i <- getIState
789 return $ x `elem` opt_cmdline (idris_options i)
791iLOG :: String -> Idris ()
792iLOG = logLvl 1
794noErrors :: Idris Bool
795noErrors = do i <- getIState
796 case errSpan i of
797 Nothing -> return True
798 _ -> return False
800setTypeCase :: Bool -> Idris ()
801setTypeCase t = do i <- getIState
802 let opts = idris_options i
803 let opt' = opts { opt_typecase = t }
804 putIState $ i { idris_options = opt' }
807-- Dealing with parameters
809expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
810 [Name] -> -- all names
811 [Name] -> -- names with no declaration
812 PTerm -> PTerm
813expandParams dec ps ns infs tm = en tm
814 where
815 -- if we shadow a name (say in a lambda binding) that is used in a call to
816 -- a lifted function, we need access to both names - once in the scope of the
817 -- binding and once to call the lifted functions. So we'll explicitly shadow
818 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
819 -- but we didn't...)
821 mkShadow (UN n) = MN 0 n
822 mkShadow (MN i n) = MN (i+1) n
823 mkShadow (NS x s) = NS (mkShadow x) s
825 en (PLam n t s)
826 | n `elem` (map fst ps ++ ns)
827 = let n' = mkShadow n in
828 PLam n' (en t) (en (shadow n n' s))
829 | otherwise = PLam n (en t) (en s)
830 en (PPi p n t s)
831 | n `elem` (map fst ps ++ ns)
832 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
833 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
834 | otherwise = PPi (enTacImp p) n (en t) (en s)
835 en (PLet n ty v s)
836 | n `elem` (map fst ps ++ ns)
837 = let n' = mkShadow n in
838 PLet n' (en ty) (en v) (en (shadow n n' s))
839 | otherwise = PLet n (en ty) (en v) (en s)
840 -- FIXME: Should only do this in a type signature!
841 en (PDPair f p (PRef f' n) t r)
842 | n `elem` (map fst ps ++ ns) && t /= Placeholder
843 = let n' = mkShadow n in
844 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
845 en (PEq f l r) = PEq f (en l) (en r)
846 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
847 en (PTyped l r) = PTyped (en l) (en r)
848 en (PPair f p l r) = PPair f p (en l) (en r)
849 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
850 en (PAlternative a as) = PAlternative a (map en as)
851 en (PHidden t) = PHidden (en t)
852 en (PUnifyLog t) = PUnifyLog (en t)
853 en (PDisamb ds t) = PDisamb ds (en t)
854 en (PNoImplicits t) = PNoImplicits (en t)
855 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
856 en (PProof ts) = PProof (map (fmap en) ts)
857 en (PTactics ts) = PTactics (map (fmap en) ts)
859 en (PQuote (Var n))
860 | n `nselem` ns = PQuote (Var (dec n))
861 en (PApp fc (PInferRef fc' n) as)
862 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
863 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
864 en (PApp fc (PRef fc' n) as)
865 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
866 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
867 | n `nselem` ns = PApp fc (PRef fc' (dec n))
868 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
869 en (PAppBind fc (PRef fc' n) as)
870 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
871 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
872 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
873 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
874 en (PRef fc n)
875 | n `elem` infs = PApp fc (PInferRef fc (dec n))
876 (map (pexp . (PRef fc)) (map fst ps))
877 | n `nselem` ns = PApp fc (PRef fc (dec n))
878 (map (pexp . (PRef fc)) (map fst ps))
879 en (PInferRef fc n)
880 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
881 (map (pexp . (PRef fc)) (map fst ps))
882 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
883 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
884 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
885 en t = t
887 nselem x [] = False
888 nselem x (y : xs) | nseq x y = True
889 | otherwise = nselem x xs
891 nseq x y = nsroot x == nsroot y
893 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
894 enTacImp other = other
896expandParamsD :: Bool -> -- True = RHS only
897 IState ->
898 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
899expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
900 = if n `elem` ns && (not rhsonly)
901 then -- trace (show (n, expandParams dec ps ns ty)) $
902 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
903 else --trace (show (n, expandParams dec ps ns ty)) $
904 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
905expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
906 = if n `elem` ns && (not rhsonly)
907 then -- trace (show (n, expandParams dec ps ns ty)) $
908 PPostulate doc syn fc o (dec n) (piBind ps
909 (expandParams dec ps ns [] ty))
910 else --trace (show (n, expandParams dec ps ns ty)) $
911 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
912expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
913 = let n' = if n `elem` ns then dec n else n in
914 PClauses fc opts n' (map expandParamsC cs)
915 where
916 expandParamsC (PClause fc n lhs ws rhs ds)
917 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
918 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
919 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
920 n' = if n `elem` ns then dec n else n
921 -- names bound on the lhs should not be expanded on the rhs
922 ns' = removeBound lhs ns in
923 PClause fc n' lhs'
924 (map (expandParams dec ps'' ns' []) ws)
925 (expandParams dec ps'' ns' [] rhs)
926 (map (expandParamsD True ist dec ps'' ns') ds)
927 expandParamsC (PWith fc n lhs ws wval ds)
928 = let -- ps' = updateps True (namesIn ist wval) (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 ns' = removeBound lhs ns in
933 PWith fc n' lhs'
934 (map (expandParams dec ps'' ns' []) ws)
935 (expandParams dec ps'' ns' [] wval)
936 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
937 updateps yn nm [] = []
938 updateps yn nm (((a, t), i):as)
939 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
940 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
942 removeBound lhs ns = ns \\ nub (bnames lhs)
944 bnames (PRef _ n) = [n]
945 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
946 bnames (PPair _ _ l r) = bnames l ++ bnames r
947 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
948 bnames _ = []
950-- | Expands parameters defined in parameter and where blocks inside of declarations
951expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
952 = PData doc argDocs syn fc co (expandPData pd)
953 where
954 -- just do the type decl, leave constructors alone (parameters will be
955 -- added implicitly)
956 expandPData (PDatadecl n ty cons)
957 = if n `elem` ns
958 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
959 (map econ cons)
960 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
961 econ (doc, argDocs, n, t, fc, fs)
962 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
963expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
964 = if tn `elem` ns
965 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
966 opts cdoc (dec cn) conty
967 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
968 opts cdoc (dec cn) conty
969 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
970expandParamsD rhs ist dec ps ns (PParams f params pds)
971 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
972 (map (expandParamsD True ist dec ps ns) pds)
973-- (map (expandParamsD ist dec ps ns) pds)
974expandParamsD rhs ist dec ps ns (PMutual f pds)
975 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
976expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
977 = PClass doc info f
978 (map (expandParams dec ps ns []) cs)
979 n
980 (map (mapsnd (expandParams dec ps ns [])) params)
981 pDocs
982 (map (expandParamsD rhs ist dec ps ns) decls)
983expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
984 = PInstance info f
985 (map (expandParams dec ps ns []) cs)
986 n
987 (map (expandParams dec ps ns []) params)
988 (expandParams dec ps ns [] ty)
989 cn
990 (map (expandParamsD rhs ist dec ps ns) decls)
991expandParamsD rhs ist dec ps ns d = d
993mapsnd f (x, t) = (x, f t)
995-- Calculate a priority for a type, for deciding elaboration order
996-- * if it's just a type variable or concrete type, do it early (0)
997-- * if there's only type variables and injective constructors, do it next (1)
998-- * if there's a function type, next (2)
999-- * finally, everything else (3)
1001getPriority :: IState -> PTerm -> Int
1002getPriority i tm = 1 -- pri tm
1003 where
1004 pri (PRef _ n) =
1005 case lookupP n (tt_ctxt i) of
1006 ((P (DCon _ _) _ _):_) -> 1
1007 ((P (TCon _ _) _ _):_) -> 1
1008 ((P Ref _ _):_) -> 1
1009 [] -> 0 -- must be locally bound, if it's not an error...
1010 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1011 pri (PTrue _ _) = 0
1012 pri (PFalse _) = 0
1013 pri (PRefl _ _) = 1
1014 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1015 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1016 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1017 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1018 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1019 pri (PTyped l r) = pri l
1020 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1021 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1022 pri (PAlternative a as) = maximum (map pri as)
1023 pri (PConstant _) = 0
1024 pri Placeholder = 1
1025 pri _ = 3
1028addStatics :: Name -> Term -> PTerm -> Idris ()
1029addStatics n tm ptm =
1030 do let (statics, dynamics) = initStatics tm ptm
1031 let stnames = nub $ concatMap freeArgNames (map snd statics)
1032 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1033 -- also get the arguments which are 'uniquely inferrable' from
1034 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1035 let statics' = nub $ map fst statics ++
1036 filter (\x -> not (elem x dnames)) stnames
1037 let stpos = staticList statics' tm
1038 i <- getIState
1039 when (not (null statics)) $
1040 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1041 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1042 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1043 addIBC (IBCStatic n)
1044 where
1045 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1046 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1047 if pstatic p == Static then ((n, ty) : static, dynamic)
1048 else if (not (searchArg p))
1049 then (static, (n, ty) : dynamic)
1050 else (static, dynamic)
1051 initStatics t pt = ([], [])
1053 freeArgNames (Bind n (Pi ty) sc)
1054 = nub $ freeArgNames ty
1055 freeArgNames tm = let (_, args) = unApply tm in
1056 concatMap freeNames args
1058 -- if a name appears in a type class or tactic implicit index, it doesn't
1059 -- affect its 'uniquely inferrable' from a static status since these are
1060 -- resolved by searching.
1061 searchArg (Constraint _ _) = True
1062 searchArg (TacImp _ _ _) = True
1063 searchArg _ = False
1065 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1066 staticList _ _ = []
1068-- Dealing with implicit arguments
1070-- Add constraint bindings from using block
1072addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1073addUsingConstraints syn fc t
1074 = do ist <- get
1075 let ns = namesIn [] ist t
1076 let cs = getConstraints t -- check declared constraints
1077 let addconsts = uconsts \\ cs
1078 -- if all names in the arguments of addconsts appear in ns,
1079 -- add the constraint implicitly
1080 return (doAdd addconsts ns t)
1081 where uconsts = filter uconst (using syn)
1082 uconst (UConstraint _ _) = True
1083 uconst _ = False
1085 doAdd [] _ t = t
1086 -- if all of args in ns, then add it
1087 doAdd (UConstraint c args : cs) ns t
1088 | all (\n -> elem n ns) args
1089 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1090 (mkConst c args) (doAdd cs ns t)
1091 | otherwise = doAdd cs ns t
1093 mkConst c args = PApp fc (PRef fc c)
1094 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1096 getConstraints (PPi (Constraint _ _) _ c sc)
1097 = getcapp c ++ getConstraints sc
1098 getConstraints (PPi _ _ c sc) = getConstraints sc
1099 getConstraints _ = []
1101 getcapp (PApp _ (PRef _ c) args)
1102 = do ns <- mapM getName args
1103 return (UConstraint c ns)
1104 getcapp _ = []
1106 getName (PExp _ _ _ (PRef _ n)) = return n
1107 getName _ = []
1109-- Add implicit Pi bindings for any names in the term which appear in an
1110-- argument position.
1112-- This has become a right mess already. Better redo it some time...
1114implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1115implicit info syn n ptm = implicit' info syn [] n ptm
1117implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1118implicit' info syn ignore n ptm
1119 = do i <- getIState
1120 let (tm', impdata) = implicitise syn ignore i ptm
1121 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1122-- let (tm'', spos) = findStatics i tm'
1123 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1124 addIBC (IBCImp n)
1125 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1126-- i <- get
1127-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1128 return tm'
1129 where
1130 -- Detect unknown names in default arguments and throw error if found.
1131 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1132 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1134 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1135 notFoundInDefault kns (PTacImplicit _ _ n script _)
1136 = do i <- getIState
1137 case notFound kns (namesIn [] i script) of
1138 Nothing -> return (n:kns)
1139 Just name -> throwError (NoSuchVariable name)
1140 notFoundInDefault kns p = return ((pname p):kns)
1142 notFound :: [Name] -> [Name] -> Maybe Name
1143 notFound kns [] = Nothing
1144 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1145 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1147implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1148implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1149 let (declimps, ns') = execState (imps True [] tm) ([], [])
1150 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1151 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1152 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1153 if null ns
1154 then (tm, reverse declimps)
1155 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1156 where
1157 uvars = map ipair (filter uimplicit (using syn))
1158 pvars = syn_params syn
1160 inUsing n = n `elem` map fst uvars
1162 ipair (UImplicit x y) = (x, y)
1163 uimplicit (UImplicit _ _) = True
1164 uimplicit _ = False
1166 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1167 | otherwise = x : dropAll xs ys
1168 dropAll [] ys = []
1170 -- Find names in argument position in a type, suitable for implicit
1171 -- binding
1172 -- Not the function position, but do everything else...
1173 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1174 implNamesIn uv t = namesIn uv ist t
1176 imps top env (PApp _ f as)
1177 = do (decls, ns) <- get
1178 let isn = concatMap (namesIn uvars ist) (map getTm as)
1179 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1180 imps top env (PPi (Imp l _ _) n ty sc)
1181 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1182 (decls , ns) <- get
1183 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1184 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1185 imps True (n:env) sc
1186 imps top env (PPi (Exp l _ _) n ty sc)
1187 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1188 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1189 _ -> [])
1190 (decls, ns) <- get -- ignore decls in HO types
1191 put (PExp (getPriority ist ty) l n Placeholder : decls,
1192 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1193 imps True (n:env) sc
1194 imps top env (PPi (Constraint l _) n ty sc)
1195 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1196 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1197 _ -> [])
1198 (decls, ns) <- get -- ignore decls in HO types
1199 put (PConstraint 10 l n Placeholder : decls,
1200 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1201 imps True (n:env) sc
1202 imps top env (PPi (TacImp l _ scr) n ty sc)
1203 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1204 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1205 _ -> [])
1206 (decls, ns) <- get -- ignore decls in HO types
1207 put (PTacImplicit 10 l n scr Placeholder : decls,
1208 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1209 imps True (n:env) sc
1210 imps top env (PEq _ l r)
1211 = do (decls, ns) <- get
1212 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1213 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1214 imps top env (PRewrite _ l r _)
1215 = do (decls, ns) <- get
1216 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1217 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1218 imps top env (PTyped l r)
1219 = imps top env l
1220 imps top env (PPair _ _ l r)
1221 = do (decls, ns) <- get
1222 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1223 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1224 imps top env (PDPair _ _ (PRef _ n) t r)
1225 = do (decls, ns) <- get
1226 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1227 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1228 imps top env (PDPair _ _ l t r)
1229 = do (decls, ns) <- get
1230 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1231 namesIn uvars ist r
1232 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1233 imps top env (PAlternative a as)
1234 = do (decls, ns) <- get
1235 let isn = concatMap (namesIn uvars ist) as
1236 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1237 imps top env (PLam n ty sc)
1238 = do imps False env ty
1239 imps False (n:env) sc
1240 imps top env (PHidden tm) = imps False env tm
1241 imps top env (PUnifyLog tm) = imps False env tm
1242 imps top env (PNoImplicits tm) = imps False env tm
1243 imps top env _ = return ()
1245 pibind using [] sc = sc
1246 pibind using (n:ns) sc
1247 = case lookup n using of
1248 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1249 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1250 (pibind using ns sc)
1252-- Add implicit arguments in function calls
1253addImplPat :: IState -> PTerm -> PTerm
1254addImplPat = addImpl' True [] []
1256addImplBound :: IState -> [Name] -> PTerm -> PTerm
1257addImplBound ist ns = addImpl' False ns [] ist
1259addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1260addImplBoundInf ist ns inf = addImpl' False ns inf ist
1262addImpl :: IState -> PTerm -> PTerm
1263addImpl = addImpl' False [] []
1265-- TODO: in patterns, don't add implicits to function names guarded by constructors
1266-- and *not* inside a PHidden
1268addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1269addImpl' inpat env infns ist ptm
1270 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1271 where
1272 ai env ds (PRef fc f)
1273 | f `elem` infns = PInferRef fc f
1274 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1275 ai env ds (PHidden (PRef fc f))
1276 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1277 ai env ds (PEq fc l r)
1278 = let l' = ai env ds l
1279 r' = ai env ds r in
1280 PEq fc l' r'
1281 ai env ds (PRewrite fc l r g)
1282 = let l' = ai env ds l
1283 r' = ai env ds r
1284 g' = fmap (ai env ds) g in
1285 PRewrite fc l' r' g'
1286 ai env ds (PTyped l r)
1287 = let l' = ai env ds l
1288 r' = ai env ds r in
1289 PTyped l' r'
1290 ai env ds (PPair fc p l r)
1291 = let l' = ai env ds l
1292 r' = ai env ds r in
1293 PPair fc p l' r'
1294 ai env ds (PDPair fc p l t r)
1295 = let l' = ai env ds l
1296 t' = ai env ds t
1297 r' = ai env ds r in
1298 PDPair fc p l' t' r'
1299 ai env ds (PAlternative a as)
1300 = let as' = map (ai env ds) as in
1301 PAlternative a as'
1302 ai env _ (PDisamb ds' as) = ai env ds' as
1303 ai env ds (PApp fc (PInferRef _ f) as)
1304 = let as' = map (fmap (ai env ds)) as in
1305 PApp fc (PInferRef fc f) as'
1306 ai env ds (PApp fc ftm@(PRef _ f) as)
1307 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1308 | not (f `elem` map fst env)
1309 = let as' = map (fmap (ai env ds)) as in
1310 handleErr $ aiFn inpat False ist fc f ds as'
1311 | Just (Just ty) <- lookup f env =
1312 let as' = map (fmap (ai env ds)) as
1313 arity = getPArity ty in
1314 mkPApp fc arity ftm as'
1315 ai env ds (PApp fc f as)
1316 = let f' = ai env ds f
1317 as' = map (fmap (ai env ds)) as in
1318 mkPApp fc 1 f' as'
1319 ai env ds (PCase fc c os)
1320 = let c' = ai env ds c
1321 os' = map (pmap (ai env ds)) os in
1322 PCase fc c' os'
1323 ai env ds (PLam n ty sc)
1324 = let ty' = ai env ds ty
1325 sc' = ai ((n, Just ty):env) ds sc in
1326 PLam n ty' sc'
1327 ai env ds (PLet n ty val sc)
1328 = let ty' = ai env ds ty
1329 val' = ai env ds val
1330 sc' = ai ((n, Just ty):env) ds sc in
1331 PLet n ty' val' sc'
1332 ai env ds (PPi p n ty sc)
1333 = let ty' = ai env ds ty
1334 sc' = ai ((n, Just ty):env) ds sc in
1335 PPi p n ty' sc'
1336 ai env ds (PGoal fc r n sc)
1337 = let r' = ai env ds r
1338 sc' = ai ((n, Nothing):env) ds sc in
1339 PGoal fc r' n sc'
1340 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1341 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1342 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1343 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1344 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1345 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1346 ai env ds tm = tm
1348 handleErr (Left err) = PElabError err
1349 handleErr (Right x) = x
1351-- if in a pattern, and there are no arguments, and there's no possible
1352-- names with zero explicit arguments, don't add implicits.
1354aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1355aiFn inpat True ist fc f ds []
1356 = case lookupDef f (tt_ctxt ist) of
1357 [] -> Right $ PPatvar fc f
1358 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1359 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1360 if (not (vname f) || tcname f
1361 || any (conCaf (tt_ctxt ist)) ialts)
1362-- any constructor alts || any allImp ialts))
1363 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1364 else Right $ PPatvar fc f
1365 where imp (PExp _ _ _ _) = False
1366 imp _ = True
1367-- allImp [] = False
1368 allImp xs = all imp xs
1369 constructor (TyDecl (DCon _ _) _) = True
1370 constructor _ = False
1372 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1374 vname (UN n) = True -- non qualified
1375 vname _ = False
1377aiFn inpat expat ist fc f ds as
1378 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1379aiFn inpat expat ist fc f ds as
1380 -- This is where namespaces get resolved by adding PAlternative
1381 = do let ns = lookupCtxtName f (idris_implicits ist)
1382 let nh = filter (\(n, _) -> notHidden n) ns
1383 let ns' = case trimAlts ds nh of
1384 [] -> nh
1385 x -> x
1386 case ns' of
1387 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1388 [] -> if f `elem` (map fst (idris_metavars ist))
1389 then Right $ PApp fc (PRef fc f) as
1390 else Right $ mkPApp fc (length as) (PRef fc f) as
1391 alts -> Right $
1392 PAlternative True $
1393 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1394 (insertImpl ns as)) alts
1395 where
1396 trimAlts [] alts = alts
1397 trimAlts ns alts
1398 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1400 nspace (NS _ s) = s
1401 nspace _ = []
1403 notHidden n = case getAccessibility n of
1404 Hidden -> False
1405 _ -> True
1407 getAccessibility n
1408 = case lookupDefAcc n False (tt_ctxt ist) of
1409 [(n,t)] -> t
1410 _ -> Public
1412 insertImpl :: [PArg] -> [PArg] -> [PArg]
1413 insertImpl ps as = insImpAcc M.empty ps as
1415 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1416 -> [PArg] -- parameters
1417 -> [PArg] -- arguments
1418 -> [PArg]
1419 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1420 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1421 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1422 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1423 insImpAcc pnas (PConstraint p l n ty : ps) given =
1424 let rtc = PResolveTC fc in
1425 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1426 insImpAcc pnas (PImp p _ l n ty : ps) given =
1427 case find n given [] of
1428 Just (tm, given') ->
1429 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1430 Nothing ->
1431 PImp p True l n Placeholder :
1432 insImpAcc (M.insert n Placeholder pnas) ps given
1433 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1434 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1435 case find n given [] of
1436 Just (tm, given') ->
1437 PTacImplicit p l n sc tm :
1438 insImpAcc (M.insert n tm pnas) ps given'
1439 Nothing ->
1440 if inpat
1441 then PTacImplicit p l n sc Placeholder :
1442 insImpAcc (M.insert n Placeholder pnas) ps given
1443 else PTacImplicit p l n sc sc :
1444 insImpAcc (M.insert n sc pnas) ps given
1445 insImpAcc _ expected [] = []
1446 insImpAcc _ _ given = given
1448 find n [] acc = Nothing
1449 find n (PImp _ _ _ n' t : gs) acc
1450 | n == n' = Just (t, reverse acc ++ gs)
1451 find n (PTacImplicit _ _ n' _ t : gs) acc
1452 | n == n' = Just (t, reverse acc ++ gs)
1453 find n (g : gs) acc = find n gs (g : acc)
1455-- replace non-linear occurrences with _
1456-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1457-- it is hard to get right!
1459stripLinear :: IState -> PTerm -> PTerm
1460stripLinear i tm = evalState (sl tm) [] where
1461 sl :: PTerm -> State [Name] PTerm
1462 sl (PRef fc f)
1463 | (_:_) <- lookupTy f (tt_ctxt i)
1464 = return $ PRef fc f
1465 | otherwise = do ns <- get
1466 if (f `elem` ns)
1467 then return Placeholder
1468 else do put (f : ns)
1469 return (PRef fc f)
1470 sl (PPatvar fc f)
1471 = do ns <- get
1472 if (f `elem` ns)
1473 then return Placeholder
1474 else do put (f : ns)
1475 return (PPatvar fc f)
1476 sl t@(PAlternative _ (a : as)) = do sl a
1477 return t
1478 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1479 args' <- mapM slA args
1480 return $ PApp fc fn args'
1481 where slA (PImp p m l n t) = do t' <- sl t
1482 return $ PImp p m l n t'
1483 slA (PExp p l n t) = do t' <- sl t
1484 return $ PExp p l n t'
1485 slA (PConstraint p l n t)
1486 = do t' <- sl t
1487 return $ PConstraint p l n t'
1488 slA (PTacImplicit p l n sc t)
1489 = do t' <- sl t
1490 return $ PTacImplicit p l n sc t'
1491 sl x = return x
1493-- Remove functions which aren't applied to anything, which must then
1494-- be resolved by unification. Assume names resolved and alternatives
1495-- filled in (so no ambiguity).
1497stripUnmatchable :: IState -> PTerm -> PTerm
1498stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1499 su :: PTerm -> PTerm
1500 su (PRef fc f)
1501 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1502 = Placeholder
1503 su (PApp fc fn args)
1504 = PApp fc fn (fmap (fmap su) args)
1505 su (PAlternative b alts)
1506 = let alts' = filter (/= Placeholder) (map su alts) in
1507 if null alts' then Placeholder
1508 else PAlternative b alts'
1509 su (PPair fc p l r) = PPair fc p (su l) (su r)
1510 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1511 su t = t
1512stripUnmatchable i tm = tm
1514mkPApp fc a f [] = f
1515mkPApp fc a f as = let rest = drop a as in
1516 appRest fc (PApp fc f (take a as)) rest
1517 where
1518 appRest fc f [] = f
1519 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1521-- Find 'static' argument positions
1522-- (the declared ones, plus any names in argument position in the declared
1523-- statics)
1524-- FIXME: It's possible that this really has to happen after elaboration
1526findStatics :: IState -> PTerm -> (PTerm, [Bool])
1527findStatics ist tm = trace (show tm) $
1528 let (ns, ss) = fs tm in
1529 runState (pos ns ss tm) []
1530 where fs (PPi p n t sc)
1531 | Static <- pstatic p
1532 = let (ns, ss) = fs sc in
1533 (namesIn [] ist t : ns, n : ss)
1534 | otherwise = let (ns, ss) = fs sc in
1535 (ns, ss)
1536 fs _ = ([], [])
1538 inOne n ns = length (filter id (map (elem n) ns)) == 1
1540 pos ns ss (PPi p n t sc)
1541 | elem n ss = do sc' <- pos ns ss sc
1542 spos <- get
1543 put (True : spos)
1544 return (PPi (p { pstatic = Static }) n t sc')
1545 | otherwise = do sc' <- pos ns ss sc
1546 spos <- get
1547 put (False : spos)
1548 return (PPi p n t sc')
1549 pos ns ss t = return t
1551-- for 6.12/7 compatibility
1552data EitherErr a b = LeftErr a | RightOK b
1554instance Monad (EitherErr a) where
1555 return = RightOK
1557 (LeftErr e) >>= k = LeftErr e
1558 RightOK v >>= k = k v
1560toEither (LeftErr e) = Left e
1561toEither (RightOK ho) = Right ho
1563-- syntactic match of a against b, returning pair of variables in a
1564-- and what they match. Returns the pair that failed if not a match.
1566matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1567matchClause = matchClause' False
1569matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1570matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1571 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1573 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1574 fullApp x = x
1576 match' x y = match (fullApp x) (fullApp y)
1577 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1578 | fi == txt "fromInteger" && b == txt "builtins",
1579 PConstant (I _) <- getTm x = match (getTm x) x'
1580 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1581 | fi == txt "fromInteger" && b == txt "builtins",
1582 PConstant (I _) <- getTm x = match (getTm x) x'
1583 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1584 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1585 match (PApp _ f args) (PApp _ f' args')
1586 | length args == length args'
1587 = do mf <- match' f f'
1588 ms <- zipWithM matchArg args args'
1589 return (mf ++ concat ms)
1590 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1591 match (PPatvar f n) xr = match (PRef f n) xr
1592 match xr (PPatvar f n) = match xr (PRef f n)
1593 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1594 match (PRef _ n) tm@(PRef _ n')
1595 | n == n' && not names &&
1596 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1597 || tm == Placeholder)
1598 = return [(n, tm)]
1599 -- if one namespace is missing, drop the other
1600 | n == n' || n == dropNS n' || dropNS n == n' = return []
1601 where dropNS (NS n _) = n
1602 dropNS n = n
1603 match (PRef _ n) tm
1604 | not names && (not (isConName n (tt_ctxt i) ||
1605 isFnName n (tt_ctxt i)) || tm == Placeholder)
1606 = return [(n, tm)]
1607 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1608 mr <- match' r r'
1609 return (ml ++ mr)
1610 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1611 = do ml <- match' l l'
1612 mr <- match' r r'
1613 return (ml ++ mr)
1614 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1615 mr <- match r r'
1616 return (ml ++ mr)
1617 match (PTyped l r) x = match l x
1618 match x (PTyped l r) = match x l
1619 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1620 mr <- match' r r'
1621 return (ml ++ mr)
1622 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1623 mt <- match' t t'
1624 mr <- match' r r'
1625 return (ml ++ mt ++ mr)
1626 match (PAlternative a as) (PAlternative a' as')
1627 = do ms <- zipWithM match' as as'
1628 return (concat ms)
1629 match a@(PAlternative _ as) b
1630 = do let ms = zipWith match' as (repeat b)
1631 case (rights (map toEither ms)) of
1632 (x: _) -> return x
1633 _ -> LeftErr (a, b)
1634 match (PCase _ _ _) _ = return [] -- lifted out
1635 match (PMetavar _) _ = return [] -- modified
1636 match (PInferRef _ _) _ = return [] -- modified
1637 match (PQuote _) _ = return []
1638 match (PProof _) _ = return []
1639 match (PTactics _) _ = return []
1640 match (PRefl _ _) (PRefl _ _) = return []
1641 match (PResolveTC _) (PResolveTC _) = return []
1642 match (PTrue _ _) (PTrue _ _) = return []
1643 match (PFalse _) (PFalse _) = return []
1644 match (PReturn _) (PReturn _) = return []
1645 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1646 ms <- match' s s'
1647 return (mt ++ ms)
1648 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1649 ms <- match' s s'
1650 return (mt ++ ms)
1651 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1652 mty <- match' ty ty'
1653 ms <- match' s s'
1654 return (mt ++ mty ++ ms)
1655 match (PHidden x) (PHidden y) = match' x y
1656 match (PUnifyLog x) y = match' x y
1657 match x (PUnifyLog y) = match' x y
1658 match (PNoImplicits x) y = match' x y
1659 match x (PNoImplicits y) = match' x y
1660 match Placeholder _ = return []
1661 match _ Placeholder = return []
1662 match (PResolveTC _) _ = return []
1663 match a b | a == b = return []
1664 | otherwise = LeftErr (a, b)
1666 checkRpts (RightOK ms) = check ms where
1667 check ((n,t):xs)
1668 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1669 then Left (t, t')
1670 else check xs
1671 check (_:xs) = check xs
1672 check [] = Right ms
1673 checkRpts (LeftErr x) = Left x
1675substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1676substMatches ms = substMatchesShadow ms []
1678substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1679substMatchesShadow [] shs t = t
1680substMatchesShadow ((n,tm):ns) shs t
1681 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1683substMatch :: Name -> PTerm -> PTerm -> PTerm
1684substMatch n = substMatchShadow n []
1686substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1687substMatchShadow n shs tm t = sm shs t where
1688 sm xs (PRef _ n') | n == n' = tm
1689 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1690 sm xs (PPi p x t sc)
1691 | x `elem` xs
1692 = let x' = nextName x in
1693 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1694 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1695 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1696 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1697 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1698 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1699 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1700 (fmap (sm xs) tm)
1701 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1702 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1703 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1704 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1705 sm xs (PHidden x) = PHidden (sm xs x)
1706 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1707 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1708 sm xs x = x
1710 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1711 fullApp x = x
1713shadow :: Name -> Name -> PTerm -> PTerm
1714shadow n n' t = sm t where
1715 sm (PRef fc x) | n == x = PRef fc n'
1716 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1717 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1718 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1719 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1720 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1721 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1722 sm (PEq f x y) = PEq f (sm x) (sm y)
1723 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1724 sm (PTyped x y) = PTyped (sm x) (sm y)
1725 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1726 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1727 sm (PAlternative a as) = PAlternative a (map sm as)
1728 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1729 sm (PProof ts) = PProof (map (fmap sm) ts)
1730 sm (PHidden x) = PHidden (sm x)
1731 sm (PUnifyLog x) = PUnifyLog (sm x)
1732 sm (PNoImplicits x) = PNoImplicits (sm x)
1733 sm x = x
1735-- Rename any binders which are repeated (so that we don't have to mess
1736-- about with shadowing anywhere else).
1738mkUniqueNames :: [Name] -> PTerm -> PTerm
1739mkUniqueNames env tm = evalState (mkUniq tm) env where
1740 inScope = boundNamesIn tm
1742 mkUniqA arg = do t' <- mkUniq (getTm arg)
1743 return (arg { getTm = t' })
1745 -- Initialise the unique name with the environment length (so we're not
1746 -- looking for too long...)
1747 initN (UN n) l = UN $ txt (str n ++ show l)
1748 initN (MN i s) l = MN (i+l) s
1749 initN n l = n
1751 -- FIXME: Probably ought to do this for completeness! It's fine as
1752 -- long as there are no bindings inside tactics though.
1753 mkUniqT tac = return tac
1755 mkUniq :: PTerm -> State [Name] PTerm
1756 mkUniq (PLam n ty sc)
1757 = do env <- get
1758 (n', sc') <-
1759 if n `elem` env
1760 then do let n' = uniqueName (initN n (length env))
1761 (env ++ inScope)
1762 return (n', shadow n n' sc)
1763 else return (n, sc)
1764 put (n' : env)
1765 ty' <- mkUniq ty
1766 sc'' <- mkUniq sc'
1767 return $! PLam n' ty' sc''
1768 mkUniq (PPi p n ty sc)
1769 = do env <- get
1770 (n', sc') <-
1771 if n `elem` env
1772 then do let n' = uniqueName (initN n (length env))
1773 (env ++ inScope)
1774 return (n', shadow n n' sc)
1775 else return (n, sc)
1776 put (n' : env)
1777 ty' <- mkUniq ty
1778 sc'' <- mkUniq sc'
1779 return $! PPi p n' ty' sc''
1780 mkUniq (PLet n ty val sc)
1781 = do env <- get
1782 (n', sc') <-
1783 if n `elem` env
1784 then do let n' = uniqueName (initN n (length env))
1785 (env ++ inScope)
1786 return (n', shadow n n' sc)
1787 else return (n, sc)
1788 put (n' : env)
1789 ty' <- mkUniq ty; val' <- mkUniq val
1790 sc'' <- mkUniq sc'
1791 return $! PLet n' ty' val' sc''
1792 mkUniq (PApp fc t args)
1793 = do t' <- mkUniq t
1794 args' <- mapM mkUniqA args
1795 return $! PApp fc t' args'
1796 mkUniq (PAppBind fc t args)
1797 = do t' <- mkUniq t
1798 args' <- mapM mkUniqA args
1799 return $! PAppBind fc t' args'
1800 mkUniq (PCase fc t alts)
1801 = do t' <- mkUniq t
1802 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1803 return (x', y')) alts
1804 return $! PCase fc t' alts'
1805 mkUniq (PPair fc p l r)
1806 = do l' <- mkUniq l; r' <- mkUniq r
1807 return $! PPair fc p l' r'
1808 mkUniq (PDPair fc p (PRef fc' n) t sc)
1809 | t /= Placeholder
1810 = do env <- get
1811 (n', sc') <- if n `elem` env
1812 then do let n' = uniqueName n (env ++ inScope)
1813 return (n', shadow n n' sc)
1814 else return (n, sc)
1815 put (n' : env)
1816 t' <- mkUniq t
1817 sc'' <- mkUniq sc'
1818 return $! PDPair fc p (PRef fc' n') t' sc''
1819 mkUniq (PDPair fc p l t r)
1820 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1821 return $! PDPair fc p l' t' r'
1822 mkUniq (PAlternative b as)
1823 = liftM (PAlternative b) (mapM mkUniq as)
1824 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1825 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1826 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1827 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1828 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1829 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1830 mkUniq t = return t