← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Substitute.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Substitute.hs
1
 
{-# LANGUAGE CPP, TypeSynonymInstances, FlexibleInstances, OverlappingInstances,
2
 
    DeriveDataTypeable, DeriveFunctor, StandaloneDeriving #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE DeriveDataTypeable #-}
 
3
{-# LANGUAGE DeriveFunctor #-}
 
4
{-# LANGUAGE FlexibleInstances #-}
 
5
{-# LANGUAGE PatternGuards #-}
 
6
{-# LANGUAGE OverlappingInstances #-}
 
7
{-# LANGUAGE StandaloneDeriving #-}
 
8
{-# LANGUAGE TupleSections #-}
 
9
{-# LANGUAGE TypeSynonymInstances #-}
 
10
 
3
11
module Agda.TypeChecking.Substitute where
4
12
 
5
 
import Control.Monad.Identity
6
 
import Control.Monad.Reader
7
13
import Control.Arrow ((***))
8
14
 
9
 
import Data.Typeable (Typeable)
10
 
import Data.List hiding (sort)
 
15
import Data.Function
 
16
import Data.Functor
 
17
import Data.List hiding (sort, drop)
11
18
import qualified Data.List as List
12
 
import Data.Function
13
19
import Data.Map (Map)
14
 
import qualified Data.Map as Map
15
 
import qualified Data.Set as Set
16
 
 
17
 
import Agda.Syntax.Common
 
20
import Data.Typeable (Typeable)
 
21
 
 
22
import Debug.Trace (trace)
 
23
 
 
24
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
 
25
import qualified Agda.Syntax.Common as Common
18
26
import Agda.Syntax.Internal
19
27
import Agda.Syntax.Position
20
28
 
22
30
import Agda.TypeChecking.Free as Free
23
31
import Agda.TypeChecking.CompiledClause
24
32
 
 
33
import Agda.Utils.List
25
34
import Agda.Utils.Monad
 
35
import Agda.Utils.Permutation
26
36
import Agda.Utils.Size
27
 
import Agda.Utils.Permutation
 
37
import Agda.Utils.Tuple
28
38
 
29
39
#include "../undefined.h"
30
40
import Agda.Utils.Impossible
31
41
 
 
42
---------------------------------------------------------------------------
 
43
-- * Application
 
44
---------------------------------------------------------------------------
 
45
 
32
46
-- | Apply something to a bunch of arguments.
33
47
--   Preserves blocking tags (application can never resolve blocking).
34
48
class Apply t where
35
 
    apply :: t -> Args -> t
 
49
  apply  :: t -> Args -> t
 
50
  applyE :: t -> Elims -> t
 
51
 
 
52
  apply t args = applyE t $ map Apply args
 
53
  applyE t es  = apply  t $ map argFromElim es
 
54
    -- precondition: all @es@ are @Apply@s
36
55
 
37
56
instance Apply Term where
38
 
    apply m [] = m
39
 
    apply m args@(a:args0) =
40
 
        case m of
41
 
            Var i args'   -> Var i (args' ++ args)
42
 
            Def c args'   -> Def c (args' ++ args)
43
 
            Con c args'   -> Con c (args' ++ args)
44
 
            Lam _ u       -> absApp u (unArg a) `apply` args0
45
 
            MetaV x args' -> MetaV x (args' ++ args)
46
 
            Shared p      -> Shared $ apply p args
47
 
            Lit{}         -> __IMPOSSIBLE__
48
 
            Level{}       -> __IMPOSSIBLE__
49
 
            Pi _ _        -> __IMPOSSIBLE__
50
 
            Sort _        -> __IMPOSSIBLE__
51
 
            DontCare mv   -> DontCare $ mv `apply` args  -- Andreas, 2011-10-02
52
 
              -- need to go under DontCare, since "with" might resurrect irrelevant term
 
57
  applyE m [] = m
 
58
  applyE m es =
 
59
    case m of
 
60
      Var i es'   -> Var i (es' ++ es)
 
61
      Def f es'   -> defApp f es' es  -- remove projection redexes
 
62
      Con c args  -> conApp c args es
 
63
      Lam _ b     ->
 
64
        case es of
 
65
          Apply a : es0 -> absApp b (unArg a) `applyE` es0
 
66
          _             -> __IMPOSSIBLE__
 
67
      MetaV x es' -> MetaV x (es' ++ es)
 
68
      Shared p    -> Shared $ applyE p es
 
69
      Lit{}       -> __IMPOSSIBLE__
 
70
      Level{}     -> __IMPOSSIBLE__
 
71
      Pi _ _      -> __IMPOSSIBLE__
 
72
      Sort _      -> __IMPOSSIBLE__
 
73
      DontCare mv -> dontCare $ mv `applyE` es  -- Andreas, 2011-10-02
 
74
        -- need to go under DontCare, since "with" might resurrect irrelevant term
 
75
 
 
76
-- | If $v$ is a record value, @canProject f v@
 
77
--   returns its field @f@.
 
78
canProject :: QName -> Term -> Maybe (Arg Term)
 
79
canProject f v =
 
80
  case ignoreSharing v of
 
81
    (Con (ConHead _ fs) vs) -> do
 
82
      i <- elemIndex f fs
 
83
      mhead (drop i vs)
 
84
    _ -> Nothing
 
85
 
 
86
-- | Eliminate a constructed term.
 
87
conApp :: ConHead -> Args -> Elims -> Term
 
88
conApp ch                args []             = Con ch args
 
89
conApp ch                args (Apply a : es) = conApp ch (args ++ [a]) es
 
90
conApp ch@(ConHead c fs) args (Proj f  : es) =
 
91
  let failure = flip trace __IMPOSSIBLE__ $
 
92
        "conApp: constructor " ++ show c ++
 
93
        " with fields " ++ show fs ++
 
94
        " projected by " ++ show f
 
95
      i = maybe failure id            $ elemIndex f fs
 
96
      v = maybe failure argToDontCare $ mhead $ drop i args
 
97
  in  applyE v es
 
98
{-
 
99
      i = maybe failure id    $ elemIndex f $ map unArg fs
 
100
      v = maybe failure unArg $ mhead $ drop i args
 
101
      -- Andreas, 2013-10-20 see Issue543a:
 
102
      -- protect result of irrelevant projection.
 
103
      r = maybe __IMPOSSIBLE__ getRelevance $ mhead $ drop i fs
 
104
      u | Irrelevant <- r = DontCare v
 
105
        | otherwise       = v
 
106
  in  applyE v es
 
107
-}
 
108
 
 
109
-- | @defApp f us vs@ applies @Def f us@ to further arguments @vs@,
 
110
--   eliminating top projection redexes.
 
111
--   If @us@ is not empty, we cannot have a projection redex, since
 
112
--   the record argument is the first one.
 
113
defApp :: QName -> Elims -> Elims -> Term
 
114
defApp f [] (Apply a : es) | Just v <- canProject f (unArg a)
 
115
  = argToDontCare v `applyE` es
 
116
defApp f es0 es = Def f $ es0 ++ es
 
117
 
 
118
-- protect irrelevant fields (see issue 610)
 
119
argToDontCare :: Common.Arg c Term -> Term
 
120
argToDontCare (Common.Arg ai v)
 
121
  | Irrelevant <- getRelevance ai     = dontCare v
 
122
  | otherwise                         = v
53
123
 
54
124
instance Apply Type where
55
125
  apply = piApply
 
126
  -- Maybe an @applyE@ instance would be useful here as well.
 
127
  -- A record type could be applied to a projection name
 
128
  -- to yield the field type.
 
129
  -- However, this works only in the monad where we can
 
130
  -- look up the fields of a record type.
56
131
 
57
132
instance Apply Sort where
58
 
  apply s [] = s
59
 
  apply s _  = __IMPOSSIBLE__
 
133
  applyE s [] = s
 
134
  applyE s _  = __IMPOSSIBLE__
60
135
 
61
136
instance Apply a => Apply (Ptr a) where
62
 
  apply p xs = fmap (`apply` xs) p
 
137
  applyE p xs = fmap (`applyE` xs) p
 
138
 
 
139
-- @applyE@ does not make sense for telecopes, definitions, clauses etc.
63
140
 
64
141
instance Subst a => Apply (Tele a) where
65
142
  apply tel               []       = tel
67
144
  apply (ExtendTel _ tel) (t : ts) = absApp tel (unArg t) `apply` ts
68
145
 
69
146
instance Apply Definition where
70
 
  apply (Defn rel x t pol occ df m c d) args = Defn rel x (piApply t args) (apply pol args) (apply occ args) df m c (apply d args)
 
147
  apply (Defn info x t pol occ df m c d) args = Defn info x (piApply t args) (apply pol args) (apply occ args) df m c (apply d args)
71
148
 
72
149
instance Apply [Base.Occurrence] where
73
 
  apply occ args = drop (length args) occ
 
150
  apply occ args = List.drop (length args) occ
74
151
 
75
152
instance Apply [Polarity] where
76
 
  apply pol args = drop (length args) pol
 
153
  apply pol args = List.drop (length args) pol
 
154
 
 
155
instance Apply Projection where
 
156
  apply p args = p
 
157
    { projIndex    = projIndex p - size args
 
158
    , projDropPars = projDropPars p `apply` args
 
159
    }
77
160
 
78
161
instance Apply Defn where
79
162
  apply d [] = d
80
163
  apply d args = case d of
81
164
    Axiom{} -> d
82
165
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
83
 
            , funProjection = Nothing {-, funArgOccurrences = occ -} } ->
 
166
            , funProjection = Nothing } ->
