git.iko.soy/Idris-dev
on 3d59246 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1768 lines 73 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.Docstrings
13import Idris.IdeSlave hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.State
23import Control.Monad.Error(throwError)
25import Data.List
26import Data.Char
27import qualified Data.Text as T
28import Data.Either
29import qualified Data.Map as M
30import Data.Maybe
31import qualified Data.Set as S
32import Data.Word (Word)
34import Debug.Trace
36import Control.Monad.Error (throwError, catchError)
37import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
39import Util.Pretty
40import Util.ScreenSize
41import Util.System
43getContext :: Idris Context
44getContext = do i <- getIState; return (tt_ctxt i)
46forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
49getObjectFiles :: Codegen -> Idris [FilePath]
50getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
52addObjectFile :: Codegen -> FilePath -> Idris ()
53addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
55getLibs :: Codegen -> Idris [String]
56getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
58addLib :: Codegen -> String -> Idris ()
59addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
61getFlags :: Codegen -> Idris [String]
62getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
64addFlag :: Codegen -> String -> Idris ()
65addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
67addDyLib :: [String] -> Idris (Either DynamicLib String)
68addDyLib libs = do i <- getIState
69 let ls = idris_dynamic_libs i
70 let importdirs = opt_importdirs (idris_options i)
71 case mapMaybe (findDyLib ls) libs of
72 x:_ -> return (Left x)
73 [] -> do
74 handle <- lift . lift .
75 mapM (\l -> catchIO (tryLoadLib importdirs l)
76 (\_ -> return Nothing)) $ libs
77 case msum handle of
78 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
79 concat (intersperse "," libs) ++ "\"")
80 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
81 return (Left x)
82 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
83 findDyLib [] l = Nothing
84 findDyLib (lib:libs) l | l == lib_name lib = Just lib
85 | otherwise = findDyLib libs l
88addHdr :: Codegen -> String -> Idris ()
89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
91addLangExt :: LanguageExt -> Idris ()
92addLangExt TypeProviders = do i <- getIState
93 putIState $ i {
94 idris_language_extensions = TypeProviders : idris_language_extensions i
95 }
96addLangExt ErrorReflection = do i <- getIState
97 putIState $ i {
98 idris_language_extensions = ErrorReflection : idris_language_extensions i
99 }
101addTrans :: (Term, Term) -> Idris ()
102addTrans t = do i <- getIState
103 putIState $ i { idris_transforms = t : idris_transforms i }
105addErrRev :: (Term, Term) -> Idris ()
106addErrRev t = do i <- getIState
107 putIState $ i { idris_errRev = t : idris_errRev i }
109totcheck :: (FC, Name) -> Idris ()
110totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
112defer_totcheck :: (FC, Name) -> Idris ()
113defer_totcheck n
114 = do i <- getIState;
115 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
117clear_totcheck :: Idris ()
118clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
120setFlags :: Name -> [FnOpt] -> Idris ()
121setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
123setAccessibility :: Name -> Accessibility -> Idris ()
124setAccessibility n a
125 = do i <- getIState
126 let ctxt = setAccess n a (tt_ctxt i)
127 putIState $ i { tt_ctxt = ctxt }
129setTotality :: Name -> Totality -> Idris ()
130setTotality n a
131 = do i <- getIState
132 let ctxt = setTotal n a (tt_ctxt i)
133 putIState $ i { tt_ctxt = ctxt }
135getTotality :: Name -> Idris Totality
136getTotality n
137 = do i <- getIState
138 case lookupTotal n (tt_ctxt i) of
139 [t] -> return t
140 _ -> return (Total [])
142-- Get coercions which might return the required type
143getCoercionsTo :: IState -> Type -> [Name]
144getCoercionsTo i ty =
145 let cs = idris_coercions i
146 (fn,_) = unApply (getRetTy ty) in
147 findCoercions fn cs
148 where findCoercions t [] = []
149 findCoercions t (n : ns) =
150 let ps = case lookupTy n (tt_ctxt i) of
151 [ty'] -> case unApply (getRetTy ty') of
152 (t', _) ->
153 if t == t' then [n] else []
154 _ -> [] in
155 ps ++ findCoercions t ns
157addToCG :: Name -> CGInfo -> Idris ()
158addToCG n cg
159 = do i <- getIState
160 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
162addTyInferred :: Name -> Idris ()
163addTyInferred n
164 = do i <- getIState
165 putIState $ i { idris_tyinfodata =
166 addDef n TIPartial (idris_tyinfodata i) }
168addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
169addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
170 mapM_ addConstraint ts
171 return ()
172 where addConstraint (x, y) = findMVApps x y
174 findMVApps x y
175 = do let (fx, argsx) = unApply x
176 let (fy, argsy) = unApply y
177 if (not (fx == fy))
178 then do
179 tryAddMV fx y
180 tryAddMV fy x
181 else mapM_ addConstraint (zip argsx argsy)
183 tryAddMV (P _ mv _) y =
184 do ist <- get
185 case lookup mv (idris_metavars ist) of
186 Just _ -> addConstraintRule mv y
187 _ -> return ()
188 tryAddMV _ _ = return ()
190 addConstraintRule :: Name -> Term -> Idris ()
191 addConstraintRule n t
192 = do ist <- get
193 logLvl 1 $ "TI constraint: " ++ show (n, t)
194 case lookupCtxt n (idris_tyinfodata ist) of
195 [TISolution ts] ->
196 do mapM_ (checkConsistent t) ts
197 let ti' = addDef n (TISolution (t : ts))
198 (idris_tyinfodata ist)
199 put $ ist { idris_tyinfodata = ti' }
200 _ ->
201 do let ti' = addDef n (TISolution [t])
202 (idris_tyinfodata ist)
203 put $ ist { idris_tyinfodata = ti' }
205 -- Check a solution is consistent with previous solutions
206 -- Meaning: If heads are both data types, they had better be the
207 -- same.
208 checkConsistent :: Term -> Term -> Idris ()
209 checkConsistent x y =
210 do let (fx, _) = unApply x
211 let (fy, _) = unApply y
212 case (fx, fy) of
213 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
214 (P (TCon _ _) n _, Constant _) -> errWhen True
215 (Constant _, P (TCon _ _) n' _) -> errWhen True
216 (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)
217 _ -> return ()
219 where errWhen True
220 = throwError (At fc
221 (CantUnify False x y (Msg "") [] 0))
222 errWhen False = return ()
224isTyInferred :: Name -> Idris Bool
225isTyInferred n
226 = do i <- getIState
227 case lookupCtxt n (idris_tyinfodata i) of
228 [TIPartial] -> return True
229 _ -> return False
231-- | Adds error handlers for a particular function and argument. If names are
232-- ambiguous, all matching handlers are updated.
233addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
234addFunctionErrorHandlers f arg hs =
235 do i <- getIState
236 let oldHandlers = idris_function_errorhandlers i
237 let newHandlers = flip (addDef f) oldHandlers $
238 case lookupCtxtExact f oldHandlers of
239 Nothing -> M.singleton arg (S.fromList hs)
240 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
241 -- will always be one of those two, thus no extra case
242 putIState $ i { idris_function_errorhandlers = newHandlers }
244getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
245getFunctionErrorHandlers f arg = do i <- getIState
246 return . maybe [] S.toList $
247 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
250-- Trace all the names in a call graph starting at the given name
251getAllNames :: Name -> Idris [Name]
252getAllNames n = allNames [] n
254allNames :: [Name] -> Name -> Idris [Name]
255allNames ns n | n `elem` ns = return []
256allNames ns n = do i <- getIState
257 case lookupCtxtExact n (idris_callgraph i) of
258 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
259 return (nub (n : concat more))
260 _ -> return [n]
262addCoercion :: Name -> Idris ()
263addCoercion n = do i <- getIState
264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
266addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
267addDocStr n doc args
268 = do i <- getIState
269 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
271addNameHint :: Name -> Name -> Idris ()
272addNameHint ty n
273 = do i <- getIState
274 ty' <- case lookupCtxtName ty (idris_implicits i) of
275 [(tyn, _)] -> return tyn
276 [] -> throwError (NoSuchVariable ty)
277 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
278 let ns' = case lookupCtxt ty' (idris_namehints i) of
279 [ns] -> ns ++ [n]
280 _ -> [n]
281 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
283getNameHints :: IState -> Name -> [Name]
284getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
285getNameHints i n =
286 case lookupCtxt n (idris_namehints i) of
287 [ns] -> ns
288 _ -> []
290addToCalledG :: Name -> [Name] -> Idris ()
291addToCalledG n ns = return () -- TODO
293-- Add a class instance function. Dodgy hack: Put integer instances first in the
294-- list so they are resolved by default.
295-- Dodgy hack 2: put constraint chasers (@@) last
297addInstance :: Bool -> Name -> Name -> Idris ()
298addInstance int n i
299 = do ist <- getIState
300 case lookupCtxt n (idris_classes ist) of
301 [CI a b c d e ins] ->
302 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
303 putIState $ ist { idris_classes = cs }
304 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
305 putIState $ ist { idris_classes = cs }
306 where addI i ins | int = i : ins
307 | chaser n = ins ++ [i]
308 | otherwise = insI i ins
309 insI i [] = [i]
310 insI i (n : ns) | chaser n = i : n : ns
311 | otherwise = n : insI i ns
313 chaser (UN nm)
314 | ('@':'@':_) <- str nm = True
315 chaser (NS n _) = chaser n
316 chaser _ = False
318addClass :: Name -> ClassInfo -> Idris ()
319addClass n i
320 = do ist <- getIState
321 let i' = case lookupCtxt n (idris_classes ist) of
322 [c] -> c { class_instances = class_instances i }
323 _ -> i
324 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
326addIBC :: IBCWrite -> Idris ()
327addIBC ibc@(IBCDef n)
328 = do i <- getIState
329 when (notDef (ibc_write i)) $
330 putIState $ i { ibc_write = ibc : ibc_write i }
331 where notDef [] = True
332 notDef (IBCDef n': is) | n == n' = False
333 notDef (_ : is) = notDef is
334addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
336clearIBC :: Idris ()
337clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
339resetNameIdx :: Idris ()
340resetNameIdx = do i <- getIState
341 put (i { idris_nameIdx = (0, emptyContext) })
343-- Used to preserve sharing of names
344addNameIdx :: Name -> Idris (Int, Name)
345addNameIdx n = do i <- getIState
346 let (i', x) = addNameIdx' i n
347 return x
349addNameIdx' :: IState -> Name -> (IState, (Int, Name))
350addNameIdx' i n
351 = let idxs = snd (idris_nameIdx i) in
352 case lookupCtxt n idxs of
353 [x] -> (i, x)
354 _ -> let i' = fst (idris_nameIdx i) + 1 in
355 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
357getHdrs :: Codegen -> Idris [String]
358getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
360setErrSpan :: FC -> Idris ()
361setErrSpan x = do i <- getIState;
362 case (errSpan i) of
363 Nothing -> putIState $ i { errSpan = Just x }
364 Just _ -> return ()
366clearErr :: Idris ()
367clearErr = do i <- getIState
368 putIState $ i { errSpan = Nothing }
370getSO :: Idris (Maybe String)
371getSO = do i <- getIState
372 return (compiled_so i)
374setSO :: Maybe String -> Idris ()
375setSO s = do i <- getIState
376 putIState $ (i { compiled_so = s })
378getIState :: Idris IState
379getIState = get
381putIState :: IState -> Idris ()
382putIState = put
384-- | A version of liftIO that puts errors into the exception type of the Idris monad
385runIO :: IO a -> Idris a
386runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
387-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
389getName :: Idris Int
390getName = do i <- getIState;
391 let idx = idris_name i;
392 putIState $ (i { idris_name = idx + 1 })
393 return idx
395-- InternalApp keeps track of the real function application for making case splits from, not the application the
396-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
397addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
398addInternalApp fp l t
399 = do i <- getIState
400 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
402getInternalApp :: FilePath -> Int -> Idris PTerm
403getInternalApp fp l = do i <- getIState
404 case lookup (fp, l) (idris_lineapps i) of
405 Just n' -> return n'
406 Nothing -> return Placeholder
407 -- TODO: What if it's not there?
409-- Pattern definitions are only used for coverage checking, so erase them
410-- when we're done
411clearOrigPats :: Idris ()
412clearOrigPats = do i <- get
413 let ps = idris_patdefs i
414 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
415 put (i { idris_patdefs = ps' })
417-- Erase types from Ps in the context (basically ending up with what's in
418-- the .ibc, which is all we need after all the analysis is done)
419clearPTypes :: Idris ()
420clearPTypes = do i <- get
421 let ctxt = tt_ctxt i
422 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
423 where pErase (CaseOp c t tys orig tot cds)
424 = CaseOp c t tys orig [] (pErase' cds)
425 pErase x = x
426 pErase' (CaseDefs _ (cs, c) _ rs)
427 = let c' = (cs, fmap pEraseType c) in
428 CaseDefs c' c' c' rs
430checkUndefined :: FC -> Name -> Idris ()
431checkUndefined fc n
432 = do i <- getContext
433 case lookupTy n i of
434 (_:_) -> throwError . Msg $ show fc ++ ":" ++
435 show n ++ " already defined"
436 _ -> return ()
438isUndefined :: FC -> Name -> Idris Bool
439isUndefined fc n
440 = do i <- getContext
441 case lookupTy n i of
442 (_:_) -> return False
443 _ -> return True
445setContext :: Context -> Idris ()
446setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
448updateContext :: (Context -> Context) -> Idris ()
449updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
451addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
452addConstraints fc (v, cs)
453 = do i <- getIState
454 let ctxt = tt_ctxt i
455 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
456 next_tvar = v }
457 let ics = zip cs (repeat fc) ++ idris_constraints i
458 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
460addDeferred = addDeferred' Ref
461addDeferredTyCon = addDeferred' (TCon 0 0)
463addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
464addDeferred' nt ns
465 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
466 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
467 i <- getIState
468 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
469 idris_metavars i }
470 where tidyNames used (Bind (MN i x) b sc)
471 = let n' = uniqueName (UN x) used in
472 Bind n' b $ tidyNames (n':used) sc
473 tidyNames used (Bind n b sc)
474 = let n' = uniqueName n used in
475 Bind n' b $ tidyNames (n':used) sc
476 tidyNames used b = b
478solveDeferred :: Name -> Idris ()
479solveDeferred n = do i <- getIState
480 putIState $ i { idris_metavars =
481 filter (\(n', _) -> n/=n')
482 (idris_metavars i),
483 ibc_write =
484 filter (notMV n) (ibc_write i)
485 }
486 where notMV n (IBCMetavar n') = not (n == n')
487 notMV n _ = True
489getUndefined :: Idris [Name]
490getUndefined = do i <- getIState
491 return (map fst (idris_metavars i) \\ primDefs)
493isMetavarName :: Name -> IState -> Bool
494isMetavarName n ist
495 = case lookupNames n (tt_ctxt ist) of
496 (t:_) -> isJust $ lookup t (idris_metavars ist)
497 _ -> False
499getWidth :: Idris ConsoleWidth
500getWidth = fmap idris_consolewidth getIState
502setWidth :: ConsoleWidth -> Idris ()
503setWidth w = do ist <- getIState
504 put ist { idris_consolewidth = w }
506renderWidth :: Idris Int
507renderWidth = do iw <- getWidth
508 case iw of
509 InfinitelyWide -> return 100000000
510 ColsWide n -> return (max n 1)
511 AutomaticWidth -> runIO getScreenWidth
515type1Doc :: Doc OutputAnnotation
516type1Doc = (annotate AnnConstType $ text "Type 1")
519isetPrompt :: String -> Idris ()
520isetPrompt p = do i <- getIState
521 case idris_outputmode i of
522 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
524setLogLevel :: Int -> Idris ()
525setLogLevel l = do i <- getIState
526 let opts = idris_options i
527 let opt' = opts { opt_logLevel = l }
528 putIState $ i { idris_options = opt' }
530setCmdLine :: [Opt] -> Idris ()
531setCmdLine opts = do i <- getIState
532 let iopts = idris_options i
533 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
535getCmdLine :: Idris [Opt]
536getCmdLine = do i <- getIState
537 return (opt_cmdline (idris_options i))
539getDumpDefun :: Idris (Maybe FilePath)
540getDumpDefun = do i <- getIState
541 return $ findC (opt_cmdline (idris_options i))
542 where findC [] = Nothing
543 findC (DumpDefun x : _) = Just x
544 findC (_ : xs) = findC xs
546getDumpCases :: Idris (Maybe FilePath)
547getDumpCases = do i <- getIState
548 return $ findC (opt_cmdline (idris_options i))
549 where findC [] = Nothing
550 findC (DumpCases x : _) = Just x
551 findC (_ : xs) = findC xs
553logLevel :: Idris Int
554logLevel = do i <- getIState
555 return (opt_logLevel (idris_options i))
557setErrContext :: Bool -> Idris ()
558setErrContext t = do i <- getIState
559 let opts = idris_options i
560 let opt' = opts { opt_errContext = t }
561 putIState $ i { idris_options = opt' }
563errContext :: Idris Bool
564errContext = do i <- getIState
565 return (opt_errContext (idris_options i))
567useREPL :: Idris Bool
568useREPL = do i <- getIState
569 return (opt_repl (idris_options i))
571setREPL :: Bool -> Idris ()
572setREPL t = do i <- getIState
573 let opts = idris_options i
574 let opt' = opts { opt_repl = t }
575 putIState $ i { idris_options = opt' }
577showOrigErr :: Idris Bool
578showOrigErr = do i <- getIState
579 return (opt_origerr (idris_options i))
581setShowOrigErr :: Bool -> Idris ()
582setShowOrigErr b = do i <- getIState
583 let opts = idris_options i
584 let opt' = opts { opt_origerr = b }
585 putIState $ i { idris_options = opt' }
587setAutoSolve :: Bool -> Idris ()
588setAutoSolve b = do i <- getIState
589 let opts = idris_options i
590 let opt' = opts { opt_autoSolve = b }
591 putIState $ i { idris_options = opt' }
593setNoBanner :: Bool -> Idris ()
594setNoBanner n = do i <- getIState
595 let opts = idris_options i
596 let opt' = opts { opt_nobanner = n }
597 putIState $ i { idris_options = opt' }
599getNoBanner :: Idris Bool
600getNoBanner = do i <- getIState
601 let opts = idris_options i
602 return (opt_nobanner opts)
604setQuiet :: Bool -> Idris ()
605setQuiet q = do i <- getIState
606 let opts = idris_options i
607 let opt' = opts { opt_quiet = q }
608 putIState $ i { idris_options = opt' }
610getQuiet :: Idris Bool
611getQuiet = do i <- getIState
612 let opts = idris_options i
613 return (opt_quiet opts)
615setCodegen :: Codegen -> Idris ()
616setCodegen t = do i <- getIState
617 let opts = idris_options i
618 let opt' = opts { opt_codegen = t }
619 putIState $ i { idris_options = opt' }
621codegen :: Idris Codegen
622codegen = do i <- getIState
623 return (opt_codegen (idris_options i))
625setOutputTy :: OutputType -> Idris ()
626setOutputTy t = do i <- getIState
627 let opts = idris_options i
628 let opt' = opts { opt_outputTy = t }
629 putIState $ i { idris_options = opt' }
631outputTy :: Idris OutputType
632outputTy = do i <- getIState
633 return $ opt_outputTy $ idris_options i
635setIdeSlave :: Bool -> Idris ()
636setIdeSlave True = do i <- getIState
637 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
638setIdeSlave False = return ()
640setTargetTriple :: String -> Idris ()
641setTargetTriple t = do i <- getIState
642 let opts = idris_options i
643 opt' = opts { opt_triple = t }
644 putIState $ i { idris_options = opt' }
646targetTriple :: Idris String
647targetTriple = do i <- getIState
648 return (opt_triple (idris_options i))
650setTargetCPU :: String -> Idris ()
651setTargetCPU t = do i <- getIState
652 let opts = idris_options i
653 opt' = opts { opt_cpu = t }
654 putIState $ i { idris_options = opt' }
656targetCPU :: Idris String
657targetCPU = do i <- getIState
658 return (opt_cpu (idris_options i))
660setOptLevel :: Word -> Idris ()
661setOptLevel t = do i <- getIState
662 let opts = idris_options i
663 opt' = opts { opt_optLevel = t }
664 putIState $ i { idris_options = opt' }
666optLevel :: Idris Word
667optLevel = do i <- getIState
668 return (opt_optLevel (idris_options i))
670verbose :: Idris Bool
671verbose = do i <- getIState
672 return (opt_verbose (idris_options i))
674setVerbose :: Bool -> Idris ()
675setVerbose t = do i <- getIState
676 let opts = idris_options i
677 let opt' = opts { opt_verbose = t }
678 putIState $ i { idris_options = opt' }
680typeInType :: Idris Bool
681typeInType = do i <- getIState
682 return (opt_typeintype (idris_options i))
684setTypeInType :: Bool -> Idris ()
685setTypeInType t = do i <- getIState
686 let opts = idris_options i
687 let opt' = opts { opt_typeintype = t }
688 putIState $ i { idris_options = opt' }
690coverage :: Idris Bool
691coverage = do i <- getIState
692 return (opt_coverage (idris_options i))
694setCoverage :: Bool -> Idris ()
695setCoverage t = do i <- getIState
696 let opts = idris_options i
697 let opt' = opts { opt_coverage = t }
698 putIState $ i { idris_options = opt' }
700setIBCSubDir :: FilePath -> Idris ()
701setIBCSubDir fp = do i <- getIState
702 let opts = idris_options i
703 let opt' = opts { opt_ibcsubdir = fp }
704 putIState $ i { idris_options = opt' }
706valIBCSubDir :: IState -> Idris FilePath
707valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
709addImportDir :: FilePath -> Idris ()
710addImportDir fp = do i <- getIState
711 let opts = idris_options i
712 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
713 putIState $ i { idris_options = opt' }
715setImportDirs :: [FilePath] -> Idris ()
716setImportDirs fps = do i <- getIState
717 let opts = idris_options i
718 let opt' = opts { opt_importdirs = fps }
719 putIState $ i { idris_options = opt' }
721allImportDirs :: Idris [FilePath]
722allImportDirs = do i <- getIState
723 let optdirs = opt_importdirs (idris_options i)
724 return ("." : reverse optdirs)
726colourise :: Idris Bool
727colourise = do i <- getIState
728 return $ idris_colourRepl i
730setColourise :: Bool -> Idris ()
731setColourise b = do i <- getIState
732 putIState $ i { idris_colourRepl = b }
734setOutH :: Handle -> Idris ()
735setOutH h = do i <- getIState
736 putIState $ i { idris_outh = h }
738impShow :: Idris Bool
739impShow = do i <- getIState
740 return (opt_showimp (idris_options i))
742setImpShow :: Bool -> Idris ()
743setImpShow t = do i <- getIState
744 let opts = idris_options i
745 let opt' = opts { opt_showimp = t }
746 putIState $ i { idris_options = opt' }
748setColour :: ColourType -> IdrisColour -> Idris ()
749setColour ct c = do i <- getIState
750 let newTheme = setColour' ct c (idris_colourTheme i)
751 putIState $ i { idris_colourTheme = newTheme }
752 where setColour' KeywordColour c t = t { keywordColour = c }
753 setColour' BoundVarColour c t = t { boundVarColour = c }
754 setColour' ImplicitColour c t = t { implicitColour = c }
755 setColour' FunctionColour c t = t { functionColour = c }
756 setColour' TypeColour c t = t { typeColour = c }
757 setColour' DataColour c t = t { dataColour = c }
758 setColour' PromptColour c t = t { promptColour = c }
760logLvl :: Int -> String -> Idris ()
761logLvl l str = do i <- getIState
762 let lvl = opt_logLevel (idris_options i)
763 when (lvl >= l) $
764 case idris_outputmode i of
765 RawOutput -> do runIO $ putStrLn str
766 IdeSlave n ->
767 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
768 runIO $ putStrLn $ convSExp "log" good n
770cmdOptType :: Opt -> Idris Bool
771cmdOptType x = do i <- getIState
772 return $ x `elem` opt_cmdline (idris_options i)
774iLOG :: String -> Idris ()
775iLOG = logLvl 1
777noErrors :: Idris Bool
778noErrors = do i <- getIState
779 case errSpan i of
780 Nothing -> return True
781 _ -> return False
783setTypeCase :: Bool -> Idris ()
784setTypeCase t = do i <- getIState
785 let opts = idris_options i
786 let opt' = opts { opt_typecase = t }
787 putIState $ i { idris_options = opt' }
790-- Dealing with parameters
792expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
793 [Name] -> -- all names
794 [Name] -> -- names with no declaration
795 PTerm -> PTerm
796expandParams dec ps ns infs tm = en tm
797 where
798 -- if we shadow a name (say in a lambda binding) that is used in a call to
799 -- a lifted function, we need access to both names - once in the scope of the
800 -- binding and once to call the lifted functions. So we'll explicitly shadow
801 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
802 -- but we didn't...)
804 mkShadow (UN n) = MN 0 n
805 mkShadow (MN i n) = MN (i+1) n
806 mkShadow (NS x s) = NS (mkShadow x) s
808 en (PLam n t s)
809 | n `elem` (map fst ps ++ ns)
810 = let n' = mkShadow n in
811 PLam n' (en t) (en (shadow n n' s))
812 | otherwise = PLam n (en t) (en s)
813 en (PPi p n t s)
814 | n `elem` (map fst ps ++ ns)
815 = let n' = mkShadow n in
816 PPi p n' (en t) (en (shadow n n' s))
817 | otherwise = PPi p n (en t) (en s)
818 en (PLet n ty v s)
819 | n `elem` (map fst ps ++ ns)
820 = let n' = mkShadow n in
821 PLet n' (en ty) (en v) (en (shadow n n' s))
822 | otherwise = PLet n (en ty) (en v) (en s)
823 -- FIXME: Should only do this in a type signature!
824 en (PDPair f p (PRef f' n) t r)
825 | n `elem` (map fst ps ++ ns) && t /= Placeholder
826 = let n' = mkShadow n in
827 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
828 en (PEq f l r) = PEq f (en l) (en r)
829 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
830 en (PTyped l r) = PTyped (en l) (en r)
831 en (PPair f p l r) = PPair f p (en l) (en r)
832 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
833 en (PAlternative a as) = PAlternative a (map en as)
834 en (PHidden t) = PHidden (en t)
835 en (PUnifyLog t) = PUnifyLog (en t)
836 en (PDisamb ds t) = PDisamb ds (en t)
837 en (PNoImplicits t) = PNoImplicits (en t)
838 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
839 en (PProof ts) = PProof (map (fmap en) ts)
840 en (PTactics ts) = PTactics (map (fmap en) ts)
842 en (PQuote (Var n))
843 | n `nselem` ns = PQuote (Var (dec n))
844 en (PApp fc (PInferRef fc' n) as)
845 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
846 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
847 en (PApp fc (PRef fc' n) as)
848 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
849 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
850 | n `nselem` ns = PApp fc (PRef fc' (dec n))
851 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
852 en (PAppBind fc (PRef fc' n) as)
853 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
854 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
855 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
856 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
857 en (PRef fc n)
858 | n `elem` infs = PApp fc (PInferRef fc (dec n))
859 (map (pexp . (PRef fc)) (map fst ps))
860 | n `nselem` ns = PApp fc (PRef fc (dec n))
861 (map (pexp . (PRef fc)) (map fst ps))
862 en (PInferRef fc n)
863 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
864 (map (pexp . (PRef fc)) (map fst ps))
865 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
866 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
867 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
868 en t = t
870 nselem x [] = False
871 nselem x (y : xs) | nseq x y = True
872 | otherwise = nselem x xs
874 nseq x y = nsroot x == nsroot y
876expandParamsD :: Bool -> -- True = RHS only
877 IState ->
878 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
879expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
880 = if n `elem` ns && (not rhsonly)
881 then -- trace (show (n, expandParams dec ps ns ty)) $
882 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
883 else --trace (show (n, expandParams dec ps ns ty)) $
884 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
885expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
886 = if n `elem` ns && (not rhsonly)
887 then -- trace (show (n, expandParams dec ps ns ty)) $
888 PPostulate doc syn fc o (dec n) (piBind ps
889 (expandParams dec ps ns [] ty))
890 else --trace (show (n, expandParams dec ps ns ty)) $
891 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
892expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
893 = let n' = if n `elem` ns then dec n else n in
894 PClauses fc opts n' (map expandParamsC cs)
895 where
896 expandParamsC (PClause fc n lhs ws rhs ds)
897 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
898 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
899 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
900 n' = if n `elem` ns then dec n else n
901 -- names bound on the lhs should not be expanded on the rhs
902 ns' = removeBound lhs ns in
903 PClause fc n' lhs'
904 (map (expandParams dec ps'' ns' []) ws)
905 (expandParams dec ps'' ns' [] rhs)
906 (map (expandParamsD True ist dec ps'' ns') ds)
907 expandParamsC (PWith fc n lhs ws wval ds)
908 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
909 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
910 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
911 n' = if n `elem` ns then dec n else n
912 ns' = removeBound lhs ns in
913 PWith fc n' lhs'
914 (map (expandParams dec ps'' ns' []) ws)
915 (expandParams dec ps'' ns' [] wval)
916 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
917 updateps yn nm [] = []
918 updateps yn nm (((a, t), i):as)
919 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
920 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
922 removeBound lhs ns = ns \\ nub (bnames lhs)
924 bnames (PRef _ n) = [n]
925 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
926 bnames (PPair _ _ l r) = bnames l ++ bnames r
927 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
928 bnames _ = []
930expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
931 = PData doc argDocs syn fc co (expandPData pd)
932 where
933 -- just do the type decl, leave constructors alone (parameters will be
934 -- added implicitly)
935 expandPData (PDatadecl n ty cons)
936 = if n `elem` ns
937 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
938 (map econ cons)
939 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
940 econ (doc, argDocs, n, t, fc, fs)
941 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
942expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
943 = if tn `elem` ns
944 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
945 cdoc (dec cn) conty
946 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
947 cdoc (dec cn) conty
948 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
949expandParamsD rhs ist dec ps ns (PParams f params pds)
950 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
951 (map (expandParamsD True ist dec ps ns) pds)
952-- (map (expandParamsD ist dec ps ns) pds)
953expandParamsD rhs ist dec ps ns (PMutual f pds)
954 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
955expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
956 = PClass doc info f
957 (map (expandParams dec ps ns []) cs)
958 n
959 (map (mapsnd (expandParams dec ps ns [])) params)
960 (map (expandParamsD rhs ist dec ps ns) decls)
961expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
962 = PInstance info f
963 (map (expandParams dec ps ns []) cs)
964 n
965 (map (expandParams dec ps ns []) params)
966 (expandParams dec ps ns [] ty)
967 cn
968 (map (expandParamsD rhs ist dec ps ns) decls)
969expandParamsD rhs ist dec ps ns d = d
971mapsnd f (x, t) = (x, f t)
973-- Calculate a priority for a type, for deciding elaboration order
974-- * if it's just a type variable or concrete type, do it early (0)
975-- * if there's only type variables and injective constructors, do it next (1)
976-- * if there's a function type, next (2)
977-- * finally, everything else (3)
979getPriority :: IState -> PTerm -> Int
980getPriority i tm = 1 -- pri tm
981 where
982 pri (PRef _ n) =
983 case lookupP n (tt_ctxt i) of
984 ((P (DCon _ _) _ _):_) -> 1
985 ((P (TCon _ _) _ _):_) -> 1
986 ((P Ref _ _):_) -> 1
987 [] -> 0 -- must be locally bound, if it's not an error...
988 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
989 pri (PTrue _ _) = 0
990 pri (PFalse _) = 0
991 pri (PRefl _ _) = 1
992 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
993 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
994 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
995 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
996 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
997 pri (PTyped l r) = pri l
998 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
999 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1000 pri (PAlternative a as) = maximum (map pri as)
1001 pri (PConstant _) = 0
1002 pri Placeholder = 1
1003 pri _ = 3
1006addStatics :: Name -> Term -> PTerm -> Idris ()
1007addStatics n tm ptm =
1008 do let (statics, dynamics) = initStatics tm ptm
1009 let stnames = nub $ concatMap freeArgNames (map snd statics)
1010 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1011 -- also get the arguments which are 'uniquely inferrable' from
1012 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1013 let statics' = nub $ map fst statics ++
1014 filter (\x -> not (elem x dnames)) stnames
1015 let stpos = staticList statics' tm
1016 i <- getIState
1017 when (not (null statics)) $
1018 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1019 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1020 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1021 addIBC (IBCStatic n)
1022 where
1023 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1024 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1025 if pstatic p == Static then ((n, ty) : static, dynamic)
1026 else if (not (searchArg p))
1027 then (static, (n, ty) : dynamic)
1028 else (static, dynamic)
1029 initStatics t pt = ([], [])
1031 freeArgNames (Bind n (Pi ty) sc)
1032 = nub $ freeArgNames ty
1033 freeArgNames tm = let (_, args) = unApply tm in
1034 concatMap freeNames args
1036 -- if a name appears in a type class or tactic implicit index, it doesn't
1037 -- affect its 'uniquely inferrable' from a static status since these are
1038 -- resolved by searching.
1039 searchArg (Constraint _ _) = True
1040 searchArg (TacImp _ _ _) = True
1041 searchArg _ = False
1043 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1044 staticList _ _ = []
1046-- Dealing with implicit arguments
1048-- Add constraint bindings from using block
1050addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1051addUsingConstraints syn fc t
1052 = do ist <- get
1053 let ns = namesIn [] ist t
1054 let cs = getConstraints t -- check declared constraints
1055 let addconsts = uconsts \\ cs
1056 -- if all names in the arguments of addconsts appear in ns,
1057 -- add the constraint implicitly
1058 return (doAdd addconsts ns t)
1059 where uconsts = filter uconst (using syn)
1060 uconst (UConstraint _ _) = True
1061 uconst _ = False
1063 doAdd [] _ t = t
1064 -- if all of args in ns, then add it
1065 doAdd (UConstraint c args : cs) ns t
1066 | all (\n -> elem n ns) args
1067 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1068 (mkConst c args) (doAdd cs ns t)
1069 | otherwise = doAdd cs ns t
1071 mkConst c args = PApp fc (PRef fc c)
1072 (map (\n -> PExp 0 [] (PRef fc n)) args)
1074 getConstraints (PPi (Constraint _ _) _ c sc)
1075 = getcapp c ++ getConstraints sc
1076 getConstraints (PPi _ _ c sc) = getConstraints sc
1077 getConstraints _ = []
1079 getcapp (PApp _ (PRef _ c) args)
1080 = do ns <- mapM getName args
1081 return (UConstraint c ns)
1082 getcapp _ = []
1084 getName (PExp _ _ (PRef _ n)) = return n
1085 getName _ = []
1087-- Add implicit Pi bindings for any names in the term which appear in an
1088-- argument position.
1090-- This has become a right mess already. Better redo it some time...
1092implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1093implicit syn n ptm = implicit' syn [] n ptm
1095implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1096implicit' syn ignore n ptm
1097 = do i <- getIState
1098 let (tm', impdata) = implicitise syn ignore i ptm
1099-- let (tm'', spos) = findStatics i tm'
1100 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1101 addIBC (IBCImp n)
1102 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1103-- i <- get
1104-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1105 return tm'
1107implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1108implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1109 let (declimps, ns') = execState (imps True [] tm) ([], [])
1110 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1111 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1112 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1113 if null ns
1114 then (tm, reverse declimps)
1115 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1116 where
1117 uvars = map ipair (filter uimplicit (using syn))
1118 pvars = syn_params syn
1120 inUsing n = n `elem` map fst uvars
1122 ipair (UImplicit x y) = (x, y)
1123 uimplicit (UImplicit _ _) = True
1124 uimplicit _ = False
1126 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1127 | otherwise = x : dropAll xs ys
1128 dropAll [] ys = []
1130 -- Find names in argument position in a type, suitable for implicit
1131 -- binding
1132 -- Not the function position, but do everything else...
1133 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1134 implNamesIn uv t = namesIn uv ist t
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 _ _) n ty sc)
1141 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1142 (decls , ns) <- get
1143 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1144 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1145 imps True (n:env) sc
1146 imps top env (PPi (Exp l _ _) n ty sc)
1147 = do let isn = nub (implNamesIn uvars 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 : decls,
1152 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1153 imps True (n:env) sc
1154 imps top env (PPi (Constraint l _) n ty sc)
1155 = do let isn = nub (implNamesIn uvars 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 : 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) n ty sc)
1163 = do let isn = nub (implNamesIn uvars 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 : 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 [] Dynamic False) n ty (pibind using ns sc)
1209 Nothing -> PPi (Imp [] 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 p l r)
1251 = let l' = ai env ds l
1252 r' = ai env ds r in
1253 PPair fc p l' r'
1254 ai env ds (PDPair fc p 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 p 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 : given) =
1375 PExp p l tm : insertImpl ps given
1376 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1377 PConstraint p l tm : insertImpl ps given
1378 insertImpl (PConstraint p l ty : ps) given =
1379 PConstraint p l (PResolveTC fc) : insertImpl ps given
1380 insertImpl (PImp p _ l n ty : 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 : 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 t@(PAlternative _ (a : as)) = do sl a
1423 return t
1424 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1425 args' <- mapM slA args
1426 return $ PApp fc fn args'
1427 where slA (PImp p m l n t) = do t' <- sl t
1428 return $ PImp p m l n t'
1429 slA (PExp p l t) = do t' <- sl t
1430 return $ PExp p l t'
1431 slA (PConstraint p l t)
1432 = do t' <- sl t
1433 return $ PConstraint p l t'
1434 slA (PTacImplicit p l n sc t)
1435 = do t' <- sl t
1436 return $ PTacImplicit p l n sc t'
1437 sl x = return x
1439-- Remove functions which aren't applied to anything, which must then
1440-- be resolved by unification. Assume names resolved and alternatives
1441-- filled in (so no ambiguity).
1443stripUnmatchable :: IState -> PTerm -> PTerm
1444stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1445 su :: PTerm -> PTerm
1446 su (PRef fc f)
1447 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1448 = Placeholder
1449 su (PApp fc fn args)
1450 = PApp fc fn (fmap (fmap su) args)
1451 su (PAlternative b alts)
1452 = let alts' = filter (/= Placeholder) (map su alts) in
1453 if null alts' then Placeholder
1454 else PAlternative b alts'
1455 su (PPair fc p l r) = PPair fc p (su l) (su r)
1456 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1457 su t = t
1458stripUnmatchable i tm = tm
1460mkPApp fc a f [] = f
1461mkPApp fc a f as = let rest = drop a as in
1462 appRest fc (PApp fc f (take a as)) rest
1463 where
1464 appRest fc f [] = f
1465 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1467-- Find 'static' argument positions
1468-- (the declared ones, plus any names in argument position in the declared
1469-- statics)
1470-- FIXME: It's possible that this really has to happen after elaboration
1472findStatics :: IState -> PTerm -> (PTerm, [Bool])
1473findStatics ist tm = trace (show tm) $
1474 let (ns, ss) = fs tm in
1475 runState (pos ns ss tm) []
1476 where fs (PPi p n t sc)
1477 | Static <- pstatic p
1478 = let (ns, ss) = fs sc in
1479 (namesIn [] ist t : ns, n : ss)
1480 | otherwise = let (ns, ss) = fs sc in
1481 (ns, ss)
1482 fs _ = ([], [])
1484 inOne n ns = length (filter id (map (elem n) ns)) == 1
1486 pos ns ss (PPi p n t sc)
1487 | elem n ss = do sc' <- pos ns ss sc
1488 spos <- get
1489 put (True : spos)
1490 return (PPi (p { pstatic = Static }) n t sc')
1491 | otherwise = do sc' <- pos ns ss sc
1492 spos <- get
1493 put (False : spos)
1494 return (PPi p n t sc')
1495 pos ns ss t = return t
1497-- for 6.12/7 compatibility
1498data EitherErr a b = LeftErr a | RightOK b
1500instance Monad (EitherErr a) where
1501 return = RightOK
1503 (LeftErr e) >>= k = LeftErr e
1504 RightOK v >>= k = k v
1506toEither (LeftErr e) = Left e
1507toEither (RightOK ho) = Right ho
1509-- syntactic match of a against b, returning pair of variables in a
1510-- and what they match. Returns the pair that failed if not a match.
1512matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1513matchClause = matchClause' False
1515matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1516matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1517 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1519 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1520 fullApp x = x
1522 match' x y = match (fullApp x) (fullApp y)
1523 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1524 | fi == txt "fromInteger" && b == txt "builtins",
1525 PConstant (I _) <- getTm x = match (getTm x) x'
1526 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1527 | fi == txt "fromInteger" && b == txt "builtins",
1528 PConstant (I _) <- getTm x = match (getTm x) x'
1529 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1530 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1531 match (PApp _ f args) (PApp _ f' args')
1532 | length args == length args'
1533 = do mf <- match' f f'
1534 ms <- zipWithM matchArg args args'
1535 return (mf ++ concat ms)
1536-- match (PRef _ n) (PRef _ n') | n == n' = return []
1537-- | otherwise = Nothing
1538 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1539 match (PPatvar f n) xr = match (PRef f n) xr
1540 match xr (PPatvar f n) = match xr (PRef f n)
1541 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1542 match (PRef _ n) tm@(PRef _ n')
1543 | n == n' && not names &&
1544 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1545 || tm == Placeholder)
1546 = return [(n, tm)]
1547 | n == n' = return []
1548 match (PRef _ n) tm
1549 | not names && (not (isConName n (tt_ctxt i) ||
1550 isFnName n (tt_ctxt i)) || tm == Placeholder)
1551 = return [(n, tm)]
1552 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1553 mr <- match' r r'
1554 return (ml ++ mr)
1555 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1556 = do ml <- match' l l'
1557 mr <- match' r r'
1558 return (ml ++ mr)
1559 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1560 mr <- match r r'
1561 return (ml ++ mr)
1562 match (PTyped l r) x = match l x
1563 match x (PTyped l r) = match x l
1564 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1565 mr <- match' r r'
1566 return (ml ++ mr)
1567 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1568 mt <- match' t t'
1569 mr <- match' r r'
1570 return (ml ++ mt ++ mr)
1571 match (PAlternative a as) (PAlternative a' as')
1572 = do ms <- zipWithM match' as as'
1573 return (concat ms)
1574 match a@(PAlternative _ as) b
1575 = do let ms = zipWith match' as (repeat b)
1576 case (rights (map toEither ms)) of
1577 (x: _) -> return x
1578 _ -> LeftErr (a, b)
1579 match (PCase _ _ _) _ = return [] -- lifted out
1580 match (PMetavar _) _ = return [] -- modified
1581 match (PInferRef _ _) _ = return [] -- modified
1582 match (PQuote _) _ = return []
1583 match (PProof _) _ = return []
1584 match (PTactics _) _ = return []
1585 match (PRefl _ _) (PRefl _ _) = return []
1586 match (PResolveTC _) (PResolveTC _) = return []
1587 match (PTrue _ _) (PTrue _ _) = return []
1588 match (PFalse _) (PFalse _) = return []
1589 match (PReturn _) (PReturn _) = return []
1590 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1591 ms <- match' s s'
1592 return (mt ++ ms)
1593 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1594 ms <- match' s s'
1595 return (mt ++ ms)
1596 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1597 mty <- match' ty ty'
1598 ms <- match' s s'
1599 return (mt ++ mty ++ ms)
1600 match (PHidden x) (PHidden y) = match' x y
1601 match (PUnifyLog x) y = match' x y
1602 match x (PUnifyLog y) = match' x y
1603 match (PNoImplicits x) y = match' x y
1604 match x (PNoImplicits y) = match' x y
1605 match Placeholder _ = return []
1606 match _ Placeholder = return []
1607 match (PResolveTC _) _ = return []
1608 match a b | a == b = return []
1609 | otherwise = LeftErr (a, b)
1611 checkRpts (RightOK ms) = check ms where
1612 check ((n,t):xs)
1613 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1614 then Left (t, t')
1615 else check xs
1616 check (_:xs) = check xs
1617 check [] = Right ms
1618 checkRpts (LeftErr x) = Left x
1620substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1621substMatches ms = substMatchesShadow ms []
1623substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1624substMatchesShadow [] shs t = t
1625substMatchesShadow ((n,tm):ns) shs t
1626 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1628substMatch :: Name -> PTerm -> PTerm -> PTerm
1629substMatch n = substMatchShadow n []
1631substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1632substMatchShadow n shs tm t = sm shs t where
1633 sm xs (PRef _ n') | n == n' = tm
1634 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1635 sm xs (PPi p x t sc)
1636 | x `elem` xs
1637 = let x' = nextName x in
1638 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1639 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1640 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1641 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1642 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1643 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1644 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1645 (fmap (sm xs) tm)
1646 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1647 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1648 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1649 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1650 sm xs (PHidden x) = PHidden (sm xs x)
1651 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1652 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1653 sm xs x = x
1655 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1656 fullApp x = x
1658shadow :: Name -> Name -> PTerm -> PTerm
1659shadow n n' t = sm t where
1660 sm (PRef fc x) | n == x = PRef fc n'
1661 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1662 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1663 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1664 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1665 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1666 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1667 sm (PEq f x y) = PEq f (sm x) (sm y)
1668 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1669 sm (PTyped x y) = PTyped (sm x) (sm y)
1670 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1671 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1672 sm (PAlternative a as) = PAlternative a (map sm as)
1673 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1674 sm (PProof ts) = PProof (map (fmap sm) ts)
1675 sm (PHidden x) = PHidden (sm x)
1676 sm (PUnifyLog x) = PUnifyLog (sm x)
1677 sm (PNoImplicits x) = PNoImplicits (sm x)
1678 sm x = x
1680-- Rename any binders which are repeated (so that we don't have to mess
1681-- about with shadowing anywhere else).
1683mkUniqueNames :: [Name] -> PTerm -> PTerm
1684mkUniqueNames env tm = evalState (mkUniq tm) env where
1685 inScope = boundNamesIn tm
1687 mkUniqA arg = do t' <- mkUniq (getTm arg)
1688 return (arg { getTm = t' })
1690 -- FIXME: Probably ought to do this for completeness! It's fine as
1691 -- long as there are no bindings inside tactics though.
1692 mkUniqT tac = return tac
1694 mkUniq :: PTerm -> State [Name] PTerm
1695 mkUniq (PLam n ty sc)
1696 = do env <- get
1697 (n', sc') <-
1698 if n `elem` env
1699 then do let n' = uniqueName n (env ++ inScope)
1700 return (n', shadow n n' sc)
1701 else return (n, sc)
1702 put (n' : env)
1703 ty' <- mkUniq ty
1704 sc'' <- mkUniq sc'
1705 return $! PLam n' ty' sc''
1706 mkUniq (PPi p n ty sc)
1707 = do env <- get
1708 (n', sc') <-
1709 if n `elem` env
1710 then do let n' = uniqueName n (env ++ inScope)
1711 return (n', shadow n n' sc)
1712 else return (n, sc)
1713 put (n' : env)
1714 ty' <- mkUniq ty
1715 sc'' <- mkUniq sc'
1716 return $! PPi p n' ty' sc''
1717 mkUniq (PLet n ty val sc)
1718 = do env <- get
1719 (n', sc') <-
1720 if n `elem` env
1721 then do let n' = uniqueName n (env ++ inScope)
1722 return (n', shadow n n' sc)
1723 else return (n, sc)
1724 put (n' : env)
1725 ty' <- mkUniq ty; val' <- mkUniq val
1726 sc'' <- mkUniq sc'
1727 return $! PLet n' ty' val' sc''
1728 mkUniq (PApp fc t args)
1729 = do t' <- mkUniq t
1730 args' <- mapM mkUniqA args
1731 return $! PApp fc t' args'
1732 mkUniq (PAppBind fc t args)
1733 = do t' <- mkUniq t
1734 args' <- mapM mkUniqA args
1735 return $! PAppBind fc t' args'
1736 mkUniq (PCase fc t alts)
1737 = do t' <- mkUniq t
1738 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1739 return (x', y')) alts
1740 return $! PCase fc t' alts'
1741 mkUniq (PPair fc p l r)
1742 = do l' <- mkUniq l; r' <- mkUniq r
1743 return $! PPair fc p l' r'
1744 mkUniq (PDPair fc p (PRef fc' n) t sc)
1745 | t /= Placeholder
1746 = do env <- get
1747 (n', sc') <- if n `elem` env
1748 then do let n' = uniqueName n (env ++ inScope)
1749 return (n', shadow n n' sc)
1750 else return (n, sc)
1751 put (n' : env)
1752 t' <- mkUniq t
1753 sc'' <- mkUniq sc'
1754 return $! PDPair fc p (PRef fc' n') t' sc''
1755 mkUniq (PDPair fc p l t r)
1756 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1757 return $! PDPair fc p l' t' r'
1758 mkUniq (PAlternative b as)
1759 = liftM (PAlternative b) (mapM mkUniq as)
1760 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1761 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1762 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1763 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1764 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1765 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1766 mkUniq t = return t