module Agda.TypeChecking.Rewriting.NonLinMatch where
import Prelude hiding (null, sequence)
import Control.Arrow (first, second)
import Control.Monad.State
import Debug.Trace
import System.IO.Unsafe
#if __GLASGOW_HASKELL__ <= 708
import Data.Foldable ( foldMap )
#endif
import Data.Maybe
import Data.Traversable (Traversable,traverse)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (elemIndex)
import Data.Monoid
import Agda.Syntax.Common
import qualified Agda.Syntax.Common as C
import Agda.Syntax.Internal
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free
import Agda.TypeChecking.Level (levelView', unLevel, reallyUnLevelView, subLevel)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (primLevelSuc, primLevelMax)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records (isRecordConstructor)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope (permuteTel)
import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
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
class PatternFrom a b where
patternFrom :: Relevance -> Int -> a -> TCM b
instance (PatternFrom a b) => PatternFrom [a] [b] where
patternFrom r k = traverse $ patternFrom r k
instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
patternFrom r k u = let r' = r `composeRelevance` getRelevance u
in traverse (patternFrom r' k) u
instance (PatternFrom a NLPat) => PatternFrom (Elim' a) (Elim' NLPat) where
patternFrom r k (Apply u) = let r' = r `composeRelevance` getRelevance u
in Apply <$> traverse (patternFrom r' k) u
patternFrom r k (Proj o f) = return $ Proj o f
instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
patternFrom r k = traverse $ patternFrom r k
instance PatternFrom Type NLPType where
patternFrom r k a = NLPType <$> patternFrom r k (getSort a)
<*> patternFrom r k (unEl a)
instance PatternFrom Sort NLPat where
patternFrom r k s = do
s <- reduce s
let done = return PWild
case s of
Type l -> patternFrom Irrelevant k (Level l)
Prop -> done
Inf -> done
SizeUniv -> done
DLub _ _ -> done
instance PatternFrom Term NLPat where
patternFrom r k v = do
v <- unLevel =<< reduce v
let done = if isIrrelevant r then
return PWild
else
return $ PTerm v
case ignoreSharing v of
Var i es
| i < k -> PBoundVar i <$> patternFrom r k es
| otherwise -> do
let mbvs = mfilter fastDistinct $ forM es $ \e -> do
e <- isApplyElim e
case ignoreSharing $ unArg e of
Var j [] | j < k -> Just $ e $> j
_ -> Nothing
case mbvs of
Just bvs -> do
let i' = ik
allBoundVars = IntSet.fromList (downFrom k)
ok = not (isIrrelevant r) ||
IntSet.fromList (map unArg bvs) == allBoundVars
id <- (!! i') <$> getContextId
if ok then return (PVar (Just id) i' bvs) else done
Nothing -> done
Lam i t -> PLam i <$> patternFrom r k t
Lit{} -> done
Def f es | isIrrelevant r -> done
Def f es -> do
Def lsuc [] <- ignoreSharing <$> primLevelSuc
Def lmax [] <- ignoreSharing <$> primLevelMax
case es of
[x] | f == lsuc -> done
[x , y] | f == lmax -> done
_ -> PDef f <$> patternFrom r k es
Con c ci vs | isIrrelevant r -> do
mr <- isRecordConstructor (conName c)
case mr of
Just (_, def) | recEtaEquality def ->
PDef (conName c) <$> patternFrom r k (Apply <$> vs)
_ -> done
Con c ci vs -> PDef (conName c) <$> patternFrom r k (Apply <$> vs)
Pi a b | isIrrelevant r -> done
Pi a b -> PPi <$> patternFrom r k a <*> patternFrom r k b
Sort s -> done
Level l -> __IMPOSSIBLE__
DontCare{} -> return PWild
MetaV{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
instance (PatternFrom a b) => PatternFrom (Abs a) (Abs b) where
patternFrom r k (Abs name x) = Abs name <$> patternFrom r (k+1) x
patternFrom r k (NoAbs name x) = NoAbs name <$> patternFrom r k x
type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
data NLMState = NLMState
{ _nlmSub :: Sub
, _nlmEqs :: PostponedEquations
}
instance Null NLMState where
empty = NLMState { _nlmSub = empty , _nlmEqs = empty }
null s = null (s^.nlmSub) && null (s^.nlmEqs)
nlmSub :: Lens' Sub NLMState
nlmSub f s = f (_nlmSub s) <&> \x -> s {_nlmSub = x}
nlmEqs :: Lens' PostponedEquations NLMState
nlmEqs f s = f (_nlmEqs s) <&> \x -> s {_nlmEqs = x}
liftRed :: ReduceM a -> NLM a
liftRed = lift . lift
instance HasOptions NLM where
pragmaOptions = liftRed pragmaOptions
commandLineOptions = liftRed commandLineOptions
runNLM :: NLM () -> ReduceM (Either Blocked_ NLMState)
runNLM nlm = do
(ok,out) <- runStateT (runExceptT nlm) empty
case ok of
Left block -> return $ Left block
Right _ -> return $ Right out
traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a
traceSDocNLM k n doc = applyWhenVerboseS k n $ \ cont -> do
ReduceEnv env st <- liftRed askR
trace (show $ fst $ unsafePerformIO $ runTCM env st doc) cont
matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked = throwError
tellSub :: Relevance -> Int -> Term -> NLM ()
tellSub r i v = do
old <- IntMap.lookup i <$> use nlmSub
case old of
Nothing -> nlmSub %= IntMap.insert i (r,v)
Just (r',v')
| isIrrelevant r -> return ()
| isIrrelevant r' -> nlmSub %= IntMap.insert i (r,v)
| otherwise -> whenJustM (liftRed $ equal v v') matchingBlocked
tellEq :: Telescope -> Telescope -> Term -> Term -> NLM ()
tellEq gamma k u v =
traceSDocNLM "rewriting" 60 (sep
[ text "adding equality between" <+> addContext (gamma `abstract` k) (prettyTCM u)
, text " and " <+> addContext k (prettyTCM v) ]) $ do
nlmEqs %= (PostponedEquation k u v:)
type Sub = IntMap (Relevance, Term)
data PostponedEquation = PostponedEquation
{ eqFreeVars :: Telescope
, eqLhs :: Term
, eqRhs :: Term
}
type PostponedEquations = [PostponedEquation]
class Match a b where
match :: Relevance
-> Telescope
-> Telescope
-> a
-> b
-> NLM ()
instance Match a b => Match [a] [b] where
match r gamma k ps vs
| length ps == length vs = zipWithM_ (match r gamma k) ps vs
| otherwise = matchingBlocked $ NotBlocked ReallyNotBlocked ()
instance Match a b => Match (Arg a) (Arg b) where
match r gamma k p v = let r' = r `composeRelevance` getRelevance p
in match r' gamma k (unArg p) (unArg v)
instance Match a b => Match (Elim' a) (Elim' b) where
match r gamma k p v =
case (p, v) of
(Apply p, Apply v) -> let r' = r `composeRelevance` getRelevance p
in match r' gamma k p v
(Proj _ x, Proj _ y) -> if x == y then return () else
traceSDocNLM "rewriting" 80 (sep
[ text "mismatch between projections " <+> prettyTCM x
, text " and " <+> prettyTCM y ]) mzero
(Apply{}, Proj{} ) -> __IMPOSSIBLE__
(Proj{} , Apply{}) -> __IMPOSSIBLE__
instance Match a b => Match (Dom a) (Dom b) where
match r gamma k p v = match r gamma k (C.unDom p) (C.unDom v)
instance Match NLPType Type where
match r gamma k (NLPType lp p) (El s a) = match r gamma k lp s >> match r gamma k p a
instance Match NLPat Sort where
match r gamma k p s = case (p , s) of
(PWild , _ ) -> return ()
(p , Type l) -> match Irrelevant gamma k p l
_ -> matchingBlocked $ NotBlocked ReallyNotBlocked ()
instance (Match a b, RaiseNLP a, Subst t2 b) => Match (Abs a) (Abs b) where
match r gamma k (Abs n p) (Abs _ v) = match r gamma (ExtendTel dummyDom (Abs n k)) p v
match r gamma k (Abs n p) (NoAbs _ v) = match r gamma (ExtendTel dummyDom (Abs n k)) p (raise 1 v)
match r gamma k (NoAbs n p) (Abs _ v) = match r gamma (ExtendTel dummyDom (Abs n k)) (raiseNLP 1 p) v
match r gamma k (NoAbs _ p) (NoAbs _ v) = match r gamma k p v
instance Match NLPat Level where
match r gamma k p l = match r gamma k p =<< liftRed (reallyUnLevelView l)
instance Match NLPat Term where
match r gamma k p v = do
vb <- liftRed $ reduceB' v
let n = size k
b = void vb
v = ignoreBlocking vb
prettyPat = addContext (gamma `abstract` k) (prettyTCM (raisePatVars n p))
prettyTerm = addContext k (prettyTCM v)
traceSDocNLM "rewriting" 100 (sep
[ text "matching" <+> prettyPat
, text "with" <+> prettyTerm]) $ do
let yes = return ()
no msg =
traceSDocNLM "rewriting" 80 (sep
[ text "mismatch between" <+> prettyPat
, text " and " <+> prettyTerm
, msg ]) $ matchingBlocked b
block b' =
traceSDocNLM "rewriting" 80 (sep
[ text "matching blocked on meta"
, text (show b) ]) $ matchingBlocked (b `mappend` b')
case p of
PWild -> yes
PVar id i bvs -> do
ctx <- zip <$> getContextNames <*> getContextId
traceSDocNLM "rewriting" 90 (text "Current context:" <+> (prettyTCM ctx)) $ do
cid <- getContextId
case (maybe Nothing (\i -> elemIndex i cid) id) of
Just j -> if v == var (j+n)
then tellSub r i (var j)
else no (text $ "(CtxId = " ++ show id ++ ")")
Nothing -> do
let allowedVars :: IntSet
allowedVars = IntSet.fromList (map unArg bvs)
isBadVar :: Int -> Bool
isBadVar i = i < n && not (i `IntSet.member` allowedVars)
perm :: Permutation
perm = Perm n $ reverse $ map unArg $ bvs
tel :: Telescope
tel = permuteTel perm k
ok <- liftRed $ reallyFree isBadVar v
case ok of
Left b -> block b
Right Nothing -> no (text "")
Right (Just v) -> tellSub r i $ teleLam tel $ renameP __IMPOSSIBLE__ perm v
PDef f ps -> do
v <- liftRed $ constructorForm =<< unLevel v
case ignoreSharing v of
Def f' es
| f == f' -> match r gamma k ps es
Con c _ vs
| f == conName c -> match r gamma k ps (Apply <$> vs)
| otherwise -> do
mr <- liftRed $ isRecordConstructor (conName c)
case mr of
Just (_, def) | recEtaEquality def -> do
let fs = recFields def
qs = map (fmap $ \f -> PDef f (ps ++ [Proj ProjSystem f])) fs
match r gamma k qs vs
_ -> no (text "")
Lam i u -> do
let pbody = PDef f (raiseNLP 1 ps ++ [Apply $ Arg i $ PTerm (var 0)])
body = absBody u
match r gamma (ExtendTel dummyDom (Abs (absName u) k)) pbody body
MetaV m es -> do
matchingBlocked $ Blocked m ()
v' -> do
mr <- liftRed $ isRecordConstructor f
case mr of
Just (_, def) | recEtaEquality def -> do
let fs = recFields def
ws = map (fmap $ \f -> v `applyE` [Proj ProjSystem f]) fs
qs = fromMaybe __IMPOSSIBLE__ $ allApplyElims ps
match r gamma k qs ws
_ -> no (text "")
PLam i p' -> do
let body = Abs (absName p') $ raise 1 v `apply` [Arg i (var 0)]
match r gamma k p' body
PPi pa pb -> case ignoreSharing v of
Pi a b -> match r gamma k pa a >> match r gamma k pb b
MetaV m es -> matchingBlocked $ Blocked m ()
_ -> no (text "")
PBoundVar i ps -> case ignoreSharing v of
Var i' es | i == i' -> match r gamma k ps es
Con c _ vs -> do
mr <- liftRed $ isRecordConstructor (conName c)
case mr of
Just (_, def) | recEtaEquality def -> do
let fs = recFields def
qs = map (fmap $ \f -> PBoundVar i (ps ++ [Proj ProjSystem f])) fs
match r gamma k qs vs
_ -> no (text "")
Lam info u -> do
let pbody = PBoundVar i (raiseNLP 1 ps ++ [Apply $ Arg info $ PTerm (var 0)])
body = absBody u
match r gamma (ExtendTel dummyDom (Abs (absName u) k)) pbody body
MetaV m es -> matchingBlocked $ Blocked m ()
_ -> no (text "")
PTerm u -> tellEq gamma k u v
reallyFree :: (Reduce a, Normalise a, Free' a FreeVars)
=> (Int -> Bool) -> a -> ReduceM (Either Blocked_ (Maybe a))
reallyFree f v = do
let xs = getVars v
if null (stronglyRigidVars xs) && null (unguardedVars xs)
then do
if null (weaklyRigidVars xs) && null (flexibleVars xs)
&& null (irrelevantVars xs)
then return $ Right $ Just v
else do
bv <- normaliseB' v
let b = void bv
v = ignoreBlocking bv
xs = getVars v
b' = foldMap (foldMap $ \m -> Blocked m ()) $ flexibleVars xs
if null (stronglyRigidVars xs) && null (unguardedVars xs)
&& null (weaklyRigidVars xs) && null (irrelevantVars xs)
then if null (flexibleVars xs)
then return $ Right $ Just v
else return $ Left $ b `mappend` b'
else return $ Right Nothing
else return $ Right Nothing
where
getVars v = runFree (\var@(i,_) -> if f i then singleton var else empty) IgnoreNot v
makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution gamma sub =
prependS __IMPOSSIBLE__ (map val [0 .. size gamma1]) EmptyS
where
val i = case IntMap.lookup i sub of
Just (Irrelevant, v) -> Just $ dontCare v
Just (_ , v) -> Just v
Nothing -> Nothing
checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM (Maybe Blocked_)
checkPostponedEquations sub eqs = forM' eqs $
\ (PostponedEquation k lhs rhs) -> equal (applySubst (liftS (size k) sub) lhs) rhs
nonLinMatch :: (Match a b) => Telescope -> a -> b -> ReduceM (Either Blocked_ Substitution)
nonLinMatch gamma p v = do
let no msg b = traceSDoc "rewriting" 80 (sep
[ text "matching failed during" <+> text msg
, text "blocking: " <+> text (show b) ]) $ return (Left b)
caseEitherM (runNLM $ match Relevant gamma EmptyTel p v) (no "matching") $ \ s -> do
let sub = makeSubstitution gamma $ s^.nlmSub
eqs = s^.nlmEqs
traceSDoc "rewriting" 90 (text $ "sub = " ++ show sub) $ do
ok <- checkPostponedEquations sub eqs
case ok of
Nothing -> return $ Right sub
Just b -> no "checking of postponed equations" b
equal :: Term -> Term -> ReduceM (Maybe Blocked_)
equal u v = do
(u, v) <- etaContract =<< normalise' (u, v)
let ok = u == v
metas = allMetas (u, v)
block = caseMaybe (headMaybe metas)
(NotBlocked ReallyNotBlocked ())
(\m -> Blocked m ())
if ok then return Nothing else
traceSDoc "rewriting" 80 (sep
[ text "mismatch between " <+> prettyTCM u
, text " and " <+> prettyTCM v
]) $ return $ Just block
normaliseB' :: (Reduce t, Normalise t) => t -> ReduceM (Blocked t)
normaliseB' = normalise' >=> reduceB'
class RaiseNLP a where
raiseNLPFrom :: Int -> Int -> a -> a
raiseNLP :: Int -> a -> a
raiseNLP = raiseNLPFrom 0
instance RaiseNLP a => RaiseNLP [a] where
raiseNLPFrom c k = fmap $ raiseNLPFrom c k
instance RaiseNLP a => RaiseNLP (Maybe a) where
raiseNLPFrom c k = fmap $ raiseNLPFrom c k
instance RaiseNLP a => RaiseNLP (Arg a) where
raiseNLPFrom c k = fmap $ raiseNLPFrom c k
instance RaiseNLP a => RaiseNLP (Elim' a) where
raiseNLPFrom c k = fmap $ raiseNLPFrom c k
instance RaiseNLP a => RaiseNLP (Dom a) where
raiseNLPFrom c k = fmap $ raiseNLPFrom c k
instance RaiseNLP NLPType where
raiseNLPFrom c k (NLPType l a) =
NLPType (raiseNLPFrom c k l) (raiseNLPFrom c k a)
instance RaiseNLP a => RaiseNLP (Abs a) where
raiseNLPFrom c k (Abs i p) = Abs i $ raiseNLPFrom (c+1) k p
raiseNLPFrom c k (NoAbs i p) = NoAbs i $ raiseNLPFrom c k p
instance RaiseNLP NLPat where
raiseNLPFrom c k p = case p of
PVar id i bvs -> let raise j = if j < c then j else j + k
in PVar id i $ map (fmap raise) bvs
PWild -> p
PDef f ps -> PDef f $ raiseNLPFrom c k ps
PLam i q -> PLam i $ raiseNLPFrom c k q
PPi a b -> PPi (raiseNLPFrom c k a) (raiseNLPFrom c k b)
PBoundVar i ps -> let j = if i < c then i else i + k
in PBoundVar j $ raiseNLPFrom c k ps
PTerm u -> PTerm $ raiseFrom c k u