git.iko.soy/Idris-dev
on df5bf81 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1129 lines 46 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import Idris.AbsSyntaxTree
11import IRTS.CodegenCommon
13import Paths_idris
15import System.Console.Haskeline
17import Control.Monad.State
19import Data.List
20import Data.Char
21import Data.Either
23import Debug.Trace
25import Util.Pretty
28getContext :: Idris Context
29getContext = do i <- getIState; return (tt_ctxt i)
31getObjectFiles :: Idris [FilePath]
32getObjectFiles = do i <- getIState; return (idris_objs i)
34addObjectFile :: FilePath -> Idris ()
35addObjectFile f = do i <- getIState; putIState $ i { idris_objs = f : idris_objs i }
37getLibs :: Idris [String]
38getLibs = do i <- getIState; return (idris_libs i)
40addLib :: String -> Idris ()
41addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }
43addHdr :: String -> Idris ()
44addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }
46totcheck :: (FC, Name) -> Idris ()
47totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
49setFlags :: Name -> [FnOpt] -> Idris ()
50setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
52setAccessibility :: Name -> Accessibility -> Idris ()
53setAccessibility n a
54 = do i <- getIState
55 let ctxt = setAccess n a (tt_ctxt i)
56 putIState $ i { tt_ctxt = ctxt }
58setTotality :: Name -> Totality -> Idris ()
59setTotality n a
60 = do i <- getIState
61 let ctxt = setTotal n a (tt_ctxt i)
62 putIState $ i { tt_ctxt = ctxt }
64getTotality :: Name -> Idris Totality
65getTotality n
66 = do i <- getIState
67 case lookupTotal n (tt_ctxt i) of
68 [t] -> return t
69 _ -> return (Total [])
71-- Get coercions which might return the required type
72getCoercionsTo :: IState -> Type -> [Name]
73getCoercionsTo i ty =
74 let cs = idris_coercions i
75 (fn,_) = unApply (getRetTy ty) in
76 findCoercions fn cs
77 where findCoercions t [] = []
78 findCoercions t (n : ns) =
79 let ps = case lookupTy Nothing n (tt_ctxt i) of
80 [ty] -> case unApply (getRetTy ty) of
81 (t', _) ->
82 if t == t' then [n] else []
83 _ -> [] in
84 ps ++ findCoercions t ns
86addToCG :: Name -> CGInfo -> Idris ()
87addToCG n cg
88 = do i <- getIState
89 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
91addCoercion :: Name -> Idris ()
92addCoercion n = do i <- getIState
93 putIState $ i { idris_coercions = n : idris_coercions i }
95addDocStr :: Name -> String -> Idris ()
96addDocStr n doc
97 = do i <- getIState
98 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
100addToCalledG :: Name -> [Name] -> Idris ()
101addToCalledG n ns = return () -- TODO
103-- Add a class instance function. Dodgy hack: Put integer instances first in the
104-- list so they are resolved by default.
105-- Dodgy hack 2: put constraint chasers (@@) last
107addInstance :: Bool -> Name -> Name -> Idris ()
108addInstance int n i
109 = do ist <- getIState
110 case lookupCtxt Nothing n (idris_classes ist) of
111 [CI a b c d ins] ->
112 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
113 putIState $ ist { idris_classes = cs }
114 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
115 putIState $ ist { idris_classes = cs }
116 where addI i ins | int = i : ins
117 | chaser n = ins ++ [i]
118 | otherwise = insI i ins
119 insI i [] = [i]
120 insI i (n : ns) | chaser n = i : n : ns
121 | otherwise = n : insI i ns
123 chaser (UN ('@':'@':_)) = True
124 chaser (NS n _) = chaser n
125 chaser _ = False
127addClass :: Name -> ClassInfo -> Idris ()
128addClass n i
129 = do ist <- getIState
130 let i' = case lookupCtxt Nothing n (idris_classes ist) of
131 [c] -> c { class_instances = class_instances i }
132 _ -> i
133 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
135addIBC :: IBCWrite -> Idris ()
136addIBC ibc@(IBCDef n)
137 = do i <- getIState
138 when (notDef (ibc_write i)) $
139 putIState $ i { ibc_write = ibc : ibc_write i }
140 where notDef [] = True
141 notDef (IBCDef n': is) | n == n' = False
142 notDef (_ : is) = notDef is
143addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
145clearIBC :: Idris ()
146clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
148getHdrs :: Idris [String]
149getHdrs = do i <- getIState; return (idris_hdrs i)
151setErrLine :: Int -> Idris ()
152setErrLine x = do i <- getIState;
153 case (errLine i) of
154 Nothing -> putIState $ i { errLine = Just x }
155 Just _ -> return ()
157clearErr :: Idris ()
158clearErr = do i <- getIState
159 putIState $ i { errLine = Nothing }
161getSO :: Idris (Maybe String)
162getSO = do i <- getIState
163 return (compiled_so i)
165setSO :: Maybe String -> Idris ()
166setSO s = do i <- getIState
167 putIState $ (i { compiled_so = s })
169getIState :: Idris IState
170getIState = get
172putIState :: IState -> Idris ()
173putIState = put
175getName :: Idris Int
176getName = do i <- getIState;
177 let idx = idris_name i;
178 putIState $ (i { idris_name = idx + 1 })
179 return idx
181checkUndefined :: FC -> Name -> Idris ()
182checkUndefined fc n
183 = do i <- getContext
184 case lookupTy Nothing n i of
185 (_:_) -> fail $ show fc ++ ":" ++
186 show n ++ " already defined"
187 _ -> return ()
189isUndefined :: FC -> Name -> Idris Bool
190isUndefined fc n
191 = do i <- getContext
192 case lookupTy Nothing n i of
193 (_:_) -> return False
194 _ -> return True
196setContext :: Context -> Idris ()
197setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
199updateContext :: (Context -> Context) -> Idris ()
200updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
202addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
203addConstraints fc (v, cs)
204 = do i <- getIState
205 let ctxt = tt_ctxt i
206 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
207 next_tvar = v }
208 let ics = zip cs (repeat fc) ++ idris_constraints i
209 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
211addDeferred :: [(Name, Type)] -> Idris ()
212addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
213 i <- getIState
214 putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
215 where tidyNames used (Bind (MN i x) b sc)
216 = let n' = uniqueName (UN x) used in
217 Bind n' b $ tidyNames (n':used) sc
218 tidyNames used (Bind n b sc)
219 = let n' = uniqueName n used in
220 Bind n' b $ tidyNames (n':used) sc
221 tidyNames used b = b
223solveDeferred :: Name -> Idris ()
224solveDeferred n = do i <- getIState
225 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
227iputStrLn :: String -> Idris ()
228iputStrLn = liftIO . putStrLn
230iWarn :: FC -> String -> Idris ()
231iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
233setLogLevel :: Int -> Idris ()
234setLogLevel l = do i <- getIState
235 let opts = idris_options i
236 let opt' = opts { opt_logLevel = l }
237 putIState $ i { idris_options = opt' }
239setCmdLine :: [Opt] -> Idris ()
240setCmdLine opts = do i <- getIState
241 let iopts = idris_options i
242 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
244getDumpDefun :: Idris (Maybe FilePath)
245getDumpDefun = do i <- getIState
246 return $ findC (opt_cmdline (idris_options i))
247 where findC [] = Nothing
248 findC (DumpDefun x : _) = Just x
249 findC (_ : xs) = findC xs
251getDumpCases :: Idris (Maybe FilePath)
252getDumpCases = do i <- getIState
253 return $ findC (opt_cmdline (idris_options i))
254 where findC [] = Nothing
255 findC (DumpCases x : _) = Just x
256 findC (_ : xs) = findC xs
258logLevel :: Idris Int
259logLevel = do i <- getIState
260 return (opt_logLevel (idris_options i))
262setErrContext :: Bool -> Idris ()
263setErrContext t = do i <- getIState
264 let opts = idris_options i
265 let opt' = opts { opt_errContext = t }
266 putIState $ i { idris_options = opt' }
268errContext :: Idris Bool
269errContext = do i <- getIState
270 return (opt_errContext (idris_options i))
272useREPL :: Idris Bool
273useREPL = do i <- getIState
274 return (opt_repl (idris_options i))
276setREPL :: Bool -> Idris ()
277setREPL t = do i <- getIState
278 let opts = idris_options i
279 let opt' = opts { opt_repl = t }
280 putIState $ i { idris_options = opt' }
282setTarget :: Target -> Idris ()
283setTarget t = do i <- getIState
284 let opts = idris_options i
285 let opt' = opts { opt_target = t }
286 putIState $ i { idris_options = opt' }
288target :: Idris Target
289target = do i <- getIState
290 return (opt_target (idris_options i))
292setOutputTy :: OutputType -> Idris ()
293setOutputTy t = do i <- getIState
294 let opts = idris_options i
295 let opt' = opts { opt_outputTy = t }
296 putIState $ i { idris_options = opt' }
298outputTy :: Idris OutputType
299outputTy = do i <- getIState
300 return $ opt_outputTy $ idris_options i
302verbose :: Idris Bool
303verbose = do i <- getIState
304 return (opt_verbose (idris_options i))
306setVerbose :: Bool -> Idris ()
307setVerbose t = do i <- getIState
308 let opts = idris_options i
309 let opt' = opts { opt_verbose = t }
310 putIState $ i { idris_options = opt' }
312typeInType :: Idris Bool
313typeInType = do i <- getIState
314 return (opt_typeintype (idris_options i))
316setTypeInType :: Bool -> Idris ()
317setTypeInType t = do i <- getIState
318 let opts = idris_options i
319 let opt' = opts { opt_typeintype = t }
320 putIState $ i { idris_options = opt' }
322coverage :: Idris Bool
323coverage = do i <- getIState
324 return (opt_coverage (idris_options i))
326setCoverage :: Bool -> Idris ()
327setCoverage t = do i <- getIState
328 let opts = idris_options i
329 let opt' = opts { opt_coverage = t }
330 putIState $ i { idris_options = opt' }
332setIBCSubDir :: FilePath -> Idris ()
333setIBCSubDir fp = do i <- getIState
334 let opts = idris_options i
335 let opt' = opts { opt_ibcsubdir = fp }
336 putIState $ i { idris_options = opt' }
338valIBCSubDir :: IState -> Idris FilePath
339valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
341addImportDir :: FilePath -> Idris ()
342addImportDir fp = do i <- getIState
343 let opts = idris_options i
344 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
345 putIState $ i { idris_options = opt' }
347setImportDirs :: [FilePath] -> Idris ()
348setImportDirs fps = do i <- getIState
349 let opts = idris_options i
350 let opt' = opts { opt_importdirs = fps }
351 putIState $ i { idris_options = opt' }
353allImportDirs :: IState -> Idris [FilePath]
354allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
355 return ("." : optdirs)
357impShow :: Idris Bool
358impShow = do i <- getIState
359 return (opt_showimp (idris_options i))
361setImpShow :: Bool -> Idris ()
362setImpShow t = do i <- getIState
363 let opts = idris_options i
364 let opt' = opts { opt_showimp = t }
365 putIState $ i { idris_options = opt' }
367logLvl :: Int -> String -> Idris ()
368logLvl l str = do i <- getIState
369 let lvl = opt_logLevel (idris_options i)
370 when (lvl >= l)
371 $ do liftIO (putStrLn str)
372 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
374cmdOptType :: Opt -> Idris Bool
375cmdOptType x = do i <- getIState
376 return $ x `elem` opt_cmdline (idris_options i)
378iLOG :: String -> Idris ()
379iLOG = logLvl 1
381noErrors :: Idris Bool
382noErrors = do i <- getIState
383 case errLine i of
384 Nothing -> return True
385 _ -> return False
387setTypeCase :: Bool -> Idris ()
388setTypeCase t = do i <- getIState
389 let opts = idris_options i
390 let opt' = opts { opt_typecase = t }
391 putIState $ i { idris_options = opt' }
394-- For inferring types of things
396bi = FC "builtin" 0
398inferTy = MN 0 "__Infer"
399inferCon = MN 0 "__infer"
400inferDecl = PDatadecl inferTy
401 PType
402 [("", inferCon, PPi impl (MN 0 "A") PType (
403 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
404 (PRef bi inferTy)), bi)]
406infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
407infP = P (TCon 6 0) inferTy (TType (UVal 0))
409getInferTerm, getInferType :: Term -> Term
410getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
411getInferTerm (App (App _ _) tm) = tm
412getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
414getInferType (Bind n b sc) = Bind n b $ getInferType sc
415getInferType (App (App _ ty) _) = ty
417-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
419primNames = [unitTy, unitCon,
420 falseTy, pairTy, pairCon,
421 eqTy, eqCon, inferTy, inferCon]
423unitTy = MN 0 "__Unit"
424unitCon = MN 0 "__II"
425unitDecl = PDatadecl unitTy PType
426 [("", unitCon, PRef bi unitTy, bi)]
428falseTy = MN 0 "__False"
429falseDecl = PDatadecl falseTy PType []
431pairTy = MN 0 "__Pair"
432pairCon = MN 0 "__MkPair"
433pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
434 [("", pairCon, PPi impl (n "A") PType (
435 PPi impl (n "B") PType (
436 PPi expl (n "a") (PRef bi (n "A")) (
437 PPi expl (n "b") (PRef bi (n "B"))
438 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
439 pexp (PRef bi (n "B"))])))), bi)]
440 where n a = MN 0 a
442eqTy = UN "="
443eqCon = UN "refl"
444eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
445 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
446 PType)
447 [("", eqCon, PPi impl (n "a") PType (
448 PPi impl (n "x") (PRef bi (n "a"))
449 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
450 pimp (n "b") Placeholder,
451 pexp (PRef bi (n "x")),
452 pexp (PRef bi (n "x"))])), bi)]
453 where n a = MN 0 a
455-- Defined in builtins.idr
456sigmaTy = UN "Exists"
457existsCon = UN "Ex_intro"
459piBind :: [(Name, PTerm)] -> PTerm -> PTerm
460piBind = piBindp expl
462piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
463piBindp p [] t = t
464piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
466-- Dealing with parameters
468expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
469 [Name] -> -- all names
470 [Name] -> -- names with no declaration
471 PTerm -> PTerm
472expandParams dec ps ns infs tm = en tm
473 where
474 -- if we shadow a name (say in a lambda binding) that is used in a call to
475 -- a lifted function, we need access to both names - once in the scope of the
476 -- binding and once to call the lifted functions. So we'll explicitly shadow
477 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
478 -- but we didn't...)
480 mkShadow (UN n) = MN 0 n
481 mkShadow (MN i n) = MN (i+1) n
482 mkShadow (NS x s) = NS (mkShadow x) s
484 en (PLam n t s)
485 | n `elem` map fst ps
486 = let n' = mkShadow n in
487 PLam n' (en t) (en (shadow n n' s))
488 | otherwise = PLam n (en t) (en s)
489 en (PPi p n t s)
490 | n `elem` map fst ps
491 = let n' = mkShadow n in
492 PPi p n' (en t) (en (shadow n n' s))
493 | otherwise = PPi p n (en t) (en s)
494 en (PLet n ty v s)
495 | n `elem` map fst ps
496 = let n' = mkShadow n in
497 PLet n' (en ty) (en v) (en (shadow n n' s))
498 | otherwise = PLet n (en ty) (en v) (en s)
499 en (PEq f l r) = PEq f (en l) (en r)
500 en (PTyped l r) = PTyped (en l) (en r)
501 en (PPair f l r) = PPair f (en l) (en r)
502 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
503 en (PAlternative a as) = PAlternative a (map en as)
504 en (PHidden t) = PHidden (en t)
505 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
506 en (PProof ts) = PProof (map (fmap en) ts)
507 en (PTactics ts) = PTactics (map (fmap en) ts)
509 en (PQuote (Var n))
510 | n `nselem` ns = PQuote (Var (dec n))
511 en (PApp fc (PInferRef fc' n) as)
512 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
513 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
514 en (PApp fc (PRef fc' n) as)
515 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
516 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
517 | n `nselem` ns = PApp fc (PRef fc' (dec n))
518 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
519 en (PRef fc n)
520 | n `elem` infs = PApp fc (PInferRef fc (dec n))
521 (map (pexp . (PRef fc)) (map fst ps))
522 | n `nselem` ns = PApp fc (PRef fc (dec n))
523 (map (pexp . (PRef fc)) (map fst ps))
524 en (PInferRef fc n)
525 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
526 (map (pexp . (PRef fc)) (map fst ps))
527 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
528 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
529 en t = t
531 nselem x [] = False
532 nselem x (y : xs) | nseq x y = True
533 | otherwise = nselem x xs
535 nseq x y = nsroot x == nsroot y
537expandParamsD :: Bool -> -- True = RHS only
538 IState ->
539 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
540expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
541 = if n `elem` ns && (not rhsonly)
542 then -- trace (show (n, expandParams dec ps ns ty)) $
543 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
544 else --trace (show (n, expandParams dec ps ns ty)) $
545 PTy doc syn fc o n (expandParams dec ps ns [] ty)
546expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
547 = if n `elem` ns && (not rhsonly)
548 then -- trace (show (n, expandParams dec ps ns ty)) $
549 PPostulate doc syn fc o (dec n) (piBind ps
550 (expandParams dec ps ns [] ty))
551 else --trace (show (n, expandParams dec ps ns ty)) $
552 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
553expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
554 = let n' = if n `elem` ns then dec n else n in
555 PClauses fc opts n' (map expandParamsC cs)
556 where
557 expandParamsC (PClause fc n lhs ws rhs ds)
558 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
559 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
560 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
561 n' = if n `elem` ns then dec n else n in
562 PClause fc n' lhs'
563 (map (expandParams dec ps'' ns []) ws)
564 (expandParams dec ps'' ns [] rhs)
565 (map (expandParamsD True ist dec ps'' ns) ds)
566 expandParamsC (PWith fc n lhs ws wval ds)
567 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
568 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
569 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
570 n' = if n `elem` ns then dec n else n in
571 PWith fc n' lhs'
572 (map (expandParams dec ps'' ns []) ws)
573 (expandParams dec ps'' ns [] wval)
574 (map (expandParamsD rhsonly ist dec ps'' ns) ds)
575 updateps yn nm [] = []
576 updateps yn nm (((a, t), i):as)
577 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
578 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
579expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
580 = PData doc syn fc co (expandPData pd)
581 where
582 -- just do the type decl, leave constructors alone (parameters will be
583 -- added implicitly)
584 expandPData (PDatadecl n ty cons)
585 = if n `elem` ns
586 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
587 (map econ cons)
588 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
589 econ (doc, n, t, fc)
590 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
591expandParamsD rhs ist dec ps ns (PParams f params pds)
592 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
593 (map (expandParamsD True ist dec ps ns) pds)
594-- (map (expandParamsD ist dec ps ns) pds)
595expandParamsD rhs ist dec ps ns (PMutual f pds)
596 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
597expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
598 = PClass doc info f
599 (map (expandParams dec ps ns []) cs)
600 n
601 (map (mapsnd (expandParams dec ps ns [])) params)
602 (map (expandParamsD rhs ist dec ps ns) decls)
603expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
604 = PInstance info f
605 (map (expandParams dec ps ns []) cs)
606 n
607 (map (expandParams dec ps ns []) params)
608 (expandParams dec ps ns [] ty)
609 cn
610 (map (expandParamsD rhs ist dec ps ns) decls)
611expandParamsD rhs ist dec ps ns d = d
613mapsnd f (x, t) = (x, f t)
615-- Calculate a priority for a type, for deciding elaboration order
616-- * if it's just a type variable or concrete type, do it early (0)
617-- * if there's only type variables and injective constructors, do it next (1)
618-- * if there's a function type, next (2)
619-- * finally, everything else (3)
621getPriority :: IState -> PTerm -> Int
622getPriority i tm = 1 -- pri tm
623 where
624 pri (PRef _ n) =
625 case lookupP Nothing n (tt_ctxt i) of
626 ((P (DCon _ _) _ _):_) -> 1
627 ((P (TCon _ _) _ _):_) -> 1
628 ((P Ref _ _):_) -> 1
629 [] -> 0 -- must be locally bound, if it's not an error...
630 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
631 pri (PTrue _) = 0
632 pri (PFalse _) = 0
633 pri (PRefl _ _) = 1
634 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
635 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
636 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
637 pri (PTyped l r) = pri l
638 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
639 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
640 pri (PAlternative a as) = maximum (map pri as)
641 pri (PConstant _) = 0
642 pri Placeholder = 1
643 pri _ = 3
645addStatics :: Name -> Term -> PTerm -> Idris ()
646addStatics n tm ptm =
647 do let (statics, dynamics) = initStatics tm ptm
648 let stnames = nub $ concatMap freeNames (map snd statics)
649 let dnames = nub $ concatMap freeNames (map snd dynamics)
650 when (not (null statics)) $
651 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
652 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
653 let statics' = nub $ map fst statics ++
654 filter (\x -> not (elem x dnames)) stnames
655 let stpos = staticList statics' tm
656 i <- getIState
657 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
658 addIBC (IBCStatic n)
659 where
660 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
661 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
662 if pstatic p == Static then ((n, ty) : static, dynamic)
663 else (static, (n, ty) : dynamic)
664 initStatics t pt = ([], [])
666 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
667 staticList _ _ = []
669-- Dealing with implicit arguments
671-- Add implicit Pi bindings for any names in the term which appear in an
672-- argument position.
674-- This has become a right mess already. Better redo it some time...
676implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
677implicit syn n ptm = implicit' syn [] n ptm
679implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
680implicit' syn ignore n ptm
681 = do i <- getIState
682 let (tm', impdata) = implicitise syn ignore i ptm
683-- let (tm'', spos) = findStatics i tm'
684 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
685 addIBC (IBCImp n)
686 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
687-- i <- get
688-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
689 return tm'
691implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
692implicitise syn ignore ist tm
693 = let (declimps, ns') = execState (imps True [] tm) ([], [])
694 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
695 ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
696 if null ns
697 then (tm, reverse declimps)
698 else implicitise syn ignore ist (pibind uvars ns tm)
699 where
700 uvars = using syn
701 pvars = syn_params syn
703 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
704 | otherwise = x : dropAll xs ys
705 dropAll [] ys = []
707 imps top env (PApp _ f as)
708 = do (decls, ns) <- get
709 let isn = concatMap (namesIn uvars ist) (map getTm as)
710 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
711 imps top env (PPi (Imp l _ doc) n ty sc)
712 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
713 (decls , ns) <- get
714 put (PImp (getPriority ist ty) l n ty doc : decls,
715 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
716 imps True (n:env) sc
717 imps top env (PPi (Exp l _ doc) n ty sc)
718 = do let isn = nub (namesIn uvars ist ty ++ case sc of
719 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
720 _ -> [])
721 (decls, ns) <- get -- ignore decls in HO types
722 put (PExp (getPriority ist ty) l ty doc : decls,
723 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
724 imps True (n:env) sc
725 imps top env (PPi (Constraint l _ doc) n ty sc)
726 = do let isn = nub (namesIn uvars ist ty ++ case sc of
727 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
728 _ -> [])
729 (decls, ns) <- get -- ignore decls in HO types
730 put (PConstraint 10 l ty doc : decls,
731 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
732 imps True (n:env) sc
733 imps top env (PPi (TacImp l _ scr doc) n ty sc)
734 = do let isn = nub (namesIn uvars ist ty ++ case sc of
735 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
736 _ -> [])
737 (decls, ns) <- get -- ignore decls in HO types
738 put (PTacImplicit 10 l n scr ty doc : decls,
739 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
740 imps True (n:env) sc
741 imps top env (PEq _ l r)
742 = do (decls, ns) <- get
743 let isn = namesIn uvars ist l ++ namesIn uvars ist r
744 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
745 imps top env (PTyped l r)
746 = imps top env l
747 imps top env (PPair _ l r)
748 = do (decls, ns) <- get
749 let isn = namesIn uvars ist l ++ namesIn uvars ist r
750 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
751 imps top env (PDPair _ (PRef _ n) t r)
752 = do (decls, ns) <- get
753 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
754 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
755 imps top env (PDPair _ l t r)
756 = do (decls, ns) <- get
757 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
758 namesIn uvars ist r
759 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
760 imps top env (PAlternative a as)
761 = do (decls, ns) <- get
762 let isn = concatMap (namesIn uvars ist) as
763 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
764 imps top env (PLam n ty sc)
765 = do imps False env ty
766 imps False (n:env) sc
767 imps top env (PHidden tm) = imps False env tm
768 imps top env _ = return ()
770 pibind using [] sc = sc
771 pibind using (n:ns) sc
772 = case lookup n using of
773 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
774 Nothing -> PPi (Imp False Dynamic "") n Placeholder
775 (pibind using ns sc)
777-- Add implicit arguments in function calls
778addImplPat :: IState -> PTerm -> PTerm
779addImplPat = addImpl' True [] []
781addImplBound :: IState -> [Name] -> PTerm -> PTerm
782addImplBound ist ns = addImpl' False ns [] ist
784addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
785addImplBoundInf ist ns inf = addImpl' False ns inf ist
787addImpl :: IState -> PTerm -> PTerm
788addImpl = addImpl' False [] []
790-- TODO: in patterns, don't add implicits to function names guarded by constructors
791-- and *not* inside a PHidden
793addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
794addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
795 where
796 ai env (PRef fc f)
797 | f `elem` infns = PInferRef fc f
798 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
799 ai env (PHidden (PRef fc f))
800 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
801 ai env (PEq fc l r) = let l' = ai env l
802 r' = ai env r in
803 PEq fc l' r'
804 ai env (PTyped l r) = let l' = ai env l
805 r' = ai env r in
806 PTyped l' r'
807 ai env (PPair fc l r) = let l' = ai env l
808 r' = ai env r in
809 PPair fc l' r'
810 ai env (PDPair fc l t r) = let l' = ai env l
811 t' = ai env t
812 r' = ai env r in
813 PDPair fc l' t' r'
814 ai env (PAlternative a as) = let as' = map (ai env) as in
815 PAlternative a as'
816 ai env (PApp fc (PInferRef _ f) as)
817 = let as' = map (fmap (ai env)) as in
818 PApp fc (PInferRef fc f) as'
819 ai env (PApp fc ftm@(PRef _ f) as)
820 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
821 | not (f `elem` map fst env)
822 = let as' = map (fmap (ai env)) as in
823 handleErr $ aiFn inpat False ist fc f as'
824 | Just (Just ty) <- lookup f env
825 = let as' = map (fmap (ai env)) as
826 arity = getPArity ty in
827 mkPApp fc arity ftm as'
828 ai env (PApp fc f as) = let f' = ai env f
829 as' = map (fmap (ai env)) as in
830 mkPApp fc 1 f' as'
831 ai env (PCase fc c os) = let c' = ai env c
832 os' = map (pmap (ai env)) os in
833 PCase fc c' os'
834 ai env (PLam n ty sc) = let ty' = ai env ty
835 sc' = ai ((n, Just ty):env) sc in
836 PLam n ty' sc'
837 ai env (PLet n ty val sc)
838 = let ty' = ai env ty
839 val' = ai env val
840 sc' = ai ((n, Just ty):env) sc in
841 PLet n ty' val' sc'
842 ai env (PPi p n ty sc) = let ty' = ai env ty
843 sc' = ai ((n, Just ty):env) sc in
844 PPi p n ty' sc'
845 ai env (PHidden tm) = PHidden (ai env tm)
846 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
847 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
848 ai env tm = tm
850 handleErr (Left err) = PElabError err
851 handleErr (Right x) = x
853-- if in a pattern, and there are no arguments, and there's no possible
854-- names with zero explicit arguments, don't add implicits.
856aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
857aiFn inpat True ist fc f []
858 = case lookupDef Nothing f (tt_ctxt ist) of
859 [] -> Right $ PPatvar fc f
860 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
861 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
862 if (not (vname f) || tcname f
863 || any constructor alts || any allImp ialts)
864 then aiFn inpat False ist fc f [] -- use it as a constructor
865 else Right $ PPatvar fc f
866 where imp (PExp _ _ _ _) = False
867 imp _ = True
868 allImp [] = False
869 allImp xs = all imp xs
870 constructor (TyDecl (DCon _ _) _) = True
871 constructor _ = False
873 vname (UN n) = True -- non qualified
874 vname _ = False
876aiFn inpat expat ist fc f as
877 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
878aiFn inpat expat ist fc f as
879 -- This is where namespaces get resolved by adding PAlternative
880 = case lookupCtxtName Nothing f (idris_implicits ist) of
881 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
882 [] -> if f `elem` idris_metavars ist
883 then Right $ PApp fc (PRef fc f) as
884 else Right $ mkPApp fc (length as) (PRef fc f) as
885 alts -> Right $
886 PAlternative True $
887 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
888 (insertImpl ns as)) alts
889 where
890 insertImpl :: [PArg] -> [PArg] -> [PArg]
891 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
892 PExp p l tm d : insertImpl ps given
893 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
894 PConstraint p l tm d : insertImpl ps given
895 insertImpl (PConstraint p l ty d : ps) given =
896 PConstraint p l (PResolveTC fc) d : insertImpl ps given
897 insertImpl (PImp p l n ty d : ps) given =
898 case find n given [] of
899 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
900 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
901 insertImpl (PTacImplicit p l n sc ty d : ps) given =
902 case find n given [] of
903 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
904 Nothing -> if inpat
905 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
906 else PTacImplicit p l n sc sc "" : insertImpl ps given
907 insertImpl expected [] = []
908 insertImpl _ given = given
910 find n [] acc = Nothing
911 find n (PImp _ _ n' t _ : gs) acc
912 | n == n' = Just (t, reverse acc ++ gs)
913 find n (PTacImplicit _ _ n' _ t _ : gs) acc
914 | n == n' = Just (t, reverse acc ++ gs)
915 find n (g : gs) acc = find n gs (g : acc)
917mkPApp fc a f [] = f
918mkPApp fc a f as = let rest = drop a as in
919 appRest fc (PApp fc f (take a as)) rest
920 where
921 appRest fc f [] = f
922 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
924-- Find 'static' argument positions
925-- (the declared ones, plus any names in argument position in the declared
926-- statics)
927-- FIXME: It's possible that this really has to happen after elaboration
929findStatics :: IState -> PTerm -> (PTerm, [Bool])
930findStatics ist tm = trace (showImp True tm) $
931 let (ns, ss) = fs tm in
932 runState (pos ns ss tm) []
933 where fs (PPi p n t sc)
934 | Static <- pstatic p
935 = let (ns, ss) = fs sc in
936 (namesIn [] ist t : ns, n : ss)
937 | otherwise = let (ns, ss) = fs sc in
938 (ns, ss)
939 fs _ = ([], [])
941 inOne n ns = length (filter id (map (elem n) ns)) == 1
943 pos ns ss (PPi p n t sc)
944 | elem n ss = do sc' <- pos ns ss sc
945 spos <- get
946 put (True : spos)
947 return (PPi (p { pstatic = Static }) n t sc')
948 | otherwise = do sc' <- pos ns ss sc
949 spos <- get
950 put (False : spos)
951 return (PPi p n t sc')
952 pos ns ss t = return t
954-- Debugging/logging stuff
956dumpDecls :: [PDecl] -> String
957dumpDecls [] = ""
958dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
960dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
961dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
962dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
963dumpDecl (PData _ _ _ _ d) = showDImp True d
964dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
965dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
966dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
967dumpDecl (PClass _ _ _ cs n ps ds)
968 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
969dumpDecl (PInstance _ _ cs n _ t _ ds)
970 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
971dumpDecl _ = "..."
972-- dumpDecl (PImport i) = "import " ++ i
974-- for 6.12/7 compatibility
975data EitherErr a b = LeftErr a | RightOK b
977instance Monad (EitherErr a) where
978 return = RightOK
980 (LeftErr e) >>= k = LeftErr e
981 RightOK v >>= k = k v
983toEither (LeftErr e) = Left e
984toEither (RightOK ho) = Right ho
986-- syntactic match of a against b, returning pair of variables in a
987-- and what they match. Returns the pair that failed if not a match.
989matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
990matchClause = matchClause' False
992matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
993matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
994 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
996 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
997 fullApp x = x
999 match' x y = match (fullApp x) (fullApp y)
1000 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1001 | PConstant (I _) <- getTm x = match (getTm x) x'
1002 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1003 | PConstant (I _) <- getTm x = match (getTm x) x'
1004 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1005 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1006 match (PApp _ f args) (PApp _ f' args')
1007 | length args == length args'
1008 = do mf <- match' f f'
1009 ms <- zipWithM matchArg args args'
1010 return (mf ++ concat ms)
1011-- match (PRef _ n) (PRef _ n') | n == n' = return []
1012-- | otherwise = Nothing
1013 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1014 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1015 match (PRef _ n) tm@(PRef _ n')
1016 | n == n' && not names &&
1017 (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1018 = return [(n, tm)]
1019 | n == n' = return []
1020 match (PRef _ n) tm
1021 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1022 = return [(n, tm)]
1023 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1024 mr <- match' r r'
1025 return (ml ++ mr)
1026 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1027 mr <- match r r'
1028 return (ml ++ mr)
1029 match (PTyped l r) x = match l x
1030 match x (PTyped l r) = match x l
1031 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1032 mr <- match' r r'
1033 return (ml ++ mr)
1034 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1035 mt <- match' t t'
1036 mr <- match' r r'
1037 return (ml ++ mt ++ mr)
1038 match (PAlternative a as) (PAlternative a' as')
1039 = do ms <- zipWithM match' as as'
1040 return (concat ms)
1041 match a@(PAlternative _ as) b
1042 = do let ms = zipWith match' as (repeat b)
1043 case (rights (map toEither ms)) of
1044 (x: _) -> return x
1045 _ -> LeftErr (a, b)
1046 match (PCase _ _ _) _ = return [] -- lifted out
1047 match (PMetavar _) _ = return [] -- modified
1048 match (PInferRef _ _) _ = return [] -- modified
1049 match (PQuote _) _ = return []
1050 match (PProof _) _ = return []
1051 match (PTactics _) _ = return []
1052 match (PRefl _ _) (PRefl _ _) = return []
1053 match (PResolveTC _) (PResolveTC _) = return []
1054 match (PTrue _) (PTrue _) = return []
1055 match (PFalse _) (PFalse _) = return []
1056 match (PReturn _) (PReturn _) = return []
1057 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1058 ms <- match' s s'
1059 return (mt ++ ms)
1060 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1061 ms <- match' s s'
1062 return (mt ++ ms)
1063 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1064 mty <- match' ty ty'
1065 ms <- match' s s'
1066 return (mt ++ mty ++ ms)
1067 match (PHidden x) (PHidden y) = match' x y
1068 match Placeholder _ = return []
1069 match _ Placeholder = return []
1070 match (PResolveTC _) _ = return []
1071 match a b | a == b = return []
1072 | otherwise = LeftErr (a, b)
1074 checkRpts (RightOK ms) = check ms where
1075 check ((n,t):xs)
1076 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1077 then Left (t, t')
1078 else check xs
1079 check (_:xs) = check xs
1080 check [] = Right ms
1081 checkRpts (LeftErr x) = Left x
1083substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1084substMatches ms = substMatchesShadow ms []
1086substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1087substMatchesShadow [] shs t = t
1088substMatchesShadow ((n,tm):ns) shs t
1089 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1091substMatch :: Name -> PTerm -> PTerm -> PTerm
1092substMatch n = substMatchShadow n []
1094substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1095substMatchShadow n shs tm t = sm shs t where
1096 sm xs (PRef _ n') | n == n' = tm
1097 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1098 sm xs (PPi p x t sc)
1099 | x `elem` xs
1100 = let x' = nextName x in
1101 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1102 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1103 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1104 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)
1105 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1106 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1107 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1108 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1109 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1110 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1111 sm xs (PHidden x) = PHidden (sm xs x)
1112 sm xs x = x
1114shadow :: Name -> Name -> PTerm -> PTerm
1115shadow n n' t = sm t where
1116 sm (PRef fc x) | n == x = PRef fc n'
1117 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1118 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1119 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1120 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1121 sm (PEq f x y) = PEq f (sm x) (sm y)
1122 sm (PTyped x y) = PTyped (sm x) (sm y)
1123 sm (PPair f x y) = PPair f (sm x) (sm y)
1124 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1125 sm (PAlternative a as) = PAlternative a (map sm as)
1126 sm (PHidden x) = PHidden (sm x)
1127 sm x = x