{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Rules.LHS.Unify
( UnificationResult
, UnificationResult'(..)
, unifyIndices ) where
import Prelude hiding (null)
import Control.Arrow ((***))
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Monad.Reader
import Control.Monad.Writer (WriterT(..), MonadWriter(..), Monoid(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Semigroup hiding (Arg)
import qualified Data.List as List
import Data.Foldable (Foldable)
import Data.Traversable (Traversable,traverse)
import qualified Data.Traversable as Trav
import Agda.Interaction.Options (optInjectiveTypeConstructors)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Builtin (constructorForm)
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Patterns.Match as Match
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.TypeChecking.SizedTypes (compareSizes)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.MetaVars (assignV, newArgsMetaCtx)
import Agda.TypeChecking.EtaContract
import Agda.Interaction.Options (optInjectiveTypeConstructors, optWithoutK)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
type UnificationResult = UnificationResult'
( Telescope
, PatternSubstitution
, [NamedArg DeBruijnPattern]
)
data UnificationResult' a
= Unifies a
| NoUnify NegativeUnification
| DontKnow [UnificationFailure]
deriving (Show, Functor, Foldable, Traversable)
unifyIndices :: MonadTCM tcm
=> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> tcm UnificationResult
unifyIndices tel flex a [] [] = return $ Unifies (tel, idS, [])
unifyIndices tel flex a us vs = liftTCM $ Bench.billTo [Bench.Typing, Bench.CheckLHS, Bench.UnifyIndices] $ do
reportSDoc "tc.lhs.unify" 10 $
sep [ "unifyIndices"
, nest 2 $ prettyTCM tel
, nest 2 $ addContext tel $ text $ show $ map flexVar flex
, nest 2 $ addContext tel $ parens (prettyTCM a)
, nest 2 $ addContext tel $ prettyList $ map prettyTCM us
, nest 2 $ addContext tel $ prettyList $ map prettyTCM vs
]
initialState <- initUnifyState tel flex a us vs
reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState
reportSDoc "tc.lhs.unify" 70 $ "initial unifyState:" <+> text (show initialState)
(result,output) <- runUnifyM $ unify initialState rightToLeftStrategy
let ps = applySubst (unifyProof output) $ teleNamedArgs (eqTel initialState)
return $ fmap (\s -> (varTel s , unifySubst output , ps)) result
data Equality = Equal
{ eqType :: Dom Type
, eqLeft :: Term
, eqRight :: Term
}
instance Reduce Equality where
reduce' (Equal a u v) = Equal <$> reduce' a <*> reduce' u <*> reduce' v
eqConstructorForm :: Equality -> TCM Equality
eqConstructorForm (Equal a u v) = Equal a <$> constructorForm u <*> constructorForm v
eqUnLevel :: Equality -> TCM Equality
eqUnLevel (Equal a u v) = Equal a <$> unLevel u <*> unLevel v
where
unLevel (Level l) = reallyUnLevelView l
unLevel u = return u
data UnifyState = UState
{ varTel :: Telescope
, flexVars :: FlexibleVars
, eqTel :: Telescope
, eqLHS :: [Arg Term]
, eqRHS :: [Arg Term]
} deriving (Show)
instance Reduce UnifyState where
reduce' (UState var flex eq lhs rhs) =
UState <$> reduce' var
<*> pure flex
<*> reduce' eq
<*> reduce' lhs
<*> reduce' rhs
reduceVarTel :: UnifyState -> TCM UnifyState
reduceVarTel s@UState{ varTel = tel } = do
tel <- reduce tel
return $ s { varTel = tel }
reduceEqTel :: UnifyState -> TCM UnifyState
reduceEqTel s@UState{ eqTel = tel } = do
tel <- reduce tel
return $ s { eqTel = tel }
instance Normalise UnifyState where
normalise' (UState var flex eq lhs rhs) =
UState <$> normalise' var
<*> pure flex
<*> normalise' eq
<*> normalise' lhs
<*> normalise' rhs
normaliseVarTel :: UnifyState -> TCM UnifyState
normaliseVarTel s@UState{ varTel = tel } = do
tel <- normalise tel
return $ s { varTel = tel }
normaliseEqTel :: UnifyState -> TCM UnifyState
normaliseEqTel s@UState{ eqTel = tel } = do
tel <- normalise tel
return $ s { eqTel = tel }
instance PrettyTCM UnifyState where
prettyTCM state = "UnifyState" $$ nest 2 (vcat $
[ "variable tel: " <+> prettyTCM gamma
, "flexible vars: " <+> prettyTCM (map flexVar $ flexVars state)
, "equation tel: " <+> addContext gamma (prettyTCM delta)
, "equations: " <+> addContext gamma (prettyList_ (zipWith prettyEquality (eqLHS state) (eqRHS state)))
])
where
gamma = varTel state
delta = eqTel state
prettyEquality x y = prettyTCM x <+> "=?=" <+> prettyTCM y
initUnifyState :: Telescope -> FlexibleVars -> Type -> Args -> Args -> TCM UnifyState
initUnifyState tel flex a lhs rhs = do
let n = size lhs
unless (n == size rhs) __IMPOSSIBLE__
TelV eqTel _ <- telView a
unless (n == size eqTel) __IMPOSSIBLE__
reduce $ UState tel flex eqTel lhs rhs
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved = null . eqTel
varCount :: UnifyState -> Int
varCount = size . varTel
getVarType :: Int -> UnifyState -> Dom Type
getVarType i s = indexWithDefault __IMPOSSIBLE__ (flattenTel $ varTel s) i
getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised i s = snd <$> indexWithDefault __IMPOSSIBLE__ (telToList $ varTel s) i
eqCount :: UnifyState -> Int
eqCount = size . eqTel
getEquality :: Int -> UnifyState -> Equality
getEquality k UState { eqTel = eqs, eqLHS = lhs, eqRHS = rhs } =
Equal (indexWithDefault __IMPOSSIBLE__ (flattenTel eqs) k)
(unArg $ indexWithDefault __IMPOSSIBLE__ lhs k)
(unArg $ indexWithDefault __IMPOSSIBLE__ rhs k)
getEqualityUnraised :: Int -> UnifyState -> Equality
getEqualityUnraised k UState { eqTel = eqs, eqLHS = lhs, eqRHS = rhs } =
Equal (snd <$> indexWithDefault __IMPOSSIBLE__ (telToList eqs) k)
(unArg $ indexWithDefault __IMPOSSIBLE__ lhs k)
(unArg $ indexWithDefault __IMPOSSIBLE__ rhs k)
getEqInfo :: Int -> UnifyState -> ArgInfo
getEqInfo k UState { eqTel = eqs } =
domInfo $ indexWithDefault __IMPOSSIBLE__ (telToList eqs) k
addEqs :: Telescope -> [Arg Term] -> [Arg Term] -> UnifyState -> UnifyState
addEqs tel us vs s =
s { eqTel = tel `abstract` eqTel s
, eqLHS = us ++ eqLHS s
, eqRHS = vs ++ eqRHS s
}
where k = size tel
addEq :: Type -> Arg Term -> Arg Term -> UnifyState -> UnifyState
addEq a u v = addEqs (ExtendTel (defaultDom a) (Abs underscore EmptyTel)) [u] [v]
solveVar :: Int
-> Term
-> UnifyState -> Maybe (UnifyState, PatternSubstitution)
solveVar k u s = case instantiateTelescope (varTel s) k u of
Nothing -> Nothing
Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState
{ varTel = tel'
, flexVars = permuteFlex (reverseP rho) $ flexVars s
, eqTel = applyPatSubst sigma $ eqTel s
, eqLHS = applyPatSubst sigma $ eqLHS s
, eqRHS = applyPatSubst sigma $ eqRHS s
}
where
permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
permuteFlex perm =
mapMaybe $ \(FlexibleVar h o k p x) ->
FlexibleVar h o k p <$> List.findIndex (x==) (permPicks perm)
applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder k tel u
| k < 0 = __IMPOSSIBLE__
| k == 0 = tel `apply1` u
| otherwise = case tel of
EmptyTel -> __IMPOSSIBLE__
ExtendTel a tel' -> ExtendTel a $
Abs (absName tel') $ applyUnder (k-1) (absBody tel') u
dropAt :: Int -> [a] -> [a]
dropAt _ [] = __IMPOSSIBLE__
dropAt k (x:xs)
| k < 0 = __IMPOSSIBLE__
| k == 0 = xs
| otherwise = x : dropAt (k-1) xs
solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq k u s = (,sigma) $ s
{ eqTel = applyUnder k (eqTel s) u'
, eqLHS = dropAt k $ eqLHS s
, eqRHS = dropAt k $ eqRHS s
}
where
u' = raise k u
n = eqCount s
sigma = liftS (n-k-1) $ consS (dotP u') idS
simplifyEq :: Int -> Term -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
simplifyEq k u s = case instantiateTelescope (eqTel s) k u of
Nothing -> Nothing
Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState
{ varTel = varTel s
, flexVars = flexVars s
, eqTel = tel'
, eqLHS = permute rho $ eqLHS s
, eqRHS = permute rho $ eqRHS s
}
data UnifyStep
= Deletion
{ deleteAt :: Int
, deleteType :: Type
, deleteLeft :: Term
, deleteRight :: Term
}
| Solution
{ solutionAt :: Int
, solutionType :: Dom Type
, solutionVar :: FlexibleVar Int
, solutionTerm :: Term
}
| Injectivity
{ injectAt :: Int
, injectType :: Type
, injectDatatype :: QName
, injectParameters :: Args
, injectIndices :: Args
, injectConstructor :: ConHead
}
| Conflict
{ conflictAt :: Int
, conflictType :: Type
, conflictDatatype :: QName
, conflictParameters :: Args
, conflictLeft :: Term
, conflictRight :: Term
}
| Cycle
{ cycleAt :: Int
, cycleType :: Type
, cycleDatatype :: QName
, cycleParameters :: Args
, cycleVar :: Int
, cycleOccursIn :: Term
}
| EtaExpandVar
{ expandVar :: FlexibleVar Int
, expandVarRecordType :: QName
, expandVarParameters :: Args
}
| EtaExpandEquation
{ expandAt :: Int
, expandRecordType :: QName
, expandParameters :: Args
}
| LitConflict
{ litConflictAt :: Int
, litType :: Type
, litConflictLeft :: Literal
, litConflictRight :: Literal
}
| StripSizeSuc
{ stripAt :: Int
, stripArgLeft :: Term
, stripArgRight :: Term
}
| SkipIrrelevantEquation
{ skipIrrelevantAt :: Int
}
| TypeConInjectivity
{ typeConInjectAt :: Int
, typeConstructor :: QName
, typeConArgsLeft :: Args
, typeConArgsRight :: Args
} deriving (Show)
instance PrettyTCM UnifyStep where
prettyTCM step = case step of
Deletion k a u v -> "Deletion" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "lhs: " <+> prettyTCM u
, "rhs: " <+> prettyTCM v
])
Solution k a i u -> "Solution" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "variable: " <+> text (show i)
, "term: " <+> prettyTCM u
])
Injectivity k a d pars ixs c -> "Injectivity" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "datatype: " <+> prettyTCM d
, "parameters: " <+> prettyList_ (map prettyTCM pars)
, "indices: " <+> prettyList_ (map prettyTCM ixs)
, "constructor:" <+> prettyTCM c
])
Conflict k a d pars u v -> "Conflict" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "datatype: " <+> prettyTCM d
, "parameters: " <+> prettyList_ (map prettyTCM pars)
, "lhs: " <+> prettyTCM u
, "rhs: " <+> prettyTCM v
])
Cycle k a d pars i u -> "Cycle" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "datatype: " <+> prettyTCM d
, "parameters: " <+> prettyList_ (map prettyTCM pars)
, "variable: " <+> text (show i)
, "term: " <+> prettyTCM u
])
EtaExpandVar fi r pars -> "EtaExpandVar" $$ nest 2 (vcat $
[ "variable: " <+> text (show fi)
, "record type:" <+> prettyTCM r
, "parameters: " <+> prettyTCM pars
])
EtaExpandEquation k r pars -> "EtaExpandEquation" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "record type:" <+> prettyTCM r
, "parameters: " <+> prettyTCM pars
])
LitConflict k a u v -> "LitConflict" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "type: " <+> prettyTCM a
, "lhs: " <+> prettyTCM u
, "rhs: " <+> prettyTCM v
])
StripSizeSuc k u v -> "StripSizeSuc" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "lhs: " <+> prettyTCM u
, "rhs: " <+> prettyTCM v
])
SkipIrrelevantEquation k -> "SkipIrrelevantEquation" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
])
TypeConInjectivity k d us vs -> "TypeConInjectivity" $$ nest 2 (vcat $
[ "position: " <+> text (show k)
, "datatype: " <+> prettyTCM d
, "lhs: " <+> prettyList_ (map prettyTCM us)
, "rhs: " <+> prettyList_ (map prettyTCM vs)
])
type UnifyStrategy = UnifyState -> ListT TCM UnifyStep
leftToRightStrategy :: UnifyStrategy
leftToRightStrategy s =
msum (for [0..n-1] $ \k -> completeStrategyAt k s)
where n = size $ eqTel s
rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy s =
msum (for (downFrom n) $ \k -> completeStrategyAt k s)
where n = size $ eqTel s
completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt k s = msum $ map (\strat -> strat k s) $
[ skipIrrelevantStrategy
, basicUnifyStrategy
, literalStrategy
, dataStrategy
, etaExpandVarStrategy
, etaExpandEquationStrategy
, injectiveTypeConStrategy
, injectivePragmaStrategy
, simplifySizesStrategy
, checkEqualityStrategy
]
isHom :: (Free a, Subst Term a) => Int -> a -> Maybe a
isHom n x = do
guard $ getAll $ runFree (All . (>= n)) IgnoreNot x
return $ raise (-n) x
findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible i flex =
let flex' = map flexVar flex
flexible i = i `elem` flex'
in List.find ((i ==) . flexVar) flex
basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy k s = do
Equal dom@Dom{unDom = a} u v <- liftTCM $ eqUnLevel (getEquality k s)
ha <- fromMaybeMP $ isHom n a
(mi, mj) <- liftTCM $ addContext (varTel s) $ (,) <$> isEtaVar u ha <*> isEtaVar v ha
liftTCM $ reportSDoc "tc.lhs.unify" 30 $ "isEtaVar results: " <+> text (show [mi,mj])
case (mi, mj) of
(Just i, Just j)
| i == j -> mzero
(Just i, Just j)
| Just fi <- findFlexible i flex
, Just fj <- findFlexible j flex -> do
let choice = chooseFlex fi fj
firstTryLeft = msum [ return (Solution k dom{unDom = ha} fi v)
, return (Solution k dom{unDom = ha} fj u)]
firstTryRight = msum [ return (Solution k dom{unDom = ha} fj u)
, return (Solution k dom{unDom = ha} fi v)]
liftTCM $ reportSDoc "tc.lhs.unify" 40 $ "fi = " <+> text (show fi)
liftTCM $ reportSDoc "tc.lhs.unify" 40 $ "fj = " <+> text (show fj)
liftTCM $ reportSDoc "tc.lhs.unify" 40 $ "chooseFlex: " <+> text (show choice)
case choice of
ChooseLeft -> firstTryLeft
ChooseRight -> firstTryRight
ExpandBoth -> mzero
ChooseEither -> firstTryRight
(Just i, _)
| Just fi <- findFlexible i flex -> return $ Solution k dom{unDom = ha} fi v
(_, Just j)
| Just fj <- findFlexible j flex -> return $ Solution k dom{unDom = ha} fj u
_ -> mzero
where
flex = flexVars s
n = eqCount s
dataStrategy :: Int -> UnifyStrategy
dataStrategy k s = do
Equal Dom{unDom = a} u v <- liftTCM $ eqConstructorForm =<< eqUnLevel (getEqualityUnraised k s)
case unEl a of
Def d es | Type{} <- getSort a -> do
npars <- catMaybesMP $ liftTCM $ getNumberOfParameters d
let (pars,ixs) = splitAt npars $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
hpars <- fromMaybeMP $ isHom k pars
liftTCM $ reportSDoc "tc.lhs.unify" 40 $ addContext (varTel s) $
"Found equation at datatype " <+> prettyTCM d
<+> " with (homogeneous) parameters " <+> prettyTCM hpars
case (u, v) of
(Con c _ _ , Con c' _ _ ) | c == c' -> return $ Injectivity k a d hpars ixs c
(Con c _ _ , Con c' _ _ ) -> return $ Conflict k a d hpars u v
(Var i [] , v ) -> ifOccursStronglyRigid i v $ return $ Cycle k a d hpars i v
(u , Var j [] ) -> ifOccursStronglyRigid j u $ return $ Cycle k a d hpars j u
_ -> mzero
_ -> mzero
where
ifOccursStronglyRigid i u ret = do
(_ , u) <- liftTCM $ forceNotFree (singleton i) u
case occurrence i u of
StronglyRigid -> ret
_ -> mzero
checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy k s = do
let Equal Dom{unDom = a} u v = getEquality k s
n = eqCount s
ha <- fromMaybeMP $ isHom n a
return $ Deletion k ha u v
literalStrategy :: Int -> UnifyStrategy
literalStrategy k s = do
let n = eqCount s
Equal Dom{unDom = a} u v <- liftTCM $ eqUnLevel $ getEquality k s
ha <- fromMaybeMP $ isHom n a
case (u , v) of
(Lit l1 , Lit l2)
| l1 == l2 -> return $ Deletion k ha u v
| otherwise -> return $ LitConflict k ha l1 l2
_ -> mzero
etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy k s = do
Equal Dom{unDom = a} u v <- liftTCM $ eqUnLevel (getEquality k s)
shouldEtaExpand u v a s `mplus` shouldEtaExpand v u a s
where
shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand (Var i es) v a s = do
fi <- fromMaybeMP $ findFlexible i (flexVars s)
liftTCM $ reportSDoc "tc.lhs.unify" 50 $
"Found flexible variable " <+> text (show i)
let Dom{unDom = b} = getVarTypeUnraised (varCount s - 1 - i) s
(d, pars) <- catMaybesMP $ liftTCM $ isEtaRecordType b
ps <- fromMaybeMP $ allProjElims es
sing <- liftTCM $ (Right True ==) <$> isSingletonRecord d pars
con <- liftTCM $ isRecCon v
guard $ not (null ps) || sing || con
liftTCM $ reportSDoc "tc.lhs.unify" 50 $
"with projections " <+> prettyTCM (map snd ps)
liftTCM $ reportSDoc "tc.lhs.unify" 50 $
"at record type " <+> prettyTCM d
return $ EtaExpandVar fi d pars
shouldEtaExpand _ _ _ _ = mzero
isRecCon (Con c _ _) = isJust <$> isRecordConstructor (conName c)
isRecCon _ = return False
etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy k s = do
let Equal Dom{unDom = a} u v = getEqualityUnraised k s
(d, pars) <- catMaybesMP $ liftTCM $ addContext tel $ isEtaRecordType a
sing <- liftTCM $ (Right True ==) <$> isSingletonRecord d pars
projLeft <- liftTCM $ shouldProject u
projRight <- liftTCM $ shouldProject v
guard $ sing || projLeft || projRight
return $ EtaExpandEquation k d pars
where
shouldProject :: Term -> TCM Bool
shouldProject u = case u of
Def f es -> usesCopatterns f
Con c _ _ -> isJust <$> isRecordConstructor (conName c)
Var _ _ -> return False
Lam _ _ -> __IMPOSSIBLE__
Lit _ -> __IMPOSSIBLE__
Pi _ _ -> __IMPOSSIBLE__
Sort _ -> __IMPOSSIBLE__
Level _ -> __IMPOSSIBLE__
MetaV _ _ -> return False
DontCare _ -> return False
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
tel = varTel s `abstract` telFromList (take k $ telToList $ eqTel s)
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy k s = do
isSizeName <- liftTCM isSizeNameTest
let Equal Dom{unDom = a} u v = getEquality k s
case unEl a of
Def d _ -> do
guard $ isSizeName d
su <- liftTCM $ sizeView u
sv <- liftTCM $ sizeView v
case (su, sv) of
(SizeSuc u, SizeSuc v) -> return $ StripSizeSuc k u v
(SizeSuc u, SizeInf ) -> return $ StripSizeSuc k u v
(SizeInf , SizeSuc v) -> return $ StripSizeSuc k u v
_ -> mzero
_ -> mzero
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy k s = do
injTyCon <- liftTCM $ optInjectiveTypeConstructors <$> pragmaOptions
guard injTyCon
eq <- liftTCM $ eqUnLevel $ getEquality k s
case eq of
Equal a u@(Def d es) v@(Def d' es') | d == d' -> do
def <- liftTCM $ getConstInfo d
guard $ case theDef def of
Datatype{} -> True
Record{} -> True
Axiom{} -> True
DataOrRecSig{} -> True
AbstractDefn{} -> False
Function{} -> False
Primitive{} -> False
GeneralizableVar{} -> __IMPOSSIBLE__
Constructor{} -> __IMPOSSIBLE__
let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
return $ TypeConInjectivity k d us vs
_ -> mzero
injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy k s = do
eq <- liftTCM $ eqUnLevel $ getEquality k s
case eq of
Equal a u@(Def d es) v@(Def d' es') | d == d' -> do
def <- liftTCM $ getConstInfo d
guard $ defInjective def
let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
return $ TypeConInjectivity k d us vs
_ -> mzero
skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy k s = do
let Equal a _ _ = getEquality k s
guard =<< isIrrelevantOrPropM a
return $ SkipIrrelevantEquation k
data UnifyLogEntry
= UnificationDone UnifyState
| UnificationStep UnifyState UnifyStep
type UnifyLog = [UnifyLogEntry]
data UnifyOutput = UnifyOutput
{ unifySubst :: PatternSubstitution
, unifyProof :: PatternSubstitution
, unifyLog :: UnifyLog
}
instance Semigroup UnifyOutput where
x <> y = UnifyOutput
{ unifySubst = unifySubst y `composeS` unifySubst x
, unifyProof = unifyProof y `composeS` unifyProof x
, unifyLog = unifyLog x ++ unifyLog y
}
instance Monoid UnifyOutput where
mempty = UnifyOutput IdS IdS []
mappend = (<>)
type UnifyM a = WriterT UnifyOutput TCM a
tellUnifySubst :: PatternSubstitution -> UnifyM ()
tellUnifySubst sub = tell $ UnifyOutput sub IdS []
tellUnifyProof :: PatternSubstitution -> UnifyM ()
tellUnifyProof sub = tell $ UnifyOutput IdS sub []
writeUnifyLog :: UnifyLogEntry -> UnifyM ()
writeUnifyLog x = tell $ UnifyOutput IdS IdS [x]
runUnifyM :: UnifyM a -> TCM (a,UnifyOutput)
runUnifyM = runWriterT
unifyStep :: UnifyState -> UnifyStep -> UnifyM (UnificationResult' UnifyState)
unifyStep s Deletion{ deleteAt = k , deleteType = a , deleteLeft = u , deleteRight = v } = do
isReflexive <- liftTCM $ addContext (varTel s) $ do
dontAssignMetas $ noConstraints $ equalTerm a u v
return Nothing
`catchError` \err -> return $ Just err
withoutK <- liftTCM $ optWithoutK <$> pragmaOptions
case isReflexive of
Just err -> return $ DontKnow []
_ | withoutK -> return $ DontKnow [UnifyReflexiveEq (varTel s) a u]
_ -> do
let (s', sigma) = solveEq k u s
tellUnifyProof sigma
Unifies <$> liftTCM (reduceEqTel s')
unifyStep s Solution{ solutionAt = k
, solutionType = dom@Dom{ unDom = a }
, solutionVar = fi@FlexibleVar{ flexVar = i }
, solutionTerm = u } = do
let m = varCount s
let dom'@Dom{ unDom = a' } = getVarType (m-1-i) s
equalTypes <- liftTCM $ addContext (varTel s) $ do
reportSDoc "tc.lhs.unify" 45 $ "Equation type: " <+> prettyTCM a
reportSDoc "tc.lhs.unify" 45 $ "Variable type: " <+> prettyTCM a'
dontAssignMetas $ noConstraints $ equalType a a'
return Nothing
`catchError` \err -> return $ Just err
let eqrel = getRelevance dom
varmod = getModality dom'
mod = applyUnless (NonStrict `moreRelevant` eqrel) (setRelevance eqrel)
$ varmod
reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom)
reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod
reportSDoc "tc.lhs.unify" 65 $ text $ "Solution must be usable in a " ++ show mod ++ " position."
usable <- liftTCM $ addContext (varTel s) $ usableRel (getRelevance mod) u
reportSDoc "tc.lhs.unify" 45 $ "Modality ok: " <+> prettyTCM usable
unless usable $ reportSLn "tc.lhs.unify" 65 $ "Rejected solution: " ++ show u
case equalTypes of
Just err -> return $ DontKnow []
Nothing | usable -> caseMaybeM (trySolveVar (m-1-i) u s)
(return $ DontKnow [UnifyRecursiveEq (varTel s) a i u])
(\(s',sub) -> do
tellUnifySubst sub
let (s'', sigma) = solveEq k (applyPatSubst sub u) s'
tellUnifyProof sigma
Unifies <$> liftTCM (reduce s''))
Nothing -> return $ DontKnow []
where
trySolveVar i u s = case solveVar i u s of
Just x -> return $ Just x
Nothing -> do
u <- liftTCM $ normalise u
s <- liftTCM $ normaliseVarTel s
return $ solveVar i u s
unifyStep s (Injectivity k a d pars ixs c) = do
ifM (liftTCM $ consOfHIT $ conName c) (return $ DontKnow []) $ do
withoutK <- liftTCM $ optWithoutK <$> pragmaOptions
let n = eqCount s
ctype <- (`piApply` pars) . defType <$> liftTCM (getConInfo c)
addContext (varTel s) $ reportSDoc "tc.lhs.unify" 40 $
"Constructor type: " <+> prettyTCM ctype
TelV ctel ctarget <- liftTCM $ telView ctype
let cixs = case unEl ctarget of
Def d' es | d == d' ->
let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
in drop (length pars) args
_ -> __IMPOSSIBLE__
dtype <- (`piApply` pars) . defType <$> liftTCM (getConstInfo d)
addContext (varTel s) $ reportSDoc "tc.lhs.unify" 40 $
"Datatype type: " <+> prettyTCM dtype
let (eqListTel1, _ : eqListTel2) = splitAt k $ telToList $ eqTel s
(eqTel1, eqTel2) = (telFromList eqListTel1, telFromList eqListTel2)
let hduTel = eqTel1 `abstract` raise (size eqTel1) ctel
res <- liftTCM $ addContext (varTel s) $ unifyIndices
hduTel
(allFlexVars hduTel)
(raise (size hduTel) dtype)
(raise (size ctel) ixs)
(raiseFrom (size ctel) (size eqTel1) cixs)
case res of
NoUnify _ -> __IMPOSSIBLE__
DontKnow _ | not withoutK -> do
let eqTel1' = eqTel1 `abstract` raise (size eqTel1) ctel
rho1 = raiseS (size ctel)
ceq = ConP c noConPatternInfo $ teleNamedArgs ctel
rho3 = consS ceq rho1
eqTel2' = applyPatSubst rho3 eqTel2
eqTel' = eqTel1' `abstract` eqTel2'
rho = liftS (size eqTel2) rho3
tellUnifyProof rho
eqTel' <- liftTCM $ reduce eqTel'
(lhs', rhs') <- liftTCM . reduce =<< do
let ps = applySubst rho $ teleNamedArgs $ eqTel s
(lhsMatch, _) <- liftTCM $ runReduceM $ Match.matchPatterns ps $ eqLHS s
(rhsMatch, _) <- liftTCM $ runReduceM $ Match.matchPatterns ps $ eqRHS s
case (lhsMatch, rhsMatch) of
(Match.Yes _ lhs', Match.Yes _ rhs') -> return
(reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs',
reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs')
_ -> __IMPOSSIBLE__
return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }
DontKnow _ -> let n = eqCount s
Equal Dom{unDom = a} u v = getEquality k s
in return $ DontKnow [UnifyIndicesNotVars
(varTel s `abstract` eqTel s) a
(raise n u) (raise n v) (raise (n-k) ixs)]
Unifies (eqTel1', rho0, _) -> do
let (rho1, rho2) = splitS (size ctel) rho0
let ceq = ConP c noConPatternInfo $ applySubst rho2 $ teleNamedArgs ctel
rho3 = consS ceq rho1
eqTel2' = applyPatSubst rho3 eqTel2
eqTel' = eqTel1' `abstract` eqTel2'
rho = liftS (size eqTel2) rho3
tellUnifyProof rho
eqTel' <- liftTCM $ reduce eqTel'
(lhs', rhs') <- liftTCM . reduce =<< do
let ps = applySubst rho $ teleNamedArgs $ eqTel s
(lhsMatch, _) <- liftTCM $ runReduceM $ Match.matchPatterns ps $ eqLHS s
(rhsMatch, _) <- liftTCM $ runReduceM $ Match.matchPatterns ps $ eqRHS s
case (lhsMatch, rhsMatch) of
(Match.Yes _ lhs', Match.Yes _ rhs') -> return
(reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs',
reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs')
_ -> __IMPOSSIBLE__
return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }
unifyStep s Conflict
{ conflictLeft = u
, conflictRight = v
} =
case u of
Con h _ _ -> do
ifM (liftTCM $ consOfHIT $ conName h) (return $ DontKnow []) $ do
return $ NoUnify $ UnifyConflict (varTel s) u v
_ -> __IMPOSSIBLE__
unifyStep s Cycle
{ cycleVar = i
, cycleOccursIn = u
} =
case u of
Con h _ _ -> do
ifM (liftTCM $ consOfHIT $ conName h) (return $ DontKnow []) $ do
return $ NoUnify $ UnifyCycle (varTel s) i u
_ -> __IMPOSSIBLE__
unifyStep s EtaExpandVar{ expandVar = fi, expandVarRecordType = d , expandVarParameters = pars } = do
delta <- liftTCM $ (`apply` pars) <$> getRecordFieldTypes d
c <- liftTCM $ getRecordConstructor d
let nfields = size delta
(varTel', rho) = expandTelescopeVar (varTel s) (m-1-i) delta c
projectFlexible = [ FlexibleVar (flexHiding fi) (flexOrigin fi) (projFlexKind j) (flexPos fi) (i+j) | j <- [0..nfields-1] ]
tellUnifySubst $ rho
Unifies <$> liftTCM (reduce $ UState
{ varTel = varTel'
, flexVars = projectFlexible ++ liftFlexibles nfields (flexVars s)
, eqTel = applyPatSubst rho $ eqTel s
, eqLHS = applyPatSubst rho $ eqLHS s
, eqRHS = applyPatSubst rho $ eqRHS s
})
where
i = flexVar fi
m = varCount s
n = eqCount s
projFlexKind :: Int -> FlexibleVarKind
projFlexKind j = case flexKind fi of
RecordFlex ks -> indexWithDefault ImplicitFlex ks j
ImplicitFlex -> ImplicitFlex
DotFlex -> DotFlex
OtherFlex -> OtherFlex
liftFlexible :: Int -> Int -> Maybe Int
liftFlexible n j = if j == i then Nothing else Just (if j > i then j + (n-1) else j)
liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
liftFlexibles n fs = mapMaybe (traverse $ liftFlexible n) fs
unifyStep s EtaExpandEquation{ expandAt = k, expandRecordType = d, expandParameters = pars } = do
delta <- liftTCM $ (`apply` pars) <$> getRecordFieldTypes d
c <- liftTCM $ getRecordConstructor d
lhs <- expandKth $ eqLHS s
rhs <- expandKth $ eqRHS s
let (tel, sigma) = expandTelescopeVar (eqTel s) k delta c
tellUnifyProof sigma
Unifies <$> liftTCM (reduceEqTel $ s
{ eqTel = tel
, eqLHS = lhs
, eqRHS = rhs
})
where
expandKth us = do
let (us1,v:us2) = fromMaybe __IMPOSSIBLE__ $ splitExactlyAt k us
vs <- liftTCM $ snd <$> etaExpandRecord d pars (unArg v)
vs <- liftTCM $ reduce vs
return $ us1 ++ vs ++ us2
unifyStep s LitConflict
{ litType = a
, litConflictLeft = l
, litConflictRight = l'
} = return $ NoUnify $ UnifyConflict (varTel s) (Lit l) (Lit l')
unifyStep s (StripSizeSuc k u v) = do
sizeTy <- liftTCM sizeType
sizeSu <- liftTCM $ sizeSuc 1 (var 0)
let n = eqCount s
sub = liftS (n-k-1) $ consS sizeSu $ raiseS 1
eqFlatTel = flattenTel $ eqTel s
eqFlatTel' = applySubst sub $ updateAt k (fmap $ const sizeTy) $ eqFlatTel
eqTel' = unflattenTel (teleNames $ eqTel s) eqFlatTel'
return $ Unifies $ s
{ eqTel = eqTel'
, eqLHS = updateAt k (const $ defaultArg u) $ eqLHS s
, eqRHS = updateAt k (const $ defaultArg v) $ eqRHS s
}
unifyStep s (SkipIrrelevantEquation k) = do
let lhs = eqLHS s
(s', sigma) =
solveEq k (DontCare $ unArg $ indexWithDefault __IMPOSSIBLE__ lhs k) s
tellUnifyProof sigma
return $ Unifies s'
unifyStep s (TypeConInjectivity k d us vs) = do
dtype <- defType <$> liftTCM (getConstInfo d)
TelV dtel _ <- liftTCM $ telView dtype
let n = eqCount s
m = size dtel
deq = Def d $ map Apply $ teleArgs dtel
Unifies <$> liftTCM (reduceEqTel $ s
{ eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq)
, eqLHS = us ++ dropAt k (eqLHS s)
, eqRHS = vs ++ dropAt k (eqRHS s)
})
unify :: UnifyState -> UnifyStrategy -> UnifyM (UnificationResult' UnifyState)
unify s strategy = if isUnifyStateSolved s
then return $ Unifies s
else tryUnifyStepsAndContinue (strategy s)
where
tryUnifyStepsAndContinue :: ListT TCM UnifyStep -> UnifyM (UnificationResult' UnifyState)
tryUnifyStepsAndContinue steps = do
x <- foldListT tryUnifyStep failure $ liftListT lift steps
case x of
Unifies s' -> unify s' strategy
NoUnify err -> return $ NoUnify err
DontKnow err -> return $ DontKnow err
tryUnifyStep :: UnifyStep
-> UnifyM (UnificationResult' UnifyState)
-> UnifyM (UnificationResult' UnifyState)
tryUnifyStep step fallback = do
addContext (varTel s) $
reportSDoc "tc.lhs.unify" 20 $ "trying unifyStep" <+> prettyTCM step
x <- unifyStep s step
case x of
Unifies s' -> do
reportSDoc "tc.lhs.unify" 20 $ "unifyStep successful."
reportSDoc "tc.lhs.unify" 20 $ "new unifyState:" <+> prettyTCM s'
writeUnifyLog $ UnificationStep s step
return x
NoUnify{} -> return x
DontKnow err1 -> do
y <- fallback
case y of
DontKnow err2 -> return $ DontKnow $ err1 ++ err2
_ -> return y
failure :: UnifyM (UnificationResult' a)
failure = return $ DontKnow []