module Agda.TypeChecking.Rules.LHS.Unify where
import Control.Arrow ((***), (&&&))
import Control.Applicative hiding (empty)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Error
import Control.Monad.Writer (WriterT(..), MonadWriter(..), Monoid(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List hiding (sort)
import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable,traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Records
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.MetaVars (assignV, newArgsMetaCtx)
import Agda.TypeChecking.EtaContract
import Agda.Interaction.Options (optInjectiveTypeConstructors)
import Agda.TypeChecking.Rules.LHS.Problem
#include "../../../undefined.h"
import Agda.Utils.Impossible
import Agda.Utils.Size
newtype Unify a = U { unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a }
deriving (Monad, MonadIO, Functor, Applicative, MonadException UnifyException, MonadWriter UnifyOutput)
instance MonadReader TCEnv Unify where
ask = U $ ReaderT $ \ _ -> ask
local cont (U (ReaderT f)) = U $ ReaderT $ \ a -> local cont (f a)
data UnifyMayPostpone = MayPostpone | MayNotPostpone
type UnifyEnv = UnifyMayPostpone
emptyUEnv = MayPostpone
noPostponing :: Unify a -> Unify a
noPostponing (U (ReaderT f)) = U . ReaderT . const $ f MayNotPostpone
askPostpone :: Unify UnifyMayPostpone
askPostpone = U . ReaderT $ return
type UnifyOutput = Unifiable
emptyUOutput :: UnifyOutput
emptyUOutput = mempty
data Unifiable
= Definitely
| Possibly
instance Monoid Unifiable where
mempty = Definitely
mappend Definitely Definitely = Definitely
mappend _ _ = Possibly
reportPostponing :: Unify ()
reportPostponing = tell Possibly
ifClean :: Unify () -> Unify a -> Unify a -> Unify a
ifClean m t e = do
ok <- snd <$> listen m
case ok of
Definitely -> t
Possibly -> e
data Equality = Equal TypeHH Term Term
type Sub = Map Nat Term
data UnifyException
= ConstructorMismatch Type Term Term
| StronglyRigidOccurrence Type Term Term
| GenericUnifyException String
instance Error UnifyException where
noMsg = strMsg ""
strMsg = GenericUnifyException
data UnifyState = USt { uniSub :: Sub
, uniConstr :: [Equality]
}
emptyUState = USt Map.empty []
constructorMismatch :: Type -> Term -> Term -> Unify a
constructorMismatch a u v = throwException $ ConstructorMismatch a u v
constructorMismatchHH :: TypeHH -> Term -> Term -> Unify a
constructorMismatchHH aHH = constructorMismatch (leftHH aHH)
instance MonadState TCState Unify where
get = U . lift . lift . lift . lift $ get
put = U . lift . lift . lift . lift . put
instance MonadTCM Unify where
liftTCM = U . lift . lift . lift . lift
instance Subst Equality where
applySubst rho (Equal a s t) =
Equal (applySubst rho a) (applySubst rho s) (applySubst rho t)
onSub :: (Sub -> a) -> Unify a
onSub f = U $ gets $ f . uniSub
modSub :: (Sub -> Sub) -> Unify ()
modSub f = U $ modify $ \s -> s { uniSub = f $ uniSub s }
checkEqualities :: [Equality] -> TCM ()
checkEqualities eqs = noConstraints $ mapM_ checkEq eqs
where
checkEq (Equal (Hom a) s t) = equalTerm a s t
checkEq (Equal (Het a1 a2) s t) = typeError $ HeterogeneousEquality s a1 t a2
checkEquality :: Type -> Term -> Term -> TCM ()
checkEquality a u v = noConstraints $ equalTerm a u v
checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()
checkEqualityHH (Hom a) u v = do
ok <- liftTCM $ noConstraints (True <$ equalTerm a u v)
`catchError` \ err -> return False
if ok then return () else addEquality a u v
checkEqualityHH aHH@(Het a1 a2) u v =
addEqualityHH aHH u v
forceHom :: TypeHH -> TCM Type
forceHom (Hom a) = return a
forceHom (Het a1 a2) = do
noConstraints $ equalType a1 a2
return a1
addEquality :: Type -> Term -> Term -> Unify ()
addEquality a = addEqualityHH (Hom a)
addEqualityHH :: TypeHH -> Term -> Term -> Unify ()
addEqualityHH aHH u v = do
reportPostponing
U $ modify $ \s -> s { uniConstr = Equal aHH u v : uniConstr s }
takeEqualities :: Unify [Equality]
takeEqualities = U $ do
s <- get
put $ s { uniConstr = [] }
return $ uniConstr s
occursCheck :: Nat -> Term -> Type -> Unify ()
occursCheck i u a = do
let fv = freeVars u
v = var i
case occurrence i fv of
StronglyRigid -> do
liftTCM $ reportSDoc "tc.lhs.unify" 20 $ prettyTCM v <+> text "occurs strongly rigidly in" <+> prettyTCM u
throwException $ StronglyRigidOccurrence a v u
NoOccurrence -> return ()
_ -> do
liftTCM $ reportSDoc "tc.lhs.unify" 20 $ prettyTCM v <+> text "occurs in" <+> prettyTCM u
typeError $ UnequalTerms CmpEq v u a
(|->) :: Nat -> (Term, Type) -> Unify ()
i |-> (u, a) = do
occursCheck i u a
liftTCM $ reportSDoc "tc.lhs.unify" 15 $ prettyTCM (var i) <+> text ":=" <+> prettyTCM u
modSub $ Map.insert i (killRange u)
rho <- onSub id
rho' <- traverse ureduce rho
modSub $ const rho'
makeSubstitution :: Sub -> S.Substitution
makeSubstitution sub
| Map.null sub = idS
| otherwise = map val [0 .. highestIndex] ++# raiseS (highestIndex + 1)
where
highestIndex = fst $ Map.findMax sub
val i = maybe (var i) id $ Map.lookup i sub
class UReduce t where
ureduce :: t -> Unify t
instance UReduce Term where
ureduce u = doEtaContractImplicit $ do
rho <- onSub makeSubstitution
liftTCM $ etaContract =<< normalise (applySubst rho u)
instance UReduce Type where
ureduce (El s t) = El s <$> ureduce t
instance UReduce t => UReduce (HomHet t) where
ureduce (Hom t) = Hom <$> ureduce t
ureduce (Het t1 t2) = Het <$> ureduce t1 <*> ureduce t2
instance UReduce t => UReduce (Maybe t) where
ureduce Nothing = return Nothing
ureduce (Just t) = Just <$> ureduce t
flattenSubstitution :: Substitution -> Substitution
flattenSubstitution s = foldr instantiate s is
where
is = [ i | (i, Just _) <- zip [0..] s ]
instantiate :: Nat -> Substitution -> Substitution
instantiate i s = map (fmap $ inst i u) s
where
Just u = s !! i
inst :: Nat -> Term -> Term -> Term
inst i u v = applySubst us v
where us = [var j | j <- [0..i 1] ] ++# u :# raiseS (i + 1)
data UnificationResult = Unifies Substitution | NoUnify Type Term Term | DontKnow TCErr
data HomHet a
= Hom a
| Het a a
deriving (Typeable, Show, Eq, Ord, Functor, Foldable, Traversable)
isHom :: HomHet a -> Bool
isHom Hom{} = True
isHom Het{} = False
fromHom :: HomHet a -> a
fromHom (Hom a) = a
fromHom (Het{}) = __IMPOSSIBLE__
leftHH :: HomHet a -> a
leftHH (Hom a) = a
leftHH (Het a1 a2) = a1
rightHH :: HomHet a -> a
rightHH (Hom a) = a
rightHH (Het a1 a2) = a2
instance (Subst a) => Subst (HomHet a) where
applySubst rho u = fmap (applySubst rho) u
instance (PrettyTCM a) => PrettyTCM (HomHet a) where
prettyTCM (Hom a) = prettyTCM a
prettyTCM (Het a1 a2) = prettyTCM a1 <+> text "||" <+> prettyTCM a2
type TermHH = HomHet Term
type TypeHH = HomHet Type
type TelHH = Tele (Dom TypeHH)
type TelViewHH = TelV TypeHH
absAppHH :: SubstHH t tHH => Abs t -> TermHH -> tHH
absAppHH (Abs _ t) u = substHH u t
absAppHH (NoAbs _ t) u = trivialHH t
class ApplyHH t where
applyHH :: t -> HomHet Args -> HomHet t
instance ApplyHH Term where
applyHH t = fmap (apply t)
instance ApplyHH Type where
applyHH t = fmap (apply t)
substHH :: SubstHH t tHH => TermHH -> t -> tHH
substHH = substUnderHH 0
class SubstHH t tHH where
substUnderHH :: Nat -> TermHH -> t -> tHH
trivialHH :: t -> tHH
instance (Free a, Subst a) => SubstHH (HomHet a) (HomHet a) where
substUnderHH n (Hom u) t = fmap (substUnder n u) t
substUnderHH n (Het u1 u2) (Hom t) =
if n `relevantIn` t then Het (substUnder n u1 t) (substUnder n u2 t)
else Hom (substUnder n u1 t)
substUnderHH n (Het u1 u2) (Het t1 t2) = Het (substUnder n u1 t1) (substUnder n u2 t2)
trivialHH = id
instance SubstHH Term (HomHet Term) where
substUnderHH n uHH t = fmap (\ u -> substUnder n u t) uHH
trivialHH = Hom
instance SubstHH Type (HomHet Type) where
substUnderHH n uHH (El s t) = fmap (\ u -> El s $ substUnder n u t) uHH
trivialHH = Hom
instance SubstHH a b => SubstHH (Arg a) (Arg b) where
substUnderHH n u = fmap $ substUnderHH n u
trivialHH = fmap trivialHH
instance SubstHH a b => SubstHH (Dom a) (Dom b) where
substUnderHH n u = fmap $ substUnderHH n u
trivialHH = fmap trivialHH
instance SubstHH a b => SubstHH (Abs a) (Abs b) where
substUnderHH n u (Abs x v) = Abs x $ substUnderHH (n + 1) u v
substUnderHH n u (NoAbs x v) = NoAbs x $ substUnderHH n u v
trivialHH = fmap trivialHH
instance (SubstHH a a', SubstHH b b') => SubstHH (a,b) (a',b') where
substUnderHH n u (x,y) = (substUnderHH n u x, substUnderHH n u y)
trivialHH = trivialHH *** trivialHH
instance SubstHH a b => SubstHH (Tele a) (Tele b) where
substUnderHH n u EmptyTel = EmptyTel
substUnderHH n u (ExtendTel t tel) = uncurry ExtendTel $ substUnderHH n u (t, tel)
trivialHH = fmap trivialHH
unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution
unifyIndices_ flex a us vs = liftTCM $ do
r <- unifyIndices flex a us vs
case r of
Unifies sub -> return sub
DontKnow err -> throwError err
NoUnify a u v -> typeError $ UnequalTerms CmpEq u v a
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult
unifyIndices flex a us vs = liftTCM $ do
a <- reduce a
reportSDoc "tc.lhs.unify" 10 $
sep [ text "unifyIndices"
, nest 2 $ text (show flex)
, nest 2 $ parens (prettyTCM a)
, nest 2 $ prettyList $ map prettyTCM us
, nest 2 $ prettyList $ map prettyTCM vs
, nest 2 $ text "context: " <+> (prettyTCM =<< getContextTelescope)
]
(r, USt s eqs) <- flip runStateT emptyUState . runExceptionT . runWriterT . flip runReaderT emptyUEnv . unUnify $ do
ifClean (unifyConstructorArgs (Hom a) us vs)
recheckConstraints
recheckEqualities
case r of
Left (ConstructorMismatch a u v) -> return $ NoUnify a u v
Left (StronglyRigidOccurrence a u v) -> return $ NoUnify a u v
Left (GenericUnifyException err) -> fail err
Right _ -> do
checkEqualities $ applySubst (makeSubstitution s) eqs
let n = maximum $ (1) : flex
return $ Unifies $ flattenSubstitution [ Map.lookup i s | i <- [0..n] ]
`catchError` \err -> return $ DontKnow err
where
flexible i = i `elem` flex
flexibleTerm (Var i []) = flexible i
flexibleTerm (Shared p) = flexibleTerm (derefPtr p)
flexibleTerm _ = False
unifyConstructorArgs ::
TypeHH
-> [Arg Term]
-> [Arg Term]
-> Unify ()
unifyConstructorArgs a12 [] [] = return ()
unifyConstructorArgs a12 vs1 vs2 = do
liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep
[ text "unifyConstructorArgs"
, nest 2 $ prettyList $ map prettyTCM vs1
, nest 2 $ prettyList $ map prettyTCM vs2
, nest 2 $ text "constructor type:" <+> prettyTCM a12
]
let n = genericLength vs1
when (n /= genericLength vs2) $ __IMPOSSIBLE__
TelV tel12 _ <- telViewUpToHH n a12
when (n /= size tel12) $ __IMPOSSIBLE__
unifyConArgs tel12 vs1 vs2
unifyConArgs ::
TelHH
-> [Arg Term]
-> [Arg Term]
-> Unify ()
unifyConArgs _ (_ : _) [] = __IMPOSSIBLE__
unifyConArgs _ [] (_ : _) = __IMPOSSIBLE__
unifyConArgs _ [] [] = return ()
unifyConArgs EmptyTel _ _ = __IMPOSSIBLE__
unifyConArgs tel0@(ExtendTel a@(Dom _ rel bHH) tel) us0@(arg@(Arg _ _ u) : us) vs0@(Arg _ _ v : vs) = do
liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep
[ text "unifyConArgs"
, nest 2 $ prettyList $ map prettyTCM us0
, nest 2 $ prettyList $ map prettyTCM vs0
, nest 2 $ text "at telescope" <+> prettyTCM bHH <+> text "..."
]
liftTCM $ reportSDoc "tc.lhs.unify" 25 $
(text $ "tel0 = " ++ show tel0)
uHH <- if (rel == Irrelevant) then return $ Hom u else
ifClean (unifyHH bHH u v) (return $ Hom u) (return $ Het u v)
liftTCM $ reportSDoc "tc.lhs.unify" 25 $
(text "uHH (before ureduce) =" <+> prettyTCM uHH)
uHH <- traverse ureduce uHH
liftTCM $ reportSDoc "tc.lhs.unify" 25 $
(text "uHH (after ureduce) =" <+> prettyTCM uHH)
unifyConArgs (tel `absAppHH` uHH) us vs
unifyArgs :: Type -> [Arg Term] -> [Arg Term] -> Unify ()
unifyArgs _ (_ : _) [] = __IMPOSSIBLE__
unifyArgs _ [] (_ : _) = __IMPOSSIBLE__
unifyArgs _ [] [] = return ()
unifyArgs a us0@(arg@(Arg _ _ u) : us) vs0@(Arg _ _ v : vs) = do
liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep
[ text "unifyArgs"
, nest 2 $ parens (prettyTCM a)
, nest 2 $ prettyList $ map prettyTCM us0
, nest 2 $ prettyList $ map prettyTCM vs0
]
a <- ureduce a
case ignoreSharing $ unEl a of
Pi b _ -> do
let dep = dependent $ unEl a
unless (domRelevance b == Irrelevant) $
(if dep then noPostponing else id) $
unify (unDom b) u v
arg <- traverse ureduce arg
unifyArgs (a `piApply` [arg]) us vs
_ -> __IMPOSSIBLE__
where dependent (Pi _ NoAbs{}) = False
dependent (Pi b c) = 0 `relevantIn` absBody c
dependent (Shared p) = dependent (derefPtr p)
dependent _ = False
recheckEqualities :: Unify ()
recheckEqualities = do
eqs <- takeEqualities
liftTCM $ checkEqualities eqs
recheckConstraints :: Unify ()
recheckConstraints = mapM_ unifyEquality =<< takeEqualities
unifyEquality :: Equality -> Unify ()
unifyEquality (Equal aHH u v) = unifyHH aHH u v
i |->> x = do
i |-> x
recheckConstraints
unifySizes :: Term -> Term -> Unify ()
unifySizes u v = do
sz <- liftTCM sizeType
su <- liftTCM $ sizeView u
sv <- liftTCM $ sizeView v
case (su, sv) of
(SizeSuc u, SizeSuc v) -> unify sz u v
(SizeSuc u, SizeInf) -> unify sz u v
(SizeInf, SizeSuc v) -> unify sz u v
_ -> unifyAtom sz u v
unifyHH ::
TypeHH
-> Term -> Term -> Unify ()
unifyHH aHH u v = do
u <- liftTCM . constructorForm =<< ureduce u
v <- liftTCM . constructorForm =<< ureduce v
aHH <- ureduce aHH
liftTCM $ reportSDoc "tc.lhs.unify" 15 $
sep [ text "unifyHH"
, nest 2 $ (parens $ prettyTCM u) <+> text "=?="
, nest 2 $ parens $ prettyTCM v
, nest 2 $ text ":" <+> prettyTCM aHH
]
isSizeName <- liftTCM isSizeNameTest
(aHH, sh) <- shapeViewHH aHH
case sh of
ElseSh -> checkEqualityHH aHH u v
DefSh d -> if isSizeName d then unifySizes u v
else unifyAtomHH aHH u v
_ -> unifyAtomHH aHH u v
unifyAtomHH ::
TypeHH
-> Term -> Term -> Unify ()
unifyAtomHH aHH0 u v = do
let (aHH, homogeneous, a) = case aHH0 of
Hom a -> (aHH0, True, a)
Het a1 a2 | a1 == a2 -> (Hom a1, True, a1)
_ -> (aHH0, False, __IMPOSSIBLE__)
fallback = checkEqualityHH aHH u v
liftTCM $ reportSDoc "tc.lhs.unify" 15 $
sep [ text "unifyAtom"
, nest 2 $ prettyTCM u <> if flexibleTerm u then text " (flexible)" else empty
, nest 2 $ text "=?="
, nest 2 $ prettyTCM v <> if flexibleTerm v then text " (flexible)" else empty
, nest 2 $ text ":" <+> prettyTCM aHH
]
case (ignoreSharing u, ignoreSharing v) of
(Level l, _) -> do
u <- liftTCM $ reallyUnLevelView l
unifyAtomHH aHH u v
(_, Level l) -> do
v <- liftTCM $ reallyUnLevelView l
unifyAtomHH aHH u v
(Var i us, Var j vs) | i == j -> checkEqualityHH aHH u v
(Var i [], _) | homogeneous && flexible i -> i |->> (v, a)
(_, Var j []) | homogeneous && flexible j -> j |->> (u, a)
(Con c us, Con c' vs)
| c == c' -> do
r <- ureduce =<< liftTCM (dataOrRecordTypeHH c aHH)
case r of
Just a'HH -> unifyConstructorArgs a'HH us vs
Nothing -> checkEqualityHH aHH u v
| otherwise -> constructorMismatchHH aHH u v
(Def d us, Def d' vs)
| d == d' -> do
def <- getConstInfo d
let ok = case theDef def of
Datatype{} -> True
Record{} -> True
Axiom{} -> True
_ -> False
inj <- liftTCM $ optInjectiveTypeConstructors <$> pragmaOptions
if inj && ok
then unifyArgs (defType def) us vs
else checkEqualityHH aHH u v
| otherwise -> checkEqualityHH aHH u v
(Lit l1, Lit l2)
| l1 == l2 -> return ()
| otherwise -> constructorMismatchHH aHH u v
(MetaV m us, _) | homogeneous -> do
ok <- liftTCM $ instMeta a m us v
liftTCM $ reportSDoc "tc.lhs.unify" 40 $
vcat [ fsep [ text "inst meta", text $ if ok then "(ok)" else "(not ok)" ]
, nest 2 $ sep [ prettyTCM u, text ":=", prettyTCM =<< normalise u ]
]
if ok then unify a u v
else addEquality a u v
(_, MetaV m vs) | homogeneous -> do
ok <- liftTCM $ instMeta a m vs u
liftTCM $ reportSDoc "tc.lhs.unify" 40 $
vcat [ fsep [ text "inst meta", text $ if ok then "(ok)" else "(not ok)" ]
, nest 2 $ sep [ prettyTCM v, text ":=", prettyTCM =<< normalise v ]
]
if ok then unify a u v
else addEquality a u v
(Con c us, _) -> do
md <- isEtaRecordTypeHH aHH
case md of
Just (d, parsHH) -> do
(tel, vs) <- liftTCM $ etaExpandRecord d (rightHH parsHH) v
b <- liftTCM $ getRecordConstructorType d
bHH <- ureduce (b `applyHH` parsHH)
unifyConstructorArgs bHH us vs
Nothing -> fallback
(_, Con c vs) -> do
md <- isEtaRecordTypeHH aHH
case md of
Just (d, parsHH) -> do
(tel, us) <- liftTCM $ etaExpandRecord d (leftHH parsHH) u
b <- liftTCM $ getRecordConstructorType d
bHH <- ureduce (b `applyHH` parsHH)
unifyConstructorArgs bHH us vs
Nothing -> fallback
_ -> fallback
unify :: Type -> Term -> Term -> Unify ()
unify a = unifyHH (Hom a)
unifyAtom :: Type -> Term -> Term -> Unify ()
unifyAtom a = unifyAtomHH (Hom a)
instMeta a m us v = do
app <- inertApplication a v
reportSDoc "tc.lhs.unify" 50 $
sep [ text "inert"
<+> sep [ text (show m), text (show us), parens $ prettyTCM v ]
, nest 2 $ text "==" <+> text (show app)
]
case app of
Nothing -> return False
Just (v', b, vs) -> do
margs <- do
mv <- lookupMeta m
TelV tel0 _ <- telView b
let tel = telFromList $ take (length vs) $ telToList tel0
b' = telePi tel (sort Prop)
withMetaInfo' mv $ do
tel <- getContextTelescope
newArgsMetaCtx b' tel us
noConstraints $ assignV m us (v' `apply` margs)
return True
`catchError` \_ -> return False
inertApplication :: Type -> Term -> TCM (Maybe (Term, Type, Args))
inertApplication a v =
case ignoreSharing v of
Con c vs -> fmap (\ b -> (Con c [], b, vs)) <$> dataOrRecordType c a
Def d vs -> do
def <- getConstInfo d
let ans = Just (Def d [], defType def, vs)
return $ case theDef def of
Datatype{} -> ans
Record{} -> ans
Axiom{} -> ans
_ -> Nothing
_ -> return Nothing
dataOrRecordType
:: QName
-> Type
-> TCM (Maybe Type)
dataOrRecordType c a = fmap (\ (d, b, args) -> b `apply` args) <$> dataOrRecordType' c a
dataOrRecordType' ::
QName
-> Type
-> TCM (Maybe (QName, Type, Args))
dataOrRecordType' c a = do
(d, args) <- do
TelV _ (El _ def) <- telView a
let Def d args = ignoreSharing def
return (d, args)
def <- theDef <$> getConstInfo d
r <- case def of
Datatype{dataPars = n} -> Just . ((,) n) . defType <$> getConstInfo c
Record {recPars = n} -> Just . ((,) n) <$> getRecordConstructorType d
_ -> return Nothing
return $ fmap (\ (n, a') -> (d, a', genericTake n args)) r
dataOrRecordTypeHH ::
QName
-> TypeHH
-> TCM (Maybe TypeHH)
dataOrRecordTypeHH c (Hom a) = fmap Hom <$> dataOrRecordType c a
dataOrRecordTypeHH c (Het a1 a2) = do
r1 <- dataOrRecordType' c a1
r2 <- dataOrRecordType' c a2
return $ case (r1, r2) of
(Just (d1, b1, pars1), Just (d2, b2, pars2)) | d1 == d2 -> Just $
if null pars1 && null pars2 then Hom b1
else Het (b1 `apply` pars1) (b2 `apply` pars2)
_ -> Nothing
isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args))
isEtaRecordTypeHH (Hom a) = fmap (\ (d, ps) -> (d, Hom ps)) <$> liftTCM (isEtaRecordType a)
isEtaRecordTypeHH (Het a1 a2) = do
m1 <- liftTCM $ isEtaRecordType a1
m2 <- liftTCM $ isEtaRecordType a2
case (m1, m2) of
(Just (d1, as1), Just (d2, as2)) | d1 == d2 -> return $ Just (d1, Het as1 as2)
_ -> return Nothing
data ShapeView a
= PiSh (Dom a) (Abs a)
| FunSh (Dom a) a
| DefSh QName
| VarSh Nat
| LitSh Literal
| SortSh
| MetaSh
| ElseSh
deriving (Typeable, Show, Eq, Ord, Functor)
shapeView :: Type -> Unify (Type, ShapeView Type)
shapeView t = do
return . (t,) $ case ignoreSharing $ unEl t of
Pi a (NoAbs _ b) -> FunSh a b
Pi a (Abs x b) -> PiSh a (Abs x b)
Def d vs -> DefSh d
Var x vs -> VarSh x
Lit l -> LitSh l
Sort s -> SortSh
MetaV m vs -> MetaSh
_ -> ElseSh
shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH)
shapeViewHH (Hom a) = do
(a, sh) <- shapeView a
return (Hom a, fmap Hom sh)
shapeViewHH (Het a1 a2) = do
(a1, sh1) <- shapeView a1
(a2, sh2) <- shapeView a2
return . (Het a1 a2,) $ case (sh1, sh2) of
(PiSh (Dom h1 r1 a1) b1, PiSh (Dom h2 r2 a2) b2)
| h1 == h2 ->
PiSh (Dom h1 (min r1 r2) (Het a1 a2)) (Abs (absName b1) (Het (absBody b1) (absBody b2)))
(FunSh (Dom h1 r1 a1) b1, FunSh (Dom h2 r2 a2) b2)
| h1 == h2 ->
FunSh (Dom h1 (min r1 r2) (Het a1 a2)) (Het b1 b2)
(DefSh d1, DefSh d2) | d1 == d2 -> DefSh d1
(VarSh x1, VarSh x2) | x1 == x2 -> VarSh x1
(LitSh l1, LitSh l2) | l1 == l2 -> LitSh l1
(SortSh, SortSh) -> SortSh
_ -> ElseSh
telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH
telViewUpToHH 0 t = return $ TelV EmptyTel t
telViewUpToHH n t = do
(t, sh) <- shapeViewHH =<< liftTCM (traverse reduce t)
case sh of
PiSh a b -> absV a (absName b) <$> telViewUpToHH (n1) (absBody b)
FunSh a b -> absV a "_" <$> telViewUpToHH (n1) (raise 1 b)
_ -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t