summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Abstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Abstract.hs')
-rw-r--r--src/full/Agda/TypeChecking/Abstract.hs14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/full/Agda/TypeChecking/Abstract.hs b/src/full/Agda/TypeChecking/Abstract.hs
index 7f65788..4b12778 100644
--- a/src/full/Agda/TypeChecking/Abstract.hs
+++ b/src/full/Agda/TypeChecking/Abstract.hs
@@ -1,7 +1,6 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
-- | Functions for abstracting terms over other terms.
module Agda.TypeChecking.Abstract where
@@ -49,14 +48,14 @@ instance IsPrefixOf Term where
(Def f us, Def g vs) | f == g -> us `isPrefixOf` vs
(Con c us, Con d vs) | c == d -> us `isPrefixOf` vs
(MetaV x us, MetaV y vs) | x == y -> us `isPrefixOf` vs
- _ -> guard (u == v) >> return []
+ (u, v) -> guard (u == v) >> return []
class AbstractTerm a where
-- | @subst u . abstractTerm u == id@
abstractTerm :: Term -> a -> a
instance AbstractTerm Term where
- abstractTerm u v | Just es <- u `isPrefixOf` v = Var 0 $ raise 1 es
+ abstractTerm u v | Just es <- u `isPrefixOf` v = Var 0 $ absT es
| otherwise =
case v of
-- Andreas, 2013-10-20: the original impl. works only at base types
@@ -87,6 +86,7 @@ instance AbstractTerm Sort where
Type n -> Type $ absS n
Prop -> Prop
Inf -> Inf
+ SizeUniv -> SizeUniv
DLub s1 s2 -> DLub (absS s1) (absS s2)
where absS x = abstractTerm u x
@@ -100,7 +100,7 @@ instance AbstractTerm PlusLevel where
instance AbstractTerm LevelAtom where
abstractTerm u l = case l of
MetaLevel m vs -> MetaLevel m $ abstractTerm u vs
- NeutralLevel v -> NeutralLevel $ abstractTerm u v
+ NeutralLevel r v -> NeutralLevel r $ abstractTerm u v
BlockedLevel _ v -> UnreducedLevel $ abstractTerm u v -- abstracting might remove the blockage
UnreducedLevel v -> UnreducedLevel $ abstractTerm u v