1
{-# LANGUAGE CPP, PatternGuards,
2
TypeSynonymInstances, FlexibleInstances #-}
2
{-# LANGUAGE FlexibleInstances #-}
3
{-# LANGUAGE PatternGuards #-}
4
{-# LANGUAGE TupleSections #-}
5
{-# LANGUAGE TypeSynonymInstances #-}
4
7
module Agda.TypeChecking.Reduce where
6
9
import Prelude hiding (mapM)
7
import Control.Monad.State hiding (mapM)
8
10
import Control.Monad.Reader hiding (mapM)
9
import Control.Monad.Error hiding (mapM)
10
11
import Control.Applicative
11
13
import Data.List as List hiding (sort)
12
import qualified Data.Map as Map
13
15
import Data.Map (Map)
14
import qualified Data.Set as Set
15
16
import Data.Traversable
16
17
import Data.Hashable
18
19
import Agda.Syntax.Position
19
import Agda.Syntax.Common
20
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
20
21
import Agda.Syntax.Internal
21
22
import Agda.Syntax.Scope.Base (Scope)
22
23
import Agda.Syntax.Literal
24
import Agda.TypeChecking.Monad
25
import Agda.TypeChecking.Monad.Context
26
import Agda.TypeChecking.Monad.Builtin
25
import Agda.TypeChecking.Monad hiding ( underAbstraction_, enterClosure, isInstantiatedMeta
26
, reportSDoc, reportSLn, getConstInfo
28
import qualified Agda.TypeChecking.Monad as TCM
29
import Agda.TypeChecking.Monad.Builtin hiding (getPrimitive, constructorForm)
27
30
import Agda.TypeChecking.Substitute
28
import Agda.TypeChecking.Free
31
import Agda.TypeChecking.CompiledClause
29
32
import Agda.TypeChecking.EtaContract
30
import Agda.TypeChecking.CompiledClause
31
33
import {-# SOURCE #-} Agda.TypeChecking.Pretty
33
import {-# SOURCE #-} Agda.TypeChecking.Level
34
35
import {-# SOURCE #-} Agda.TypeChecking.Patterns.Match
35
36
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Match
38
import Agda.TypeChecking.Reduce.Monad
37
40
import Agda.Utils.Monad
38
41
import Agda.Utils.HashMap (HashMap)
39
import qualified Agda.Utils.HashMap as HMap
42
import Agda.Utils.Maybe
43
import Agda.Utils.Monad
44
import Agda.Utils.Tuple
41
46
#include "../undefined.h"
42
47
import Agda.Utils.Impossible
44
traceFun :: String -> TCM a -> TCM a
46
reportSLn "tc.inst" 100 $ "[ " ++ s
48
reportSLn "tc.inst" 100 $ "]"
51
traceFun' :: Show a => String -> TCM a -> TCM a
53
reportSLn "tc.inst" 100 $ "[ " ++ s
55
reportSLn "tc.inst" 100 $ " result = " ++ show x ++ "\n]"
49
instantiate :: Instantiate a => a -> TCM a
50
instantiate = runReduceM . instantiate'
52
instantiateFull :: InstantiateFull a => a -> TCM a
53
instantiateFull = runReduceM . instantiateFull'
55
reduce :: Reduce a => a -> TCM a
56
reduce = runReduceM . reduce'
58
reduceB :: Reduce a => a -> TCM (Blocked a)
59
reduceB = runReduceM . reduceB'
61
normalise :: Normalise a => a -> TCM a
62
normalise = runReduceM . normalise'
64
simplify :: Simplify a => a -> TCM a
65
simplify = runReduceM . simplify'
58
67
-- | Instantiate something.
59
68
-- Results in an open meta variable or a non meta.
60
69
-- Doesn't do any reduction, and preserves blocking tags (when blocking meta
61
70
-- is uninstantiated).
62
71
class Instantiate t where
63
instantiate :: t -> TCM t
72
instantiate' :: t -> ReduceM t
65
74
instance Instantiate Term where
66
instantiate t@(MetaV x args) = do
75
instantiate' t@(MetaV x es) = do
67
76
mi <- mvInstantiation <$> lookupMeta x
69
InstV a -> instantiate $ a `apply` args
72
BlockedConst _ -> return t
73
PostponedTypeCheckingProblem _ -> return t
74
InstS _ -> __IMPOSSIBLE__
75
instantiate (Level l) = levelTm <$> instantiate l
76
instantiate (Sort s) = sortTm <$> instantiate s
77
instantiate v@Shared{} = updateSharedTerm instantiate v
78
instantiate t = return t
78
InstV a -> instantiate' $ a `applyE` es
81
BlockedConst _ -> return t
82
PostponedTypeCheckingProblem _ _ -> return t
83
InstS _ -> __IMPOSSIBLE__
84
instantiate' (Level l) = levelTm <$> instantiate' l
85
instantiate' (Sort s) = sortTm <$> instantiate' s
86
instantiate' v@Shared{} =
87
__IMPOSSIBLE__ -- updateSharedTerm instantiate' v
88
instantiate' t = return t
80
90
instance Instantiate Level where
81
instantiate (Max as) = levelMax <$> instantiate as
91
instantiate' (Max as) = levelMax <$> instantiate' as
83
93
instance Instantiate PlusLevel where
84
instantiate l@ClosedLevel{} = return l
85
instantiate (Plus n a) = Plus n <$> instantiate a
94
instantiate' l@ClosedLevel{} = return l
95
instantiate' (Plus n a) = Plus n <$> instantiate' a
87
97
instance Instantiate LevelAtom where
88
instantiate l = case l of
98
instantiate' l = case l of
89
99
MetaLevel m vs -> do
90
v <- instantiate (MetaV m vs)
100
v <- instantiate' (MetaV m vs)
91
101
case ignoreSharing v of
92
102
MetaV m vs -> return $ MetaLevel m vs
93
103
_ -> return $ UnreducedLevel v
94
UnreducedLevel l -> UnreducedLevel <$> instantiate l
104
UnreducedLevel l -> UnreducedLevel <$> instantiate' l
97
107
instance Instantiate a => Instantiate (Blocked a) where
98
instantiate v@NotBlocked{} = return v
99
instantiate v@(Blocked x u) = do
108
instantiate' v@NotBlocked{} = return v
109
instantiate' v@(Blocked x u) = do
100
110
mi <- mvInstantiation <$> lookupMeta x
102
InstV _ -> notBlocked <$> instantiate u
105
BlockedConst _ -> return v
106
PostponedTypeCheckingProblem _ -> return v
107
InstS _ -> __IMPOSSIBLE__
112
InstV _ -> notBlocked <$> instantiate' u
115
BlockedConst _ -> return v
116
PostponedTypeCheckingProblem _ _ -> return v
117
InstS _ -> __IMPOSSIBLE__
109
119
instance Instantiate Type where
110
instantiate (El s t) = El <$> instantiate s <*> instantiate t
120
instantiate' (El s t) = El <$> instantiate' s <*> instantiate' t
112
122
instance Instantiate Sort where
113
instantiate s = case s of
114
Type l -> levelSort <$> instantiate l
123
instantiate' s = case s of
124
Type l -> levelSort <$> instantiate' l
117
127
instance Instantiate Elim where
118
instantiate (Apply v) = Apply <$> instantiate v
119
instantiate (Proj f) = pure $ Proj f
128
instantiate' (Apply v) = Apply <$> instantiate' v
129
instantiate' (Proj f) = pure $ Proj f
121
131
instance Instantiate t => Instantiate (Abs t) where
122
instantiate = traverse instantiate
132
instantiate' = traverse instantiate'
124
134
instance Instantiate t => Instantiate (Arg t) where
125
instantiate = traverse instantiate
135
instantiate' = traverse instantiate'
127
137
instance Instantiate t => Instantiate (Dom t) where
128
instantiate = traverse instantiate
138
instantiate' = traverse instantiate'
130
140
instance Instantiate t => Instantiate [t] where
131
instantiate = traverse instantiate
141
instantiate' = traverse instantiate'
133
143
instance (Instantiate a, Instantiate b) => Instantiate (a,b) where
134
instantiate (x,y) = (,) <$> instantiate x <*> instantiate y
144
instantiate' (x,y) = (,) <$> instantiate' x <*> instantiate' y
137
147
instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where
138
instantiate (x,y,z) = (,,) <$> instantiate x <*> instantiate y <*> instantiate z
148
instantiate' (x,y,z) = (,,) <$> instantiate' x <*> instantiate' y <*> instantiate' z
140
150
instance Instantiate a => Instantiate (Closure a) where
142
x <- enterClosure cl instantiate
152
x <- enterClosure cl instantiate'
143
153
return $ cl { clValue = x }
145
155
instance Instantiate Telescope where
146
instantiate tel = return tel
156
instantiate' tel = return tel
148
158
instance Instantiate Constraint where
149
instantiate (ValueCmp cmp t u v) = do
150
(t,u,v) <- instantiate (t,u,v)
159
instantiate' (ValueCmp cmp t u v) = do
160
(t,u,v) <- instantiate' (t,u,v)
151
161
return $ ValueCmp cmp t u v
152
instantiate (ElimCmp cmp t v as bs) =
153
ElimCmp cmp <$> instantiate t <*> instantiate v <*> instantiate as <*> instantiate bs
154
instantiate (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> instantiate (u,v)
155
instantiate (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> instantiate (a,b)
156
instantiate (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> instantiate (tela,telb)
157
instantiate (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> instantiate (a,b)
158
instantiate (Guarded c pid) = Guarded <$> instantiate c <*> pure pid
159
instantiate (UnBlock m) = return $ UnBlock m
160
instantiate (FindInScope m args) = FindInScope m <$> mapM instantiate args
161
instantiate (IsEmpty r t) = IsEmpty r <$> instantiate t
162
instantiate' (ElimCmp cmp t v as bs) =
163
ElimCmp cmp <$> instantiate' t <*> instantiate' v <*> instantiate' as <*> instantiate' bs
164
instantiate' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> instantiate' (u,v)
165
instantiate' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> instantiate' (a,b)
166
instantiate' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> instantiate' (tela,telb)
167
instantiate' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> instantiate' (a,b)
168
instantiate' (Guarded c pid) = Guarded <$> instantiate' c <*> pure pid
169
instantiate' (UnBlock m) = return $ UnBlock m
170
instantiate' (FindInScope m args) = FindInScope m <$> mapM instantiate' args
171
instantiate' (IsEmpty r t) = IsEmpty r <$> instantiate' t
163
173
instance (Ord k, Instantiate e) => Instantiate (Map k e) where
164
instantiate = traverse instantiate
174
instantiate' = traverse instantiate'
167
177
---------------------------------------------------------------------------
244
249
instance (Subst t, Reduce t) => Reduce (Abs t) where
245
reduce b@(Abs x _) = Abs x <$> underAbstraction_ b reduce
246
reduce (NoAbs x v) = NoAbs x <$> reduce v
250
reduce' b@(Abs x _) = Abs x <$> underAbstraction_ b reduce'
251
reduce' (NoAbs x v) = NoAbs x <$> reduce' v
248
253
-- Lists are never blocked
249
254
instance Reduce t => Reduce [t] where
250
reduce = traverse reduce
255
reduce' = traverse reduce'
252
257
instance Reduce t => Reduce (Arg t) where
253
reduce a@(Arg h Irrelevant t) = return a -- Don't reduce irr. args!?
254
reduce a = traverse reduce a
258
reduce' a = case getRelevance a of
259
Irrelevant -> return a -- Don't reduce' irr. args!?
260
_ -> traverse reduce' a
256
reduceB t = traverse id <$> traverse reduceB t
262
reduceB' t = traverse id <$> traverse reduceB' t
258
264
instance Reduce t => Reduce (Dom t) where
259
reduce = traverse reduce
260
reduceB t = traverse id <$> traverse reduceB t
265
reduce' = traverse reduce'
266
reduceB' t = traverse id <$> traverse reduceB' t
262
268
-- Tuples are never blocked
263
269
instance (Reduce a, Reduce b) => Reduce (a,b) where
264
reduce (x,y) = (,) <$> reduce x <*> reduce y
270
reduce' (x,y) = (,) <$> reduce' x <*> reduce' y
266
272
instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where
267
reduce (x,y,z) = (,,) <$> reduce x <*> reduce y <*> reduce z
273
reduce' (x,y,z) = (,,) <$> reduce' x <*> reduce' y <*> reduce' z
269
275
instance Reduce Term where
270
reduceB v = {-# SCC "reduce<Term>" #-} do
276
reduceB' v = {-# SCC "reduce'<Term>" #-} do
278
let done = return $ notBlocked v
273
280
-- Andreas, 2012-11-05 not reducing meta args does not destroy anything
274
281
-- and seems to save 2% sec on the standard library
275
MetaV x args -> return $ notBlocked v
276
Def f args -> unfoldDefinition False reduceB (Def f []) f args
278
-- Constructors can reduce when they come from an
282
-- MetaV x args -> notBlocked . MetaV x <$> reduce' args
284
Def f es -> unfoldDefinitionE False reduceB' (Def f []) f es
286
-- Constructors can reduce' when they come from an
279
287
-- instantiated module.
280
v <- unfoldDefinition False reduceB (Con c []) c args
288
v <- unfoldDefinition False reduceB' (Con c []) (conName c) args
281
289
traverse reduceNat v
282
Sort s -> fmap sortTm <$> reduceB s
283
Level l -> fmap levelTm <$> reduceB l
284
Pi _ _ -> return $ notBlocked v
285
Lit _ -> return $ notBlocked v
286
Var _ _ -> return $ notBlocked v
287
Lam _ _ -> return $ notBlocked v
288
DontCare _ -> return $ notBlocked v
289
Shared{} -> updateSharedTermF reduceB v
290
Sort s -> fmap sortTm <$> reduceB' s
291
Level l -> ifM (elem LevelReductions <$> asks envAllowedReductions)
292
{- then -} (fmap levelTm <$> reduceB' l)
294
-- Level l -> fmap levelTm <$> reduceB' l
300
Shared{} -> __IMPOSSIBLE__ -- updateSharedTermF reduceB' v
291
302
-- NOTE: reduceNat can traverse the entire term.
292
reduceNat v@Shared{} = updateSharedTerm reduceNat v
303
reduceNat v@Shared{} = __IMPOSSIBLE__ -- updateSharedTerm reduceNat v
293
304
reduceNat v@(Con c []) = do
294
305
mz <- getBuiltin' builtinZero
296
307
_ | Just v == mz -> return $ Lit $ LitInt (getRange c) 0
298
reduceNat v@(Con c [Arg NotHidden Relevant w]) = do
309
reduceNat v@(Con c [a]) | notHidden a && isRelevant a = do
299
310
ms <- fmap ignoreSharing <$> getBuiltin' builtinSuc
301
_ | Just (Con c []) == ms -> inc <$> reduce w
312
_ | Just (Con c []) == ms -> inc <$> reduce' (unArg a)
304
315
inc w = case ignoreSharing w of
305
316
Lit (LitInt r n) -> Lit (LitInt (fuseRange c r) $ n + 1)
306
_ -> Con c [Arg NotHidden Relevant w]
317
_ -> Con c [defaultArg w]
307
318
reduceNat v = return v
309
320
-- | If the first argument is 'True', then a single delayed clause may
311
322
unfoldDefinition ::
312
Bool -> (Term -> TCM (Blocked Term)) ->
313
Term -> QName -> Args -> TCM (Blocked Term)
314
unfoldDefinition unfoldDelayed keepGoing v0 f args =
323
Bool -> (Term -> ReduceM (Blocked Term)) ->
324
Term -> QName -> Args -> ReduceM (Blocked Term)
325
unfoldDefinition b keepGoing v f args = snd <$> do
326
unfoldDefinition' b (\ t -> (NoSimplification,) <$> keepGoing t) v f $
330
Bool -> (Term -> ReduceM (Blocked Term)) ->
331
Term -> QName -> Elims -> ReduceM (Blocked Term)
332
unfoldDefinitionE b keepGoing v f es = snd <$>
333
unfoldDefinition' b (\ t -> (NoSimplification,) <$> keepGoing t) v f es
336
Bool -> (Term -> ReduceM (Simplification, Blocked Term)) ->
337
Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
338
unfoldDefinition' unfoldDelayed keepGoing v0 f es =
315
339
{-# SCC "reduceDef" #-} do
316
340
info <- getConstInfo f
341
let def = theDef info
318
344
Constructor{conSrcCon = c} ->
319
return $ notBlocked $ Con (c `withRangeOf` f) args
345
retSimpl $ notBlocked $ Con (c `withRangeOf` f) [] `applyE` es
320
346
Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do
322
reducePrimitive x v0 f args pf (defDelayed info)
323
(maybe [] id cls) (defCompiled info)
324
_ -> reduceNormal v0 f (map notReduced args) (defDelayed info)
347
pf <- fromMaybe __IMPOSSIBLE__ <$> getPrimitive' x
348
reducePrimitive x v0 f es pf (defDelayed info) (defNonterminating info)
349
cls (defCompiled info)
351
allowed <- asks envAllowedReductions
353
-- case f is projection-like:
354
if isProperProjection def then
355
if ProjectionReductions `elem` allowed then do
356
-- we cannot call elimView right away, since it calls back to reduce'
357
-- get rid of projection if possible
358
(simpl, w) <- onlyReduceProjections $ do
359
reduceNormal (retSimpl <=< reduceB') v0 f (map notReduced args)
360
(defDelayed info) (defNonterminating info)
361
(defClauses info) (defCompiled info)
362
-- Now @w@ should not have any reducible projection in the head.
363
-- By not allowing reentrace (dontReduceProjections),
364
-- we can now call elimView without risk of circularity.
366
Blocked{} -> return (simpl, w)
368
ev <- dontReduceProjections $ elimView w'
370
DefElim f es -> performedSimplification' simpl $ do
372
_ -> return (simpl, w)
373
else retSimpl $ notBlocked v
374
-- case f is not a projection:
375
else if FunctionReductions `elem` allowed then
376
-- proceed as before, without calling elimView
378
if FunctionReductions `elem` allowed ||
379
(isJust (isProjection_ def) && ProjectionReductions `elem` allowed) -- includes projection-like
381
reduceNormalE keepGoing v0 f (map notReduced es)
382
(defDelayed info) (defNonterminating info)
325
383
(defClauses info) (defCompiled info)
384
else retSimpl $ notBlocked v
327
reducePrimitive x v0 f args pf delayed cls mcc
328
| n < ar = return $ notBlocked $ v0 `apply` args -- not fully applied
329
| otherwise = {-# SCC "reducePrimitive" #-} do
330
let (args1,args2) = genericSplitAt ar args
333
NoReduction args1' ->
335
return $ apply (Def f []) <$> traverse id (map mredToBlocked args1' ++ map notBlocked args2)
337
reduceNormal v0 f (args1' ++
338
map notReduced args2)
341
keepGoing $ v `apply` args2
343
n = genericLength args
345
def = primFunImplementation pf
346
mredToBlocked :: MaybeReduced a -> Blocked a
347
mredToBlocked (MaybeRed NotReduced x) = notBlocked x
348
mredToBlocked (MaybeRed (Reduced b) x) = x <$ b
350
reduceNormal :: Term -> QName -> [MaybeReduced (Arg Term)] -> Delayed -> [Clause] -> Maybe CompiledClauses -> TCM (Blocked Term)
351
reduceNormal v0 f args delayed def mcc = {-# SCC "reduceNormal" #-} do
353
_ | Delayed <- delayed,
354
not unfoldDelayed -> defaultResult
355
[] -> defaultResult -- no definition for head
357
ev <- maybe (appDef' v0 cls args)
358
(\cc -> appDef v0 cc args) mcc
387
retSimpl v = (,v) <$> getSimplification
389
reduceDefElim :: QName -> [Elim] -> ReduceM (Simplification, Blocked Term)
390
reduceDefElim f es = do
391
info <- getConstInfo f
392
reduceNormalE keepGoing (Def f []) f (map notReduced es)
393
(defDelayed info) (defNonterminating info)
394
(defClauses info) (defCompiled info)
397
reducePrimitive x v0 f es pf delayed nonterminating cls mcc
398
| genericLength es < ar
399
= retSimpl $ notBlocked $ v0 `applyE` es -- not fully applied
400
| otherwise = {-# SCC "reducePrimitive" #-} do
401
let (es1,es2) = genericSplitAt ar es
402
args1 = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1
403
r <- primFunImplementation pf args1
405
NoReduction args1' -> do
406
let es1' = map (fmap Apply) args1'
408
retSimpl $ applyE (Def f []) <$> do
410
map mredToBlocked es1' ++ map notBlocked es2
412
reduceNormalE keepGoing v0 f
413
(es1' ++ map notReduced es2)
414
delayed nonterminating cls mcc
415
YesReduction simpl v -> performedSimplification' simpl $
416
keepGoing $ v `applyE` es2
419
mredToBlocked :: MaybeReduced a -> Blocked a
420
mredToBlocked (MaybeRed NotReduced x) = notBlocked x
421
mredToBlocked (MaybeRed (Reduced b) x) = x <$ b
424
reduceNormal :: (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> [MaybeReduced (Arg Term)] -> Delayed -> Bool -> [Clause] -> Maybe CompiledClauses -> ReduceM (Simplification, Blocked Term)
425
reduceNormal keepGoing v0 f args = reduceNormalE keepGoing v0 f $ map (fmap Apply) args
428
reduceNormalE :: (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> [MaybeReduced Elim] -> Delayed -> Bool -> [Clause] -> Maybe CompiledClauses -> ReduceM (Simplification, Blocked Term)
429
reduceNormalE keepGoing v0 f es delayed nonterminating def mcc = {-# SCC "reduceNormal" #-} do
431
_ | nonterminating -> defaultResult
432
_ | Delayed <- delayed,
433
not unfoldDelayed -> defaultResult
434
[] -> defaultResult -- no definition for head
436
-- stop here if we only want to reduce' (proper) projections
437
-- but the symbol @f@ is not one
438
cls -> ifM (asks envOnlyReduceProjections `and2M` do not . maybe False projProper <$> isProjection f) defaultResult $ do
441
cls -> allowAllReductions $ do
442
-- In subterms, we allow all reductions.
445
ev <- appDefE_ f v0 cls mcc es
360
447
NoReduction v -> do
361
reportSDoc "tc.reduce" 90 $ vcat
362
[ text "*** tried to reduce " <+> prettyTCM f
363
, text " args " <+> prettyTCM (map (unArg . ignoreReduced) args)
364
, text " stuck on" <+> prettyTCM (ignoreBlocking v) ]
367
reportSDoc "tc.reduce" 90 $ vcat
368
[ text "*** reduced definition: " <+> prettyTCM f
370
reportSDoc "tc.reduce" 100 $ text " result" <+> prettyTCM v $$
371
text " raw " <+> text (show v)
448
traceSDoc "tc.reduce'" 90 (vcat
449
[ text "*** tried to reduce' " <+> prettyTCM f
450
, text " es = " <+> sep (map (prettyTCM . ignoreReduced) es)
451
-- [ text "*** tried to reduce' " <+> prettyTCM vfull
452
, text " stuck on" <+> prettyTCM (ignoreBlocking v) ]) $ do
454
YesReduction simpl v -> performedSimplification' simpl $ do
455
traceSDoc "tc.reduce'" 90 (text "*** reduced definition: " <+> prettyTCM f) $ do
456
traceSDoc "tc.reduce'" 95 (text " result" <+> prettyTCM v) $ do
457
traceSDoc "tc.reduce'" 100 (text " raw " <+> text (show v)) $ do
373
where defaultResult = return $ notBlocked $ v0 `apply` (map ignoreReduced args)
459
where defaultResult = retSimpl $ notBlocked $ vfull
460
vfull = v0 `applyE` map ignoreReduced es
461
-- where defaultResult = retSimpl $ notBlocked $ v0 `apply` (map ignoreReduced args)
375
463
-- | Reduce a non-primitive definition if it is a copy linking to another def.
376
464
reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
377
465
reduceDefCopy f vs = do
378
info <- getConstInfo f
466
info <- TCM.getConstInfo f
379
467
if (defCopy info) then reduceDef_ info f vs else return $ NoReduction ()
381
469
-- | Reduce a non-primitive definition once unless it is delayed.
382
470
reduceDef :: QName -> Args -> TCM (Reduced () Term)
383
471
reduceDef f vs = do
384
info <- getConstInfo f
472
info <- TCM.getConstInfo f
385
473
reduceDef_ info f vs
387
475
reduceDef_ :: Definition -> QName -> Args -> TCM (Reduced () Term)
391
478
args = map notReduced vs
392
479
cls = (defClauses info)
393
480
mcc = (defCompiled info)
394
delayed = (defDelayed info)
396
Delayed -> return $ NoReduction ()
398
ev <- maybe (appDef' v0 cls args)
399
(\cc -> appDef v0 cc args) mcc
481
if (defDelayed info == Delayed) || (defNonterminating info)
482
then return $ NoReduction ()
484
ev <- runReduceM $ appDef_ f v0 cls mcc args
401
YesReduction t -> return $ YesReduction t
402
NoReduction args' -> return $ NoReduction ()
486
YesReduction simpl t -> return $ YesReduction simpl t
487
NoReduction args' -> return $ NoReduction ()
489
-- | Reduce simple (single clause) definitions.
490
reduceHead :: Term -> TCM (Blocked Term)
491
reduceHead = runReduceM . reduceHead'
493
reduceHead' :: Term -> ReduceM (Blocked Term)
494
reduceHead' v = do -- ignoreAbstractMode $ do
495
-- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage
498
-- first, possibly rewrite literal v to constructor form
499
v <- constructorForm v
500
reportSDoc "tc.inj.reduce" 30 $ text "reduceHead" <+> prettyTCM v
501
case ignoreSharing v of
504
abstractMode <- envAbstractMode <$> ask
505
isAbstract <- treatAbstractly f
506
reportSLn "tc.inj.reduce" 50 $
507
"reduceHead: we are in " ++ show abstractMode++ "; " ++ show f ++
508
" is treated " ++ if isAbstract then "abstractly" else "concretely"
511
red = unfoldDefinitionE False reduceHead' v0 f es
512
def <- theDef <$> getConstInfo f
514
-- Andreas, 2012-11-06 unfold aliases (single clause terminating functions)
515
-- see test/succeed/Issue747
516
-- We restrict this to terminating functions to not make the
517
-- type checker loop here on non-terminating functions.
518
-- see test/fail/TerminationInfiniteRecord
519
Function{ funClauses = [ _ ], funDelayed = NotDelayed, funTerminates = Just True } -> do
520
reportSLn "tc.inj.reduce" 50 $ "reduceHead: head " ++ show f ++ " is Function"
522
Datatype{ dataClause = Just _ } -> red
523
Record{ recClause = Just _ } -> red
524
_ -> return $ notBlocked v
525
_ -> return $ notBlocked v
527
-- | Apply a definition using the compiled clauses, or fall back to
528
-- ordinary clauses if no compiled clauses exist.
529
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
530
appDef_ f v0 cls mcc args = appDefE_ f v0 cls mcc $ map (fmap Apply) args
532
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
533
appDefE_ f v0 cls mcc args =
534
local (\ e -> e { envAppDef = Just f }) $
535
maybe (appDefE' v0 cls args)
536
(\cc -> appDefE v0 cc args) mcc
539
-- | Apply a defined function to it's arguments, using the compiled clauses.
404
540
-- The original term is the first argument applied to the third.
405
appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Term) Term)
406
appDef v cc args = liftTCM $ do
407
r <- matchCompiled cc args
541
appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
542
appDef v cc args = appDefE v cc $ map (fmap Apply) args
544
appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
546
r <- matchCompiledE cc es
409
YesReduction t -> return $ YesReduction t
410
NoReduction args' -> return $ NoReduction $ fmap (apply v) args'
412
appDef' :: Term -> [Clause] -> MaybeReducedArgs -> TCM (Reduced (Blocked Term) Term)
413
appDef' _ [] _ = {- ' -} __IMPOSSIBLE__
414
appDef' v cls@(Clause {clausePats = ps} : _) args
415
| m < n = return $ NoReduction $ notBlocked $ v `apply` map ignoreReduced args
548
YesReduction simpl t -> return $ YesReduction simpl t
549
NoReduction es' -> return $ NoReduction $ applyE v <$> es'
551
-- | Apply a defined function to it's arguments, using the original clauses.
552
appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
553
appDef' v cls args = appDefE' v cls $ map (fmap Apply) args
555
{- OLD. With varying function arity, check for underapplication is UNSOUND.
556
appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
557
appDefE' _ [] _ = {- ' -} __IMPOSSIBLE__
558
appDefE' v cls@(Clause {clausePats = ps} : _) es
559
-- case underapplied: no reduction
560
| m < n = return $ NoReduction $ notBlocked $ v `applyE` map ignoreReduced es
417
let (args0, args1) = splitAt n args
418
r <- goCls cls (map ignoreReduced args0)
562
let (es0, es1) = splitAt n es
563
r <- goCls cls (map ignoreReduced es0)
420
YesReduction u -> return $ YesReduction $ u `apply` map ignoreReduced args1
421
NoReduction v -> return $ NoReduction $ (`apply` map ignoreReduced args1) <$> v
565
YesReduction simpl u -> return $ YesReduction simpl $ u `applyE` map ignoreReduced es1
566
NoReduction v -> return $ NoReduction $ (`applyE` map ignoreReduced es1) <$> v
424
569
n = genericLength ps
425
m = genericLength args
427
goCls :: [Clause] -> Args -> TCM (Reduced (Blocked Term) Term)
428
goCls [] args = typeError $ IncompletePatternMatching v args
429
goCls (cl@(Clause { clausePats = pats
430
, clauseBody = body }) : cls) args = do
431
(m, args) <- matchPatterns pats args
434
DontKnow Nothing -> return $ NoReduction $ notBlocked $ v `apply` args
435
DontKnow (Just m) -> return $ NoReduction $ blocked m $ v `apply` args
437
| hasBody body -> return $ YesReduction (
438
-- TODO: let matchPatterns also return the reduced forms
439
-- of the original arguments!
441
| otherwise -> return $ NoReduction $ notBlocked $ v `apply` args
443
hasBody (Body _) = True
444
hasBody NoBody = False
445
hasBody (Bind b) = hasBody (unAbs b)
447
app [] (Body v') = v'
448
app (arg : args) (Bind b) = app args $ absApp b arg -- CBN
449
app _ NoBody = __IMPOSSIBLE__
450
app (_ : _) (Body _) = __IMPOSSIBLE__
451
app [] (Bind _) = __IMPOSSIBLE__
572
appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
573
appDefE' v cls es = goCls cls $ map ignoreReduced es
575
goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term)
577
reportSLn "tc.reduce'" 95 $ "Reduce.goCls tries reduction, #clauses = " ++ show (length cl)
578
let cantReduce es = return $ NoReduction $ notBlocked $ v `applyE` es
580
-- Andreas, 2013-10-26 In case of an incomplete match,
581
-- we just do not reduce'. This allows adding single function
582
-- clauses after they have been type-checked, to type-check
583
-- the remaining clauses (see Issue 907).
584
[] -> cantReduce es -- WAS: typeError $ IncompletePatternMatching v es
585
cl @ Clause { clauseBody = body } : cls -> do
586
let pats = namedClausePats cl
588
-- if clause is underapplied, skip to next clause
589
if length es < n then goCls cls es else do
590
let (es0, es1) = splitAt n es
591
(m, es0) <- matchCopatterns pats es0
592
es <- return $ es0 ++ es1
595
DontKnow Nothing -> cantReduce es
596
DontKnow (Just m) -> return $ NoReduction $ blocked m $ v `applyE` es
597
Yes simpl vs -- vs is the subst. for the variables bound in body
598
| isJust (getBody body) -- clause has body?
599
-> return $ YesReduction simpl $
600
-- TODO: let matchPatterns also return the reduced forms
601
-- of the original arguments!
602
-- Andreas, 2013-05-19 isn't this done now?
603
app vs body EmptyS `applyE` es1
604
| otherwise -> cantReduce es
607
-- NEW version, building an explicit substitution from arguments
608
-- and executing it using parallel substitution.
609
-- Calculating the de Bruijn indices: ;-) for the Bind case
610
-- Simply-typed version
611
-- (we are not interested in types, only in de Bruijn indices here)
617
app :: [Term] -> ClauseBody -> Substitution -> Term
618
app [] (Body v) sigma = applySubst sigma v
619
-- app (v : vs) (Bind b) sigma = app es (absBody b) (v :# sigma) -- CBN
620
app (v : vs) (Bind (Abs _ b)) sigma = app vs b (v :# sigma) -- CBN
621
app (v : vs) (Bind (NoAbs _ b)) sigma = app vs b sigma
622
app _ NoBody sigma = __IMPOSSIBLE__
623
app (_ : _) (Body _) sigma = __IMPOSSIBLE__
624
app [] (Bind _) sigma = __IMPOSSIBLE__
626
{- OLD version, one substitution after another
627
app :: [Elim] -> ClauseBody -> Term
628
app [] (Body v') = v'
629
app (Proj f : es) b = app es b
630
app (Apply arg : es) (Bind b) = app es $ absApp b $ unArg arg -- CBN
631
app _ NoBody = __IMPOSSIBLE__
632
app (_ : _) (Body _) = __IMPOSSIBLE__
633
app [] (Bind _) = __IMPOSSIBLE__
454
636
instance Reduce a => Reduce (Closure a) where
456
x <- enterClosure cl reduce
638
x <- enterClosure cl reduce'
457
639
return $ cl { clValue = x }
459
641
instance Reduce Telescope where
460
reduce tel = return tel
642
reduce' tel = return tel
462
644
instance Reduce Constraint where
463
reduce (ValueCmp cmp t u v) = do
464
(t,u,v) <- reduce (t,u,v)
645
reduce' (ValueCmp cmp t u v) = do
646
(t,u,v) <- reduce' (t,u,v)
465
647
return $ ValueCmp cmp t u v
466
reduce (ElimCmp cmp t v as bs) =
467
ElimCmp cmp <$> reduce t <*> reduce v <*> reduce as <*> reduce bs
468
reduce (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> reduce (u,v)
469
reduce (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> reduce (a,b)
470
reduce (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> reduce (tela,telb)
471
reduce (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> reduce (a,b)
472
reduce (Guarded c pid) = Guarded <$> reduce c <*> pure pid
473
reduce (UnBlock m) = return $ UnBlock m
474
reduce (FindInScope m cands) = FindInScope m <$> mapM reduce cands
475
reduce (IsEmpty r t) = IsEmpty r <$> reduce t
648
reduce' (ElimCmp cmp t v as bs) =
649
ElimCmp cmp <$> reduce' t <*> reduce' v <*> reduce' as <*> reduce' bs
650
reduce' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> reduce' (u,v)
651
reduce' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> reduce' (a,b)
652
reduce' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> reduce' (tela,telb)
653
reduce' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> reduce' (a,b)
654
reduce' (Guarded c pid) = Guarded <$> reduce' c <*> pure pid
655
reduce' (UnBlock m) = return $ UnBlock m
656
reduce' (FindInScope m cands) = FindInScope m <$> mapM reduce' cands
657
reduce' (IsEmpty r t) = IsEmpty r <$> reduce' t
477
659
instance (Ord k, Reduce e) => Reduce (Map k e) where
478
reduce = traverse reduce
660
reduce' = traverse reduce'
662
---------------------------------------------------------------------------
664
---------------------------------------------------------------------------
666
-- | Only unfold definitions if this leads to simplification
667
-- which means that a constructor/literal pattern is matched.
668
class Simplify t where
669
simplify' :: t -> ReduceM t
671
instance Simplify Term where
676
let keepGoing v = (,NotBlocked v) <$> getSimplification
677
(simpl, v) <- unfoldDefinition' False keepGoing (Def f []) f vs
678
reportSDoc "tc.simplify'" 20 $
679
text ("simplify': unfolding definition returns " ++ show simpl)
680
<+> prettyTCM (ignoreBlocking v)
682
YesSimplification -> simplifyBlocked' v -- Dangerous, but if @simpl@ then @v /= Def f vs@
683
NoSimplification -> Def f <$> simplify' vs
684
MetaV x vs -> MetaV x <$> simplify' vs
685
Con c vs -> Con c <$> simplify' vs
686
Sort s -> sortTm <$> simplify' s
687
Level l -> levelTm <$> simplify' l
688
Pi a b -> Pi <$> simplify' a <*> simplify' b
690
Var i vs -> Var i <$> simplify' vs
691
Lam h v -> Lam h <$> simplify' v
692
DontCare v -> dontCare <$> simplify' v
693
Shared{} -> __IMPOSSIBLE__ -- updateSharedTerm simplify' v
695
simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
696
simplifyBlocked' (Blocked _ t) = return t
697
simplifyBlocked' (NotBlocked t) = simplify' t
699
instance Simplify Type where
700
simplify' (El s t) = El <$> simplify' s <*> simplify' t
702
instance Simplify Elim where
703
simplify' (Apply v) = Apply <$> simplify' v
704
simplify' (Proj f) = pure $ Proj f
706
instance Simplify Sort where
709
DLub s1 s2 -> dLub <$> simplify' s1 <*> simplify' s2
710
Type s -> levelSort <$> simplify' s
714
instance Simplify Level where
715
simplify' (Max as) = levelMax <$> simplify' as
717
instance Simplify PlusLevel where
718
simplify' l@ClosedLevel{} = return l
719
simplify' (Plus n l) = Plus n <$> simplify' l
721
instance Simplify LevelAtom where
725
MetaLevel m vs -> MetaLevel m <$> simplify' vs
726
BlockedLevel m v -> BlockedLevel m <$> simplify' v
727
NeutralLevel v -> NeutralLevel <$> simplify' v -- ??
728
UnreducedLevel v -> UnreducedLevel <$> simplify' v -- ??
730
instance (Subst t, Simplify t) => Simplify (Abs t) where
731
simplify' a@(Abs x _) = Abs x <$> underAbstraction_ a simplify'
732
simplify' (NoAbs x v) = NoAbs x <$> simplify' v
734
instance Simplify t => Simplify (Arg t) where
735
simplify' = traverse simplify'
737
instance Simplify t => Simplify (Named name t) where
738
simplify' = traverse simplify'
740
instance Simplify t => Simplify (Dom t) where
741
simplify' = traverse simplify'
743
instance Simplify t => Simplify [t] where
744
simplify' = traverse simplify'
746
instance (Ord k, Simplify e) => Simplify (Map k e) where
747
simplify' = traverse simplify'
749
instance Simplify a => Simplify (Maybe a) where
750
simplify' = traverse simplify'
752
instance (Simplify a, Simplify b) => Simplify (a,b) where
753
simplify' (x,y) = (,) <$> simplify' x <*> simplify' y
755
instance (Simplify a, Simplify b, Simplify c) => Simplify (a,b,c) where
757
do (x,(y,z)) <- simplify' (x,(y,z))
760
instance Simplify a => Simplify (Closure a) where
762
x <- enterClosure cl simplify'
763
return $ cl { clValue = x }
765
instance (Subst a, Simplify a) => Simplify (Tele a) where
766
simplify' EmptyTel = return EmptyTel
767
simplify' (ExtendTel a b) = uncurry ExtendTel <$> simplify' (a, b)
769
instance Simplify ProblemConstraint where
770
simplify' (PConstr pid c) = PConstr pid <$> simplify' c
772
instance Simplify Constraint where
773
simplify' (ValueCmp cmp t u v) = do
774
(t,u,v) <- simplify' (t,u,v)
775
return $ ValueCmp cmp t u v
776
simplify' (ElimCmp cmp t v as bs) =
777
ElimCmp cmp <$> simplify' t <*> simplify' v <*> simplify' as <*> simplify' bs
778
simplify' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> simplify' (u,v)
779
simplify' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> simplify' (a,b)
780
simplify' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> simplify' (tela,telb)
781
simplify' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> simplify' (a,b)
782
simplify' (Guarded c pid) = Guarded <$> simplify' c <*> pure pid
783
simplify' (UnBlock m) = return $ UnBlock m
784
simplify' (FindInScope m cands) = FindInScope m <$> mapM simplify' cands
785
simplify' (IsEmpty r t) = IsEmpty r <$> simplify' t
787
instance Simplify Bool where
790
instance Simplify Pattern where
791
simplify' p = case p of
794
ConP c mt ps -> ConP c <$> simplify' mt <*> simplify' ps
795
DotP v -> DotP <$> simplify' v
798
instance Simplify ClauseBody where
799
simplify' (Body t) = Body <$> simplify' t
800
simplify' (Bind b) = Bind <$> simplify' b
801
simplify' NoBody = return NoBody
803
instance Simplify DisplayForm where
804
simplify' (Display n ps v) = Display n <$> simplify' ps <*> return v
480
807
---------------------------------------------------------------------------
481
808
-- * Normalisation
482
809
---------------------------------------------------------------------------
484
811
class Normalise t where
485
normalise :: t -> TCM t
812
normalise' :: t -> ReduceM t
487
814
instance Normalise Sort where
491
DLub s1 s2 -> dLub <$> normalise s1 <*> normalise s2
818
DLub s1 s2 -> dLub <$> normalise' s1 <*> normalise' s2
493
Type s -> levelSort <$> normalise s
820
Type s -> levelSort <$> normalise' s
494
821
Inf -> return Inf
496
823
instance Normalise Type where
497
normalise (El s t) = El <$> normalise s <*> normalise t
824
normalise' (El s t) = El <$> normalise' s <*> normalise' t
499
826
instance Normalise Term where
503
Var n vs -> Var n <$> normalise vs
504
Con c vs -> Con c <$> normalise vs
505
Def f vs -> Def f <$> normalise vs
506
MetaV x vs -> MetaV x <$> normalise vs
830
Var n vs -> Var n <$> normalise' vs
831
Con c vs -> Con c <$> normalise' vs
832
Def f vs -> Def f <$> normalise' vs
833
MetaV x vs -> MetaV x <$> normalise' vs
507
834
Lit _ -> return v
508
Level l -> levelTm <$> normalise l
509
Lam h b -> Lam h <$> normalise b
510
Sort s -> sortTm <$> normalise s
511
Pi a b -> uncurry Pi <$> normalise (a,b)
512
Shared{} -> updateSharedTerm normalise v
835
Level l -> levelTm <$> normalise' l
836
Lam h b -> Lam h <$> normalise' b
837
Sort s -> sortTm <$> normalise' s
838
Pi a b -> uncurry Pi <$> normalise' (a,b)
839
Shared{} -> __IMPOSSIBLE__ -- updateSharedTerm normalise' v
513
840
DontCare _ -> return v
515
842
instance Normalise Elim where
516
normalise (Apply v) = Apply <$> normalise v
517
normalise (Proj f) = pure $ Proj f
843
normalise' (Apply v) = Apply <$> normalise' v
844
normalise' (Proj f) = pure $ Proj f
519
846
instance Normalise Level where
520
normalise (Max as) = levelMax <$> normalise as
847
normalise' (Max as) = levelMax <$> normalise' as
522
849
instance Normalise PlusLevel where
523
normalise l@ClosedLevel{} = return l
524
normalise (Plus n l) = Plus n <$> normalise l
850
normalise' l@ClosedLevel{} = return l
851
normalise' (Plus n l) = Plus n <$> normalise' l
526
853
instance Normalise LevelAtom where
530
MetaLevel m vs -> MetaLevel m <$> normalise vs
531
BlockedLevel m v -> BlockedLevel m <$> normalise v
532
NeutralLevel v -> NeutralLevel <$> normalise v
857
MetaLevel m vs -> MetaLevel m <$> normalise' vs
858
BlockedLevel m v -> BlockedLevel m <$> normalise' v
859
NeutralLevel v -> NeutralLevel <$> normalise' v
533
860
UnreducedLevel{} -> __IMPOSSIBLE__ -- I hope
535
862
instance Normalise ClauseBody where
536
normalise (Body t) = Body <$> normalise t
537
normalise (Bind b) = Bind <$> normalise b
538
normalise NoBody = return NoBody
863
normalise' (Body t) = Body <$> normalise' t
864
normalise' (Bind b) = Bind <$> normalise' b
865
normalise' NoBody = return NoBody
540
867
instance (Subst t, Normalise t) => Normalise (Abs t) where
541
normalise a@(Abs x _) = Abs x <$> underAbstraction_ a normalise
542
normalise (NoAbs x v) = NoAbs x <$> normalise v
868
normalise' a@(Abs x _) = Abs x <$> underAbstraction_ a normalise'
869
normalise' (NoAbs x v) = NoAbs x <$> normalise' v
544
871
instance Normalise t => Normalise (Arg t) where
545
normalise a@(Arg h Irrelevant t) = return a -- Andreas, 2012-04-02: Do not normalize irrelevant terms!?
546
normalise a = traverse normalise a
872
normalise' a | isIrrelevant a = return a -- Andreas, 2012-04-02: Do not normalize irrelevant terms!?
873
| otherwise = traverse normalise' a
875
instance Normalise t => Normalise (Named name t) where
876
normalise' = traverse normalise'
548
878
instance Normalise t => Normalise (Dom t) where
549
normalise = traverse normalise
879
normalise' = traverse normalise'
551
881
instance Normalise t => Normalise [t] where
552
normalise = traverse normalise
882
normalise' = traverse normalise'
554
884
instance (Normalise a, Normalise b) => Normalise (a,b) where
555
normalise (x,y) = (,) <$> normalise x <*> normalise y
885
normalise' (x,y) = (,) <$> normalise' x <*> normalise' y
557
887
instance (Normalise a, Normalise b, Normalise c) => Normalise (a,b,c) where
559
do (x,(y,z)) <- normalise (x,(y,z))
889
do (x,(y,z)) <- normalise' (x,(y,z))
562
892
instance Normalise a => Normalise (Closure a) where
564
x <- enterClosure cl normalise
894
x <- enterClosure cl normalise'
565
895
return $ cl { clValue = x }
567
897
instance (Subst a, Normalise a) => Normalise (Tele a) where
568
normalise EmptyTel = return EmptyTel
569
normalise (ExtendTel a b) = uncurry ExtendTel <$> normalise (a, b)
898
normalise' EmptyTel = return EmptyTel
899
normalise' (ExtendTel a b) = uncurry ExtendTel <$> normalise' (a, b)
571
901
instance Normalise ProblemConstraint where
572
normalise (PConstr pid c) = PConstr pid <$> normalise c
902
normalise' (PConstr pid c) = PConstr pid <$> normalise' c
574
904
instance Normalise Constraint where
575
normalise (ValueCmp cmp t u v) = do
576
(t,u,v) <- normalise (t,u,v)
905
normalise' (ValueCmp cmp t u v) = do
906
(t,u,v) <- normalise' (t,u,v)
577
907
return $ ValueCmp cmp t u v
578
normalise (ElimCmp cmp t v as bs) =
579
ElimCmp cmp <$> normalise t <*> normalise v <*> normalise as <*> normalise bs
580
normalise (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> normalise (u,v)
581
normalise (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> normalise (a,b)
582
normalise (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> normalise (tela,telb)
583
normalise (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> normalise (a,b)
584
normalise (Guarded c pid) = Guarded <$> normalise c <*> pure pid
585
normalise (UnBlock m) = return $ UnBlock m
586
normalise (FindInScope m cands) = FindInScope m <$> mapM normalise cands
587
normalise (IsEmpty r t) = IsEmpty r <$> normalise t
908
normalise' (ElimCmp cmp t v as bs) =
909
ElimCmp cmp <$> normalise' t <*> normalise' v <*> normalise' as <*> normalise' bs
910
normalise' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> normalise' (u,v)
911
normalise' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> normalise' (a,b)
912
normalise' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> normalise' (tela,telb)
913
normalise' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> normalise' (a,b)
914
normalise' (Guarded c pid) = Guarded <$> normalise' c <*> pure pid
915
normalise' (UnBlock m) = return $ UnBlock m
916
normalise' (FindInScope m cands) = FindInScope m <$> mapM normalise' cands
917
normalise' (IsEmpty r t) = IsEmpty r <$> normalise' t
919
instance Normalise Bool where
589
922
instance Normalise Pattern where
590
normalise p = case p of
923
normalise' p = case p of
591
924
VarP _ -> return p
592
925
LitP _ -> return p
593
ConP c mt ps -> ConP c <$> normalise mt <*> normalise ps
594
DotP v -> DotP <$> normalise v
926
ConP c mt ps -> ConP c <$> normalise' mt <*> normalise' ps
927
DotP v -> DotP <$> normalise' v
596
930
instance Normalise DisplayForm where
597
normalise (Display n ps v) = Display n <$> normalise ps <*> return v
931
normalise' (Display n ps v) = Display n <$> normalise' ps <*> return v
599
933
instance (Ord k, Normalise e) => Normalise (Map k e) where
600
normalise = traverse normalise
934
normalise' = traverse normalise'
602
936
instance Normalise a => Normalise (Maybe a) where
603
normalise = traverse normalise
937
normalise' = traverse normalise'
605
939
---------------------------------------------------------------------------
606
940
-- * Full instantiation
607
941
---------------------------------------------------------------------------
943
-- STALE: Full instantiatiation = normalisation [ instantiate' / reduce' ]
609
944
-- How can we express this? We need higher order classes!
946
-- | @instantiateFull'@ 'instantiate's metas everywhere (and recursively)
947
-- but does not 'reduce'.
611
948
class InstantiateFull t where
612
instantiateFull :: t -> TCM t
949
instantiateFull' :: t -> ReduceM t
614
951
instance InstantiateFull Name where
615
instantiateFull = return
952
instantiateFull' = return
617
954
instance InstantiateFull Sort where
618
instantiateFull s = do
955
instantiateFull' s = do
621
Type n -> levelSort <$> instantiateFull n
958
Type n -> levelSort <$> instantiateFull' n
623
DLub s1 s2 -> dLub <$> instantiateFull s1 <*> instantiateFull s2
960
DLub s1 s2 -> dLub <$> instantiateFull' s1 <*> instantiateFull' s2
626
963
instance InstantiateFull Type where
627
instantiateFull (El s t) =
628
El <$> instantiateFull s <*> instantiateFull t
964
instantiateFull' (El s t) =
965
El <$> instantiateFull' s <*> instantiateFull' t
630
967
instance InstantiateFull Term where
631
instantiateFull v = etaOnce =<< do -- Andreas, 2010-11-12 DONT ETA!! eta-reduction breaks subject reduction
968
instantiateFull' v = etaOnce =<< do -- Andreas, 2010-11-12 DONT ETA!! eta-reduction breaks subject reduction
632
969
-- but removing etaOnce now breaks everything
635
Var n vs -> Var n <$> instantiateFull vs
636
Con c vs -> Con c <$> instantiateFull vs
637
Def f vs -> Def f <$> instantiateFull vs
638
MetaV x vs -> MetaV x <$> instantiateFull vs
972
Var n vs -> Var n <$> instantiateFull' vs
973
Con c vs -> Con c <$> instantiateFull' vs
974
Def f vs -> Def f <$> instantiateFull' vs
975
MetaV x vs -> MetaV x <$> instantiateFull' vs
639
976
Lit _ -> return v
640
Level l -> levelTm <$> instantiateFull l
641
Lam h b -> Lam h <$> instantiateFull b
642
Sort s -> sortTm <$> instantiateFull s
643
Pi a b -> uncurry Pi <$> instantiateFull (a,b)
644
Shared{} -> updateSharedTerm instantiateFull v
645
DontCare v -> DontCare <$> instantiateFull v
977
Level l -> levelTm <$> instantiateFull' l
978
Lam h b -> Lam h <$> instantiateFull' b
979
Sort s -> sortTm <$> instantiateFull' s
980
Pi a b -> uncurry Pi <$> instantiateFull' (a,b)
981
Shared{} -> __IMPOSSIBLE__ -- updateSharedTerm instantiateFull' v
982
DontCare v -> dontCare <$> instantiateFull' v
647
984
instance InstantiateFull Level where
648
instantiateFull (Max as) = levelMax <$> instantiateFull as
985
instantiateFull' (Max as) = levelMax <$> instantiateFull' as
650
987
instance InstantiateFull PlusLevel where
651
instantiateFull l@ClosedLevel{} = return l
652
instantiateFull (Plus n l) = Plus n <$> instantiateFull l
988
instantiateFull' l@ClosedLevel{} = return l
989
instantiateFull' (Plus n l) = Plus n <$> instantiateFull' l
654
991
instance InstantiateFull LevelAtom where
655
instantiateFull l = case l of
992
instantiateFull' l = case l of
656
993
MetaLevel m vs -> do
657
v <- instantiateFull (MetaV m vs)
994
v <- instantiateFull' (MetaV m vs)
658
995
case ignoreSharing v of
659
996
MetaV m vs -> return $ MetaLevel m vs
660
997
_ -> return $ UnreducedLevel v
661
NeutralLevel v -> NeutralLevel <$> instantiateFull v
998
NeutralLevel v -> NeutralLevel <$> instantiateFull' v
662
999
BlockedLevel m v ->
663
1000
ifM (isInstantiatedMeta m)
664
(UnreducedLevel <$> instantiateFull v)
665
(BlockedLevel m <$> instantiateFull v)
666
UnreducedLevel v -> UnreducedLevel <$> instantiateFull v
1001
(UnreducedLevel <$> instantiateFull' v)
1002
(BlockedLevel m <$> instantiateFull' v)
1003
UnreducedLevel v -> UnreducedLevel <$> instantiateFull' v
1005
instance InstantiateFull Bool where
1006
instantiateFull' = return
668
1008
instance InstantiateFull Pattern where
669
instantiateFull v@VarP{} = return v
670
instantiateFull (DotP t) = DotP <$> instantiateFull t
671
instantiateFull (ConP n mt ps) = ConP n <$> instantiateFull mt <*> instantiateFull ps
672
instantiateFull l@LitP{} = return l
1009
instantiateFull' v@VarP{} = return v
1010
instantiateFull' (DotP t) = DotP <$> instantiateFull' t
1011
instantiateFull' (ConP n mt ps) = ConP n <$> instantiateFull' mt <*> instantiateFull' ps
1012
instantiateFull' l@LitP{} = return l
1013
instantiateFull' p@ProjP{} = return p
674
1015
instance InstantiateFull ClauseBody where
675
instantiateFull (Body t) = Body <$> instantiateFull t
676
instantiateFull (Bind b) = Bind <$> instantiateFull b
677
instantiateFull NoBody = return NoBody
1016
instantiateFull' (Body t) = Body <$> instantiateFull' t
1017
instantiateFull' (Bind b) = Bind <$> instantiateFull' b
1018
instantiateFull' NoBody = return NoBody
679
1020
instance (Subst t, InstantiateFull t) => InstantiateFull (Abs t) where
680
instantiateFull a@(Abs x _) = Abs x <$> underAbstraction_ a instantiateFull
681
instantiateFull (NoAbs x a) = NoAbs x <$> instantiateFull a
1021
instantiateFull' a@(Abs x _) = Abs x <$> underAbstraction_ a instantiateFull'
1022
instantiateFull' (NoAbs x a) = NoAbs x <$> instantiateFull' a
683
1024
instance InstantiateFull t => InstantiateFull (Arg t) where
684
instantiateFull = traverse instantiateFull
1025
instantiateFull' = traverse instantiateFull'
1027
instance InstantiateFull t => InstantiateFull (Named name t) where
1028
instantiateFull' = traverse instantiateFull'
686
1030
instance InstantiateFull t => InstantiateFull (Dom t) where
687
instantiateFull = traverse instantiateFull
1031
instantiateFull' = traverse instantiateFull'
689
1033
instance InstantiateFull t => InstantiateFull [t] where
690
instantiateFull = traverse instantiateFull
1034
instantiateFull' = traverse instantiateFull'
692
1036
instance (InstantiateFull a, InstantiateFull b) => InstantiateFull (a,b) where
693
instantiateFull (x,y) = (,) <$> instantiateFull x <*> instantiateFull y
1037
instantiateFull' (x,y) = (,) <$> instantiateFull' x <*> instantiateFull' y
695
1039
instance (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a,b,c) where
696
instantiateFull (x,y,z) =
697
do (x,(y,z)) <- instantiateFull (x,(y,z))
1040
instantiateFull' (x,y,z) =
1041
do (x,(y,z)) <- instantiateFull' (x,(y,z))
700
1044
instance InstantiateFull a => InstantiateFull (Closure a) where
701
instantiateFull cl = do
702
x <- enterClosure cl instantiateFull
1045
instantiateFull' cl = do
1046
x <- enterClosure cl instantiateFull'
703
1047
return $ cl { clValue = x }
705
1049
instance InstantiateFull ProblemConstraint where
706
instantiateFull (PConstr p c) = PConstr p <$> instantiateFull c
1050
instantiateFull' (PConstr p c) = PConstr p <$> instantiateFull' c
708
1052
instance InstantiateFull Constraint where
709
instantiateFull c = case c of
1053
instantiateFull' c = case c of
710
1054
ValueCmp cmp t u v -> do
711
(t,u,v) <- instantiateFull (t,u,v)
1055
(t,u,v) <- instantiateFull' (t,u,v)
712
1056
return $ ValueCmp cmp t u v
713
1057
ElimCmp cmp t v as bs ->
714
ElimCmp cmp <$> instantiateFull t <*> instantiateFull v <*> instantiateFull as <*> instantiateFull bs
715
LevelCmp cmp u v -> uncurry (LevelCmp cmp) <$> instantiateFull (u,v)
716
TypeCmp cmp a b -> uncurry (TypeCmp cmp) <$> instantiateFull (a,b)
717
TelCmp a b cmp tela telb -> uncurry (TelCmp a b cmp) <$> instantiateFull (tela,telb)
718
SortCmp cmp a b -> uncurry (SortCmp cmp) <$> instantiateFull (a,b)
719
Guarded c pid -> Guarded <$> instantiateFull c <*> pure pid
1058
ElimCmp cmp <$> instantiateFull' t <*> instantiateFull' v <*> instantiateFull' as <*> instantiateFull' bs
1059
LevelCmp cmp u v -> uncurry (LevelCmp cmp) <$> instantiateFull' (u,v)
1060
TypeCmp cmp a b -> uncurry (TypeCmp cmp) <$> instantiateFull' (a,b)
1061
TelCmp a b cmp tela telb -> uncurry (TelCmp a b cmp) <$> instantiateFull' (tela,telb)
1062
SortCmp cmp a b -> uncurry (SortCmp cmp) <$> instantiateFull' (a,b)
1063
Guarded c pid -> Guarded <$> instantiateFull' c <*> pure pid
720
1064
UnBlock m -> return $ UnBlock m
721
FindInScope m cands -> FindInScope m <$> mapM instantiateFull cands
722
IsEmpty r t -> IsEmpty r <$> instantiateFull t
1065
FindInScope m cands -> FindInScope m <$> mapM instantiateFull' cands
1066
IsEmpty r t -> IsEmpty r <$> instantiateFull' t
724
1068
instance InstantiateFull Elim where
725
instantiateFull (Apply v) = Apply <$> instantiateFull v
726
instantiateFull (Proj f) = pure $ Proj f
1069
instantiateFull' (Apply v) = Apply <$> instantiateFull' v
1070
instantiateFull' (Proj f) = pure $ Proj f
728
1072
instance (Ord k, InstantiateFull e) => InstantiateFull (Map k e) where
729
instantiateFull = traverse instantiateFull
1073
instantiateFull' = traverse instantiateFull'
731
1075
instance (Eq k, Hashable k, InstantiateFull e) => InstantiateFull (HashMap k e) where
732
instantiateFull = traverse instantiateFull
1076
instantiateFull' = traverse instantiateFull'
734
1078
instance InstantiateFull ModuleName where
735
instantiateFull = return
1079
instantiateFull' = return
737
1081
instance InstantiateFull Scope where
738
instantiateFull = return
1082
instantiateFull' = return
740
1084
instance InstantiateFull Signature where
741
instantiateFull (Sig a b) = uncurry Sig <$> instantiateFull (a, b)
1085
instantiateFull' (Sig a b) = uncurry Sig <$> instantiateFull' (a, b)
743
1087
instance InstantiateFull Section where
744
instantiateFull (Section tel n) = flip Section n <$> instantiateFull tel
1088
instantiateFull' (Section tel n) = flip Section n <$> instantiateFull' tel
746
1090
instance (Subst a, InstantiateFull a) => InstantiateFull (Tele a) where
747
instantiateFull EmptyTel = return EmptyTel
748
instantiateFull (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull (a, b)
1091
instantiateFull' EmptyTel = return EmptyTel
1092
instantiateFull' (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull' (a, b)
750
1094
instance InstantiateFull Char where
751
instantiateFull = return
1095
instantiateFull' = return
753
1097
instance InstantiateFull Definition where
754
instantiateFull (Defn rel x t pol occ df i c d) = do
755
(t, (df, d)) <- instantiateFull (t, (df, d))
1098
instantiateFull' (Defn rel x t pol occ df i c d) = do
1099
(t, (df, d)) <- instantiateFull' (t, (df, d))
756
1100
return $ Defn rel x t pol occ df i c d
758
1102
instance InstantiateFull a => InstantiateFull (Open a) where
759
instantiateFull (OpenThing n a) = OpenThing n <$> instantiateFull a
1103
instantiateFull' (OpenThing n a) = OpenThing n <$> instantiateFull' a
761
1105
instance InstantiateFull DisplayForm where
762
instantiateFull (Display n ps v) = uncurry (Display n) <$> instantiateFull (ps, v)
1106
instantiateFull' (Display n ps v) = uncurry (Display n) <$> instantiateFull' (ps, v)
764
1108
instance InstantiateFull DisplayTerm where
765
instantiateFull (DTerm v) = DTerm <$> instantiateFull v
766
instantiateFull (DDot v) = DDot <$> instantiateFull v
767
instantiateFull (DCon c vs) = DCon c <$> instantiateFull vs
768
instantiateFull (DDef c vs) = DDef c <$> instantiateFull vs
769
instantiateFull (DWithApp vs ws) = uncurry DWithApp <$> instantiateFull (vs, ws)
1109
instantiateFull' (DTerm v) = DTerm <$> instantiateFull' v
1110
instantiateFull' (DDot v) = DDot <$> instantiateFull' v
1111
instantiateFull' (DCon c vs) = DCon c <$> instantiateFull' vs
1112
instantiateFull' (DDef c vs) = DDef c <$> instantiateFull' vs
1113
instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)
771
1115
instance InstantiateFull Defn where
772
instantiateFull d = case d of
1116
instantiateFull' d = case d of
773
1117
Axiom{} -> return d
774
1118
Function{ funClauses = cs, funCompiled = cc, funInv = inv } -> do
775
(cs, cc, inv) <- instantiateFull (cs, cc, inv)
1119
(cs, cc, inv) <- instantiateFull' (cs, cc, inv)
776
1120
return $ d { funClauses = cs, funCompiled = cc, funInv = inv }
777
1121
Datatype{ dataSort = s, dataClause = cl } -> do
778
s <- instantiateFull s
779
cl <- instantiateFull cl
1122
s <- instantiateFull' s
1123
cl <- instantiateFull' cl
780
1124
return $ d { dataSort = s, dataClause = cl }
781
1125
Record{ recConType = t, recClause = cl, recTel = tel } -> do
782
t <- instantiateFull t
783
cl <- instantiateFull cl
784
tel <- instantiateFull tel
1126
t <- instantiateFull' t
1127
cl <- instantiateFull' cl
1128
tel <- instantiateFull' tel
785
1129
return $ d { recConType = t, recClause = cl, recTel = tel }
786
1130
Constructor{} -> return d
787
1131
Primitive{ primClauses = cs } -> do
788
cs <- instantiateFull cs
1132
cs <- instantiateFull' cs
789
1133
return $ d { primClauses = cs }
791
1135
instance InstantiateFull FunctionInverse where
792
instantiateFull NotInjective = return NotInjective
793
instantiateFull (Inverse inv) = Inverse <$> instantiateFull inv
1136
instantiateFull' NotInjective = return NotInjective
1137
instantiateFull' (Inverse inv) = Inverse <$> instantiateFull' inv
795
1139
instance InstantiateFull a => InstantiateFull (WithArity a) where
796
instantiateFull (WithArity n a) = WithArity n <$> instantiateFull a
1140
instantiateFull' (WithArity n a) = WithArity n <$> instantiateFull' a
798
1142
instance InstantiateFull a => InstantiateFull (Case a) where
799
instantiateFull (Branches cs ls m) =
800
Branches <$> instantiateFull cs
801
<*> instantiateFull ls
802
<*> instantiateFull m
1143
instantiateFull' (Branches cs ls m) =
1144
Branches <$> instantiateFull' cs
1145
<*> instantiateFull' ls
1146
<*> instantiateFull' m
804
1148
instance InstantiateFull CompiledClauses where
805
instantiateFull Fail = return Fail
806
instantiateFull (Done m t) = Done m <$> instantiateFull t
807
instantiateFull (Case n bs) = Case n <$> instantiateFull bs
1149
instantiateFull' Fail = return Fail
1150
instantiateFull' (Done m t) = Done m <$> instantiateFull' t
1151
instantiateFull' (Case n bs) = Case n <$> instantiateFull' bs
809
1153
instance InstantiateFull Clause where
810
instantiateFull (Clause r tel perm ps b) =
811
Clause r <$> instantiateFull tel
1154
instantiateFull' (Clause r tel perm ps b t) =
1155
Clause r <$> instantiateFull' tel
813
<*> instantiateFull ps
814
<*> instantiateFull b
1157
<*> instantiateFull' ps
1158
<*> instantiateFull' b
1159
<*> instantiateFull' t
816
1161
instance InstantiateFull Interface where
817
instantiateFull (Interface ms mod scope inside
1162
instantiateFull' (Interface h ms mod scope inside
818
1163
sig b hsImports highlighting pragmas patsyns) =
819
Interface ms mod scope inside
820
<$> instantiateFull sig
821
<*> instantiateFull b
1164
Interface h ms mod scope inside
1165
<$> instantiateFull' sig
1166
<*> instantiateFull' b
822
1167
<*> return hsImports
823
1168
<*> return highlighting
824
1169
<*> return pragmas
825
1170
<*> return patsyns
827
1172
instance InstantiateFull a => InstantiateFull (Builtin a) where
828
instantiateFull (Builtin t) = Builtin <$> instantiateFull t
829
instantiateFull (Prim x) = Prim <$> instantiateFull x
1173
instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t
1174
instantiateFull' (Prim x) = Prim <$> instantiateFull' x
831
1176
instance InstantiateFull QName where
832
instantiateFull = return
1177
instantiateFull' = return
834
1179
instance InstantiateFull a => InstantiateFull (Maybe a) where
835
instantiateFull = mapM instantiateFull
838
{- DUPLICATE of Telescope.telView
840
telViewM :: Type -> TCM TelView
842
t <- reduce t -- also instantiates meta if in head position
843
case ignoreSharing $ unEl t of
844
Pi a b -> absV a (absName b) <$> telViewM (absBody b)
845
_ -> return $ TelV EmptyTel t
847
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
1180
instantiateFull' = mapM instantiateFull'
added
removed
src/full/Agda/TypeChecking/Reduce.hs
