git.iko.soy/Idris-dev
on caed480 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1723 lines 71 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
23import Data.List
24import Data.Char
25import qualified Data.Text as T
26import Data.Either
27import Data.Maybe
28import Data.Word (Word)
30import Debug.Trace
32import Control.Monad.Error (throwError, catchError)
33import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
35import Util.Pretty
36import Util.System
38getContext :: Idris Context
39getContext = do i <- getIState; return (tt_ctxt i)
41forCodegen :: Codegen -> [(Codegen, a)] -> [a]
42forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
44getObjectFiles :: Codegen -> Idris [FilePath]
45getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
47addObjectFile :: Codegen -> FilePath -> Idris ()
48addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
50getLibs :: Codegen -> Idris [String]
51getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
53addLib :: Codegen -> String -> Idris ()
54addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
56getFlags :: Codegen -> Idris [String]
57getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
59addFlag :: Codegen -> String -> Idris ()
60addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
62addDyLib :: [String] -> Idris (Either DynamicLib String)
63addDyLib libs = do i <- getIState
64 let ls = idris_dynamic_libs i
65 case mapMaybe (findDyLib ls) libs of
66 x:_ -> return (Left x)
67 [] -> do
68 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
69 case msum handle of
70 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
71 concat (intersperse "," libs) ++ "\"")
72 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
73 return (Left x)
74 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
75 findDyLib [] l = Nothing
76 findDyLib (lib:libs) l | l == lib_name lib = Just lib
77 | otherwise = findDyLib libs l
80addHdr :: Codegen -> String -> Idris ()
81addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
83addLangExt :: LanguageExt -> Idris ()
84addLangExt TypeProviders = do i <- getIState
85 putIState $ i {
86 idris_language_extensions = TypeProviders : idris_language_extensions i
87 }
88addLangExt ErrorReflection = do i <- getIState
89 putIState $ i {
90 idris_language_extensions = ErrorReflection : idris_language_extensions i
91 }
93addTrans :: (Term, Term) -> Idris ()
94addTrans t = do i <- getIState
95 putIState $ i { idris_transforms = t : idris_transforms i }
97totcheck :: (FC, Name) -> Idris ()
98totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
100defer_totcheck :: (FC, Name) -> Idris ()
101defer_totcheck n
102 = do i <- getIState;
103 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
105clear_totcheck :: Idris ()
106clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
108setFlags :: Name -> [FnOpt] -> Idris ()
109setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
111setAccessibility :: Name -> Accessibility -> Idris ()
112setAccessibility n a
113 = do i <- getIState
114 let ctxt = setAccess n a (tt_ctxt i)
115 putIState $ i { tt_ctxt = ctxt }
117setTotality :: Name -> Totality -> Idris ()
118setTotality n a
119 = do i <- getIState
120 let ctxt = setTotal n a (tt_ctxt i)
121 putIState $ i { tt_ctxt = ctxt }
123getTotality :: Name -> Idris Totality
124getTotality n
125 = do i <- getIState
126 case lookupTotal n (tt_ctxt i) of
127 [t] -> return t
128 _ -> return (Total [])
130-- Get coercions which might return the required type
131getCoercionsTo :: IState -> Type -> [Name]
132getCoercionsTo i ty =
133 let cs = idris_coercions i
134 (fn,_) = unApply (getRetTy ty) in
135 findCoercions fn cs
136 where findCoercions t [] = []
137 findCoercions t (n : ns) =
138 let ps = case lookupTy n (tt_ctxt i) of
139 [ty'] -> case unApply (getRetTy ty') of
140 (t', _) ->
141 if t == t' then [n] else []
142 _ -> [] in
143 ps ++ findCoercions t ns
145addToCG :: Name -> CGInfo -> Idris ()
146addToCG n cg
147 = do i <- getIState
148 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
150-- Trace all the names in a call graph starting at the given name
151getAllNames :: Name -> Idris [Name]
152getAllNames n = allNames [] n
154allNames :: [Name] -> Name -> Idris [Name]
155allNames ns n | n `elem` ns = return []
156allNames ns n = do i <- getIState
157 case lookupCtxtExact n (idris_callgraph i) of
158 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
159 return (nub (n : concat more))
160 _ -> return [n]
162addCoercion :: Name -> Idris ()
163addCoercion n = do i <- getIState
164 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
166addDocStr :: Name -> String -> Idris ()
167addDocStr n doc
168 = do i <- getIState
169 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
171addNameHint :: Name -> Name -> Idris ()
172addNameHint ty n
173 = do i <- getIState
174 ty' <- case lookupCtxtName ty (idris_implicits i) of
175 [(tyn, _)] -> return tyn
176 [] -> throwError (NoSuchVariable ty)
177 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
178 let ns' = case lookupCtxt ty' (idris_namehints i) of
179 [ns] -> ns ++ [n]
180 _ -> [n]
181 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
183getNameHints :: IState -> Name -> [Name]
184getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
185getNameHints i n =
186 case lookupCtxt n (idris_namehints i) of
187 [ns] -> ns
188 _ -> []
190addToCalledG :: Name -> [Name] -> Idris ()
191addToCalledG n ns = return () -- TODO
193-- Add a class instance function. Dodgy hack: Put integer instances first in the
194-- list so they are resolved by default.
195-- Dodgy hack 2: put constraint chasers (@@) last
197addInstance :: Bool -> Name -> Name -> Idris ()
198addInstance int n i
199 = do ist <- getIState
200 case lookupCtxt n (idris_classes ist) of
201 [CI a b c d e ins] ->
202 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
203 putIState $ ist { idris_classes = cs }
204 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
205 putIState $ ist { idris_classes = cs }
206 where addI i ins | int = i : ins
207 | chaser n = ins ++ [i]
208 | otherwise = insI i ins
209 insI i [] = [i]
210 insI i (n : ns) | chaser n = i : n : ns
211 | otherwise = n : insI i ns
213 chaser (UN nm)
214 | ('@':'@':_) <- str nm = True
215 chaser (NS n _) = chaser n
216 chaser _ = False
218addClass :: Name -> ClassInfo -> Idris ()
219addClass n i
220 = do ist <- getIState
221 let i' = case lookupCtxt n (idris_classes ist) of
222 [c] -> c { class_instances = class_instances i }
223 _ -> i
224 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
226addIBC :: IBCWrite -> Idris ()
227addIBC ibc@(IBCDef n)
228 = do i <- getIState
229 when (notDef (ibc_write i)) $
230 putIState $ i { ibc_write = ibc : ibc_write i }
231 where notDef [] = True
232 notDef (IBCDef n': is) | n == n' = False
233 notDef (_ : is) = notDef is
234addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
236clearIBC :: Idris ()
237clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
239resetNameIdx :: Idris ()
240resetNameIdx = do i <- getIState
241 put (i { idris_nameIdx = (0, emptyContext) })
243-- Used to preserve sharing of names
244addNameIdx :: Name -> Idris (Int, Name)
245addNameIdx n = do i <- getIState
246 let (i', x) = addNameIdx' i n
247 return x
249addNameIdx' :: IState -> Name -> (IState, (Int, Name))
250addNameIdx' i n
251 = let idxs = snd (idris_nameIdx i) in
252 case lookupCtxt n idxs of
253 [x] -> (i, x)
254 _ -> let i' = fst (idris_nameIdx i) + 1 in
255 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
257getHdrs :: Codegen -> Idris [String]
258getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
260setErrLine :: Int -> Idris ()
261setErrLine x = do i <- getIState;
262 case (errLine i) of
263 Nothing -> putIState $ i { errLine = Just x }
264 Just _ -> return ()
266clearErr :: Idris ()
267clearErr = do i <- getIState
268 putIState $ i { errLine = Nothing }
270getSO :: Idris (Maybe String)
271getSO = do i <- getIState
272 return (compiled_so i)
274setSO :: Maybe String -> Idris ()
275setSO s = do i <- getIState
276 putIState $ (i { compiled_so = s })
278getIState :: Idris IState
279getIState = get
281putIState :: IState -> Idris ()
282putIState = put
284-- | A version of liftIO that puts errors into the exception type of the Idris monad
285runIO :: IO a -> Idris a
286runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
287-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
289getName :: Idris Int
290getName = do i <- getIState;
291 let idx = idris_name i;
292 putIState $ (i { idris_name = idx + 1 })
293 return idx
295addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
296addInternalApp fp l t
297 = do i <- getIState
298 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
300getInternalApp :: FilePath -> Int -> Idris PTerm
301getInternalApp fp l = do i <- getIState
302 case lookup (fp, l) (idris_lineapps i) of
303 Just n' -> return n'
304 Nothing -> return Placeholder
305 -- TODO: What if it's not there?
307-- Pattern definitions are only used for coverage checking, so erase them
308-- when we're done
309clearOrigPats :: Idris ()
310clearOrigPats = do i <- get
311 let ps = idris_patdefs i
312 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
313 put (i { idris_patdefs = ps' })
315-- Erase types from Ps in the context (basically ending up with what's in
316-- the .ibc, which is all we need after all the analysis is done)
317clearPTypes :: Idris ()
318clearPTypes = do i <- get
319 let ctxt = tt_ctxt i
320 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
321 where pErase (CaseOp c t tys orig tot cds)
322 = CaseOp c t tys orig [] (pErase' cds)
323 pErase x = x
324 pErase' (CaseDefs _ (cs, c) _ rs)
325 = let c' = (cs, fmap pEraseType c) in
326 CaseDefs c' c' c' rs
328checkUndefined :: FC -> Name -> Idris ()
329checkUndefined fc n
330 = do i <- getContext
331 case lookupTy n i of
332 (_:_) -> fail $ show fc ++ ":" ++
333 show n ++ " already defined"
334 _ -> return ()
336isUndefined :: FC -> Name -> Idris Bool
337isUndefined fc n
338 = do i <- getContext
339 case lookupTy n i of
340 (_:_) -> return False
341 _ -> return True
343setContext :: Context -> Idris ()
344setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
346updateContext :: (Context -> Context) -> Idris ()
347updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
349addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
350addConstraints fc (v, cs)
351 = do i <- getIState
352 let ctxt = tt_ctxt i
353 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
354 next_tvar = v }
355 let ics = zip cs (repeat fc) ++ idris_constraints i
356 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
358addDeferred = addDeferred' Ref
359addDeferredTyCon = addDeferred' (TCon 0 0)
361addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
362addDeferred' nt ns
363 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
364 i <- getIState
365 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
366 idris_metavars i }
367 where tidyNames used (Bind (MN i x) b sc)
368 = let n' = uniqueName (UN x) used in
369 Bind n' b $ tidyNames (n':used) sc
370 tidyNames used (Bind n b sc)
371 = let n' = uniqueName n used in
372 Bind n' b $ tidyNames (n':used) sc
373 tidyNames used b = b
375solveDeferred :: Name -> Idris ()
376solveDeferred n = do i <- getIState
377 putIState $ i { idris_metavars =
378 filter (\(n', _) -> n/=n')
379 (idris_metavars i) }
381getUndefined :: Idris [Name]
382getUndefined = do i <- getIState
383 return (map fst (idris_metavars i) \\ primDefs)
385ihPrintResult :: Handle -> String -> Idris ()
386ihPrintResult h s = do i <- getIState
387 case idris_outputmode i of
388 RawOutput -> case s of
389 "" -> return ()
390 s -> runIO $ hPutStrLn h s
391 IdeSlave n ->
392 let good = SexpList [SymbolAtom "ok", toSExp s] in
393 runIO $ hPutStrLn h $ convSExp "return" good n
395ihPrintError :: Handle -> String -> Idris ()
396ihPrintError h s = do i <- getIState
397 case idris_outputmode i of
398 RawOutput -> case s of
399 "" -> return ()
400 s -> runIO $ hPutStrLn h s
401 IdeSlave n ->
402 let good = SexpList [SymbolAtom "error", toSExp s] in
403 runIO . hPutStrLn h $ convSExp "return" good n
405ihputStrLn :: Handle -> String -> Idris ()
406ihputStrLn h s = do i <- getIState
407 case idris_outputmode i of
408 RawOutput -> runIO $ hPutStrLn h s
409 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
411iputStrLn = ihputStrLn stdout
412iPrintError = ihPrintError stdout
413iPrintResult = ihPrintResult stdout
414iWarn = ihWarn stdout
416ideslavePutSExp :: SExpable a => String -> a -> Idris ()
417ideslavePutSExp cmd info = do i <- getIState
418 case idris_outputmode i of
419 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
420 _ -> return ()
422-- this needs some typing magic and more structured output towards emacs
423iputGoal :: String -> Idris ()
424iputGoal s = do i <- getIState
425 case idris_outputmode i of
426 RawOutput -> runIO $ putStrLn s
427 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
429isetPrompt :: String -> Idris ()
430isetPrompt p = do i <- getIState
431 case idris_outputmode i of
432 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
434ihWarn :: Handle -> FC -> String -> Idris ()
435ihWarn h fc err = do i <- getIState
436 case idris_outputmode i of
437 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
438 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
440setLogLevel :: Int -> Idris ()
441setLogLevel l = do i <- getIState
442 let opts = idris_options i
443 let opt' = opts { opt_logLevel = l }
444 putIState $ i { idris_options = opt' }
446setCmdLine :: [Opt] -> Idris ()
447setCmdLine opts = do i <- getIState
448 let iopts = idris_options i
449 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
451getCmdLine :: Idris [Opt]
452getCmdLine = do i <- getIState
453 return (opt_cmdline (idris_options i))
455getDumpDefun :: Idris (Maybe FilePath)
456getDumpDefun = do i <- getIState
457 return $ findC (opt_cmdline (idris_options i))
458 where findC [] = Nothing
459 findC (DumpDefun x : _) = Just x
460 findC (_ : xs) = findC xs
462getDumpCases :: Idris (Maybe FilePath)
463getDumpCases = do i <- getIState
464 return $ findC (opt_cmdline (idris_options i))
465 where findC [] = Nothing
466 findC (DumpCases x : _) = Just x
467 findC (_ : xs) = findC xs
469logLevel :: Idris Int
470logLevel = do i <- getIState
471 return (opt_logLevel (idris_options i))
473setErrContext :: Bool -> Idris ()
474setErrContext t = do i <- getIState
475 let opts = idris_options i
476 let opt' = opts { opt_errContext = t }
477 putIState $ i { idris_options = opt' }
479errContext :: Idris Bool
480errContext = do i <- getIState
481 return (opt_errContext (idris_options i))
483useREPL :: Idris Bool
484useREPL = do i <- getIState
485 return (opt_repl (idris_options i))
487setREPL :: Bool -> Idris ()
488setREPL t = do i <- getIState
489 let opts = idris_options i
490 let opt' = opts { opt_repl = t }
491 putIState $ i { idris_options = opt' }
493setNoBanner :: Bool -> Idris ()
494setNoBanner n = do i <- getIState
495 let opts = idris_options i
496 let opt' = opts {opt_nobanner = n}
497 putIState $ i { idris_options = opt' }
499getNoBanner :: Idris Bool
500getNoBanner = do i <- getIState
501 let opts = idris_options i
502 return (opt_nobanner opts)
504setQuiet :: Bool -> Idris ()
505setQuiet q = do i <- getIState
506 let opts = idris_options i
507 let opt' = opts { opt_quiet = q }
508 putIState $ i { idris_options = opt' }
510getQuiet :: Idris Bool
511getQuiet = do i <- getIState
512 let opts = idris_options i
513 return (opt_quiet opts)
515setCodegen :: Codegen -> Idris ()
516setCodegen t = do i <- getIState
517 let opts = idris_options i
518 let opt' = opts { opt_codegen = t }
519 putIState $ i { idris_options = opt' }
521codegen :: Idris Codegen
522codegen = do i <- getIState
523 return (opt_codegen (idris_options i))
525setOutputTy :: OutputType -> Idris ()
526setOutputTy t = do i <- getIState
527 let opts = idris_options i
528 let opt' = opts { opt_outputTy = t }
529 putIState $ i { idris_options = opt' }
531outputTy :: Idris OutputType
532outputTy = do i <- getIState
533 return $ opt_outputTy $ idris_options i
535setIdeSlave :: Bool -> Idris ()
536setIdeSlave True = do i <- getIState
537 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
538setIdeSlave False = return ()
540setTargetTriple :: String -> Idris ()
541setTargetTriple t = do i <- getIState
542 let opts = idris_options i
543 opt' = opts { opt_triple = t }
544 putIState $ i { idris_options = opt' }
546targetTriple :: Idris String
547targetTriple = do i <- getIState
548 return (opt_triple (idris_options i))
550setTargetCPU :: String -> Idris ()
551setTargetCPU t = do i <- getIState
552 let opts = idris_options i
553 opt' = opts { opt_cpu = t }
554 putIState $ i { idris_options = opt' }
556targetCPU :: Idris String
557targetCPU = do i <- getIState
558 return (opt_cpu (idris_options i))
560setOptLevel :: Word -> Idris ()
561setOptLevel t = do i <- getIState
562 let opts = idris_options i
563 opt' = opts { opt_optLevel = t }
564 putIState $ i { idris_options = opt' }
566optLevel :: Idris Word
567optLevel = do i <- getIState
568 return (opt_optLevel (idris_options i))
570verbose :: Idris Bool
571verbose = do i <- getIState
572 return (opt_verbose (idris_options i))
574setVerbose :: Bool -> Idris ()
575setVerbose t = do i <- getIState
576 let opts = idris_options i
577 let opt' = opts { opt_verbose = t }
578 putIState $ i { idris_options = opt' }
580typeInType :: Idris Bool
581typeInType = do i <- getIState
582 return (opt_typeintype (idris_options i))
584setTypeInType :: Bool -> Idris ()
585setTypeInType t = do i <- getIState
586 let opts = idris_options i
587 let opt' = opts { opt_typeintype = t }
588 putIState $ i { idris_options = opt' }
590coverage :: Idris Bool
591coverage = do i <- getIState
592 return (opt_coverage (idris_options i))
594setCoverage :: Bool -> Idris ()
595setCoverage t = do i <- getIState
596 let opts = idris_options i
597 let opt' = opts { opt_coverage = t }
598 putIState $ i { idris_options = opt' }
600setIBCSubDir :: FilePath -> Idris ()
601setIBCSubDir fp = do i <- getIState
602 let opts = idris_options i
603 let opt' = opts { opt_ibcsubdir = fp }
604 putIState $ i { idris_options = opt' }
606valIBCSubDir :: IState -> Idris FilePath
607valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
609addImportDir :: FilePath -> Idris ()
610addImportDir fp = do i <- getIState
611 let opts = idris_options i
612 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
613 putIState $ i { idris_options = opt' }
615setImportDirs :: [FilePath] -> Idris ()
616setImportDirs fps = do i <- getIState
617 let opts = idris_options i
618 let opt' = opts { opt_importdirs = fps }
619 putIState $ i { idris_options = opt' }
621allImportDirs :: Idris [FilePath]
622allImportDirs = do i <- getIState
623 let optdirs = opt_importdirs (idris_options i)
624 return ("." : reverse optdirs)
626colourise :: Idris Bool
627colourise = do i <- getIState
628 return $ idris_colourRepl i
630setColourise :: Bool -> Idris ()
631setColourise b = do i <- getIState
632 putIState $ i { idris_colourRepl = b }
634setOutH :: Handle -> Idris ()
635setOutH h = do i <- getIState
636 putIState $ i { idris_outh = h }
638impShow :: Idris Bool
639impShow = do i <- getIState
640 return (opt_showimp (idris_options i))
642setImpShow :: Bool -> Idris ()
643setImpShow t = do i <- getIState
644 let opts = idris_options i
645 let opt' = opts { opt_showimp = t }
646 putIState $ i { idris_options = opt' }
648setColour :: ColourType -> IdrisColour -> Idris ()
649setColour ct c = do i <- getIState
650 let newTheme = setColour' ct c (idris_colourTheme i)
651 putIState $ i { idris_colourTheme = newTheme }
652 where setColour' KeywordColour c t = t { keywordColour = c }
653 setColour' BoundVarColour c t = t { boundVarColour = c }
654 setColour' ImplicitColour c t = t { implicitColour = c }
655 setColour' FunctionColour c t = t { functionColour = c }
656 setColour' TypeColour c t = t { typeColour = c }
657 setColour' DataColour c t = t { dataColour = c }
658 setColour' PromptColour c t = t { promptColour = c }
660logLvl :: Int -> String -> Idris ()
661logLvl l str = do i <- getIState
662 let lvl = opt_logLevel (idris_options i)
663 when (lvl >= l) $
664 case idris_outputmode i of
665 RawOutput -> do runIO $ putStrLn str
666 IdeSlave n ->
667 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
668 runIO $ putStrLn $ convSExp "log" good n
670cmdOptType :: Opt -> Idris Bool
671cmdOptType x = do i <- getIState
672 return $ x `elem` opt_cmdline (idris_options i)
674iLOG :: String -> Idris ()
675iLOG = logLvl 1
677noErrors :: Idris Bool
678noErrors = do i <- getIState
679 case errLine i of
680 Nothing -> return True
681 _ -> return False
683setTypeCase :: Bool -> Idris ()
684setTypeCase t = do i <- getIState
685 let opts = idris_options i
686 let opt' = opts { opt_typecase = t }
687 putIState $ i { idris_options = opt' }
690-- For inferring types of things
692bi = fileFC "builtin"
694inferTy = sMN 0 "__Infer"
695inferCon = sMN 0 "__infer"
696inferDecl = PDatadecl inferTy
697 PType
698 [("", inferCon, PPi impl (sMN 0 "iType") PType (
699 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
700 (PRef bi inferTy)), bi)]
701inferOpts = []
703infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
704infP = P (TCon 6 0) inferTy (TType (UVal 0))
706getInferTerm, getInferType :: Term -> Term
707getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
708getInferTerm (App (App _ _) tm) = tm
709getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
711getInferType (Bind n b sc) = Bind n b $ getInferType sc
712getInferType (App (App _ ty) _) = ty
714-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
716primNames = [unitTy, unitCon,
717 falseTy, pairTy, pairCon,
718 eqTy, eqCon, inferTy, inferCon]
720unitTy = sMN 0 "__Unit"
721unitCon = sMN 0 "__II"
722unitDecl = PDatadecl unitTy PType
723 [("", unitCon, PRef bi unitTy, bi)]
724unitOpts = [DefaultEliminator]
726falseTy = sMN 0 "__False"
727falseDecl = PDatadecl falseTy PType []
728falseOpts = []
730pairTy = sMN 0 "__Pair"
731pairCon = sMN 0 "__MkPair"
732pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
733 [("", pairCon, PPi impl (n "A") PType (
734 PPi impl (n "B") PType (
735 PPi expl (n "a") (PRef bi (n "A")) (
736 PPi expl (n "b") (PRef bi (n "B"))
737 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
738 pexp (PRef bi (n "B"))])))), bi)]
739 where n a = sMN 0 a
740pairOpts = []
742eqTy = sUN "="
743eqCon = sUN "refl"
744eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
745 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
746 PType)
747 [("", eqCon, PPi impl (n "A") PType (
748 PPi impl (n "x") (PRef bi (n "A"))
749 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
750 pimp (n "B") Placeholder False,
751 pexp (PRef bi (n "x")),
752 pexp (PRef bi (n "x"))])), bi)]
753 where n a = sMN 0 a
754eqOpts = []
756elimName = sUN "__Elim"
757elimMethElimTy = sUN "__elimTy"
758elimMethElim = sUN "elim"
759elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
760 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
761 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
763-- Defined in builtins.idr
764sigmaTy = sUN "Exists"
765existsCon = sUN "Ex_intro"
767piBind :: [(Name, PTerm)] -> PTerm -> PTerm
768piBind = piBindp expl
770piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
771piBindp p [] t = t
772piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
774-- Dealing with parameters
776expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
777 [Name] -> -- all names
778 [Name] -> -- names with no declaration
779 PTerm -> PTerm
780expandParams dec ps ns infs tm = en tm
781 where
782 -- if we shadow a name (say in a lambda binding) that is used in a call to
783 -- a lifted function, we need access to both names - once in the scope of the
784 -- binding and once to call the lifted functions. So we'll explicitly shadow
785 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
786 -- but we didn't...)
788 mkShadow (UN n) = MN 0 n
789 mkShadow (MN i n) = MN (i+1) n
790 mkShadow (NS x s) = NS (mkShadow x) s
792 en (PLam n t s)
793 | n `elem` (map fst ps ++ ns)
794 = let n' = mkShadow n in
795 PLam n' (en t) (en (shadow n n' s))
796 | otherwise = PLam n (en t) (en s)
797 en (PPi p n t s)
798 | n `elem` (map fst ps ++ ns)
799 = let n' = mkShadow n in
800 PPi p n' (en t) (en (shadow n n' s))
801 | otherwise = PPi p n (en t) (en s)
802 en (PLet n ty v s)
803 | n `elem` (map fst ps ++ ns)
804 = let n' = mkShadow n in
805 PLet n' (en ty) (en v) (en (shadow n n' s))
806 | otherwise = PLet n (en ty) (en v) (en s)
807 -- FIXME: Should only do this in a type signature!
808 en (PDPair f (PRef f' n) t r)
809 | n `elem` (map fst ps ++ ns) && t /= Placeholder
810 = let n' = mkShadow n in
811 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
812 en (PEq f l r) = PEq f (en l) (en r)
813 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
814 en (PTyped l r) = PTyped (en l) (en r)
815 en (PPair f l r) = PPair f (en l) (en r)
816 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
817 en (PAlternative a as) = PAlternative a (map en as)
818 en (PHidden t) = PHidden (en t)
819 en (PUnifyLog t) = PUnifyLog (en t)
820 en (PNoImplicits t) = PNoImplicits (en t)
821 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
822 en (PProof ts) = PProof (map (fmap en) ts)
823 en (PTactics ts) = PTactics (map (fmap en) ts)
825 en (PQuote (Var n))
826 | n `nselem` ns = PQuote (Var (dec n))
827 en (PApp fc (PInferRef fc' n) as)
828 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
829 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
830 en (PApp fc (PRef fc' n) as)
831 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
832 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
833 | n `nselem` ns = PApp fc (PRef fc' (dec n))
834 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
835 en (PAppBind fc (PRef fc' n) as)
836 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
837 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
838 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
839 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
840 en (PRef fc n)
841 | n `elem` infs = PApp fc (PInferRef fc (dec n))
842 (map (pexp . (PRef fc)) (map fst ps))
843 | n `nselem` ns = PApp fc (PRef fc (dec n))
844 (map (pexp . (PRef fc)) (map fst ps))
845 en (PInferRef fc n)
846 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
847 (map (pexp . (PRef fc)) (map fst ps))
848 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
849 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
850 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
851 en t = t
853 nselem x [] = False
854 nselem x (y : xs) | nseq x y = True
855 | otherwise = nselem x xs
857 nseq x y = nsroot x == nsroot y
859expandParamsD :: Bool -> -- True = RHS only
860 IState ->
861 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
862expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
863 = if n `elem` ns && (not rhsonly)
864 then -- trace (show (n, expandParams dec ps ns ty)) $
865 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
866 else --trace (show (n, expandParams dec ps ns ty)) $
867 PTy doc syn fc o n (expandParams dec ps ns [] ty)
868expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
869 = if n `elem` ns && (not rhsonly)
870 then -- trace (show (n, expandParams dec ps ns ty)) $
871 PPostulate doc syn fc o (dec n) (piBind ps
872 (expandParams dec ps ns [] ty))
873 else --trace (show (n, expandParams dec ps ns ty)) $
874 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
875expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
876 = let n' = if n `elem` ns then dec n else n in
877 PClauses fc opts n' (map expandParamsC cs)
878 where
879 expandParamsC (PClause fc n lhs ws rhs ds)
880 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
881 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
882 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
883 n' = if n `elem` ns then dec n else n
884 -- names bound on the lhs should not be expanded on the rhs
885 ns' = removeBound lhs ns in
886 PClause fc n' lhs'
887 (map (expandParams dec ps'' ns' []) ws)
888 (expandParams dec ps'' ns' [] rhs)
889 (map (expandParamsD True ist dec ps'' ns') ds)
890 expandParamsC (PWith fc n lhs ws wval ds)
891 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
892 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
893 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
894 n' = if n `elem` ns then dec n else n
895 ns' = removeBound lhs ns in
896 PWith fc n' lhs'
897 (map (expandParams dec ps'' ns' []) ws)
898 (expandParams dec ps'' ns' [] wval)
899 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
900 updateps yn nm [] = []
901 updateps yn nm (((a, t), i):as)
902 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
903 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
905 removeBound lhs ns = ns \\ nub (bnames lhs)
907 bnames (PRef _ n) = [n]
908 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
909 bnames (PPair _ l r) = bnames l ++ bnames r
910 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
911 bnames _ = []
913expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
914 = PData doc syn fc co (expandPData pd)
915 where
916 -- just do the type decl, leave constructors alone (parameters will be
917 -- added implicitly)
918 expandPData (PDatadecl n ty cons)
919 = if n `elem` ns
920 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
921 (map econ cons)
922 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
923 econ (doc, n, t, fc)
924 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
925expandParamsD rhs ist dec ps ns (PParams f params pds)
926 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
927 (map (expandParamsD True ist dec ps ns) pds)
928-- (map (expandParamsD ist dec ps ns) pds)
929expandParamsD rhs ist dec ps ns (PMutual f pds)
930 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
931expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
932 = PClass doc info f
933 (map (expandParams dec ps ns []) cs)
934 n
935 (map (mapsnd (expandParams dec ps ns [])) params)
936 (map (expandParamsD rhs ist dec ps ns) decls)
937expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
938 = PInstance info f
939 (map (expandParams dec ps ns []) cs)
940 n
941 (map (expandParams dec ps ns []) params)
942 (expandParams dec ps ns [] ty)
943 cn
944 (map (expandParamsD rhs ist dec ps ns) decls)
945expandParamsD rhs ist dec ps ns d = d
947mapsnd f (x, t) = (x, f t)
949-- Calculate a priority for a type, for deciding elaboration order
950-- * if it's just a type variable or concrete type, do it early (0)
951-- * if there's only type variables and injective constructors, do it next (1)
952-- * if there's a function type, next (2)
953-- * finally, everything else (3)
955getPriority :: IState -> PTerm -> Int
956getPriority i tm = 1 -- pri tm
957 where
958 pri (PRef _ n) =
959 case lookupP n (tt_ctxt i) of
960 ((P (DCon _ _) _ _):_) -> 1
961 ((P (TCon _ _) _ _):_) -> 1
962 ((P Ref _ _):_) -> 1
963 [] -> 0 -- must be locally bound, if it's not an error...
964 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
965 pri (PTrue _) = 0
966 pri (PFalse _) = 0
967 pri (PRefl _ _) = 1
968 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
969 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
970 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
971 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
972 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
973 pri (PTyped l r) = pri l
974 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
975 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
976 pri (PAlternative a as) = maximum (map pri as)
977 pri (PConstant _) = 0
978 pri Placeholder = 1
979 pri _ = 3
981addStatics :: Name -> Term -> PTerm -> Idris ()
982addStatics n tm ptm =
983 do let (statics, dynamics) = initStatics tm ptm
984 let stnames = nub $ concatMap freeArgNames (map snd statics)
985 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
986 -- also get the arguments which are 'uniquely inferrable' from
987 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
988 let statics' = nub $ map fst statics ++
989 filter (\x -> not (elem x dnames)) stnames
990 let stpos = staticList statics' tm
991 i <- getIState
992 when (not (null statics)) $
993 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
994 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
995 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
996 addIBC (IBCStatic n)
997 where
998 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
999 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1000 if pstatic p == Static then ((n, ty) : static, dynamic)
1001 else if (not (searchArg p))
1002 then (static, (n, ty) : dynamic)
1003 else (static, dynamic)
1004 initStatics t pt = ([], [])
1006 freeArgNames (Bind n (Pi ty) sc)
1007 = nub $ freeArgNames ty
1008 freeArgNames tm = let (_, args) = unApply tm in
1009 concatMap freeNames args
1011 -- if a name appears in a type class or tactic implicit index, it doesn't
1012 -- affect its 'uniquely inferrable' from a static status since these are
1013 -- resolved by searching.
1014 searchArg (Constraint _ _ _) = True
1015 searchArg (TacImp _ _ _ _) = True
1016 searchArg _ = False
1018 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1019 staticList _ _ = []
1021-- Dealing with implicit arguments
1023-- Add constraint bindings from using block
1025addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1026addUsingConstraints syn fc t
1027 = do ist <- get
1028 let ns = namesIn [] ist t
1029 let cs = getConstraints t -- check declared constraints
1030 let addconsts = uconsts \\ cs
1031 -- if all names in the arguments of addconsts appear in ns,
1032 -- add the constraint implicitly
1033 return (doAdd addconsts ns t)
1034 where uconsts = filter uconst (using syn)
1035 uconst (UConstraint _ _) = True
1036 uconst _ = False
1038 doAdd [] _ t = t
1039 -- if all of args in ns, then add it
1040 doAdd (UConstraint c args : cs) ns t
1041 | all (\n -> elem n ns) args
1042 = PPi (Constraint False Dynamic "") (sMN 0 "cu")
1043 (mkConst c args) (doAdd cs ns t)
1044 | otherwise = doAdd cs ns t
1046 mkConst c args = PApp fc (PRef fc c)
1047 (map (\n -> PExp 0 False (PRef fc n) "") args)
1049 getConstraints (PPi (Constraint _ _ _) _ c sc)
1050 = getcapp c ++ getConstraints sc
1051 getConstraints (PPi _ _ c sc) = getConstraints sc
1052 getConstraints _ = []
1054 getcapp (PApp _ (PRef _ c) args)
1055 = do ns <- mapM getName args
1056 return (UConstraint c ns)
1057 getcapp _ = []
1059 getName (PExp _ _ (PRef _ n) _) = return n
1060 getName _ = []
1062-- Add implicit Pi bindings for any names in the term which appear in an
1063-- argument position.
1065-- This has become a right mess already. Better redo it some time...
1067implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1068implicit syn n ptm = implicit' syn [] n ptm
1070implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1071implicit' syn ignore n ptm
1072 = do i <- getIState
1073 let (tm', impdata) = implicitise syn ignore i ptm
1074-- let (tm'', spos) = findStatics i tm'
1075 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1076 addIBC (IBCImp n)
1077 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1078-- i <- get
1079-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1080 return tm'
1082implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1083implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1084 let (declimps, ns') = execState (imps True [] tm) ([], [])
1085 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1086 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1087 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1088 if null ns
1089 then (tm, reverse declimps)
1090 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1091 where
1092 uvars = map ipair (filter uimplicit (using syn))
1093 pvars = syn_params syn
1095 inUsing n = n `elem` map fst uvars
1097 ipair (UImplicit x y) = (x, y)
1098 uimplicit (UImplicit _ _) = True
1099 uimplicit _ = False
1101 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1102 | otherwise = x : dropAll xs ys
1103 dropAll [] ys = []
1105 imps top env (PApp _ f as)
1106 = do (decls, ns) <- get
1107 let isn = concatMap (namesIn uvars ist) (map getTm as)
1108 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1109 imps top env (PPi (Imp l _ doc _) n ty sc)
1110 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1111 (decls , ns) <- get
1112 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1113 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1114 imps True (n:env) sc
1115 imps top env (PPi (Exp l _ doc _) n ty sc)
1116 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1117 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1118 _ -> [])
1119 (decls, ns) <- get -- ignore decls in HO types
1120 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1121 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1122 imps True (n:env) sc
1123 imps top env (PPi (Constraint l _ doc) n ty sc)
1124 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1125 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1126 _ -> [])
1127 (decls, ns) <- get -- ignore decls in HO types
1128 put (PConstraint 10 l Placeholder doc : decls,
1129 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1130 imps True (n:env) sc
1131 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1132 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1133 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1134 _ -> [])
1135 (decls, ns) <- get -- ignore decls in HO types
1136 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1137 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1138 imps True (n:env) sc
1139 imps top env (PEq _ l r)
1140 = do (decls, ns) <- get
1141 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1142 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1143 imps top env (PRewrite _ l r _)
1144 = do (decls, ns) <- get
1145 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1146 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1147 imps top env (PTyped l r)
1148 = imps top env l
1149 imps top env (PPair _ l r)
1150 = do (decls, ns) <- get
1151 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1152 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1153 imps top env (PDPair _ (PRef _ n) t r)
1154 = do (decls, ns) <- get
1155 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1156 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1157 imps top env (PDPair _ l t r)
1158 = do (decls, ns) <- get
1159 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1160 namesIn uvars ist r
1161 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1162 imps top env (PAlternative a as)
1163 = do (decls, ns) <- get
1164 let isn = concatMap (namesIn uvars ist) as
1165 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1166 imps top env (PLam n ty sc)
1167 = do imps False env ty
1168 imps False (n:env) sc
1169 imps top env (PHidden tm) = imps False env tm
1170 imps top env (PUnifyLog tm) = imps False env tm
1171 imps top env (PNoImplicits tm) = imps False env tm
1172 imps top env _ = return ()
1174 pibind using [] sc = sc
1175 pibind using (n:ns) sc
1176 = case lookup n using of
1177 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1178 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1179 (pibind using ns sc)
1181-- Add implicit arguments in function calls
1182addImplPat :: IState -> PTerm -> PTerm
1183addImplPat = addImpl' True [] []
1185addImplBound :: IState -> [Name] -> PTerm -> PTerm
1186addImplBound ist ns = addImpl' False ns [] ist
1188addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1189addImplBoundInf ist ns inf = addImpl' False ns inf ist
1191addImpl :: IState -> PTerm -> PTerm
1192addImpl = addImpl' False [] []
1194-- TODO: in patterns, don't add implicits to function names guarded by constructors
1195-- and *not* inside a PHidden
1197addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1198addImpl' inpat env infns ist ptm
1199 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1200 where
1201 ai env ds (PRef fc f)
1202 | f `elem` infns = PInferRef fc f
1203 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1204 ai env ds (PHidden (PRef fc f))
1205 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1206 ai env ds (PEq fc l r)
1207 = let l' = ai env ds l
1208 r' = ai env ds r in
1209 PEq fc l' r'
1210 ai env ds (PRewrite fc l r g)
1211 = let l' = ai env ds l
1212 r' = ai env ds r
1213 g' = fmap (ai env ds) g in
1214 PRewrite fc l' r' g'
1215 ai env ds (PTyped l r)
1216 = let l' = ai env ds l
1217 r' = ai env ds r in
1218 PTyped l' r'
1219 ai env ds (PPair fc l r)
1220 = let l' = ai env ds l
1221 r' = ai env ds r in
1222 PPair fc l' r'
1223 ai env ds (PDPair fc l t r)
1224 = let l' = ai env ds l
1225 t' = ai env ds t
1226 r' = ai env ds r in
1227 PDPair fc l' t' r'
1228 ai env ds (PAlternative a as)
1229 = let as' = map (ai env ds) as in
1230 PAlternative a as'
1231 ai env _ (PDisamb ds' as) = ai env ds' as
1232 ai env ds (PApp fc (PInferRef _ f) as)
1233 = let as' = map (fmap (ai env ds)) as in
1234 PApp fc (PInferRef fc f) as'
1235 ai env ds (PApp fc ftm@(PRef _ f) as)
1236 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1237 | not (f `elem` map fst env)
1238 = let as' = map (fmap (ai env ds)) as in
1239 handleErr $ aiFn inpat False ist fc f ds as'
1240 | Just (Just ty) <- lookup f env =
1241 let as' = map (fmap (ai env ds)) as
1242 arity = getPArity ty in
1243 mkPApp fc arity ftm as'
1244 ai env ds (PApp fc f as)
1245 = let f' = ai env ds f
1246 as' = map (fmap (ai env ds)) as in
1247 mkPApp fc 1 f' as'
1248 ai env ds (PCase fc c os)
1249 = let c' = ai env ds c
1250 os' = map (pmap (ai env ds)) os in
1251 PCase fc c' os'
1252 ai env ds (PLam n ty sc)
1253 = let ty' = ai env ds ty
1254 sc' = ai ((n, Just ty):env) ds sc in
1255 PLam n ty' sc'
1256 ai env ds (PLet n ty val sc)
1257 = let ty' = ai env ds ty
1258 val' = ai env ds val
1259 sc' = ai ((n, Just ty):env) ds sc in
1260 PLet n ty' val' sc'
1261 ai env ds (PPi p n ty sc)
1262 = let ty' = ai env ds ty
1263 sc' = ai ((n, Just ty):env) ds sc in
1264 PPi p n ty' sc'
1265 ai env ds (PGoal fc r n sc)
1266 = let r' = ai env ds r
1267 sc' = ai ((n, Nothing):env) ds sc in
1268 PGoal fc r' n sc'
1269 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1270 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1271 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1272 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1273 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1274 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1275 ai env ds tm = tm
1277 handleErr (Left err) = PElabError err
1278 handleErr (Right x) = x
1280-- if in a pattern, and there are no arguments, and there's no possible
1281-- names with zero explicit arguments, don't add implicits.
1283aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1284aiFn inpat True ist fc f ds []
1285 = case lookupDef f (tt_ctxt ist) of
1286 [] -> Right $ PPatvar fc f
1287 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1288 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1289 if (not (vname f) || tcname f
1290 || any (conCaf (tt_ctxt ist)) ialts)
1291-- any constructor alts || any allImp ialts))
1292 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1293 else Right $ PPatvar fc f
1294 where imp (PExp _ _ _ _) = False
1295 imp _ = True
1296-- allImp [] = False
1297 allImp xs = all imp xs
1298 constructor (TyDecl (DCon _ _) _) = True
1299 constructor _ = False
1301 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1303 vname (UN n) = True -- non qualified
1304 vname _ = False
1306aiFn inpat expat ist fc f ds as
1307 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1308aiFn inpat expat ist fc f ds as
1309 -- This is where namespaces get resolved by adding PAlternative
1310 = do let ns = lookupCtxtName f (idris_implicits ist)
1311 let nh = filter (\(n, _) -> notHidden n) ns
1312 let ns' = case trimAlts ds nh of
1313 [] -> nh
1314 x -> x
1315 case ns' of
1316 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1317 [] -> if f `elem` (map fst (idris_metavars ist))
1318 then Right $ PApp fc (PRef fc f) as
1319 else Right $ mkPApp fc (length as) (PRef fc f) as
1320 alts -> Right $
1321 PAlternative True $
1322 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1323 (insertImpl ns as)) alts
1324 where
1325 trimAlts [] alts = alts
1326 trimAlts ns alts
1327 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1329 nspace (NS _ s) = s
1330 nspace _ = []
1332 notHidden n = case getAccessibility n of
1333 Hidden -> False
1334 _ -> True
1336 getAccessibility n
1337 = case lookupDefAcc n False (tt_ctxt ist) of
1338 [(n,t)] -> t
1339 _ -> Public
1342 insertImpl :: [PArg] -> [PArg] -> [PArg]
1343 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1344 PExp p l tm d : insertImpl ps given
1345 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1346 PConstraint p l tm d : insertImpl ps given
1347 insertImpl (PConstraint p l ty d : ps) given =
1348 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1349 insertImpl (PImp p _ l n ty d : ps) given =
1350 case find n given [] of
1351 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1352 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1353 insertImpl (PTacImplicit p l n sc' ty d : ps) given =
1354 let sc = addImpl ist sc' in
1355 case find n given [] of
1356 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1357 Nothing -> if inpat
1358 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1359 else PTacImplicit p l n sc sc "" : insertImpl ps given
1360 insertImpl expected [] = []
1361 insertImpl _ given = given
1363 find n [] acc = Nothing
1364 find n (PImp _ _ _ n' t _ : gs) acc
1365 | n == n' = Just (t, reverse acc ++ gs)
1366 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1367 | n == n' = Just (t, reverse acc ++ gs)
1368 find n (g : gs) acc = find n gs (g : acc)
1370-- replace non-linear occurrences with _
1371-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1372-- it is hard to get right!
1374stripLinear :: IState -> PTerm -> PTerm
1375stripLinear i tm = evalState (sl tm) [] where
1376 sl :: PTerm -> State [Name] PTerm
1377 sl (PRef fc f)
1378 | (_:_) <- lookupTy f (tt_ctxt i)
1379 = return $ PRef fc f
1380 | otherwise = do ns <- get
1381 if (f `elem` ns)
1382 then return Placeholder
1383 else do put (f : ns)
1384 return (PRef fc f)
1385 sl (PPatvar fc f)
1386 = do ns <- get
1387 if (f `elem` ns)
1388 then return Placeholder
1389 else do put (f : ns)
1390 return (PPatvar fc f)
1391 sl (PApp fc fn args) = do fn' <- sl fn
1392 args' <- mapM slA args
1393 return $ PApp fc fn' args'
1394 where slA (PImp p m l n t d) = do t' <- sl t
1395 return $ PImp p m l n t' d
1396 slA (PExp p l t d) = do t' <- sl t
1397 return $ PExp p l t' d
1398 slA (PConstraint p l t d)
1399 = do t' <- sl t
1400 return $ PConstraint p l t' d
1401 slA (PTacImplicit p l n sc t d)
1402 = do t' <- sl t
1403 return $ PTacImplicit p l n sc t' d
1404 sl x = return x
1406-- Remove functions which aren't applied to anything, which must then
1407-- be resolved by unification. Assume names resolved and alternatives
1408-- filled in (so no ambiguity).
1410stripUnmatchable :: IState -> PTerm -> PTerm
1411stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1412 su :: PTerm -> PTerm
1413 su (PRef fc f)
1414 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1415 = Placeholder
1416 su (PApp fc fn args)
1417 = PApp fc fn (fmap (fmap su) args)
1418 su (PAlternative b alts)
1419 = let alts' = filter (/= Placeholder) (map su alts) in
1420 if null alts' then Placeholder
1421 else PAlternative b alts'
1422 su (PPair fc l r) = PPair fc (su l) (su r)
1423 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1424 su t = t
1425stripUnmatchable i tm = tm
1427mkPApp fc a f [] = f
1428mkPApp fc a f as = let rest = drop a as in
1429 appRest fc (PApp fc f (take a as)) rest
1430 where
1431 appRest fc f [] = f
1432 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1434-- Find 'static' argument positions
1435-- (the declared ones, plus any names in argument position in the declared
1436-- statics)
1437-- FIXME: It's possible that this really has to happen after elaboration
1439findStatics :: IState -> PTerm -> (PTerm, [Bool])
1440findStatics ist tm = trace (showImp Nothing True False tm) $
1441 let (ns, ss) = fs tm in
1442 runState (pos ns ss tm) []
1443 where fs (PPi p n t sc)
1444 | Static <- pstatic p
1445 = let (ns, ss) = fs sc in
1446 (namesIn [] ist t : ns, n : ss)
1447 | otherwise = let (ns, ss) = fs sc in
1448 (ns, ss)
1449 fs _ = ([], [])
1451 inOne n ns = length (filter id (map (elem n) ns)) == 1
1453 pos ns ss (PPi p n t sc)
1454 | elem n ss = do sc' <- pos ns ss sc
1455 spos <- get
1456 put (True : spos)
1457 return (PPi (p { pstatic = Static }) n t sc')
1458 | otherwise = do sc' <- pos ns ss sc
1459 spos <- get
1460 put (False : spos)
1461 return (PPi p n t sc')
1462 pos ns ss t = return t
1464-- for 6.12/7 compatibility
1465data EitherErr a b = LeftErr a | RightOK b
1467instance Monad (EitherErr a) where
1468 return = RightOK
1470 (LeftErr e) >>= k = LeftErr e
1471 RightOK v >>= k = k v
1473toEither (LeftErr e) = Left e
1474toEither (RightOK ho) = Right ho
1476-- syntactic match of a against b, returning pair of variables in a
1477-- and what they match. Returns the pair that failed if not a match.
1479matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1480matchClause = matchClause' False
1482matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1483matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1484 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1486 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1487 fullApp x = x
1489 match' x y = match (fullApp x) (fullApp y)
1490 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1491 | fi == txt "fromInteger" && b == txt "builtins",
1492 PConstant (I _) <- getTm x = match (getTm x) x'
1493 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1494 | fi == txt "fromInteger" && b == txt "builtins",
1495 PConstant (I _) <- getTm x = match (getTm x) x'
1496 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1497 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1498 match (PApp _ f args) (PApp _ f' args')
1499 | length args == length args'
1500 = do mf <- match' f f'
1501 ms <- zipWithM matchArg args args'
1502 return (mf ++ concat ms)
1503-- match (PRef _ n) (PRef _ n') | n == n' = return []
1504-- | otherwise = Nothing
1505 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1506 match (PPatvar f n) xr = match (PRef f n) xr
1507 match xr (PPatvar f n) = match xr (PRef f n)
1508 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1509 match (PRef _ n) tm@(PRef _ n')
1510 | n == n' && not names &&
1511 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1512 || tm == Placeholder)
1513 = return [(n, tm)]
1514 | n == n' = return []
1515 match (PRef _ n) tm
1516 | not names && (not (isConName n (tt_ctxt i) ||
1517 isFnName n (tt_ctxt i)) || tm == Placeholder)
1518 = return [(n, tm)]
1519 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1520 mr <- match' r r'
1521 return (ml ++ mr)
1522 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1523 = do ml <- match' l l'
1524 mr <- match' r r'
1525 return (ml ++ mr)
1526 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1527 mr <- match r r'
1528 return (ml ++ mr)
1529 match (PTyped l r) x = match l x
1530 match x (PTyped l r) = match x l
1531 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1532 mr <- match' r r'
1533 return (ml ++ mr)
1534 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1535 mt <- match' t t'
1536 mr <- match' r r'
1537 return (ml ++ mt ++ mr)
1538 match (PAlternative a as) (PAlternative a' as')
1539 = do ms <- zipWithM match' as as'
1540 return (concat ms)
1541 match a@(PAlternative _ as) b
1542 = do let ms = zipWith match' as (repeat b)
1543 case (rights (map toEither ms)) of
1544 (x: _) -> return x
1545 _ -> LeftErr (a, b)
1546 match (PCase _ _ _) _ = return [] -- lifted out
1547 match (PMetavar _) _ = return [] -- modified
1548 match (PInferRef _ _) _ = return [] -- modified
1549 match (PQuote _) _ = return []
1550 match (PProof _) _ = return []
1551 match (PTactics _) _ = return []
1552 match (PRefl _ _) (PRefl _ _) = return []
1553 match (PResolveTC _) (PResolveTC _) = return []
1554 match (PTrue _) (PTrue _) = return []
1555 match (PFalse _) (PFalse _) = return []
1556 match (PReturn _) (PReturn _) = return []
1557 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1558 ms <- match' s s'
1559 return (mt ++ ms)
1560 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1561 ms <- match' s s'
1562 return (mt ++ ms)
1563 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1564 mty <- match' ty ty'
1565 ms <- match' s s'
1566 return (mt ++ mty ++ ms)
1567 match (PHidden x) (PHidden y) = match' x y
1568 match (PUnifyLog x) y = match' x y
1569 match x (PUnifyLog y) = match' x y
1570 match (PNoImplicits x) y = match' x y
1571 match x (PNoImplicits y) = match' x y
1572 match Placeholder _ = return []
1573 match _ Placeholder = return []
1574 match (PResolveTC _) _ = return []
1575 match a b | a == b = return []
1576 | otherwise = LeftErr (a, b)
1578 checkRpts (RightOK ms) = check ms where
1579 check ((n,t):xs)
1580 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1581 then Left (t, t')
1582 else check xs
1583 check (_:xs) = check xs
1584 check [] = Right ms
1585 checkRpts (LeftErr x) = Left x
1587substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1588substMatches ms = substMatchesShadow ms []
1590substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1591substMatchesShadow [] shs t = t
1592substMatchesShadow ((n,tm):ns) shs t
1593 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1595substMatch :: Name -> PTerm -> PTerm -> PTerm
1596substMatch n = substMatchShadow n []
1598substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1599substMatchShadow n shs tm t = sm shs t where
1600 sm xs (PRef _ n') | n == n' = tm
1601 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1602 sm xs (PPi p x t sc)
1603 | x `elem` xs
1604 = let x' = nextName x in
1605 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1606 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1607 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1608 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1609 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1610 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1611 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1612 (fmap (sm xs) tm)
1613 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1614 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1615 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1616 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1617 sm xs (PHidden x) = PHidden (sm xs x)
1618 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1619 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1620 sm xs x = x
1622 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1623 fullApp x = x
1625shadow :: Name -> Name -> PTerm -> PTerm
1626shadow n n' t = sm t where
1627 sm (PRef fc x) | n == x = PRef fc n'
1628 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1629 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1630 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1631 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1632 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1633 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1634 sm (PEq f x y) = PEq f (sm x) (sm y)
1635 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1636 sm (PTyped x y) = PTyped (sm x) (sm y)
1637 sm (PPair f x y) = PPair f (sm x) (sm y)
1638 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1639 sm (PAlternative a as) = PAlternative a (map sm as)
1640 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1641 sm (PProof ts) = PProof (map (fmap sm) ts)
1642 sm (PHidden x) = PHidden (sm x)
1643 sm (PUnifyLog x) = PUnifyLog (sm x)
1644 sm (PNoImplicits x) = PNoImplicits (sm x)
1645 sm x = x
1647-- Rename any binders which are repeated (so that we don't have to mess
1648-- about with shadowing anywhere else).
1650mkUniqueNames :: [Name] -> PTerm -> PTerm
1651mkUniqueNames env tm = evalState (mkUniq tm) env where
1652 inScope = boundNamesIn tm
1654 mkUniqA arg = do t' <- mkUniq (getTm arg)
1655 return (arg { getTm = t' })
1657 -- FIXME: Probably ought to do this for completeness! It's fine as
1658 -- long as there are no bindings inside tactics though.
1659 mkUniqT tac = return tac
1661 mkUniq :: PTerm -> State [Name] PTerm
1662 mkUniq (PLam n ty sc)
1663 = do env <- get
1664 (n', sc') <-
1665 if n `elem` env
1666 then do let n' = uniqueName n (env ++ inScope)
1667 return (n', shadow n n' sc)
1668 else return (n, sc)
1669 put (n' : env)
1670 ty' <- mkUniq ty
1671 sc'' <- mkUniq sc'
1672 return $! PLam n' ty' sc''
1673 mkUniq (PPi p n ty sc)
1674 = do env <- get
1675 (n', sc') <-
1676 if n `elem` env
1677 then do let n' = uniqueName n (env ++ inScope)
1678 return (n', shadow n n' sc)
1679 else return (n, sc)
1680 put (n' : env)
1681 ty' <- mkUniq ty
1682 sc'' <- mkUniq sc'
1683 return $! PPi p n' ty' sc''
1684 mkUniq (PLet n ty val sc)
1685 = do env <- get
1686 (n', sc') <-
1687 if n `elem` env
1688 then do let n' = uniqueName n (env ++ inScope)
1689 return (n', shadow n n' sc)
1690 else return (n, sc)
1691 put (n' : env)
1692 ty' <- mkUniq ty; val' <- mkUniq val
1693 sc'' <- mkUniq sc'
1694 return $! PLet n' ty' val' sc''
1695 mkUniq (PApp fc t args)
1696 = do t' <- mkUniq t
1697 args' <- mapM mkUniqA args
1698 return $! PApp fc t' args'
1699 mkUniq (PAppBind fc t args)
1700 = do t' <- mkUniq t
1701 args' <- mapM mkUniqA args
1702 return $! PAppBind fc t' args'
1703 mkUniq (PCase fc t alts)
1704 = do t' <- mkUniq t
1705 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1706 return (x', y')) alts
1707 return $! PCase fc t' alts'
1708 mkUniq (PPair fc l r)
1709 = do l' <- mkUniq l; r' <- mkUniq r
1710 return $! PPair fc l' r'
1711 mkUniq (PDPair fc l t r)
1712 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1713 return $! PDPair fc l' t' r'
1714 mkUniq (PAlternative b as)
1715 = liftM (PAlternative b) (mapM mkUniq as)
1716 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1717 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1718 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1719 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1720 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1721 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1722 mkUniq t = return t