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