← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Internal/Generic.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2009-07-20 19:49:41 UTC
  • Revision ID: james.westby@ubuntu.com-20090720194941-hcjy91vrn16csh7d
Tags: upstream-2.2.4+dfsg
Import upstream version 2.2.4+dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Internal/Generic.hs
 
1
{-# LANGUAGE CPP #-}
 
2
 
 
3
module Agda.Syntax.Internal.Generic where
 
4
 
 
5
import Control.Applicative
 
6
import Data.Traversable
 
7
import Data.Monoid
 
8
import Data.Foldable
 
9
import Agda.Syntax.Common
 
10
import Agda.Syntax.Internal
 
11
 
 
12
#include "../../undefined.h"
 
13
import Agda.Utils.Impossible
 
14
 
 
15
class TermLike a where
 
16
  traverseTerm  :: (Term -> Term) -> a -> a
 
17
  traverseTermM :: (Monad m, Applicative m) => (Term -> m Term) -> a -> m a
 
18
  foldTerm      :: Monoid m => (Term -> m) -> a -> m
 
19
 
 
20
instance TermLike a => TermLike (Arg a) where
 
21
  traverseTerm  f = fmap (traverseTerm f)
 
22
  traverseTermM f = traverse (traverseTermM f)
 
23
  foldTerm f = foldMap (foldTerm f)
 
24
 
 
25
instance TermLike a => TermLike [a] where
 
26
  traverseTerm f = fmap (traverseTerm f)
 
27
  traverseTermM f = traverse (traverseTermM f)
 
28
  foldTerm f = foldMap (foldTerm f)
 
29
 
 
30
instance (TermLike a, TermLike b) => TermLike (a, b) where
 
31
  traverseTerm f (x, y) = (traverseTerm f x, traverseTerm f y)
 
32
  traverseTermM f (x, y) = (,) <$> traverseTermM f x <*> traverseTermM f y
 
33
  foldTerm f (x, y) = foldTerm f x `mappend` foldTerm f y
 
34
 
 
35
instance TermLike a => TermLike (Abs a) where
 
36
  traverseTerm f = fmap (traverseTerm f)
 
37
  traverseTermM f = traverse (traverseTermM f)
 
38
  foldTerm f = foldMap (foldTerm f)
 
39
 
 
40
instance TermLike Term where
 
41
  traverseTerm f t = case t of
 
42
    Var i xs -> f $ Var i $ traverseTerm f xs
 
43
    Def c xs -> f $ Def c $ traverseTerm f xs
 
44
    Con c xs -> f $ Con c $ traverseTerm f xs
 
45
    Lam h b  -> f $ Lam h $ traverseTerm f b
 
46
    Pi a b   -> f $ uncurry Pi $ traverseTerm f (a, b)
 
47
    Fun a b  -> f $ uncurry Fun $ traverseTerm f (a, b)
 
48
    MetaV m xs -> f $ MetaV m $ traverseTerm f xs
 
49
    Lit _    -> f t
 
50
    Sort _   -> f t
 
51
 
 
52
  traverseTermM f t = case t of
 
53
    Var i xs -> f =<< Var i <$> traverseTermM f xs
 
54
    Def c xs -> f =<< Def c <$> traverseTermM f xs
 
55
    Con c xs -> f =<< Con c <$> traverseTermM f xs
 
56
    Lam h b  -> f =<< Lam h <$> traverseTermM f b
 
57
    Pi a b   -> f =<< uncurry Pi <$> traverseTermM f (a, b)
 
58
    Fun a b  -> f =<< uncurry Fun <$> traverseTermM f (a, b)
 
59
    MetaV m xs -> f =<< MetaV m <$> traverseTermM f xs
 
60
    Lit _    -> f t
 
61
    Sort _   -> f t
 
62
 
 
63
  foldTerm f t = f t `mappend` case t of
 
64
    Var i xs   -> foldTerm f xs
 
65
    Def c xs   -> foldTerm f xs
 
66
    Con c xs   -> foldTerm f xs
 
67
    Lam h b    -> foldTerm f b
 
68
    Pi a b     -> foldTerm f (a, b)
 
69
    Fun a b    -> foldTerm f (a, b)
 
70
    MetaV m xs -> foldTerm f xs
 
71
    Lit _      -> mempty
 
72
    Sort _     -> mempty
 
73
 
 
74
instance TermLike Type where
 
75
  traverseTerm f (El s t) = El s $ traverseTerm f t
 
76
  traverseTermM f (El s t) = El s <$> traverseTermM f t
 
77
  foldTerm f (El s t) = foldTerm f t
 
78