git.iko.soy/Idris-dev
on 60abf37 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1725 lines 72 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.IdeSlave
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.State
22import Control.Monad.Error(throwError)
24import Data.List
25import Data.Char
26import qualified Data.Text as T
27import Data.Either
28import qualified Data.Map as M
29import Data.Maybe
30import qualified Data.Set as S
31import Data.Word (Word)
33import Debug.Trace
35import Control.Monad.Error (throwError, catchError)
36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
38import Util.Pretty
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 case mapMaybe (findDyLib ls) libs of
69 x:_ -> return (Left x)
70 [] -> do
71 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
72 case msum handle of
73 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
74 concat (intersperse "," libs) ++ "\"")
75 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
76 return (Left x)
77 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
78 findDyLib [] l = Nothing
79 findDyLib (lib:libs) l | l == lib_name lib = Just lib
80 | otherwise = findDyLib libs l
83addHdr :: Codegen -> String -> Idris ()
84addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
86addLangExt :: LanguageExt -> Idris ()
87addLangExt TypeProviders = do i <- getIState
88 putIState $ i {
89 idris_language_extensions = TypeProviders : idris_language_extensions i
90 }
91addLangExt ErrorReflection = do i <- getIState
92 putIState $ i {
93 idris_language_extensions = ErrorReflection : idris_language_extensions i
94 }
96addTrans :: (Term, Term) -> Idris ()
97addTrans t = do i <- getIState
98 putIState $ i { idris_transforms = t : idris_transforms i }
100addErrRev :: (Term, Term) -> Idris ()
101addErrRev t = do i <- getIState
102 putIState $ i { idris_errRev = t : idris_errRev i }
104totcheck :: (FC, Name) -> Idris ()
105totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
107defer_totcheck :: (FC, Name) -> Idris ()
108defer_totcheck n
109 = do i <- getIState;
110 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
112clear_totcheck :: Idris ()
113clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
115setFlags :: Name -> [FnOpt] -> Idris ()
116setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
118setAccessibility :: Name -> Accessibility -> Idris ()
119setAccessibility n a
120 = do i <- getIState
121 let ctxt = setAccess n a (tt_ctxt i)
122 putIState $ i { tt_ctxt = ctxt }
124setTotality :: Name -> Totality -> Idris ()
125setTotality n a
126 = do i <- getIState
127 let ctxt = setTotal n a (tt_ctxt i)
128 putIState $ i { tt_ctxt = ctxt }
130getTotality :: Name -> Idris Totality
131getTotality n
132 = do i <- getIState
133 case lookupTotal n (tt_ctxt i) of
134 [t] -> return t
135 _ -> return (Total [])
137-- Get coercions which might return the required type
138getCoercionsTo :: IState -> Type -> [Name]
139getCoercionsTo i ty =
140 let cs = idris_coercions i
141 (fn,_) = unApply (getRetTy ty) in
142 findCoercions fn cs
143 where findCoercions t [] = []
144 findCoercions t (n : ns) =
145 let ps = case lookupTy n (tt_ctxt i) of
146 [ty'] -> case unApply (getRetTy ty') of
147 (t', _) ->
148 if t == t' then [n] else []
149 _ -> [] in
150 ps ++ findCoercions t ns
152addToCG :: Name -> CGInfo -> Idris ()
153addToCG n cg
154 = do i <- getIState
155 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
157-- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.
158addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
159addFunctionErrorHandlers f arg hs =
160 do i <- getIState
161 let oldHandlers = idris_function_errorhandlers i
162 let newHandlers = flip (addDef f) oldHandlers $
163 case lookupCtxtExact f oldHandlers of
164 Nothing -> M.singleton arg (S.fromList hs)
165 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
166 -- will always be one of those two, thus no extra case
167 putIState $ i { idris_function_errorhandlers = newHandlers }
169getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
170getFunctionErrorHandlers f arg = do i <- getIState
171 return . maybe [] S.toList $
172 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
175-- Trace all the names in a call graph starting at the given name
176getAllNames :: Name -> Idris [Name]
177getAllNames n = allNames [] n
179allNames :: [Name] -> Name -> Idris [Name]
180allNames ns n | n `elem` ns = return []
181allNames ns n = do i <- getIState
182 case lookupCtxtExact n (idris_callgraph i) of
183 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
184 return (nub (n : concat more))
185 _ -> return [n]
187addCoercion :: Name -> Idris ()
188addCoercion n = do i <- getIState
189 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
191addDocStr :: Name -> String -> Idris ()
192addDocStr n doc
193 = do i <- getIState
194 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
196addNameHint :: Name -> Name -> Idris ()
197addNameHint ty n
198 = do i <- getIState
199 ty' <- case lookupCtxtName ty (idris_implicits i) of
200 [(tyn, _)] -> return tyn
201 [] -> throwError (NoSuchVariable ty)
202 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
203 let ns' = case lookupCtxt ty' (idris_namehints i) of
204 [ns] -> ns ++ [n]
205 _ -> [n]
206 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
208getNameHints :: IState -> Name -> [Name]
209getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
210getNameHints i n =
211 case lookupCtxt n (idris_namehints i) of
212 [ns] -> ns
213 _ -> []
215addToCalledG :: Name -> [Name] -> Idris ()
216addToCalledG n ns = return () -- TODO
218-- Add a class instance function. Dodgy hack: Put integer instances first in the
219-- list so they are resolved by default.
220-- Dodgy hack 2: put constraint chasers (@@) last
222addInstance :: Bool -> Name -> Name -> Idris ()
223addInstance int n i
224 = do ist <- getIState
225 case lookupCtxt n (idris_classes ist) of
226 [CI a b c d e ins] ->
227 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
228 putIState $ ist { idris_classes = cs }
229 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
230 putIState $ ist { idris_classes = cs }
231 where addI i ins | int = i : ins
232 | chaser n = ins ++ [i]
233 | otherwise = insI i ins
234 insI i [] = [i]
235 insI i (n : ns) | chaser n = i : n : ns
236 | otherwise = n : insI i ns
238 chaser (UN nm)
239 | ('@':'@':_) <- str nm = True
240 chaser (NS n _) = chaser n
241 chaser _ = False
243addClass :: Name -> ClassInfo -> Idris ()
244addClass n i
245 = do ist <- getIState
246 let i' = case lookupCtxt n (idris_classes ist) of
247 [c] -> c { class_instances = class_instances i }
248 _ -> i
249 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
251addIBC :: IBCWrite -> Idris ()
252addIBC ibc@(IBCDef n)
253 = do i <- getIState
254 when (notDef (ibc_write i)) $
255 putIState $ i { ibc_write = ibc : ibc_write i }
256 where notDef [] = True
257 notDef (IBCDef n': is) | n == n' = False
258 notDef (_ : is) = notDef is
259addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
261clearIBC :: Idris ()
262clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
264resetNameIdx :: Idris ()
265resetNameIdx = do i <- getIState
266 put (i { idris_nameIdx = (0, emptyContext) })
268-- Used to preserve sharing of names
269addNameIdx :: Name -> Idris (Int, Name)
270addNameIdx n = do i <- getIState
271 let (i', x) = addNameIdx' i n
272 return x
274addNameIdx' :: IState -> Name -> (IState, (Int, Name))
275addNameIdx' i n
276 = let idxs = snd (idris_nameIdx i) in
277 case lookupCtxt n idxs of
278 [x] -> (i, x)
279 _ -> let i' = fst (idris_nameIdx i) + 1 in
280 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
282getHdrs :: Codegen -> Idris [String]
283getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
285setErrLine :: Int -> Idris ()
286setErrLine x = do i <- getIState;
287 case (errLine i) of
288 Nothing -> putIState $ i { errLine = Just x }
289 Just _ -> return ()
291clearErr :: Idris ()
292clearErr = do i <- getIState
293 putIState $ i { errLine = Nothing }
295getSO :: Idris (Maybe String)
296getSO = do i <- getIState
297 return (compiled_so i)
299setSO :: Maybe String -> Idris ()
300setSO s = do i <- getIState
301 putIState $ (i { compiled_so = s })
303getIState :: Idris IState
304getIState = get
306putIState :: IState -> Idris ()
307putIState = put
309-- | A version of liftIO that puts errors into the exception type of the Idris monad
310runIO :: IO a -> Idris a
311runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
312-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
314getName :: Idris Int
315getName = do i <- getIState;
316 let idx = idris_name i;
317 putIState $ (i { idris_name = idx + 1 })
318 return idx
320addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
321addInternalApp fp l t
322 = do i <- getIState
323 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
325getInternalApp :: FilePath -> Int -> Idris PTerm
326getInternalApp fp l = do i <- getIState
327 case lookup (fp, l) (idris_lineapps i) of
328 Just n' -> return n'
329 Nothing -> return Placeholder
330 -- TODO: What if it's not there?
332-- Pattern definitions are only used for coverage checking, so erase them
333-- when we're done
334clearOrigPats :: Idris ()
335clearOrigPats = do i <- get
336 let ps = idris_patdefs i
337 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
338 put (i { idris_patdefs = ps' })
340-- Erase types from Ps in the context (basically ending up with what's in
341-- the .ibc, which is all we need after all the analysis is done)
342clearPTypes :: Idris ()
343clearPTypes = do i <- get
344 let ctxt = tt_ctxt i
345 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
346 where pErase (CaseOp c t tys orig tot cds)
347 = CaseOp c t tys orig [] (pErase' cds)
348 pErase x = x
349 pErase' (CaseDefs _ (cs, c) _ rs)
350 = let c' = (cs, fmap pEraseType c) in
351 CaseDefs c' c' c' rs
353checkUndefined :: FC -> Name -> Idris ()
354checkUndefined fc n
355 = do i <- getContext
356 case lookupTy n i of
357 (_:_) -> throwError . Msg $ show fc ++ ":" ++
358 show n ++ " already defined"
359 _ -> return ()
361isUndefined :: FC -> Name -> Idris Bool
362isUndefined fc n
363 = do i <- getContext
364 case lookupTy n i of
365 (_:_) -> return False
366 _ -> return True
368setContext :: Context -> Idris ()
369setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
371updateContext :: (Context -> Context) -> Idris ()
372updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
374addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
375addConstraints fc (v, cs)
376 = do i <- getIState
377 let ctxt = tt_ctxt i
378 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
379 next_tvar = v }
380 let ics = zip cs (repeat fc) ++ idris_constraints i
381 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
383addDeferred = addDeferred' Ref
384addDeferredTyCon = addDeferred' (TCon 0 0)
386addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
387addDeferred' nt ns
388 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
389 i <- getIState
390 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
391 idris_metavars i }
392 where tidyNames used (Bind (MN i x) b sc)
393 = let n' = uniqueName (UN x) used in
394 Bind n' b $ tidyNames (n':used) sc
395 tidyNames used (Bind n b sc)
396 = let n' = uniqueName n used in
397 Bind n' b $ tidyNames (n':used) sc
398 tidyNames used b = b
400solveDeferred :: Name -> Idris ()
401solveDeferred n = do i <- getIState
402 putIState $ i { idris_metavars =
403 filter (\(n', _) -> n/=n')
404 (idris_metavars i) }
406getUndefined :: Idris [Name]
407getUndefined = do i <- getIState
408 return (map fst (idris_metavars i) \\ primDefs)
410ihPrintResult :: Handle -> String -> Idris ()
411ihPrintResult h s = do i <- getIState
412 case idris_outputmode i of
413 RawOutput -> case s of
414 "" -> return ()
415 s -> runIO $ hPutStrLn h s
416 IdeSlave n ->
417 let good = SexpList [SymbolAtom "ok", toSExp s] in
418 runIO $ hPutStrLn h $ convSExp "return" good n
420-- | Write a pretty-printed term to the console with semantic coloring
421consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
422consoleDisplayAnnotated h output = do ist <- getIState
423 runIO . hPutStrLn h .
424 displayDecorated (consoleDecorate ist) .
425 renderCompact $ output
427-- | Write pretty-printed output to IDESlave with semantic annotations
428ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
429ideSlaveReturnAnnotated n h out = do ist <- getIState
430 let (str, spans) = displaySpans .
431 renderCompact .
432 fmap (fancifyAnnots ist) $
433 out
434 good = [SymbolAtom "ok", toSExp str, toSExp spans]
435 runIO . hPutStrLn h $ convSExp "return" good n
437ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
438ihPrintTermWithType h tm ty = do ist <- getIState
439 let output = tm <+> colon <+> ty
440 case idris_outputmode ist of
441 RawOutput -> consoleDisplayAnnotated h output
442 IdeSlave n -> ideSlaveReturnAnnotated n h output
444-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
445ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
446ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n
447ihPrintFunTypes h n overloads = do imp <- impShow
448 ist <- getIState
449 let output = vsep (map (uncurry (ppOverload imp)) overloads)
450 case idris_outputmode ist of
451 RawOutput -> consoleDisplayAnnotated h output
452 IdeSlave n -> ideSlaveReturnAnnotated n h output
453 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
454 ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm
456fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
457fancifyAnnots ist annot@(AnnName n _ _) =
458 do let ctxt = tt_ctxt ist
459 case () of
460 _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
461 _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
462 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
463 _ | otherwise -> annot
464fancifyAnnots _ annot = annot
466type1Doc :: Doc OutputAnnotation
467type1Doc = (annotate AnnConstType $ text "Type 1")
469ihPrintError :: Handle -> String -> Idris ()
470ihPrintError h s = do i <- getIState
471 case idris_outputmode i of
472 RawOutput -> case s of
473 "" -> return ()
474 s -> runIO $ hPutStrLn h s
475 IdeSlave n ->
476 let good = SexpList [SymbolAtom "error", toSExp s] in
477 runIO . hPutStrLn h $ convSExp "return" good n
479ihputStrLn :: Handle -> String -> Idris ()
480ihputStrLn h s = do i <- getIState
481 case idris_outputmode i of
482 RawOutput -> runIO $ hPutStrLn h s
483 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
485iputStrLn = ihputStrLn stdout
486iPrintError = ihPrintError stdout
487iPrintResult = ihPrintResult stdout
488iWarn = ihWarn stdout
490ideslavePutSExp :: SExpable a => String -> a -> Idris ()
491ideslavePutSExp cmd info = do i <- getIState
492 case idris_outputmode i of
493 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
494 _ -> return ()
496-- this needs some typing magic and more structured output towards emacs
497iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
498iputGoal g = do i <- getIState
499 case idris_outputmode i of
500 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
501 IdeSlave n -> runIO . putStrLn $
502 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
504isetPrompt :: String -> Idris ()
505isetPrompt p = do i <- getIState
506 case idris_outputmode i of
507 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
509ihWarn :: Handle -> FC -> String -> Idris ()
510ihWarn h fc err = do i <- getIState
511 case idris_outputmode i of
512 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
513 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
515setLogLevel :: Int -> Idris ()
516setLogLevel l = do i <- getIState
517 let opts = idris_options i
518 let opt' = opts { opt_logLevel = l }
519 putIState $ i { idris_options = opt' }
521setCmdLine :: [Opt] -> Idris ()
522setCmdLine opts = do i <- getIState
523 let iopts = idris_options i
524 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
526getCmdLine :: Idris [Opt]
527getCmdLine = do i <- getIState
528 return (opt_cmdline (idris_options i))
530getDumpDefun :: Idris (Maybe FilePath)
531getDumpDefun = do i <- getIState
532 return $ findC (opt_cmdline (idris_options i))
533 where findC [] = Nothing
534 findC (DumpDefun x : _) = Just x
535 findC (_ : xs) = findC xs
537getDumpCases :: Idris (Maybe FilePath)
538getDumpCases = do i <- getIState
539 return $ findC (opt_cmdline (idris_options i))
540 where findC [] = Nothing
541 findC (DumpCases x : _) = Just x
542 findC (_ : xs) = findC xs
544logLevel :: Idris Int
545logLevel = do i <- getIState
546 return (opt_logLevel (idris_options i))
548setErrContext :: Bool -> Idris ()
549setErrContext t = do i <- getIState
550 let opts = idris_options i
551 let opt' = opts { opt_errContext = t }
552 putIState $ i { idris_options = opt' }
554errContext :: Idris Bool
555errContext = do i <- getIState
556 return (opt_errContext (idris_options i))
558useREPL :: Idris Bool
559useREPL = do i <- getIState
560 return (opt_repl (idris_options i))
562setREPL :: Bool -> Idris ()
563setREPL t = do i <- getIState
564 let opts = idris_options i
565 let opt' = opts { opt_repl = t }
566 putIState $ i { idris_options = opt' }
568showOrigErr :: Idris Bool
569showOrigErr = do i <- getIState
570 return (opt_origerr (idris_options i))
572setShowOrigErr :: Bool -> Idris ()
573setShowOrigErr b = do i <- getIState
574 let opts = idris_options i
575 let opt' = opts { opt_origerr = b }
576 putIState $ i { idris_options = opt' }
578setNoBanner :: Bool -> Idris ()
579setNoBanner n = do i <- getIState
580 let opts = idris_options i
581 let opt' = opts { opt_nobanner = n }
582 putIState $ i { idris_options = opt' }
584getNoBanner :: Idris Bool
585getNoBanner = do i <- getIState
586 let opts = idris_options i
587 return (opt_nobanner opts)
589setQuiet :: Bool -> Idris ()
590setQuiet q = do i <- getIState
591 let opts = idris_options i
592 let opt' = opts { opt_quiet = q }
593 putIState $ i { idris_options = opt' }
595getQuiet :: Idris Bool
596getQuiet = do i <- getIState
597 let opts = idris_options i
598 return (opt_quiet opts)
600setCodegen :: Codegen -> Idris ()
601setCodegen t = do i <- getIState
602 let opts = idris_options i
603 let opt' = opts { opt_codegen = t }
604 putIState $ i { idris_options = opt' }
606codegen :: Idris Codegen
607codegen = do i <- getIState
608 return (opt_codegen (idris_options i))
610setOutputTy :: OutputType -> Idris ()
611setOutputTy t = do i <- getIState
612 let opts = idris_options i
613 let opt' = opts { opt_outputTy = t }
614 putIState $ i { idris_options = opt' }
616outputTy :: Idris OutputType
617outputTy = do i <- getIState
618 return $ opt_outputTy $ idris_options i
620setIdeSlave :: Bool -> Idris ()
621setIdeSlave True = do i <- getIState
622 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
623setIdeSlave False = return ()
625setTargetTriple :: String -> Idris ()
626setTargetTriple t = do i <- getIState
627 let opts = idris_options i
628 opt' = opts { opt_triple = t }
629 putIState $ i { idris_options = opt' }
631targetTriple :: Idris String
632targetTriple = do i <- getIState
633 return (opt_triple (idris_options i))
635setTargetCPU :: String -> Idris ()
636setTargetCPU t = do i <- getIState
637 let opts = idris_options i
638 opt' = opts { opt_cpu = t }
639 putIState $ i { idris_options = opt' }
641targetCPU :: Idris String
642targetCPU = do i <- getIState
643 return (opt_cpu (idris_options i))
645setOptLevel :: Word -> Idris ()
646setOptLevel t = do i <- getIState
647 let opts = idris_options i
648 opt' = opts { opt_optLevel = t }
649 putIState $ i { idris_options = opt' }
651optLevel :: Idris Word
652optLevel = do i <- getIState
653 return (opt_optLevel (idris_options i))
655verbose :: Idris Bool
656verbose = do i <- getIState
657 return (opt_verbose (idris_options i))
659setVerbose :: Bool -> Idris ()
660setVerbose t = do i <- getIState
661 let opts = idris_options i
662 let opt' = opts { opt_verbose = t }
663 putIState $ i { idris_options = opt' }
665typeInType :: Idris Bool
666typeInType = do i <- getIState
667 return (opt_typeintype (idris_options i))
669setTypeInType :: Bool -> Idris ()
670setTypeInType t = do i <- getIState
671 let opts = idris_options i
672 let opt' = opts { opt_typeintype = t }
673 putIState $ i { idris_options = opt' }
675coverage :: Idris Bool
676coverage = do i <- getIState
677 return (opt_coverage (idris_options i))
679setCoverage :: Bool -> Idris ()
680setCoverage t = do i <- getIState
681 let opts = idris_options i
682 let opt' = opts { opt_coverage = t }
683 putIState $ i { idris_options = opt' }
685setIBCSubDir :: FilePath -> Idris ()
686setIBCSubDir fp = do i <- getIState
687 let opts = idris_options i
688 let opt' = opts { opt_ibcsubdir = fp }
689 putIState $ i { idris_options = opt' }
691valIBCSubDir :: IState -> Idris FilePath
692valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
694addImportDir :: FilePath -> Idris ()
695addImportDir fp = do i <- getIState
696 let opts = idris_options i
697 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
698 putIState $ i { idris_options = opt' }
700setImportDirs :: [FilePath] -> Idris ()
701setImportDirs fps = do i <- getIState
702 let opts = idris_options i
703 let opt' = opts { opt_importdirs = fps }
704 putIState $ i { idris_options = opt' }
706allImportDirs :: Idris [FilePath]
707allImportDirs = do i <- getIState
708 let optdirs = opt_importdirs (idris_options i)
709 return ("." : reverse optdirs)
711colourise :: Idris Bool
712colourise = do i <- getIState
713 return $ idris_colourRepl i
715setColourise :: Bool -> Idris ()
716setColourise b = do i <- getIState
717 putIState $ i { idris_colourRepl = b }
719setOutH :: Handle -> Idris ()
720setOutH h = do i <- getIState
721 putIState $ i { idris_outh = h }
723impShow :: Idris Bool
724impShow = do i <- getIState
725 return (opt_showimp (idris_options i))
727setImpShow :: Bool -> Idris ()
728setImpShow t = do i <- getIState
729 let opts = idris_options i
730 let opt' = opts { opt_showimp = t }
731 putIState $ i { idris_options = opt' }
733setColour :: ColourType -> IdrisColour -> Idris ()
734setColour ct c = do i <- getIState
735 let newTheme = setColour' ct c (idris_colourTheme i)
736 putIState $ i { idris_colourTheme = newTheme }
737 where setColour' KeywordColour c t = t { keywordColour = c }
738 setColour' BoundVarColour c t = t { boundVarColour = c }
739 setColour' ImplicitColour c t = t { implicitColour = c }
740 setColour' FunctionColour c t = t { functionColour = c }
741 setColour' TypeColour c t = t { typeColour = c }
742 setColour' DataColour c t = t { dataColour = c }
743 setColour' PromptColour c t = t { promptColour = c }
745logLvl :: Int -> String -> Idris ()
746logLvl l str = do i <- getIState
747 let lvl = opt_logLevel (idris_options i)
748 when (lvl >= l) $
749 case idris_outputmode i of
750 RawOutput -> do runIO $ putStrLn str
751 IdeSlave n ->
752 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
753 runIO $ putStrLn $ convSExp "log" good n
755cmdOptType :: Opt -> Idris Bool
756cmdOptType x = do i <- getIState
757 return $ x `elem` opt_cmdline (idris_options i)
759iLOG :: String -> Idris ()
760iLOG = logLvl 1
762noErrors :: Idris Bool
763noErrors = do i <- getIState
764 case errLine i of
765 Nothing -> return True
766 _ -> return False
768setTypeCase :: Bool -> Idris ()
769setTypeCase t = do i <- getIState
770 let opts = idris_options i
771 let opt' = opts { opt_typecase = t }
772 putIState $ i { idris_options = opt' }
775-- Dealing with parameters
777expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
778 [Name] -> -- all names
779 [Name] -> -- names with no declaration
780 PTerm -> PTerm
781expandParams dec ps ns infs tm = en tm
782 where
783 -- if we shadow a name (say in a lambda binding) that is used in a call to
784 -- a lifted function, we need access to both names - once in the scope of the
785 -- binding and once to call the lifted functions. So we'll explicitly shadow
786 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
787 -- but we didn't...)
789 mkShadow (UN n) = MN 0 n
790 mkShadow (MN i n) = MN (i+1) n
791 mkShadow (NS x s) = NS (mkShadow x) s
793 en (PLam n t s)
794 | n `elem` (map fst ps ++ ns)
795 = let n' = mkShadow n in
796 PLam n' (en t) (en (shadow n n' s))
797 | otherwise = PLam n (en t) (en s)
798 en (PPi p n t s)
799 | n `elem` (map fst ps ++ ns)
800 = let n' = mkShadow n in
801 PPi p n' (en t) (en (shadow n n' s))
802 | otherwise = PPi p n (en t) (en s)
803 en (PLet n ty v s)
804 | n `elem` (map fst ps ++ ns)
805 = let n' = mkShadow n in
806 PLet n' (en ty) (en v) (en (shadow n n' s))
807 | otherwise = PLet n (en ty) (en v) (en s)
808 -- FIXME: Should only do this in a type signature!
809 en (PDPair f (PRef f' n) t r)
810 | n `elem` (map fst ps ++ ns) && t /= Placeholder
811 = let n' = mkShadow n in
812 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
813 en (PEq f l r) = PEq f (en l) (en r)
814 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
815 en (PTyped l r) = PTyped (en l) (en r)
816 en (PPair f l r) = PPair f (en l) (en r)
817 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
818 en (PAlternative a as) = PAlternative a (map en as)
819 en (PHidden t) = PHidden (en t)
820 en (PUnifyLog t) = PUnifyLog (en t)
821 en (PNoImplicits t) = PNoImplicits (en t)
822 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
823 en (PProof ts) = PProof (map (fmap en) ts)
824 en (PTactics ts) = PTactics (map (fmap en) ts)
826 en (PQuote (Var n))
827 | n `nselem` ns = PQuote (Var (dec n))
828 en (PApp fc (PInferRef fc' n) as)
829 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
830 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
831 en (PApp fc (PRef fc' n) as)
832 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
833 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
834 | n `nselem` ns = PApp fc (PRef fc' (dec n))
835 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
836 en (PAppBind fc (PRef fc' n) as)
837 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
838 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
839 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
840 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
841 en (PRef fc n)
842 | n `elem` infs = PApp fc (PInferRef fc (dec n))
843 (map (pexp . (PRef fc)) (map fst ps))
844 | n `nselem` ns = PApp fc (PRef fc (dec n))
845 (map (pexp . (PRef fc)) (map fst ps))
846 en (PInferRef fc n)
847 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
848 (map (pexp . (PRef fc)) (map fst ps))
849 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
850 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
851 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
852 en t = t
854 nselem x [] = False
855 nselem x (y : xs) | nseq x y = True
856 | otherwise = nselem x xs
858 nseq x y = nsroot x == nsroot y
860expandParamsD :: Bool -> -- True = RHS only
861 IState ->
862 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
863expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
864 = if n `elem` ns && (not rhsonly)
865 then -- trace (show (n, expandParams dec ps ns ty)) $
866 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
867 else --trace (show (n, expandParams dec ps ns ty)) $
868 PTy doc syn fc o n (expandParams dec ps ns [] ty)
869expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
870 = if n `elem` ns && (not rhsonly)
871 then -- trace (show (n, expandParams dec ps ns ty)) $
872 PPostulate doc syn fc o (dec n) (piBind ps
873 (expandParams dec ps ns [] ty))
874 else --trace (show (n, expandParams dec ps ns ty)) $
875 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
876expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
877 = let n' = if n `elem` ns then dec n else n in
878 PClauses fc opts n' (map expandParamsC cs)
879 where
880 expandParamsC (PClause fc n lhs ws rhs ds)
881 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
882 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
883 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
884 n' = if n `elem` ns then dec n else n
885 -- names bound on the lhs should not be expanded on the rhs
886 ns' = removeBound lhs ns in
887 PClause fc n' lhs'
888 (map (expandParams dec ps'' ns' []) ws)
889 (expandParams dec ps'' ns' [] rhs)
890 (map (expandParamsD True ist dec ps'' ns') ds)
891 expandParamsC (PWith fc n lhs ws wval ds)
892 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
893 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
894 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
895 n' = if n `elem` ns then dec n else n
896 ns' = removeBound lhs ns in
897 PWith fc n' lhs'
898 (map (expandParams dec ps'' ns' []) ws)
899 (expandParams dec ps'' ns' [] wval)
900 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
901 updateps yn nm [] = []
902 updateps yn nm (((a, t), i):as)
903 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
904 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
906 removeBound lhs ns = ns \\ nub (bnames lhs)
908 bnames (PRef _ n) = [n]
909 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
910 bnames (PPair _ l r) = bnames l ++ bnames r
911 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
912 bnames _ = []
914expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
915 = PData doc syn fc co (expandPData pd)
916 where
917 -- just do the type decl, leave constructors alone (parameters will be
918 -- added implicitly)
919 expandPData (PDatadecl n ty cons)
920 = if n `elem` ns
921 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
922 (map econ cons)
923 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
924 econ (doc, n, t, fc, fs)
925 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
926expandParamsD rhs ist dec ps ns (PParams f params pds)
927 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
928 (map (expandParamsD True ist dec ps ns) pds)
929-- (map (expandParamsD ist dec ps ns) pds)
930expandParamsD rhs ist dec ps ns (PMutual f pds)
931 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
932expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
933 = PClass doc info f
934 (map (expandParams dec ps ns []) cs)
935 n
936 (map (mapsnd (expandParams dec ps ns [])) params)
937 (map (expandParamsD rhs ist dec ps ns) decls)
938expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
939 = PInstance info f
940 (map (expandParams dec ps ns []) cs)
941 n
942 (map (expandParams dec ps ns []) params)
943 (expandParams dec ps ns [] ty)
944 cn
945 (map (expandParamsD rhs ist dec ps ns) decls)
946expandParamsD rhs ist dec ps ns d = d
948mapsnd f (x, t) = (x, f t)
950-- Calculate a priority for a type, for deciding elaboration order
951-- * if it's just a type variable or concrete type, do it early (0)
952-- * if there's only type variables and injective constructors, do it next (1)
953-- * if there's a function type, next (2)
954-- * finally, everything else (3)
956getPriority :: IState -> PTerm -> Int
957getPriority i tm = 1 -- pri tm
958 where
959 pri (PRef _ n) =
960 case lookupP n (tt_ctxt i) of
961 ((P (DCon _ _) _ _):_) -> 1
962 ((P (TCon _ _) _ _):_) -> 1
963 ((P Ref _ _):_) -> 1
964 [] -> 0 -- must be locally bound, if it's not an error...
965 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
966 pri (PTrue _) = 0
967 pri (PFalse _) = 0
968 pri (PRefl _ _) = 1
969 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
970 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
971 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
972 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
973 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
974 pri (PTyped l r) = pri l
975 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
976 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
977 pri (PAlternative a as) = maximum (map pri as)
978 pri (PConstant _) = 0
979 pri Placeholder = 1
980 pri _ = 3
982addStatics :: Name -> Term -> PTerm -> Idris ()
983addStatics n tm ptm =
984 do let (statics, dynamics) = initStatics tm ptm
985 let stnames = nub $ concatMap freeArgNames (map snd statics)
986 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
987 -- also get the arguments which are 'uniquely inferrable' from
988 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
989 let statics' = nub $ map fst statics ++
990 filter (\x -> not (elem x dnames)) stnames
991 let stpos = staticList statics' tm
992 i <- getIState
993 when (not (null statics)) $
994 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
995 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
996 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
997 addIBC (IBCStatic n)
998 where
999 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1000 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1001 if pstatic p == Static then ((n, ty) : static, dynamic)
1002 else if (not (searchArg p))
1003 then (static, (n, ty) : dynamic)
1004 else (static, dynamic)
1005 initStatics t pt = ([], [])
1007 freeArgNames (Bind n (Pi ty) sc)
1008 = nub $ freeArgNames ty
1009 freeArgNames tm = let (_, args) = unApply tm in
1010 concatMap freeNames args
1012 -- if a name appears in a type class or tactic implicit index, it doesn't
1013 -- affect its 'uniquely inferrable' from a static status since these are
1014 -- resolved by searching.
1015 searchArg (Constraint _ _ _) = True
1016 searchArg (TacImp _ _ _ _) = True
1017 searchArg _ = False
1019 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1020 staticList _ _ = []
1022-- Dealing with implicit arguments
1024-- Add constraint bindings from using block
1026addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1027addUsingConstraints syn fc t
1028 = do ist <- get
1029 let ns = namesIn [] ist t
1030 let cs = getConstraints t -- check declared constraints
1031 let addconsts = uconsts \\ cs
1032 -- if all names in the arguments of addconsts appear in ns,
1033 -- add the constraint implicitly
1034 return (doAdd addconsts ns t)
1035 where uconsts = filter uconst (using syn)
1036 uconst (UConstraint _ _) = True
1037 uconst _ = False
1039 doAdd [] _ t = t
1040 -- if all of args in ns, then add it
1041 doAdd (UConstraint c args : cs) ns t
1042 | all (\n -> elem n ns) args
1043 = PPi (Constraint [] Dynamic "") (sMN 0 "cu")
1044 (mkConst c args) (doAdd cs ns t)
1045 | otherwise = doAdd cs ns t
1047 mkConst c args = PApp fc (PRef fc c)
1048 (map (\n -> PExp 0 [] (PRef fc n) "") args)
1050 getConstraints (PPi (Constraint _ _ _) _ c sc)
1051 = getcapp c ++ getConstraints sc
1052 getConstraints (PPi _ _ c sc) = getConstraints sc
1053 getConstraints _ = []
1055 getcapp (PApp _ (PRef _ c) args)
1056 = do ns <- mapM getName args
1057 return (UConstraint c ns)
1058 getcapp _ = []
1060 getName (PExp _ _ (PRef _ n) _) = return n
1061 getName _ = []
1063-- Add implicit Pi bindings for any names in the term which appear in an
1064-- argument position.
1066-- This has become a right mess already. Better redo it some time...
1068implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1069implicit syn n ptm = implicit' syn [] n ptm
1071implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1072implicit' syn ignore n ptm
1073 = do i <- getIState
1074 let (tm', impdata) = implicitise syn ignore i ptm
1075-- let (tm'', spos) = findStatics i tm'
1076 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1077 addIBC (IBCImp n)
1078 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1079-- i <- get
1080-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1081 return tm'
1083implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1084implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1085 let (declimps, ns') = execState (imps True [] tm) ([], [])
1086 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1087 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1088 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1089 if null ns
1090 then (tm, reverse declimps)
1091 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1092 where
1093 uvars = map ipair (filter uimplicit (using syn))
1094 pvars = syn_params syn
1096 inUsing n = n `elem` map fst uvars
1098 ipair (UImplicit x y) = (x, y)
1099 uimplicit (UImplicit _ _) = True
1100 uimplicit _ = False
1102 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1103 | otherwise = x : dropAll xs ys
1104 dropAll [] ys = []
1106 imps top env (PApp _ f as)
1107 = do (decls, ns) <- get
1108 let isn = concatMap (namesIn uvars ist) (map getTm as)
1109 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1110 imps top env (PPi (Imp l _ doc _) n ty sc)
1111 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1112 (decls , ns) <- get
1113 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1114 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1115 imps True (n:env) sc
1116 imps top env (PPi (Exp l _ doc _) n ty sc)
1117 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1118 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1119 _ -> [])
1120 (decls, ns) <- get -- ignore decls in HO types
1121 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1122 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1123 imps True (n:env) sc
1124 imps top env (PPi (Constraint l _ doc) n ty sc)
1125 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1126 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1127 _ -> [])
1128 (decls, ns) <- get -- ignore decls in HO types
1129 put (PConstraint 10 l Placeholder doc : decls,
1130 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1131 imps True (n:env) sc
1132 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1133 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1134 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1135 _ -> [])
1136 (decls, ns) <- get -- ignore decls in HO types
1137 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1138 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1139 imps True (n:env) sc
1140 imps top env (PEq _ l r)
1141 = do (decls, ns) <- get
1142 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1143 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1144 imps top env (PRewrite _ l r _)
1145 = do (decls, ns) <- get
1146 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1147 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1148 imps top env (PTyped l r)
1149 = imps top env l
1150 imps top env (PPair _ l r)
1151 = do (decls, ns) <- get
1152 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1153 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1154 imps top env (PDPair _ (PRef _ n) t r)
1155 = do (decls, ns) <- get
1156 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1157 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1158 imps top env (PDPair _ l t r)
1159 = do (decls, ns) <- get
1160 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1161 namesIn uvars ist r
1162 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1163 imps top env (PAlternative a as)
1164 = do (decls, ns) <- get
1165 let isn = concatMap (namesIn uvars ist) as
1166 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1167 imps top env (PLam n ty sc)
1168 = do imps False env ty
1169 imps False (n:env) sc
1170 imps top env (PHidden tm) = imps False env tm
1171 imps top env (PUnifyLog tm) = imps False env tm
1172 imps top env (PNoImplicits tm) = imps False env tm
1173 imps top env _ = return ()
1175 pibind using [] sc = sc
1176 pibind using (n:ns) sc
1177 = case lookup n using of
1178 Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)
1179 Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder
1180 (pibind using ns sc)
1182-- Add implicit arguments in function calls
1183addImplPat :: IState -> PTerm -> PTerm
1184addImplPat = addImpl' True [] []
1186addImplBound :: IState -> [Name] -> PTerm -> PTerm
1187addImplBound ist ns = addImpl' False ns [] ist
1189addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1190addImplBoundInf ist ns inf = addImpl' False ns inf ist
1192addImpl :: IState -> PTerm -> PTerm
1193addImpl = addImpl' False [] []
1195-- TODO: in patterns, don't add implicits to function names guarded by constructors
1196-- and *not* inside a PHidden
1198addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1199addImpl' inpat env infns ist ptm
1200 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1201 where
1202 ai env ds (PRef fc f)
1203 | f `elem` infns = PInferRef fc f
1204 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1205 ai env ds (PHidden (PRef fc f))
1206 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1207 ai env ds (PEq fc l r)
1208 = let l' = ai env ds l
1209 r' = ai env ds r in
1210 PEq fc l' r'
1211 ai env ds (PRewrite fc l r g)
1212 = let l' = ai env ds l
1213 r' = ai env ds r
1214 g' = fmap (ai env ds) g in
1215 PRewrite fc l' r' g'
1216 ai env ds (PTyped l r)
1217 = let l' = ai env ds l
1218 r' = ai env ds r in
1219 PTyped l' r'
1220 ai env ds (PPair fc l r)
1221 = let l' = ai env ds l
1222 r' = ai env ds r in
1223 PPair fc l' r'
1224 ai env ds (PDPair fc l t r)
1225 = let l' = ai env ds l
1226 t' = ai env ds t
1227 r' = ai env ds r in
1228 PDPair fc l' t' r'
1229 ai env ds (PAlternative a as)
1230 = let as' = map (ai env ds) as in
1231 PAlternative a as'
1232 ai env _ (PDisamb ds' as) = ai env ds' as
1233 ai env ds (PApp fc (PInferRef _ f) as)
1234 = let as' = map (fmap (ai env ds)) as in
1235 PApp fc (PInferRef fc f) as'
1236 ai env ds (PApp fc ftm@(PRef _ f) as)
1237 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1238 | not (f `elem` map fst env)
1239 = let as' = map (fmap (ai env ds)) as in
1240 handleErr $ aiFn inpat False ist fc f ds as'
1241 | Just (Just ty) <- lookup f env =
1242 let as' = map (fmap (ai env ds)) as
1243 arity = getPArity ty in
1244 mkPApp fc arity ftm as'
1245 ai env ds (PApp fc f as)
1246 = let f' = ai env ds f
1247 as' = map (fmap (ai env ds)) as in
1248 mkPApp fc 1 f' as'
1249 ai env ds (PCase fc c os)
1250 = let c' = ai env ds c
1251 os' = map (pmap (ai env ds)) os in
1252 PCase fc c' os'
1253 ai env ds (PLam n ty sc)
1254 = let ty' = ai env ds ty
1255 sc' = ai ((n, Just ty):env) ds sc in
1256 PLam n ty' sc'
1257 ai env ds (PLet n ty val sc)
1258 = let ty' = ai env ds ty
1259 val' = ai env ds val
1260 sc' = ai ((n, Just ty):env) ds sc in
1261 PLet n ty' val' sc'
1262 ai env ds (PPi p n ty sc)
1263 = let ty' = ai env ds ty
1264 sc' = ai ((n, Just ty):env) ds sc in
1265 PPi p n ty' sc'
1266 ai env ds (PGoal fc r n sc)
1267 = let r' = ai env ds r
1268 sc' = ai ((n, Nothing):env) ds sc in
1269 PGoal fc r' n sc'
1270 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1271 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1272 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1273 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1274 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1275 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1276 ai env ds tm = tm
1278 handleErr (Left err) = PElabError err
1279 handleErr (Right x) = x
1281-- if in a pattern, and there are no arguments, and there's no possible
1282-- names with zero explicit arguments, don't add implicits.
1284aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1285aiFn inpat True ist fc f ds []
1286 = case lookupDef f (tt_ctxt ist) of
1287 [] -> Right $ PPatvar fc f
1288 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1289 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1290 if (not (vname f) || tcname f
1291 || any (conCaf (tt_ctxt ist)) ialts)
1292-- any constructor alts || any allImp ialts))
1293 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1294 else Right $ PPatvar fc f
1295 where imp (PExp _ _ _ _) = False
1296 imp _ = True
1297-- allImp [] = False
1298 allImp xs = all imp xs
1299 constructor (TyDecl (DCon _ _) _) = True
1300 constructor _ = False
1302 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1304 vname (UN n) = True -- non qualified
1305 vname _ = False
1307aiFn inpat expat ist fc f ds as
1308 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1309aiFn inpat expat ist fc f ds as
1310 -- This is where namespaces get resolved by adding PAlternative
1311 = do let ns = lookupCtxtName f (idris_implicits ist)
1312 let nh = filter (\(n, _) -> notHidden n) ns
1313 let ns' = case trimAlts ds nh of
1314 [] -> nh
1315 x -> x
1316 case ns' of
1317 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1318 [] -> if f `elem` (map fst (idris_metavars ist))
1319 then Right $ PApp fc (PRef fc f) as
1320 else Right $ mkPApp fc (length as) (PRef fc f) as
1321 alts -> Right $
1322 PAlternative True $
1323 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1324 (insertImpl ns as)) alts
1325 where
1326 trimAlts [] alts = alts
1327 trimAlts ns alts
1328 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1330 nspace (NS _ s) = s
1331 nspace _ = []
1333 notHidden n = case getAccessibility n of
1334 Hidden -> False
1335 _ -> True
1337 getAccessibility n
1338 = case lookupDefAcc n False (tt_ctxt ist) of
1339 [(n,t)] -> t
1340 _ -> Public
1343 insertImpl :: [PArg] -> [PArg] -> [PArg]
1344 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1345 PExp p l tm d : insertImpl ps given
1346 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1347 PConstraint p l tm d : insertImpl ps given
1348 insertImpl (PConstraint p l ty d : ps) given =
1349 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1350 insertImpl (PImp p _ l n ty d : ps) given =
1351 case find n given [] of
1352 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1353 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1354 insertImpl (PTacImplicit p l n sc' ty d : ps) given =
1355 let sc = addImpl ist sc' in
1356 case find n given [] of
1357 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1358 Nothing -> if inpat
1359 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1360 else PTacImplicit p l n sc sc "" : insertImpl ps given
1361 insertImpl expected [] = []
1362 insertImpl _ given = given
1364 find n [] acc = Nothing
1365 find n (PImp _ _ _ n' t _ : gs) acc
1366 | n == n' = Just (t, reverse acc ++ gs)
1367 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1368 | n == n' = Just (t, reverse acc ++ gs)
1369 find n (g : gs) acc = find n gs (g : acc)
1371-- replace non-linear occurrences with _
1372-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1373-- it is hard to get right!
1375stripLinear :: IState -> PTerm -> PTerm
1376stripLinear i tm = evalState (sl tm) [] where
1377 sl :: PTerm -> State [Name] PTerm
1378 sl (PRef fc f)
1379 | (_:_) <- lookupTy f (tt_ctxt i)
1380 = return $ PRef fc f
1381 | otherwise = do ns <- get
1382 if (f `elem` ns)
1383 then return Placeholder
1384 else do put (f : ns)
1385 return (PRef fc f)
1386 sl (PPatvar fc f)
1387 = do ns <- get
1388 if (f `elem` ns)
1389 then return Placeholder
1390 else do put (f : ns)
1391 return (PPatvar fc f)
1392 sl (PApp fc fn args) = do fn' <- sl fn
1393 args' <- mapM slA args
1394 return $ PApp fc fn' args'
1395 where slA (PImp p m l n t d) = do t' <- sl t
1396 return $ PImp p m l n t' d
1397 slA (PExp p l t d) = do t' <- sl t
1398 return $ PExp p l t' d
1399 slA (PConstraint p l t d)
1400 = do t' <- sl t
1401 return $ PConstraint p l t' d
1402 slA (PTacImplicit p l n sc t d)
1403 = do t' <- sl t
1404 return $ PTacImplicit p l n sc t' d
1405 sl x = return x
1407-- Remove functions which aren't applied to anything, which must then
1408-- be resolved by unification. Assume names resolved and alternatives
1409-- filled in (so no ambiguity).
1411stripUnmatchable :: IState -> PTerm -> PTerm
1412stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1413 su :: PTerm -> PTerm
1414 su (PRef fc f)
1415 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1416 = Placeholder
1417 su (PApp fc fn args)
1418 = PApp fc fn (fmap (fmap su) args)
1419 su (PAlternative b alts)
1420 = let alts' = filter (/= Placeholder) (map su alts) in
1421 if null alts' then Placeholder
1422 else PAlternative b alts'
1423 su (PPair fc l r) = PPair fc (su l) (su r)
1424 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1425 su t = t
1426stripUnmatchable i tm = tm
1428mkPApp fc a f [] = f
1429mkPApp fc a f as = let rest = drop a as in
1430 appRest fc (PApp fc f (take a as)) rest
1431 where
1432 appRest fc f [] = f
1433 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1435-- Find 'static' argument positions
1436-- (the declared ones, plus any names in argument position in the declared
1437-- statics)
1438-- FIXME: It's possible that this really has to happen after elaboration
1440findStatics :: IState -> PTerm -> (PTerm, [Bool])
1441findStatics ist tm = trace (show tm) $
1442 let (ns, ss) = fs tm in
1443 runState (pos ns ss tm) []
1444 where fs (PPi p n t sc)
1445 | Static <- pstatic p
1446 = let (ns, ss) = fs sc in
1447 (namesIn [] ist t : ns, n : ss)
1448 | otherwise = let (ns, ss) = fs sc in
1449 (ns, ss)
1450 fs _ = ([], [])
1452 inOne n ns = length (filter id (map (elem n) ns)) == 1
1454 pos ns ss (PPi p n t sc)
1455 | elem n ss = do sc' <- pos ns ss sc
1456 spos <- get
1457 put (True : spos)
1458 return (PPi (p { pstatic = Static }) n t sc')
1459 | otherwise = do sc' <- pos ns ss sc
1460 spos <- get
1461 put (False : spos)
1462 return (PPi p n t sc')
1463 pos ns ss t = return t
1465-- for 6.12/7 compatibility
1466data EitherErr a b = LeftErr a | RightOK b
1468instance Monad (EitherErr a) where
1469 return = RightOK
1471 (LeftErr e) >>= k = LeftErr e
1472 RightOK v >>= k = k v
1474toEither (LeftErr e) = Left e
1475toEither (RightOK ho) = Right ho
1477-- syntactic match of a against b, returning pair of variables in a
1478-- and what they match. Returns the pair that failed if not a match.
1480matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1481matchClause = matchClause' False
1483matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1484matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1485 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1487 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1488 fullApp x = x
1490 match' x y = match (fullApp x) (fullApp y)
1491 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1492 | fi == txt "fromInteger" && b == txt "builtins",
1493 PConstant (I _) <- getTm x = match (getTm x) x'
1494 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1495 | fi == txt "fromInteger" && b == txt "builtins",
1496 PConstant (I _) <- getTm x = match (getTm x) x'
1497 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1498 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1499 match (PApp _ f args) (PApp _ f' args')
1500 | length args == length args'
1501 = do mf <- match' f f'
1502 ms <- zipWithM matchArg args args'
1503 return (mf ++ concat ms)
1504-- match (PRef _ n) (PRef _ n') | n == n' = return []
1505-- | otherwise = Nothing
1506 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1507 match (PPatvar f n) xr = match (PRef f n) xr
1508 match xr (PPatvar f n) = match xr (PRef f n)
1509 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1510 match (PRef _ n) tm@(PRef _ n')
1511 | n == n' && not names &&
1512 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1513 || tm == Placeholder)
1514 = return [(n, tm)]
1515 | n == n' = return []
1516 match (PRef _ n) tm
1517 | not names && (not (isConName n (tt_ctxt i) ||
1518 isFnName n (tt_ctxt i)) || tm == Placeholder)
1519 = return [(n, tm)]
1520 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1521 mr <- match' r r'
1522 return (ml ++ mr)
1523 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1524 = do ml <- match' l l'
1525 mr <- match' r r'
1526 return (ml ++ mr)
1527 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1528 mr <- match r r'
1529 return (ml ++ mr)
1530 match (PTyped l r) x = match l x
1531 match x (PTyped l r) = match x l
1532 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1533 mr <- match' r r'
1534 return (ml ++ mr)
1535 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1536 mt <- match' t t'
1537 mr <- match' r r'
1538 return (ml ++ mt ++ mr)
1539 match (PAlternative a as) (PAlternative a' as')
1540 = do ms <- zipWithM match' as as'
1541 return (concat ms)
1542 match a@(PAlternative _ as) b
1543 = do let ms = zipWith match' as (repeat b)
1544 case (rights (map toEither ms)) of
1545 (x: _) -> return x
1546 _ -> LeftErr (a, b)
1547 match (PCase _ _ _) _ = return [] -- lifted out
1548 match (PMetavar _) _ = return [] -- modified
1549 match (PInferRef _ _) _ = return [] -- modified
1550 match (PQuote _) _ = return []
1551 match (PProof _) _ = return []
1552 match (PTactics _) _ = return []
1553 match (PRefl _ _) (PRefl _ _) = return []
1554 match (PResolveTC _) (PResolveTC _) = return []
1555 match (PTrue _) (PTrue _) = return []
1556 match (PFalse _) (PFalse _) = return []
1557 match (PReturn _) (PReturn _) = return []
1558 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1559 ms <- match' s s'
1560 return (mt ++ ms)
1561 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1562 ms <- match' s s'
1563 return (mt ++ ms)
1564 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1565 mty <- match' ty ty'
1566 ms <- match' s s'
1567 return (mt ++ mty ++ ms)
1568 match (PHidden x) (PHidden y) = match' x y
1569 match (PUnifyLog x) y = match' x y
1570 match x (PUnifyLog y) = match' x y
1571 match (PNoImplicits x) y = match' x y
1572 match x (PNoImplicits y) = match' x y
1573 match Placeholder _ = return []
1574 match _ Placeholder = return []
1575 match (PResolveTC _) _ = return []
1576 match a b | a == b = return []
1577 | otherwise = LeftErr (a, b)
1579 checkRpts (RightOK ms) = check ms where
1580 check ((n,t):xs)
1581 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1582 then Left (t, t')
1583 else check xs
1584 check (_:xs) = check xs
1585 check [] = Right ms
1586 checkRpts (LeftErr x) = Left x
1588substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1589substMatches ms = substMatchesShadow ms []
1591substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1592substMatchesShadow [] shs t = t
1593substMatchesShadow ((n,tm):ns) shs t
1594 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1596substMatch :: Name -> PTerm -> PTerm -> PTerm
1597substMatch n = substMatchShadow n []
1599substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1600substMatchShadow n shs tm t = sm shs t where
1601 sm xs (PRef _ n') | n == n' = tm
1602 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1603 sm xs (PPi p x t sc)
1604 | x `elem` xs
1605 = let x' = nextName x in
1606 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1607 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1608 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1609 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1610 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1611 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1612 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1613 (fmap (sm xs) tm)
1614 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1615 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1616 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1617 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1618 sm xs (PHidden x) = PHidden (sm xs x)
1619 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1620 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1621 sm xs x = x
1623 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1624 fullApp x = x
1626shadow :: Name -> Name -> PTerm -> PTerm
1627shadow n n' t = sm t where
1628 sm (PRef fc x) | n == x = PRef fc n'
1629 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1630 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1631 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1632 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1633 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1634 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1635 sm (PEq f x y) = PEq f (sm x) (sm y)
1636 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1637 sm (PTyped x y) = PTyped (sm x) (sm y)
1638 sm (PPair f x y) = PPair f (sm x) (sm y)
1639 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1640 sm (PAlternative a as) = PAlternative a (map sm as)
1641 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1642 sm (PProof ts) = PProof (map (fmap sm) ts)
1643 sm (PHidden x) = PHidden (sm x)
1644 sm (PUnifyLog x) = PUnifyLog (sm x)
1645 sm (PNoImplicits x) = PNoImplicits (sm x)
1646 sm x = x
1648-- Rename any binders which are repeated (so that we don't have to mess
1649-- about with shadowing anywhere else).
1651mkUniqueNames :: [Name] -> PTerm -> PTerm
1652mkUniqueNames env tm = evalState (mkUniq tm) env where
1653 inScope = boundNamesIn tm
1655 mkUniqA arg = do t' <- mkUniq (getTm arg)
1656 return (arg { getTm = t' })
1658 -- FIXME: Probably ought to do this for completeness! It's fine as
1659 -- long as there are no bindings inside tactics though.
1660 mkUniqT tac = return tac
1662 mkUniq :: PTerm -> State [Name] PTerm
1663 mkUniq (PLam n ty sc)
1664 = do env <- get
1665 (n', sc') <-
1666 if n `elem` env
1667 then do let n' = uniqueName n (env ++ inScope)
1668 return (n', shadow n n' sc)
1669 else return (n, sc)
1670 put (n' : env)
1671 ty' <- mkUniq ty
1672 sc'' <- mkUniq sc'
1673 return $! PLam n' ty' sc''
1674 mkUniq (PPi p n ty sc)
1675 = do env <- get
1676 (n', sc') <-
1677 if n `elem` env
1678 then do let n' = uniqueName n (env ++ inScope)
1679 return (n', shadow n n' sc)
1680 else return (n, sc)
1681 put (n' : env)
1682 ty' <- mkUniq ty
1683 sc'' <- mkUniq sc'
1684 return $! PPi p n' ty' sc''
1685 mkUniq (PLet n ty val sc)
1686 = do env <- get
1687 (n', sc') <-
1688 if n `elem` env
1689 then do let n' = uniqueName n (env ++ inScope)
1690 return (n', shadow n n' sc)
1691 else return (n, sc)
1692 put (n' : env)
1693 ty' <- mkUniq ty; val' <- mkUniq val
1694 sc'' <- mkUniq sc'
1695 return $! PLet n' ty' val' sc''
1696 mkUniq (PApp fc t args)
1697 = do t' <- mkUniq t
1698 args' <- mapM mkUniqA args
1699 return $! PApp fc t' args'
1700 mkUniq (PAppBind fc t args)
1701 = do t' <- mkUniq t
1702 args' <- mapM mkUniqA args
1703 return $! PAppBind fc t' args'
1704 mkUniq (PCase fc t alts)
1705 = do t' <- mkUniq t
1706 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1707 return (x', y')) alts
1708 return $! PCase fc t' alts'
1709 mkUniq (PPair fc l r)
1710 = do l' <- mkUniq l; r' <- mkUniq r
1711 return $! PPair fc l' r'
1712 mkUniq (PDPair fc l t r)
1713 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1714 return $! PDPair fc l' t' r'
1715 mkUniq (PAlternative b as)
1716 = liftM (PAlternative b) (mapM mkUniq as)
1717 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1718 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1719 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1720 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1721 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1722 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1723 mkUniq t = return t