git.iko.soy/Idris-dev
on b8a2bbf help sign in
Idris-dev/src/Idris/AbsSyntax.hs
625 lines 23 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
9import Control.Monad.State
10import Data.List
11import Data.Char
12import Debug.Trace
14import qualified Epic.Epic as E
16data IOption = IOption { opt_logLevel :: Int,
17 opt_typecase :: Bool
18 }
19 deriving (Show, Eq)
21defaultOpts = IOption 0 False
23-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
24-- without typechecking).
25-- This will include all the functions and data declarations, plus fixity declarations
26-- and syntax macros.
28data IState = IState { tt_ctxt :: Context,
29 idris_infixes :: [FixDecl],
30 idris_implicits :: Ctxt [PArg],
31 idris_log :: String,
32 idris_options :: IOption,
33 idris_name :: Int,
34 idris_metavars :: [Name],
35 syntax_rules :: [Syntax],
36 imported :: [FilePath],
37 idris_prims :: [(Name, ([E.Name], E.Term))]
38 }
40idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] []
42-- The monad for the main REPL - reading and processing files and updating
43-- global state (hence the IO inner monad).
44type Idris a = StateT IState IO a
46getContext :: Idris Context
47getContext = do i <- get; return (tt_ctxt i)
49getIState :: Idris IState
50getIState = get
52putIState :: IState -> Idris ()
53putIState = put
55getName :: Idris Int
56getName = do i <- get;
57 let idx = idris_name i;
58 put (i { idris_name = idx + 1 })
59 return idx
61checkUndefined :: FC -> Name -> Idris ()
62checkUndefined fc n
63 = do i <- getContext
64 case lookupCtxt n i of
65 Just _ -> fail $ show fc ++ ":" ++
66 show n ++ " already defined"
67 _ -> return ()
69setContext :: Context -> Idris ()
70setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
72updateContext :: (Context -> Context) -> Idris ()
73updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
75addDeferred :: [(Name, Type)] -> Idris ()
76addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns
77 i <- get
78 put (i { idris_metavars = map fst ns ++ idris_metavars i })
80solveDeferred :: Name -> Idris ()
81solveDeferred n = do i <- get
82 put (i { idris_metavars = idris_metavars i \\ [n] })
84iputStrLn :: String -> Idris ()
85iputStrLn = lift.putStrLn
87setLogLevel :: Int -> Idris ()
88setLogLevel l = do i <- get
89 let opts = idris_options i
90 let opt' = opts { opt_logLevel = l }
91 put (i { idris_options = opt' } )
93logLevel :: Idris Int
94logLevel = do i <- get
95 return (opt_logLevel (idris_options i))
97logLvl :: Int -> String -> Idris ()
98logLvl l str = do i <- get
99 let lvl = opt_logLevel (idris_options i)
100 when (lvl >= l)
101 $ do lift (putStrLn str)
102 put (i { idris_log = idris_log i ++ str ++ "\n" } )
104iLOG :: String -> Idris ()
105iLOG = logLvl 1
107setTypeCase :: Bool -> Idris ()
108setTypeCase t = do i <- get
109 let opts = idris_options i
110 let opt' = opts { opt_typecase = t }
111 put (i { idris_options = opt' })
113-- Commands in the REPL
115data Command = Quit | Help | Eval PTerm
116 | Compile String
117 | Metavars
118 | TTShell
119 | LogLvl Int
120 | NOP
122-- Parsed declarations
124data Fixity = Infixl { prec :: Int }
125 | Infixr { prec :: Int }
126 | InfixN { prec :: Int }
127 | PrefixN { prec :: Int }
128 deriving Eq
130instance Show Fixity where
131 show (Infixl i) = "infixl " ++ show i
132 show (Infixr i) = "infixr " ++ show i
133 show (InfixN i) = "infix " ++ show i
134 show (PrefixN i) = "prefix " ++ show i
136data FixDecl = Fix Fixity String
137 deriving (Show, Eq)
139instance Ord FixDecl where
140 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
142data Plicity = Imp | Exp deriving (Show, Eq)
144data PDecl' t = PFix FC Fixity [String] -- fixity declaration
145 | PTy FC Name t -- type declaration
146 | PClauses FC Name [PClause' t] -- pattern clause
147 | PData FC (PData' t) -- data declaration
148 | PParams FC [(Name, PTerm)] [PDecl' t] -- params block
149 | PSyntax FC Syntax
150 deriving Functor
152data PClause' t = PClause Name t [t] t [PDecl]
153 | PWith Name t [t] t [PDecl]
154 deriving Functor
156data PData' t = PDatadecl { d_name :: Name,
157 d_tcon :: t,
158 d_cons :: [(Name, t, FC)] }
159 deriving Functor
161-- Handy to get a free function for applying PTerm -> PTerm functions
162-- across a program, by deriving Functor
164type PDecl = PDecl' PTerm
165type PData = PData' PTerm
166type PClause = PClause' PTerm
168-- get all the names declared in a decl
170declared :: PDecl -> [Name]
171declared (PFix _ _ _) = []
172declared (PTy _ n t) = [n]
173declared (PClauses _ n _) = [] -- not a declaration
174declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts
175 where fstt (a, _, _) = a
176declared (PParams _ _ ds) = concatMap declared ds
177-- declared (PImport _) = []
179-- High level language terms
180--
181data PTerm = PQuote Raw
182 | PRef FC Name
183 | PLam Name PTerm PTerm
184 | PPi Plicity Name PTerm PTerm
185 | PLet Name PTerm PTerm PTerm
186 | PApp FC PTerm [PArg]
187 | PTrue FC
188 | PFalse FC
189 | PRefl FC
190 | PEq FC PTerm PTerm
191 | PPair FC PTerm PTerm
192 | PDPair FC PTerm PTerm
193 | PHidden PTerm -- irrelevant or hidden pattern
194 | PSet
195 | PConstant Const
196 | Placeholder
197 | PDoBlock [PDo]
198 | PReturn FC
199 | PMetavar Name
200 | PElabError String -- error to report on elaboration
201 deriving Eq
203data PDo = DoExp FC PTerm
204 | DoBind FC Name PTerm
205 | DoLet FC Name PTerm
206 deriving Eq
208data PArg' t = PImp { pname :: Name, getTm :: t }
209 | PExp { getTm :: t }
210 deriving (Show, Eq, Functor)
212type PArg = PArg' PTerm
214-- Syntactic sugar info (TODO: namespaces, modules)
216data DSL = DSL { dsl_bind :: Name,
217 dsl_return :: Name }
218 deriving Show
220data Syntax = Rule [SSymbol] PTerm
221 deriving Show
223data SSymbol = Keyword Name
224 | Symbol String
225 | Expr Name
226 deriving Show
228initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
230data SyntaxInfo = Syn { using :: [(Name, PTerm)],
231 syn_params :: [(Name, PTerm)],
232 no_imp :: [Name],
233 dsl_info :: DSL }
234 deriving Show
236defaultSyntax = Syn [] [] [] initDSL
238--- Pretty printing declarations and terms
240instance Show PTerm where
241 show tm = showImp False tm
243instance Show PDecl where
244 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
245 show (PTy _ n ty) = show n ++ " : " ++ show ty
246 show (PClauses _ n c) = showSep "\n" (map show c)
247 show (PData _ d) = show d
249instance Show PClause where
250 show c = showCImp True c
252instance Show PData where
253 show d = showDImp False d
255showCImp :: Bool -> PClause -> String
256showCImp impl (PClause n l ws r w)
257 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
258 ++ " where " ++ show w
259 where
260 showWs [] = ""
261 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
262showCImp impl (PWith n l ws r w)
263 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
264 ++ " { " ++ show w ++ " } "
265 where
266 showWs [] = ""
267 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
270showDImp :: Bool -> PData -> String
271showDImp impl (PDatadecl n ty cons)
272 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
273 ++ showSep "\n\t| "
274 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
276getImps :: [PArg] -> [(Name, PTerm)]
277getImps [] = []
278getImps (PImp n tm : xs) = (n, tm) : getImps xs
279getImps (_ : xs) = getImps xs
281getExps :: [PArg] -> [PTerm]
282getExps [] = []
283getExps (PExp tm : xs) = tm : getExps xs
284getExps (_ : xs) = getExps xs
286getAll :: [PArg] -> [PTerm]
287getAll = map getTm
289showImp :: Bool -> PTerm -> String
290showImp impl tm = se 10 tm where
291 se p (PQuote r) = "![" ++ show r ++ "]"
292 se p (PRef _ n) = show n
293 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
294 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
295 " in " ++ se 10 sc
296 se p (PPi Exp n ty sc)
297 | n `elem` allNamesIn sc = bracket p 2 $
298 "(" ++ show n ++ " : " ++ se 10 ty ++
299 ") -> " ++ se 10 sc
300 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
301 se p (PPi Imp n ty sc)
302 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
303 "} -> " ++ se 10 sc
304 | otherwise = se 10 sc
305 se p (PApp _ (PRef _ f) [])
306 | not impl = show f
307 se p (PApp _ (PRef _ op@(UN [f:_])) args)
308 | length (getExps args) == 2 && not impl && not (isAlpha f)
309 = let [l, r] = getExps args in
310 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
311 se p (PApp _ f as)
312 = let (imps, args) = (getImps as, getExps as) in
313 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
314 ++ concatMap seArg args
315 se p (PHidden tm) = "." ++ se 0 tm
316 se p (PRefl _) = "refl"
317 se p (PTrue _) = "()"
318 se p (PFalse _) = "_|_"
319 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
320 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
321 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
322 se p PSet = "Set"
323 se p (PConstant c) = show c
324 se p (PMetavar n) = "?" ++ show n
325 se p Placeholder = "_"
327 seArg arg = " " ++ se 0 arg
328 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
330 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
331 | otherwise = str
333allNamesIn :: PTerm -> [Name]
334allNamesIn tm = nub $ ni [] tm
335 where
336 ni env (PRef _ n)
337 | not (n `elem` env) = [n]
338 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
339 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
340 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
341 ni env (PHidden tm) = ni env tm
342 ni env (PEq _ l r) = ni env l ++ ni env r
343 ni env (PPair _ l r) = ni env l ++ ni env r
344 ni env (PDPair _ l r) = ni env l ++ ni env r
345 ni env _ = []
347namesIn :: IState -> PTerm -> [Name]
348namesIn ist tm = nub $ ni [] tm
349 where
350 ni env (PRef _ n)
351 | not (n `elem` env)
352 = case lookupCtxt n (idris_implicits ist) of
353 Nothing -> [n]
354 _ -> []
355 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
356 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
357 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
358 ni env (PEq _ l r) = ni env l ++ ni env r
359 ni env (PPair _ l r) = ni env l ++ ni env r
360 ni env (PDPair _ l r) = ni env l ++ ni env r
361 ni env (PHidden tm) = ni env tm
362 ni env _ = []
364-- For inferring types of things
366bi = FC "builtin" 0
368inferTy = MN 0 "__Infer"
369inferCon = MN 0 "__infer"
370inferDecl = PDatadecl inferTy
371 PSet
372 [(inferCon, PPi Imp (MN 0 "A") PSet (
373 PPi Exp (MN 0 "a") (PRef bi (MN 0 "A"))
374 (PRef bi inferTy)), bi)]
376infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
377infP = P (TCon 6 0) inferTy (Set 0)
379getInferTerm, getInferType :: Term -> Term
380getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
381getInferTerm (App (App _ _) tm) = tm
382getInferTerm tm = error ("getInferTerm " ++ show tm)
384getInferType (Bind n b sc) = Bind n b $ getInferType sc
385getInferType (App (App _ ty) _) = ty
387-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
389unitTy = MN 0 "__Unit"
390unitCon = MN 0 "__II"
391unitDecl = PDatadecl unitTy PSet
392 [(unitCon, PRef bi unitTy, bi)]
394falseTy = MN 0 "__False"
395falseDecl = PDatadecl falseTy PSet []
397pairTy = MN 0 "__Pair"
398pairCon = MN 0 "__MkPair"
399pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
400 [(pairCon, PPi Imp (n "A") PSet (
401 PPi Imp (n "B") PSet (
402 PPi Exp (n "a") (PRef bi (n "A")) (
403 PPi Exp (n "b") (PRef bi (n "B"))
404 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),
405 PExp (PRef bi (n "B"))])))), bi)]
406 where n a = MN 0 a
408eqTy = UN ["="]
409eqCon = UN ["refl"]
410eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
411 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
412 PSet)
413 [(eqCon, PPi Imp (n "a") PSet (
414 PPi Imp (n "x") (PRef bi (n "a"))
415 (PApp bi (PRef bi eqTy) [PImp (n "a") Placeholder,
416 PImp (n "b") Placeholder,
417 PExp (PRef bi (n "x")),
418 PExp (PRef bi (n "x"))])), bi)]
419 where n a = MN 0 a
421-- Defined in builtins.idr
422sigmaTy = UN ["Sigma"]
423existsCon = UN ["Exists"]
425piBind :: [(Name, PTerm)] -> PTerm -> PTerm
426piBind [] t = t
427piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
429-- Dealing with implicit arguments
431-- Add implicit Pi bindings for any names in the term which appear in an
432-- argument position.
434-- This has become a right mess already. Better redo it some time...
436implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
437implicitise syn ist tm
438 = let uvars = using syn
439 pvars = syn_params syn
440 (declimps, ns') = execState (imps True [] tm) ([], [])
441 ns = ns' \\ (map fst pvars ++ no_imp syn) in
442 if null ns
443 then (tm, reverse declimps)
444 else implicitise syn ist (pibind uvars ns tm)
445 where
446 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
447 | otherwise = x : dropAll xs ys
448 dropAll [] ys = []
450 imps top env (PApp _ f as)
451 = do (decls, ns) <- get
452 let isn = concatMap (namesIn ist) (map getTm as)
453 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
454 imps top env (PPi Imp n ty sc)
455 = do let isn = nub (namesIn ist ty) `dropAll` [n]
456 (decls , ns) <- get
457 put (PImp n ty : decls,
458 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
459 imps True (n:env) sc
460 imps top env (PPi Exp n ty sc)
461 = do let isn = nub (namesIn ist ty ++ case sc of
462 (PRef _ x) -> namesIn ist sc `dropAll` [n]
463 _ -> [])
464 (decls, ns) <- get -- ignore decls in HO types
465 put (PExp ty : decls,
466 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
467 imps True (n:env) sc
468 imps top env (PEq _ l r)
469 = do (decls, ns) <- get
470 let isn = namesIn ist l ++ namesIn ist r
471 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
472 imps top env (PPair _ l r)
473 = do (decls, ns) <- get
474 let isn = namesIn ist l ++ namesIn ist r
475 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
476 imps top env (PDPair _ (PRef _ n) r)
477 = do (decls, ns) <- get
478 let isn = nub (namesIn ist r) \\ [n]
479 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
480 imps top env (PDPair _ l r)
481 = do (decls, ns) <- get
482 let isn = namesIn ist l ++ namesIn ist r
483 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
484 imps top env (PLam n ty sc)
485 = do imps False env ty
486 imps False (n:env) sc
487 imps top env (PHidden tm) = imps False env tm
488 imps top env _ = return ()
490 pibind using [] sc = sc
491 pibind using (n:ns) sc = case lookup n using of
492 Just ty -> PPi Imp n ty (pibind using ns sc)
493 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
495-- Add implicit arguments in function calls
497addImpl :: IState -> PTerm -> PTerm
498addImpl ist ptm = ai [] ptm
499 where
500 ai env (PRef fc f) = aiFn fc env (PRef fc f) []
501 ai env (PEq fc l r) = let l' = ai env l
502 r' = ai env r in
503 PEq fc l' r'
504 ai env (PPair fc l r) = let l' = ai env l
505 r' = ai env r in
506 PPair fc l' r'
507 ai env (PDPair fc l r) = let l' = ai env l
508 r' = ai env r in
509 PDPair fc l' r'
510 ai env (PApp fc (PRef _ f) as)
511 = let as' = map (fmap (ai env)) as in
512 aiFn fc env (PRef fc f) as'
513 ai env (PApp fc f as) = let f' = ai env f
514 as' = map (fmap (ai env)) as in
515 aiFn fc env f' as'
516 ai env (PLam n ty sc) = let ty' = ai env ty
517 sc' = ai (n:env) sc in
518 PLam n ty' sc'
519 ai env (PLet n ty val sc)
520 = let ty' = ai env ty
521 val' = ai env val
522 sc' = ai (n:env) sc in
523 PLet n ty' val' sc'
524 ai env (PPi p n ty sc) = let ty' = ai env ty
525 sc' = ai (n:env) sc in
526 PPi p n ty' sc'
527 ai env (PHidden tm) = PHidden (ai env tm)
528 ai env tm = tm
530 aiFn _ env (PRef fc f) as | not (f `elem` env)
531 = case lookupCtxt f (idris_implicits ist) of
532 Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)
533 Nothing -> pApp fc 1 (PRef fc f) as
534 aiFn fc env f as = pApp fc 1 f as
536 pApp fc a f [] = f
537 pApp fc a f as = let rest = drop a as in
538 appRest fc (PApp fc f (take a as)) rest
540 appRest fc f [] = f
541 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
543 insertImpl :: [PArg] -> [PArg] -> [PArg]
544 insertImpl (PExp ty : ps) (PExp tm : given) =
545 PExp tm : insertImpl ps given
546 insertImpl (PImp n ty : ps) given =
547 case find n given [] of
548 Just (tm, given') -> PImp n tm : insertImpl ps given'
549 Nothing -> PImp n Placeholder : insertImpl ps given
550 insertImpl expected [] = []
551 insertImpl [] given = given
553 find n [] acc = Nothing
554 find n (PImp n' t : gs) acc
555 | n == n' = Just (t, reverse acc ++ gs)
556 find n (g : gs) acc = find n gs (g : acc)
558-- Debugging/logging stuff
560dumpDecls :: [PDecl] -> String
561dumpDecls [] = ""
562dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
564dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
565dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
566dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
567dumpDecl (PData _ d) = showDImp True d
568dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
569dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
570-- dumpDecl (PImport i) = "import " ++ i
572-- syntactic match of a against b, returning pair of variables in a
573-- and what they match. Returns 'Nothing' if not a match.
575matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
576matchClause x y = match x y where
577 matchArg x y = match (getTm x) (getTm y)
579 match (PApp _ f args) (PApp _ f' args')
580 | length args == length args'
581 = do mf <- match f f'
582 ms <- zipWithM matchArg args args'
583 return (mf ++ concat ms)
584 match (PRef _ n) (PRef _ n') | n == n' = return []
585 | otherwise = Nothing
586 match (PRef _ n) tm = return [(n, tm)]
587 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
588 mr <- match r r'
589 return (ml ++ mr)
590 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
591 mr <- match r r'
592 return (ml ++ mr)
593 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
594 mr <- match r r'
595 return (ml ++ mr)
596 match (PRefl _) (PRefl _) = return []
597 match (PTrue _) (PTrue _) = return []
598 match (PFalse _) (PFalse _) = return []
599 match (PReturn _) (PReturn _) = return []
600 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
601 ms <- match s s'
602 return (mt ++ ms)
603 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
604 ms <- match s s'
605 return (mt ++ ms)
606 match (PHidden x) (PHidden y) = match x y
607 match a b | a == b = return []
608 | otherwise = Nothing
610substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
611substMatches [] t = t
612substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
614substMatch :: Name -> PTerm -> PTerm -> PTerm
615substMatch n tm t = sm t where
616 sm (PRef _ n') | n == n' = tm
617 sm (PLam x t sc) = PLam x (sm t) (sm sc)
618 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
619 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
620 sm (PEq f x y) = PEq f (sm x) (sm y)
621 sm (PPair f x y) = PPair f (sm x) (sm y)
622 sm (PDPair f x y) = PDPair f (sm x) (sm y)
623 sm (PHidden x) = PHidden (sm x)
624 sm x = x