84
167
      d { funClauses    = apply cs args
85
168
        , funCompiled   = apply cc args
86
169
        , funInv        = apply inv args
87
170
        }
88
 
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
89
 
            , funProjection = Just (r, n) {-, funArgOccurrences = occ -} }
90
 
      | m < n  -> d { funProjection = Just (r, n - m) }
91
 
      | otherwise ->
 
171
 
 
172
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
 
173
            , funProjection = Just p} ->
 
174
      case p `apply` args of
 
175
        p@Projection{ projIndex = n }
 
176
          | n < 0     -> __IMPOSSIBLE__
 
177
          -- case: applied only to parameters
 
178
          | n > 0     -> d { funProjection = Just p }
 
179
          -- case: applied also to record value
 
180
          | otherwise ->
 
181
              d { funClauses        = apply cs args'
 
182
                , funCompiled       = apply cc args'
 
183
                , funInv            = apply inv args'
 
184
                , funProjection     = Nothing -- WAS: Just $ p { projIndex = 0 }
 
185
                }
 
186
              where args' = [last args]  -- the record value
 
187
{-
 
188
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
 
189
            , funProjection = Just p@Projection{ projIndex = n } }
 
190
        -- case: only applying parameters
 
191
      | size args < n -> d { funProjection = Just $ p `apply` args }
 
