git.iko.soy/Idris-dev
on ebcb29b help sign in
Idris-dev/src/Idris/AbsSyntax.hs
696 lines 25 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate
10import Control.Monad.State
11import Data.List
12import Data.Char
13import Debug.Trace
15import qualified Epic.Epic as E
17data IOption = IOption { opt_logLevel :: Int,
18 opt_typecase :: Bool
19 }
20 deriving (Show, Eq)
22defaultOpts = IOption 0 False
24-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
25-- without typechecking).
26-- This will include all the functions and data declarations, plus fixity declarations
27-- and syntax macros.
29data IState = IState { tt_ctxt :: Context,
30 idris_infixes :: [FixDecl],
31 idris_implicits :: Ctxt [PArg],
32 idris_statics :: Ctxt [Bool],
33 idris_log :: String,
34 idris_options :: IOption,
35 idris_name :: Int,
36 idris_metavars :: [Name],
37 syntax_rules :: [Syntax],
38 syntax_keywords :: [String],
39 imported :: [FilePath],
40 idris_prims :: [(Name, ([E.Name], E.Term))]
41 }
43idrisInit = IState emptyContext [] emptyContext emptyContext
44 "" defaultOpts 6 [] [] [] [] []
46-- The monad for the main REPL - reading and processing files and updating
47-- global state (hence the IO inner monad).
48type Idris a = StateT IState IO a
51getContext :: Idris Context
52getContext = do i <- get; return (tt_ctxt i)
54getIState :: Idris IState
55getIState = get
57putIState :: IState -> Idris ()
58putIState = put
60getName :: Idris Int
61getName = do i <- get;
62 let idx = idris_name i;
63 put (i { idris_name = idx + 1 })
64 return idx
66checkUndefined :: FC -> Name -> Idris ()
67checkUndefined fc n
68 = do i <- getContext
69 case lookupCtxt n i of
70 Just _ -> fail $ show fc ++ ":" ++
71 show n ++ " already defined"
72 _ -> return ()
74setContext :: Context -> Idris ()
75setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
77updateContext :: (Context -> Context) -> Idris ()
78updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
80addDeferred :: [(Name, Type)] -> Idris ()
81addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns
82 i <- get
83 put (i { idris_metavars = map fst ns ++ idris_metavars i })
85solveDeferred :: Name -> Idris ()
86solveDeferred n = do i <- get
87 put (i { idris_metavars = idris_metavars i \\ [n] })
89iputStrLn :: String -> Idris ()
90iputStrLn = lift.putStrLn
92setLogLevel :: Int -> Idris ()
93setLogLevel l = do i <- get
94 let opts = idris_options i
95 let opt' = opts { opt_logLevel = l }
96 put (i { idris_options = opt' } )
98logLevel :: Idris Int
99logLevel = do i <- get
100 return (opt_logLevel (idris_options i))
102logLvl :: Int -> String -> Idris ()
103logLvl l str = do i <- get
104 let lvl = opt_logLevel (idris_options i)
105 when (lvl >= l)
106 $ do lift (putStrLn str)
107 put (i { idris_log = idris_log i ++ str ++ "\n" } )
109iLOG :: String -> Idris ()
110iLOG = logLvl 1
112setTypeCase :: Bool -> Idris ()
113setTypeCase t = do i <- get
114 let opts = idris_options i
115 let opt' = opts { opt_typecase = t }
116 put (i { idris_options = opt' })
118-- Commands in the REPL
120data Command = Quit | Help | Eval PTerm
121 | Compile String
122 | Metavars | Prove Name
123 | TTShell
124 | LogLvl Int | Spec PTerm | HNF PTerm
125 | NOP
127-- Parsed declarations
129data Fixity = Infixl { prec :: Int }
130 | Infixr { prec :: Int }
131 | InfixN { prec :: Int }
132 | PrefixN { prec :: Int }
133 deriving Eq
135instance Show Fixity where
136 show (Infixl i) = "infixl " ++ show i
137 show (Infixr i) = "infixr " ++ show i
138 show (InfixN i) = "infix " ++ show i
139 show (PrefixN i) = "prefix " ++ show i
141data FixDecl = Fix Fixity String
142 deriving (Show, Eq)
144instance Ord FixDecl where
145 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
148data Static = Static | Dynamic
149 deriving (Show, Eq)
151-- Mark bindings with their explicitness, and laziness
152data Plicity = Imp { plazy :: Bool,
153 pstatic :: Static }
154 | Exp { plazy :: Bool,
155 pstatic :: Static }
156 deriving (Show, Eq)
158impl = Imp False Dynamic
159expl = Exp False Dynamic
161data PDecl' t = PFix FC Fixity [String] -- fixity declaration
162 | PTy FC Name t -- type declaration
163 | PClauses FC Name [PClause' t] -- pattern clause
164 | PData FC (PData' t) -- data declaration
165 | PParams FC [(Name, PTerm)] [PDecl' t] -- params block
166 | PSyntax FC Syntax
167 deriving Functor
169data PClause' t = PClause Name t [t] t [PDecl]
170 | PWith Name t [t] t [PDecl]
171 deriving Functor
173data PData' t = PDatadecl { d_name :: Name,
174 d_tcon :: t,
175 d_cons :: [(Name, t, FC)] }
176 deriving Functor
178-- Handy to get a free function for applying PTerm -> PTerm functions
179-- across a program, by deriving Functor
181type PDecl = PDecl' PTerm
182type PData = PData' PTerm
183type PClause = PClause' PTerm
185-- get all the names declared in a decl
187declared :: PDecl -> [Name]
188declared (PFix _ _ _) = []
189declared (PTy _ n t) = [n]
190declared (PClauses _ n _) = [] -- not a declaration
191declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts
192 where fstt (a, _, _) = a
193declared (PParams _ _ ds) = concatMap declared ds
194-- declared (PImport _) = []
196-- High level language terms
197--
198data PTerm = PQuote Raw
199 | PRef FC Name
200 | PLam Name PTerm PTerm
201 | PPi Plicity Name PTerm PTerm
202 | PLet Name PTerm PTerm PTerm
203 | PApp FC PTerm [PArg]
204 | PTrue FC
205 | PFalse FC
206 | PRefl FC
207 | PEq FC PTerm PTerm
208 | PPair FC PTerm PTerm
209 | PDPair FC PTerm PTerm
210 | PHidden PTerm -- irrelevant or hidden pattern
211 | PSet
212 | PConstant Const
213 | Placeholder
214 | PDoBlock [PDo]
215 | PReturn FC
216 | PMetavar Name
217 | PProof [PTactic]
218 | PElabError String -- error to report on elaboration
219 deriving Eq
221data PTactic = Intro [Name]
222 | Refine Name
223 | Exact PTerm
224 | Solve
225 | Attack
226 | ProofState | ProofTerm
227 | Qed
228 deriving (Show, Eq)
230data PDo = DoExp FC PTerm
231 | DoBind FC Name PTerm
232 | DoLet FC Name PTerm
233 deriving Eq
235data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }
236 | PExp { lazyarg :: Bool, getTm :: t }
237 deriving (Show, Eq, Functor)
239pimp = PImp False
240pexp = PExp False
242type PArg = PArg' PTerm
244-- Syntactic sugar info (TODO: namespaces, modules)
246data DSL = DSL { dsl_bind :: Name,
247 dsl_return :: Name }
248 deriving Show
250data Syntax = Rule [SSymbol] PTerm
251 deriving Show
253data SSymbol = Keyword Name
254 | Symbol String
255 | Expr Name
256 deriving Show
258initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
260data SyntaxInfo = Syn { using :: [(Name, PTerm)],
261 syn_params :: [(Name, PTerm)],
262 no_imp :: [Name],
263 dsl_info :: DSL }
264 deriving Show
266defaultSyntax = Syn [] [] [] initDSL
268--- Pretty printing declarations and terms
270instance Show PTerm where
271 show tm = showImp False tm
273instance Show PDecl where
274 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
275 show (PTy _ n ty) = show n ++ " : " ++ show ty
276 show (PClauses _ n c) = showSep "\n" (map show c)
277 show (PData _ d) = show d
279instance Show PClause where
280 show c = showCImp True c
282instance Show PData where
283 show d = showDImp False d
285showCImp :: Bool -> PClause -> String
286showCImp impl (PClause n l ws r w)
287 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
288 ++ " where " ++ show w
289 where
290 showWs [] = ""
291 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
292showCImp impl (PWith n l ws r w)
293 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
294 ++ " { " ++ show w ++ " } "
295 where
296 showWs [] = ""
297 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
300showDImp :: Bool -> PData -> String
301showDImp impl (PDatadecl n ty cons)
302 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
303 ++ showSep "\n\t| "
304 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
306getImps :: [PArg] -> [(Name, PTerm)]
307getImps [] = []
308getImps (PImp _ n tm : xs) = (n, tm) : getImps xs
309getImps (_ : xs) = getImps xs
311getExps :: [PArg] -> [PTerm]
312getExps [] = []
313getExps (PExp _ tm : xs) = tm : getExps xs
314getExps (_ : xs) = getExps xs
316getAll :: [PArg] -> [PTerm]
317getAll = map getTm
319showImp :: Bool -> PTerm -> String
320showImp impl tm = se 10 tm where
321 se p (PQuote r) = "![" ++ show r ++ "]"
322 se p (PRef _ n) = show n
323 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
324 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
325 " in " ++ se 10 sc
326 se p (PPi (Exp l s) n ty sc)
327 | n `elem` allNamesIn sc = bracket p 2 $
328 if l then "|(" else "(" ++
329 show n ++ " : " ++ se 10 ty ++
330 ") " ++ st ++
331 "-> " ++ se 10 sc
332 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
333 where st = case s of
334 Static -> "[static] "
335 _ -> ""
336 se p (PPi (Imp l s) n ty sc)
337 | impl = bracket p 2 $ if l then "|{" else "{" ++
338 show n ++ " : " ++ se 10 ty ++
339 "} " ++ st ++ "-> " ++ se 10 sc
340 | otherwise = se 10 sc
341 where st = case s of
342 Static -> "[static] "
343 _ -> ""
344 se p (PApp _ (PRef _ f) [])
345 | not impl = show f
346 se p (PApp _ (PRef _ op@(UN [f:_])) args)
347 | length (getExps args) == 2 && not impl && not (isAlpha f)
348 = let [l, r] = getExps args in
349 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
350 se p (PApp _ f as)
351 = let (imps, args) = (getImps as, getExps as) in
352 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
353 ++ concatMap seArg args
354 se p (PHidden tm) = "." ++ se 0 tm
355 se p (PRefl _) = "refl"
356 se p (PTrue _) = "()"
357 se p (PFalse _) = "_|_"
358 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
359 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
360 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
361 se p PSet = "Set"
362 se p (PConstant c) = show c
363 se p (PProof ts) = "proof { " ++ show ts ++ "}"
364 se p (PMetavar n) = "?" ++ show n
365 se p Placeholder = "_"
367 seArg arg = " " ++ se 0 arg
368 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
370 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
371 | otherwise = str
373allNamesIn :: PTerm -> [Name]
374allNamesIn tm = nub $ ni [] tm
375 where
376 ni env (PRef _ n)
377 | not (n `elem` env) = [n]
378 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
379 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
380 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
381 ni env (PHidden tm) = ni env tm
382 ni env (PEq _ l r) = ni env l ++ ni env r
383 ni env (PPair _ l r) = ni env l ++ ni env r
384 ni env (PDPair _ l r) = ni env l ++ ni env r
385 ni env _ = []
387namesIn :: IState -> PTerm -> [Name]
388namesIn ist tm = nub $ ni [] tm
389 where
390 ni env (PRef _ n)
391 | not (n `elem` env)
392 = case lookupCtxt n (idris_implicits ist) of
393 Nothing -> [n]
394 _ -> []
395 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
396 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
397 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
398 ni env (PEq _ l r) = ni env l ++ ni env r
399 ni env (PPair _ l r) = ni env l ++ ni env r
400 ni env (PDPair _ l r) = ni env l ++ ni env r
401 ni env (PHidden tm) = ni env tm
402 ni env _ = []
404-- For inferring types of things
406bi = FC "builtin" 0
408inferTy = MN 0 "__Infer"
409inferCon = MN 0 "__infer"
410inferDecl = PDatadecl inferTy
411 PSet
412 [(inferCon, PPi impl (MN 0 "A") PSet (
413 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
414 (PRef bi inferTy)), bi)]
416infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
417infP = P (TCon 6 0) inferTy (Set 0)
419getInferTerm, getInferType :: Term -> Term
420getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
421getInferTerm (App (App _ _) tm) = tm
422getInferTerm tm = error ("getInferTerm " ++ show tm)
424getInferType (Bind n b sc) = Bind n b $ getInferType sc
425getInferType (App (App _ ty) _) = ty
427-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
429unitTy = MN 0 "__Unit"
430unitCon = MN 0 "__II"
431unitDecl = PDatadecl unitTy PSet
432 [(unitCon, PRef bi unitTy, bi)]
434falseTy = MN 0 "__False"
435falseDecl = PDatadecl falseTy PSet []
437pairTy = MN 0 "__Pair"
438pairCon = MN 0 "__MkPair"
439pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
440 [(pairCon, PPi impl (n "A") PSet (
441 PPi impl (n "B") PSet (
442 PPi expl (n "a") (PRef bi (n "A")) (
443 PPi expl (n "b") (PRef bi (n "B"))
444 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
445 pexp (PRef bi (n "B"))])))), bi)]
446 where n a = MN 0 a
448eqTy = UN ["="]
449eqCon = UN ["refl"]
450eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
451 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
452 PSet)
453 [(eqCon, PPi impl (n "a") PSet (
454 PPi impl (n "x") (PRef bi (n "a"))
455 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
456 pimp (n "b") Placeholder,
457 pexp (PRef bi (n "x")),
458 pexp (PRef bi (n "x"))])), bi)]
459 where n a = MN 0 a
461-- Defined in builtins.idr
462sigmaTy = UN ["Sigma"]
463existsCon = UN ["Exists"]
465piBind :: [(Name, PTerm)] -> PTerm -> PTerm
466piBind [] t = t
467piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
469-- Dealing with implicit arguments
471-- Add implicit Pi bindings for any names in the term which appear in an
472-- argument position.
474-- This has become a right mess already. Better redo it some time...
476implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
477implicitise syn ist tm
478 = let uvars = using syn
479 pvars = syn_params syn
480 (declimps, ns') = execState (imps True [] tm) ([], [])
481 ns = ns' \\ (map fst pvars ++ no_imp syn) in
482 if null ns
483 then (tm, reverse declimps)
484 else implicitise syn ist (pibind uvars ns tm)
485 where
486 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
487 | otherwise = x : dropAll xs ys
488 dropAll [] ys = []
490 imps top env (PApp _ f as)
491 = do (decls, ns) <- get
492 let isn = concatMap (namesIn ist) (map getTm as)
493 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
494 imps top env (PPi (Imp l _) n ty sc)
495 = do let isn = nub (namesIn ist ty) `dropAll` [n]
496 (decls , ns) <- get
497 put (PImp l n ty : decls,
498 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
499 imps True (n:env) sc
500 imps top env (PPi (Exp l _) n ty sc)
501 = do let isn = nub (namesIn ist ty ++ case sc of
502 (PRef _ x) -> namesIn ist sc `dropAll` [n]
503 _ -> [])
504 (decls, ns) <- get -- ignore decls in HO types
505 put (PExp l ty : decls,
506 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
507 imps True (n:env) sc
508 imps top env (PEq _ l r)
509 = do (decls, ns) <- get
510 let isn = namesIn ist l ++ namesIn ist r
511 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
512 imps top env (PPair _ l r)
513 = do (decls, ns) <- get
514 let isn = namesIn ist l ++ namesIn ist r
515 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
516 imps top env (PDPair _ (PRef _ n) r)
517 = do (decls, ns) <- get
518 let isn = nub (namesIn ist r) \\ [n]
519 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
520 imps top env (PDPair _ l r)
521 = do (decls, ns) <- get
522 let isn = namesIn ist l ++ namesIn ist r
523 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
524 imps top env (PLam n ty sc)
525 = do imps False env ty
526 imps False (n:env) sc
527 imps top env (PHidden tm) = imps False env tm
528 imps top env _ = return ()
530 pibind using [] sc = sc
531 pibind using (n:ns) sc
532 = case lookup n using of
533 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
534 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
536-- Add implicit arguments in function calls
538addImpl :: IState -> PTerm -> PTerm
539addImpl ist ptm = ai [] ptm
540 where
541 ai env (PRef fc f) = aiFn fc env (PRef fc f) []
542 ai env (PEq fc l r) = let l' = ai env l
543 r' = ai env r in
544 PEq fc l' r'
545 ai env (PPair fc l r) = let l' = ai env l
546 r' = ai env r in
547 PPair fc l' r'
548 ai env (PDPair fc l r) = let l' = ai env l
549 r' = ai env r in
550 PDPair fc l' r'
551 ai env (PApp fc (PRef _ f) as)
552 = let as' = map (fmap (ai env)) as in
553 aiFn fc env (PRef fc f) as'
554 ai env (PApp fc f as) = let f' = ai env f
555 as' = map (fmap (ai env)) as in
556 aiFn fc env f' as'
557 ai env (PLam n ty sc) = let ty' = ai env ty
558 sc' = ai (n:env) sc in
559 PLam n ty' sc'
560 ai env (PLet n ty val sc)
561 = let ty' = ai env ty
562 val' = ai env val
563 sc' = ai (n:env) sc in
564 PLet n ty' val' sc'
565 ai env (PPi p n ty sc) = let ty' = ai env ty
566 sc' = ai (n:env) sc in
567 PPi p n ty' sc'
568 ai env (PHidden tm) = PHidden (ai env tm)
569 ai env tm = tm
571 aiFn _ env (PRef fc f) as | not (f `elem` env)
572 = case lookupCtxt f (idris_implicits ist) of
573 Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)
574 Nothing -> pApp fc 1 (PRef fc f) as
575 aiFn fc env f as = pApp fc 1 f as
577 pApp fc a f [] = f
578 pApp fc a f as = let rest = drop a as in
579 appRest fc (PApp fc f (take a as)) rest
581 appRest fc f [] = f
582 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
584 insertImpl :: [PArg] -> [PArg] -> [PArg]
585 insertImpl (PExp l ty : ps) (PExp _ tm : given) =
586 PExp l tm : insertImpl ps given
587 insertImpl (PImp l n ty : ps) given =
588 case find n given [] of
589 Just (tm, given') -> PImp l n tm : insertImpl ps given'
590 Nothing -> PImp l n Placeholder : insertImpl ps given
591 insertImpl expected [] = []
592 insertImpl [] given = given
594 find n [] acc = Nothing
595 find n (PImp _ n' t : gs) acc
596 | n == n' = Just (t, reverse acc ++ gs)
597 find n (g : gs) acc = find n gs (g : acc)
599-- Find 'static' argument positions
600-- (the declared ones, plus any names in argument position in the declared
601-- statics)
602-- FIXME: It's possible that this really has to happen after elaboration
604findStatics :: IState -> PTerm -> (PTerm, [Bool])
605findStatics ist tm = let (ns, ss) = fs tm in
606 runState (pos ns ss tm) []
607 where fs (PPi p n t sc)
608 | Static <- pstatic p
609 = let (ns, ss) = fs sc in
610 (namesIn ist t : ns, namesIn ist t ++ n : ss)
611 | otherwise = let (ns, ss) = fs sc in
612 (namesIn ist t : ns, ss)
613 fs _ = ([], [])
615 inOne n ns = length (filter id (map (elem n) ns)) == 1
617 pos ns ss (PPi p n t sc)
618 | n `inOne` ns && elem n ss
619 = do sc' <- pos ns ss sc
620 spos <- get
621 put (True : spos)
622 return (PPi (p { pstatic = Static }) n t sc')
623 | otherwise = do sc' <- pos ns ss sc
624 spos <- get
625 put (False : spos)
626 return (PPi p n t sc')
627 pos ns ss t = return t
629-- Debugging/logging stuff
631dumpDecls :: [PDecl] -> String
632dumpDecls [] = ""
633dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
635dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
636dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
637dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
638dumpDecl (PData _ d) = showDImp True d
639dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
640dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
641-- dumpDecl (PImport i) = "import " ++ i
643-- syntactic match of a against b, returning pair of variables in a
644-- and what they match. Returns 'Nothing' if not a match.
646matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
647matchClause x y = match x y where
648 matchArg x y = match (getTm x) (getTm y)
650 match (PApp _ f args) (PApp _ f' args')
651 | length args == length args'
652 = do mf <- match f f'
653 ms <- zipWithM matchArg args args'
654 return (mf ++ concat ms)
655 match (PRef _ n) (PRef _ n') | n == n' = return []
656 | otherwise = Nothing
657 match (PRef _ n) tm = return [(n, tm)]
658 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
659 mr <- match r r'
660 return (ml ++ mr)
661 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
662 mr <- match r r'
663 return (ml ++ mr)
664 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
665 mr <- match r r'
666 return (ml ++ mr)
667 match (PRefl _) (PRefl _) = return []
668 match (PTrue _) (PTrue _) = return []
669 match (PFalse _) (PFalse _) = return []
670 match (PReturn _) (PReturn _) = return []
671 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
672 ms <- match s s'
673 return (mt ++ ms)
674 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
675 ms <- match s s'
676 return (mt ++ ms)
677 match (PHidden x) (PHidden y) = match x y
678 match a b | a == b = return []
679 | otherwise = Nothing
681substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
682substMatches [] t = t
683substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
685substMatch :: Name -> PTerm -> PTerm -> PTerm
686substMatch n tm t = sm t where
687 sm (PRef _ n') | n == n' = tm
688 sm (PLam x t sc) = PLam x (sm t) (sm sc)
689 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
690 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
691 sm (PEq f x y) = PEq f (sm x) (sm y)
692 sm (PPair f x y) = PPair f (sm x) (sm y)
693 sm (PDPair f x y) = PDPair f (sm x) (sm y)
694 sm (PHidden x) = PHidden (sm x)
695 sm x = x