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