← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Abstract/Views.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Abstract/Views.hs
1
 
{-# LANGUAGE TupleSections, PatternGuards #-}
 
1
{-# LANGUAGE NoMonomorphismRestriction #-}
 
2
{-# LANGUAGE PatternGuards             #-}
 
3
{-# LANGUAGE TupleSections             #-}
2
4
 
3
5
module Agda.Syntax.Abstract.Views where
4
6
 
5
7
import Control.Applicative
6
8
import Control.Arrow (first)
7
9
import Control.Monad.Identity
 
10
 
 
11
import Data.Foldable (foldMap)
 
12
import Data.Monoid
8
13
import Data.Traversable
9
14
 
10
15
import Agda.Syntax.Position
33
38
-- | Gather top-level 'AsP'atterns to expose underlying pattern.
34
39
asView :: A.Pattern -> ([Name], A.Pattern)
35
40
asView (A.AsP _ x p) = first (x :) $ asView p
36
 
asView p             = ([], p)
 
41
asView p             = ([], p)
37
42
 
38
43
-- | Check whether we are dealing with a universe.
39
44
isSet :: Expr -> Bool
56
61
-- | Apply an expression rewriting to every subexpression, inside-out.
57
62
--   See 'Agda.Syntax.Internal.Generic'
58
63
class ExprLike a where
 
64
  foldExpr :: Monoid m => (Expr -> m) -> a -> m
59
65
  traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
60
66
  mapExpr :: (Expr -> Expr) -> (a -> a)
61
67
  mapExpr f e = runIdentity $ traverseExpr (Identity . f) e
62
68
 
63
69
instance ExprLike Expr where
 
70
  foldExpr f e =
 
71
    case e of
 
72
      Var{}                -> m
 
73
      Def{}                -> m
 
74
      Proj{}               -> m
 
75
      Con{}                -> m
 
76
      PatternSyn{}         -> m
 
77
      Lit{}                -> m
 
78
      QuestionMark{}       -> m
 
79
      Underscore{}         -> m
 
80
      App _ e e'           -> m `mappend` fold e `mappend` fold e'
 
81
      WithApp _ e es       -> m `mappend` fold e `mappend` fold es
 
82
      Lam _ b e            -> m `mappend` fold b `mappend` fold e
 
83
      AbsurdLam{}          -> m
 
84
      ExtendedLam _ _ _ cs -> m `mappend` fold cs
 
85
      Pi _ tel e           -> m `mappend` fold tel `mappend` fold e
 
86
      Fun _ e e'           -> m `mappend` fold e `mappend` fold e'
 
87
      Set{}                -> m
 
88
      Prop{}               -> m
 
89
      Let _ bs e           -> m `mappend` fold bs `mappend` fold e
 
90
      ETel tel             -> m `mappend` fold tel
 
91
      Rec _ as             -> m `mappend` fold as
 
92
      RecUpdate _ e as     -> m `mappend` fold e `mappend` fold as
 
93
      ScopedExpr _ e       -> m `mappend` fold e
 
94
      QuoteGoal _ _ e      -> m `mappend` fold e
 
95
      QuoteContext _ _ e   -> m `mappend` fold e
 
96
      Quote{}              -> m
 
97
      QuoteTerm{}          -> m
 
98
      Unquote{}            -> m
 
99
      DontCare e           -> m `mappend` fold e
 
100
   where
 
101
     m    = f e
 
102
     fold = foldExpr f
 
103
 
64
104
  traverseExpr f e = do
65
105
    let trav e = traverseExpr f e
66
106
    case e of
67
107
      Var{}                   -> f e
68
108
      Def{}                   -> f e
 
109
      Proj{}                  -> f e
69
110
      Con{}                   -> f e
70
111
      Lit{}                   -> f e
71
112
      QuestionMark{}          -> f e
94
135
 
95
136
-- | TODO: currently does not go into colors.
96
137
instance ExprLike a => ExprLike (Common.Arg c a) where
 
138
  foldExpr     = foldMap . foldExpr
97
139
  traverseExpr = traverse . traverseExpr
98
140
 
99
141
instance ExprLike a => ExprLike (Named x a) where
 
142
  foldExpr     = foldMap . foldExpr
100
143
  traverseExpr = traverse . traverseExpr
101
144
 
102
145
instance ExprLike a => ExprLike [a] where
 
146
  foldExpr     = foldMap . foldExpr
103
147
  traverseExpr = traverse . traverseExpr
104
148
 
105
149
instance ExprLike a => ExprLike (x, a) where
 
150
  foldExpr     f (x, e) = foldExpr f e
106
151
  traverseExpr f (x, e) = (x,) <$> traverseExpr f e
107
152
 
108
153
instance ExprLike LamBinding where
 
154
  foldExpr f e =
 
155
    case e of
 
156
      DomainFree{}  -> mempty
 
157
      DomainFull bs -> foldExpr f bs
109
158
  traverseExpr f e =
110
159
    case e of
111
160
      DomainFree{}  -> return e
112
161
      DomainFull bs -> DomainFull <$> traverseExpr f bs
113
162
 
114
163
instance ExprLike TypedBindings where
 
164
  foldExpr     f (TypedBindings r b) = foldExpr f b
115
165
  traverseExpr f (TypedBindings r b) = TypedBindings r <$> traverseExpr f b
116
166
 
117
167
instance ExprLike TypedBinding where
 
168
  foldExpr f e =
 
169
    case e of
 
170
      TBind _ _ e  -> foldExpr f e
 
171
      TLet _ ds    -> foldExpr f ds
118
172
  traverseExpr f e =
119
173
    case e of
120
174
      TBind r xs e -> TBind r xs <$> traverseExpr f e
121
175
      TLet r ds    -> TLet r <$> traverseExpr f ds
122
176
 
123
177
instance ExprLike LetBinding where
 
178
  foldExpr f e =
 
179
    case e of
 
180
      LetBind _ _ _ e e' -> fold e `mappend` fold e'
 
181
      LetPatBind _ p e   -> fold p `mappend` fold e
 
182
      LetApply{}         -> mempty
 
183
      LetOpen{}          -> mempty
 
184
    where fold e = foldExpr f e
 
185
 
124
186
  traverseExpr f e = do
125
187
    let trav e = traverseExpr f e
126
188
    case e of
131
193
 
132
194
-- | TODO: currently does not go into patterns.
133
195
instance ExprLike (Pattern' a) where
 
196
  foldExpr     f _ = mempty
134
197
  traverseExpr f e = return e
135
198
 
136
199
-- | TODO: currently does not go into clauses.
137
200
instance ExprLike (Clause' a) where
 
201
  foldExpr     f _ = mempty
138
202
  traverseExpr f e = return e
 
203
 
 
204
{- TODO: finish
 
205
instance ExprLike (Clause' a) where
 
206
  foldExpr f (Clause _ rhs ds) = fold rhs `mappend` fold ds
 
207
    where fold e = foldExpr f e
 
208
  traverseExpr f (Clause lhs rhs ds) = Clause lhs <$> trav rhs <*> trav ds
 
209
    where trav e = traverseExpr f e
 
210
 
 
211
instance ExprLike RHS where
 
212
  foldExpr f rhs =
 
213
    case rhs of
 
214
      RHS e                  -> fold e
 
215
      AbsurdRHS{}            -> mempty
 
216
      WithRHS _ es cs        -> fold es `mappend` fold cs
 
217
      RewriteRHS _ es rhs ds -> fold es `mappend` fold rhs `mappend` fold ds
 
218
    where fold e = foldExpr f e
 
219
 
 
220
  traverseExpr f rhs =
 
221
    case rhs of
 
222
      RHS e                   -> RHS <$> trav e
 
223
      AbsurdRHS{}             -> pure rhs
 
224
      WithRHS x es cs         -> WithRHS x <$> trav es <*> trav cs
 
225
      RewriteRHS xs es rhs ds -> RewriteRHS xs <$> trav es <*> trav rhs <*> trav ds
 
226
    where trav e = traverseExpr f e
 
227
 
 
228
instance ExprLike Declaration where
 
229
  foldExpr f d =
 
230
    case d of
 
231
-}