192
        -- case: apply also to record value
 
193
      | otherwise     ->
92
194
        d { funClauses        = apply cs args'
93
195
          , funCompiled       = apply cc args'
94
196
          , funInv            = apply inv args'
95
 
          , funProjection     = Just (r, 0)
 
197
          , funProjection     = Just $ p { projIndex = 0 } -- Nothing ?
96
198
          }
97
 
      where args' = [last args]
98
 
            m = size args
99
 
    Datatype{ dataPars = np, dataClause = cl
 
199
      where args' = [last args]  -- the record value
 
200
-}
 
201
    Datatype{ dataPars = np, dataSmallPars = sps, dataNonLinPars = nlps, dataClause = cl
100
202
            {-, dataArgOccurrences = occ-} } ->
101
 
      d { dataPars = np - size args, dataClause = apply cl args
 
203
      d { dataPars = np - size args
 
204
        , dataSmallPars  = apply sps args
 
205
        , dataNonLinPars = apply nlps args
 
206
        , dataClause     = apply cl args
 
207
--        , dataArgOccurrences = List.drop (length args) occ
102
208
        }
103
209
    Record{ recPars = np, recConType = t, recClause = cl, recTel = tel
104
210
          {-, recArgOccurrences = occ-} } ->
105
211
      d { recPars = np - size args, recConType = apply t args
106
212
        , recClause = apply cl args, recTel = apply tel args
 
213
--        , recArgOccurrences = List.drop (length args) occ
107
214
        }
108
215
    Constructor{ conPars = np } ->
109
216
      d { conPars = np - size args }
118
221
    apply (PrimFun x ar def) args   = PrimFun x (ar - size args) $ \vs -> def (args ++ vs)
119
222
 
120
223
instance Apply Clause where
121
 
    apply (Clause r tel perm ps b) args =
122
 
      Clause r (apply tel args) (apply perm args)
123
 
             (drop (size args) ps) (apply b args)
 
224
    apply (Clause r tel perm ps b t) args =
 
225
      Clause r
 
226
             (apply tel args)
 
227
             (apply perm args)
 
228
             (List.drop (size args) ps)
 
229
             (apply b args)
 
230
             (applySubst (parallelS (map unArg args)) t)
124
231
 
125
232
instance Apply CompiledClauses where
126
233
  apply cc args = case cc of
127
234
    Fail     -> Fail
128
235
    Done hs t
129
 
      | length hs >= len -> Done (drop len hs)
 
236
      | length hs >= len -> Done (List.drop len hs)
130
237
                                 (applySubst
131
238
                                    (parallelS $
132
239
                                       [ var i | i <- [0..length hs - len - 1]] ++
140
247
      len = length args
141
248
 
142
249
instance Apply a => Apply (WithArity a) where
143
 
  apply (WithArity n a) args = WithArity n $ apply a args
 
250
  apply  (WithArity n a) args = WithArity n $ apply  a args
 
251
  applyE (WithArity n a) es   = WithArity n $ applyE a es
144
252
 
145
253
instance Apply a => Apply (Case a) where
146
254
  apply (Branches cs ls m) args =
147
255
    Branches (apply cs args) (apply ls args) (apply m args)
 
256
  applyE (Branches cs ls m) es =
 
257
    Branches (applyE cs es) (applyE ls es) (applyE m es)
148
258
 
149
259
instance Apply FunctionInverse where
150
260
  apply NotInjective  args = NotInjective
151
261
  apply (Inverse inv) args = Inverse $ apply inv args
152
262
 
153
263
instance Apply ClauseBody where
154
 
    apply  b                 []       = b
155
 
    apply (Bind (Abs   _ b)) (a:args) = subst (unArg a) b `apply` args
156
 
    apply (Bind (NoAbs _ b)) (_:args) = b `apply` args
157
 
    apply (Body v)           args     = Body $ v `apply` args
158
 
    apply  NoBody             _       = NoBody
 
264
  apply  b       []       = b
 
265
  apply (Bind b) (a:args) = absApp b (unArg a) `apply` args
 
266
  apply (Body v) args     = Body $ v `apply` args
 
267
  apply  NoBody   _       = NoBody
 
268
  applyE  b       []             = b
 
269
 
 
270
  applyE (Bind b) (Apply a : es) = absApp b (unArg a) `applyE` es
 
271
  applyE (Bind b) (Proj{}  : es) = __IMPOSSIBLE__
 
272
  applyE (Body v) es             = Body $ v `applyE` es
 
273
  applyE  NoBody   _             = NoBody
159
274
 
160
275
instance Apply DisplayTerm where
161
276
  apply (DTerm v)          args = DTerm $ apply v args
162
277
  apply (DDot v)           args = DDot  $ apply v args
163
278
  apply (DCon c vs)        args = DCon c $ vs ++ map (fmap DTerm) args
164
279
  apply (DDef c vs)        args = DDef c $ vs ++ map (fmap DTerm) args
165
 
  apply (DWithApp v args') args = DWithApp v $ args' ++ args
 
280
  apply (DWithApp v ws args') args = DWithApp v ws $ args' ++ args
166
281
 
167
282
instance Apply t => Apply [t] where
168
 
    apply ts args = map (`apply` args) ts
 
283
  apply  ts args = map (`apply` args) ts
 
284
  applyE ts es   = map (`applyE` es) ts
169
285
 
170
286
instance Apply t => Apply (Blocked t) where
171
 
    apply b args = fmap (`apply` args) b
 
287
  apply  b args = fmap (`apply` args) b
 
288
  applyE b es   = fmap (`applyE` es) b
172
289
 
173
290
instance Apply t => Apply (Maybe t) where
174
 
  apply x args = fmap (`apply` args) x
 
291
  apply  x args = fmap (`apply` args) x
 
292
  applyE x es   = fmap (`applyE` es) x
175
293
 
176
294
instance Apply v => Apply (Map k v) where
177
 
  apply x args = fmap (`apply` args) x
 
295
  apply  x args = fmap (`apply` args) x
 
296
  applyE x es   = fmap (`applyE` es) x
178
297
 
179
298
instance (Apply a, Apply b) => Apply (a,b) where
180
 
    apply (x,y) args = (apply x args, apply y args)
 
299
  apply  (x,y) args = (apply  x args, apply  y args)
 
300
  applyE (x,y) es   = (applyE x es  , applyE y es  )
181
301
 
182
302
instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
183
 
    apply (x,y,z) args = (apply x args, apply y args, apply z args)
 
303
  apply  (x,y,z) args = (apply  x args, apply  y args, apply  z args)
 
304
  applyE (x,y,z) es   = (applyE x es  , applyE y es  , applyE z es  )
 
305
 
 
306
instance DoDrop a => Apply (Drop a) where
 
307
  apply x args = dropMore (size args) x
 
308
 
 
309
instance DoDrop a => Abstract (Drop a) where
 
310
  abstract tel x = unDrop (size tel) x
184
311
 
185
312
instance Apply Permutation where
186
313
  -- The permutation must start with [0..m - 1]
 
314
  -- NB: section (- m) not possible (unary minus), hence (flip (-) m)
187
315
  apply (Perm n xs) args = Perm (n - m) $ map (flip (-) m) $ genericDrop m xs
188
316
    where
189
317
      m = size args
199
327
piApply t []                      = t
200
328
piApply (El _ (Pi  _ b)) (a:args) = absApp b (unArg a) `piApply` args
201
329
piApply (El s (Shared p)) args    = piApply (El s $ derefPtr p) args
202
 
piApply _ _                       = __IMPOSSIBLE__
203
 
 
 
330
piApply t args                    =
 
331
  trace ("piApply t = " ++ show t ++ "\n  args = " ++ show args) __IMPOSSIBLE__
 
332
 
 
333
---------------------------------------------------------------------------
 
334
-- * Abstraction
 
335
---------------------------------------------------------------------------
 
336
 
 
337
-- | @(abstract args v) `apply` args --> v[args]@.
204
338
class Abstract t where
205
339
    abstract :: Telescope -> t -> t
206
340
 
220
353
  abstract (ExtendTel arg tel') tel = ExtendTel arg $ fmap (`abstract` tel) tel'
221
354
 
222
355
instance Abstract Definition where
223
 
  abstract tel (Defn rel x t pol occ df m c d) =
224
 
    Defn rel x (abstract tel t) (abstract tel pol) (abstract tel occ) df m c (abstract tel d)
 
356
  abstract tel (Defn info x t pol occ df m c d) =
 
357
    Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) df m c (abstract tel d)
225
358
 
226
359
instance Abstract [Base.Occurrence] where
227
360
  abstract tel []  = []
231
364
  abstract tel []  = []
232
365
  abstract tel pol = replicate (size tel) Invariant ++ pol -- TODO: check polarity
233
366
 
 
367
instance Abstract Projection where
 
368
  abstract tel p = p
 
369
    { projIndex    = size tel + projIndex p
 
370
    , projDropPars = abstract tel $ projDropPars p
 
371
    }
 
372
 
234
373
instance Abstract Defn where
235
374
  abstract tel d = case d of
236
375
    Axiom{} -> d
237
376
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
238
 
            , funProjection = Nothing {-, funArgOccurrences = occ-} } ->
239
 
      d { funClauses = abstract tel cs, funCompiled = abstract tel cc
240
 
        , funInv = abstract tel inv
241
 
        }
242
 
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
243
 
            , funProjection = Just (r, n) {-, funArgOccurrences = occ-} } ->
244
 
      d { funProjection = Just (r, n + size tel) }
245
 
    Datatype{ dataPars = np, dataClause = cl {-, dataArgOccurrences = occ-} } ->
246
 
      d { dataPars = np + size tel, dataClause = abstract tel cl
247
 
        }
248
 
    Record{ recPars = np, recConType = t, recClause = cl, recTel = tel'
249
 
          {-, recArgOccurrences = occ-} } ->
250
 
      d { recPars = np + size tel, recConType = abstract tel t
251
 
        , recClause = abstract tel cl, recTel = abstract tel tel'
 
377
            , funProjection = Nothing  } ->
 
378
      d { funClauses  = abstract tel cs
 
379
        , funCompiled = abstract tel cc
 
380
        , funInv      = abstract tel inv
 
381
        }
 
382
    Function{ funProjection = Just p } ->
 
383
      d { funProjection = Just $ abstract tel p }
 
384
    Datatype{ dataPars = np, dataSmallPars = sps, dataNonLinPars = nlps, dataClause = cl } ->
 
385
      d { dataPars       = np + size tel
 
386
        , dataSmallPars  = abstract tel sps
 
387
        , dataNonLinPars = abstract tel nlps
 
388
        , dataClause     = abstract tel cl
 
389
        }
 
390
    Record{ recPars = np, recConType = t, recClause = cl, recTel = tel' } ->
 
391
      d { recPars    = np + size tel
 
392
        , recConType = abstract tel t
 
393
        , recClause  = abstract tel cl
 
394
        , recTel     = abstract tel tel'
252
395
        }
253
396
    Constructor{ conPars = np } ->
254
397
      d { conPars = np + size tel }
263
403
        where n = size tel
264
404
 
265
405
instance Abstract Clause where
266
 
  abstract tel (Clause r tel' perm ps b) =
 
406
  abstract tel (Clause r tel' perm ps b t) =
267
407
    Clause r (abstract tel tel') (abstract tel perm)
268
 
           (telVars tel ++ ps) (abstract tel b)
 
408
           (namedTelVars tel ++ ps) (abstract tel b)
 
409
           t -- nothing to do for t, since it lives under the telescope
269
410
 
270
411
instance Abstract CompiledClauses where
271
412
  abstract tel Fail = Fail
281
422
    Branches (abstract tel cs) (abstract tel ls) (abstract tel m)
282
423
 
283
424
telVars :: Telescope -> [Arg Pattern]
284
 
telVars EmptyTel                    = []
285
 
telVars (ExtendTel (Dom h r a) tel) = Arg h r (VarP $ absName tel) : telVars (unAbs tel)
 
425
telVars = map (fmap namedThing) . namedTelVars
 
426
 
 
427
namedTelVars :: Telescope -> [NamedArg Pattern]
 
428
namedTelVars EmptyTel                            = []
 
429
namedTelVars (ExtendTel (Common.Dom info a) tel) =
 
430
  Common.Arg info (namedVarP $ absName tel) :
 
431
  namedTelVars (unAbs tel)
286
432
 
287
433
instance Abstract FunctionInverse where
288
434
  abstract tel NotInjective  = NotInjective
304
450
abstractArgs :: Abstract a => Args -> a -> a
305
451
abstractArgs args x = abstract tel x
306
452
    where
307
 
        tel   = foldr (\(Arg h r x) -> ExtendTel (Dom h r $ sort Prop) . Abs x) EmptyTel
308
 
              $ zipWith (fmap . const) names args
309
 
        names = cycle $ map (:[]) ['a'..'z']
 
453
        tel   = foldr (\(Common.Arg info x) -> ExtendTel (Common.Dom info $ sort Prop) . Abs x)
 
454
                      EmptyTel
 
455
              $ zipWith (<$) names args
 
456
        names = cycle $ map (stringToArgName . (:[])) ['a'..'z']
 
457
 
 
458
---------------------------------------------------------------------------
 
459
-- * Explicit substitutions
 
460
---------------------------------------------------------------------------
310
461
 
311
462
-- | Substitutions.
312
463
 
404
555
             | otherwise -> raise n $ lookupS rho (i - n)
405
556
  EmptyS                 -> __IMPOSSIBLE__
406
557
 
 
558
---------------------------------------------------------------------------
 
559
-- * Substitution and raising/shifting/weakening
 
560
---------------------------------------------------------------------------
 
561
 
407
562
-- | Apply a substitution.
408
563
 
409
564
-- For terms:
434
589
instance Subst Term where
435
590
  applySubst IdS t = t
436
591
  applySubst rho t    = case t of
437
 
    Var i vs    -> lookupS rho i `apply` applySubst rho vs
 
592
    Var i es    -> lookupS rho i `applyE` applySubst rho es
438
593
    Lam h m     -> Lam h $ applySubst rho m
439
 
    Def c vs    -> Def c $ applySubst rho vs
 
594
    Def f es    -> defApp f [] $ applySubst rho es
440
595
    Con c vs    -> Con c $ applySubst rho vs
441
 
    MetaV x vs  -> MetaV x $ applySubst rho vs
 
596
    MetaV x es  -> MetaV x $ applySubst rho es
442
597
    Lit l       -> Lit l
443
598
    Level l     -> levelTm $ applySubst rho l
444
599
    Pi a b      -> uncurry Pi $ applySubst rho (a,b)
445
600
    Sort s      -> sortTm $ applySubst rho s
446
601
    Shared p    -> Shared $ applySubst rho p
447
 
    DontCare mv -> DontCare $ applySubst rho mv
 
602
    DontCare mv -> dontCare $ applySubst rho mv
448
603
 
449
604
instance Subst a => Subst (Ptr a) where
450
605
  applySubst rho = fmap (applySubst rho)
468
623
  applySubst rho (Plus n l) = Plus n $ applySubst rho l
469
624
 
470
625
instance Subst LevelAtom where
471
 
  applySubst rho      (MetaLevel m vs)   = MetaLevel m    $ applySubst rho vs
472
 
  applySubst rho      (BlockedLevel m v) = BlockedLevel m $ applySubst rho v
473
 
  applySubst rho      (NeutralLevel v)   = UnreducedLevel $ applySubst rho v
474
 
  applySubst rho      (UnreducedLevel v) = UnreducedLevel $ applySubst rho v
 
626
  applySubst rho (MetaLevel m vs)   = MetaLevel m    $ applySubst rho vs
 
627
  applySubst rho (BlockedLevel m v) = BlockedLevel m $ applySubst rho v
 
628
  applySubst rho (NeutralLevel v)   = UnreducedLevel $ applySubst rho v
 
629
  applySubst rho (UnreducedLevel v) = UnreducedLevel $ applySubst rho v
 
630
 
 
631
instance Subst Bool where
 
632
  applySubst rho = id
 
633
 
 
634
instance Subst Name where
 
635
  applySubst rho = id
475
636
 
476
637
instance Subst Pattern where
477
638
  applySubst rho p = case p of
478
 
    VarP s       -> VarP s
479
 
    LitP l       -> LitP l
480
639
    ConP c mt ps -> ConP c (applySubst rho mt) $ applySubst rho ps
481
640
    DotP t       -> DotP $ applySubst rho t
 
641
    VarP s       -> p
 
642
    LitP l       -> p
 
643
    ProjP _      -> p
482
644
 
483
645
instance Subst t => Subst (Blocked t) where
484
 
  applySubst rho b      = fmap (applySubst rho) b
 
646
  applySubst rho b = fmap (applySubst rho) b
485
647
 
486
648
instance Subst DisplayForm where
487
649
  applySubst rho (Display n ps v) =
489
651
              (applySubst (liftS n rho) v)
490
652
 
491
653
instance Subst DisplayTerm where
492
 
  applySubst rho      (DTerm v)        = DTerm $ applySubst rho v
493
 
  applySubst rho      (DDot v)         = DDot  $ applySubst rho v
494
 
  applySubst rho      (DCon c vs)      = DCon c $ applySubst rho vs
495
 
  applySubst rho      (DDef c vs)      = DDef c $ applySubst rho vs
496
 
  applySubst rho      (DWithApp vs ws) = uncurry DWithApp $ applySubst rho (vs, ws)
 
654
  applySubst rho (DTerm v)        = DTerm $ applySubst rho v
 
655
  applySubst rho (DDot v)         = DDot  $ applySubst rho v
 
656
  applySubst rho (DCon c vs)      = DCon c $ applySubst rho vs
 
657
  applySubst rho (DDef c vs)      = DDef c $ applySubst rho vs
 
658
  applySubst rho (DWithApp v vs ws) = uncurry3 DWithApp $ applySubst rho (v, vs, ws)
497
659
 
498
660
instance Subst a => Subst (Tele a) where
499
 
  applySubst rho  EmptyTel              = EmptyTel
500
 
  applySubst rho (ExtendTel t tel)      = uncurry ExtendTel $ applySubst rho (t, tel)
 
661
  applySubst rho  EmptyTel         = EmptyTel
 
662
  applySubst rho (ExtendTel t tel) = uncurry ExtendTel $ applySubst rho (t, tel)
501
663
 
502
664
instance Subst Constraint where
503
665
  applySubst rho c = case c of
526
688
instance Subst a => Subst (Arg a) where
527
689
  applySubst rho = fmap (applySubst rho)
528
690
 
 
691
instance Subst a => Subst (Named name a) where
 
692
  applySubst rho = fmap (applySubst rho)
 
693
 
529
694
instance Subst a => Subst (Dom a) where
530
695
  applySubst rho = fmap (applySubst rho)
531
696
 
541
706
instance (Subst a, Subst b) => Subst (a,b) where
542
707
  applySubst rho (x,y) = (applySubst rho x, applySubst rho y)
543
708
 
 
709
instance (Subst a, Subst b, Subst c) => Subst (a,b,c) where
 
710
  applySubst rho (x,y,z) = (applySubst rho x, applySubst rho y, applySubst rho z)
 
711
 
 
712
instance (Subst a, Subst b, Subst c, Subst d) => Subst (a,b,c,d) where
 
713
  applySubst rho (x,y,z,u) = (applySubst rho x, applySubst rho y, applySubst rho z, applySubst rho u)
 
714
 
544
715
instance Subst ClauseBody where
545
716
  applySubst rho (Body t) = Body $ applySubst rho t
546
717
  applySubst rho (Bind b) = Bind $ applySubst rho b
547
718
  applySubst _   NoBody   = NoBody
548
719
 
549
 
data TelV a = TelV (Tele (Dom a)) a
 
720
---------------------------------------------------------------------------
 
721
-- * Telescopes
 
722
---------------------------------------------------------------------------
 
723
 
 
724
type TelView = TelV Type
 
725
data TelV a  = TelV { theTel :: Tele (Dom a), theCore :: a }
550
726
  deriving (Typeable, Show, Eq, Ord, Functor)
551
727
 
552
 
type TelView = TelV Type
553
 
 
554
 
telFromList :: [Dom (String, Type)] -> Telescope
555
 
telFromList = foldr (\(Dom h r (x, a)) -> ExtendTel (Dom h r a) . Abs x) EmptyTel
556
 
 
557
 
telToList :: Telescope -> [Dom (String, Type)]
558
 
telToList EmptyTel = []
559
 
telToList (ExtendTel arg tel) = fmap ((,) $ absName tel) arg : telToList (absBody tel)
 
728
type ListTel' a = [Dom (a, Type)]
 
729
type ListTel = ListTel' ArgName
 
730
 
 
731
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
 
732
telFromList' f = foldr extTel EmptyTel
 
733
  where
 
734
    extTel (Common.Dom info (x, a)) = ExtendTel (Common.Dom info a) . Abs (f x)
 
735
 
 
736
telFromList :: ListTel -> Telescope
 
737
telFromList = telFromList' id
 
738
 
 
739
telToList :: Telescope -> ListTel
 
740
telToList EmptyTel            = []
 
741
telToList (ExtendTel arg tel) = fmap (absName tel,) arg : telToList (absBody tel)
 
742
  -- Andreas, 2013-12-14: This would work also for 'NoAbs',
 
743
  -- since 'absBody' raises.
 
744
 
 
745
-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
 
746
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
 
747
bindsToTel' f []     t = []
 
748
bindsToTel' f (x:xs) t = fmap (f x,) t : bindsToTel' f xs (raise 1 t)
 
749
 
 
750
bindsToTel :: [Name] -> Dom Type -> ListTel
 
751
bindsToTel = bindsToTel' nameToArgName
560
752
 
561
753
telView' :: Type -> TelView
562
754
telView' t = case ignoreSharing $ unEl t of
566
758
    absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
567
759
 
568
760
-- | @mkPi dom t = telePi (telFromList [dom]) t@
569
 
mkPi :: Dom (String, Type) -> Type -> Type
570
 
mkPi (Dom h r (x, a)) b = el $ Pi (Dom h r a) (mkAbs x b)
 
761
mkPi :: Dom (ArgName, Type) -> Type -> Type
 
762
mkPi (Common.Dom info (x, a)) b = el $ Pi (Common.Dom info a) (mkAbs x b)
571
763
  where
572
764
    el = El $ dLub (getSort a) (Abs x (getSort b)) -- dLub checks x freeIn
573
765
 
 
766
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
 
767
telePi' reAbs = telePi where
 
768
  telePi EmptyTel          t = t
 
769
  telePi (ExtendTel u tel) t = el $ Pi u $ reAbs b
 
770
    where
 
771
      b  = (`telePi` t) <$> tel
 
772
      s1 = getSort $ unDom u
 
773
      s2 = getSort <$> b
 
774
      el = El $ dLub s1 s2
 
775
 
 
776
-- | Uses free variable analysis to introduce 'noAbs' bindings.
574
777
telePi :: Telescope -> Type -> Type
575
 
telePi  EmptyTel         t = t
576
 
telePi (ExtendTel u tel) t = el $ Pi u (reAbs b)
577
 
  where
578
 
    el = El (dLub s1 s2)
579
 
    b = fmap (flip telePi t) tel
580
 
    s1 = getSort $ unDom u
581
 
    s2 = fmap getSort b
582
 
 
 
778
telePi = telePi' reAbs
 
779
 
 
780
-- | Everything will be a 'Abs'.
 
781
telePi_ :: Telescope -> Type -> Type
 
782
telePi_ = telePi' id
 
783
 
 
784
{- OLD
583
785
-- | Everything will be a pi.
584
 
telePi_ :: Telescope -> Type -> Type
585
786
telePi_  EmptyTel        t = t
586
787
telePi_ (ExtendTel u tel) t = el $ Pi u b
587
788
  where
589
790
    b  = fmap (flip telePi_ t) tel
590
791
    s1 = getSort $ unDom u
591
792
    s2 = fmap getSort b
 
793
-}
592
794
 
593
795
teleLam :: Telescope -> Term -> Term
594
796
teleLam  EmptyTel         t = t
595
 
teleLam (ExtendTel u tel) t = Lam (domHiding u) $ flip teleLam t <$> tel
 
797
teleLam (ExtendTel u tel) t = Lam (domInfo u) $ flip teleLam t <$> tel
 
798
 
 
799
-- | Performs void ('noAbs') abstraction over telescope.
 
800
class TeleNoAbs a where
 
801
  teleNoAbs :: a -> Term -> Term
 
802
 
 
803
instance TeleNoAbs ListTel where
 
804
  teleNoAbs tel t = foldr (\ (Common.Dom ai (x, _)) -> Lam ai . NoAbs x) t tel
 
805
 
 
806
instance TeleNoAbs Telescope where
 
807
  teleNoAbs tel = teleNoAbs $ telToList tel
596
808
 
597
809
-- | Dependent least upper bound, to assign a level to expressions
598
810
--   like @forall i -> Set i@.
604
816
  Flexible      -> DLub s1 b
605
817
  Irrelevantly  -> DLub s1 b
606
818
  NoOccurrence  -> sLub s1 (absApp b __IMPOSSIBLE__)
607
 
  Free.Unused   -> sLub s1 (absApp b __IMPOSSIBLE__)
 
819
--  Free.Unused   -> sLub s1 (absApp b __IMPOSSIBLE__) -- triggers Issue784
 
820
  Free.Unused   -> DLub s1 b
608
821
  StronglyRigid -> Inf
609
822
  WeaklyRigid   -> Inf
610
823
 
 
824
---------------------------------------------------------------------------
 
825
-- * Functions on abstractions
611
826
--   and things we couldn't do before we could define 'absBody'
 
827
---------------------------------------------------------------------------
612
828
 
613
829
-- | Instantiate an abstraction
614
830
absApp :: Subst t => Abs t -> Term -> t
620
835
absBody (Abs   _ v) = v
621
836
absBody (NoAbs _ v) = raise 1 v
622
837
 
623
 
mkAbs :: (Subst a, Free a) => String -> a -> Abs a
 
838
mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
624
839
mkAbs x v | 0 `freeIn` v = Abs x v
625
840
          | otherwise    = NoAbs x (raise (-1) v)
626
841
 
650
865
    Lam h b -> Lam h $ underAbs (loop $ n-1) a b
651
866
    _       -> __IMPOSSIBLE__
652
867
 
 
868
-- | @getBody@ returns the properly raised clause 'Body',
 
869
--   and 'Nothing' if 'NoBody'.
 
870
--
 
871
--   @getBodyUnraised@ just grabs the body, without raising the de Bruijn indices.
 
872
--   This is useful if you want to consider the body in context 'clauseTel'.
 
873
class GetBody a where
 
874
  getBody         :: a -> Maybe Term
 
875
  getBodyUnraised :: a -> Maybe Term
 
876
 
 
877
instance GetBody ClauseBody where
 
878
  getBody = body 0
 
879
    where
 
880
      -- collect all shiftings and do them in the end in one go
 
881
      body :: Int -> ClauseBody -> Maybe Term
 
882
      body _ NoBody             = Nothing
 
883
      body n (Body v)           = Just $ raise n v
 
884
      body n (Bind (NoAbs _ v)) = body n v
 
885
      body n (Bind (Abs   _ v)) = body (n + 1) v
 
886
 
 
887
  getBodyUnraised NoBody   = Nothing
 
888
  getBodyUnraised (Body v) = Just v
 
889
  getBodyUnraised (Bind b) = getBodyUnraised $ unAbs b  -- Does not raise!
 
890
 
 
891
instance GetBody Clause where
 
892
  getBody         = getBody         . clauseBody
 
893
  getBodyUnraised = getBodyUnraised . clauseBody
 
894
 
 
895
---------------------------------------------------------------------------
 
896
-- * Syntactic equality and order
 
897
---------------------------------------------------------------------------
 
898
 
653
899
deriving instance (Subst a, Eq a) => Eq (Tele a)
654
900
deriving instance (Subst a, Ord a) => Ord (Tele a)
655
901
 
736
982
  Abs   _ a `compare` Abs   _ b = a `compare` b
737
983
  a         `compare` b         = absBody a `compare` absBody b
738
984
 
 
985
---------------------------------------------------------------------------
 
986
-- * Level stuff
 
987
---------------------------------------------------------------------------
739
988
 
740
989
sLub :: Sort -> Sort -> Sort
741
990
sLub s Prop = s
757
1005
levelMax as0 = Max $ ns ++ List.sort bs
758
1006
  where
759
1007
    as = Prelude.concatMap expand as0
 
1008
    -- ns is empty or a singleton
760
1009
    ns = case [ n | ClosedLevel n <- as, n > 0 ] of
761
1010
      []  -> []
762
 
      ns  -> [ ClosedLevel n | n <- [Prelude.maximum ns], n > greatestB ]
 
1011
      ns  -> [ ClosedLevel n | let n = Prelude.maximum ns, n > greatestB ]
763
1012
    bs = subsume [ b | b@Plus{} <- as ]
764
1013
    greatestB | null bs   = 0
765
1014
              | otherwise = Prelude.maximum [ n | Plus n _ <- bs ]
820
1069
    Max [Plus 0 l] -> unLevelAtom l
821
1070
    _              -> Level l
822
1071
 
823
 
unLevelAtom (MetaLevel x vs)   = MetaV x vs
 
1072
unLevelAtom (MetaLevel x es)   = MetaV x es
824
1073
unLevelAtom (NeutralLevel v)   = v
825
1074
unLevelAtom (UnreducedLevel v) = v
826
1075
unLevelAtom (BlockedLevel _ v) = v
827
1076
 
 
1077
---------------------------------------------------------------------------
 
1078
-- * Boring instances
 
1079
---------------------------------------------------------------------------
828
1080
 
829
1081
instance Sized Substitution where
830
1082
  size IdS          = 1