From 4cdd3c3f372124286606d5d4d7cf455cb390ccc9 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Sun, 17 Mar 2019 00:01:48 +0900 Subject: [PATCH] [ rewriting ] Use typed conversion for non-linear rewrite rules --- .../TypeChecking/Rewriting/NonLinMatch.hs | 55 +++++++++---------- 1 file changed, 27 insertions(+), 28 deletions(-) diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs index c58d6e96b7d..1beb0554782 100644 --- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs @@ -45,13 +45,14 @@ import Agda.Syntax.Common import qualified Agda.Syntax.Common as C import Agda.Syntax.Internal +import Agda.TypeChecking.Conversion.Pure import Agda.TypeChecking.Datatypes import Agda.TypeChecking.EtaContract import Agda.TypeChecking.Free import Agda.TypeChecking.Free.Reduce import Agda.TypeChecking.Level import Agda.TypeChecking.Monad -import Agda.TypeChecking.Monad.Builtin (getBuiltin', builtinLevel, primLevelSuc, primLevelMax) +import Agda.TypeChecking.Monad.Builtin (HasBuiltins(..), getBuiltin', builtinLevel, primLevelSuc, primLevelMax) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records import Agda.TypeChecking.Reduce @@ -235,23 +236,23 @@ runNLM nlm = do matchingBlocked :: Blocked_ -> NLM () matchingBlocked = throwError --- | Add substitution @i |-> v@ to result of matching. -tellSub :: Relevance -> Int -> Term -> NLM () -tellSub r i v = do +-- | Add substitution @i |-> v : a@ to result of matching. +tellSub :: Relevance -> Int -> Type -> Term -> NLM () +tellSub r i a 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 (equal v v') matchingBlocked + | otherwise -> whenJustM (equal a v v') matchingBlocked -tellEq :: Telescope -> Telescope -> Term -> Term -> NLM () -tellEq gamma k u v = do +tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM () +tellEq gamma k a u v = do traceSDoc "rewriting.match" 30 (sep [ "adding equality between" <+> addContext (gamma `abstract` k) (prettyTCM u) , " and " <+> addContext k (prettyTCM v) ]) $ do - nlmEqs %= (PostponedEquation k u v:) + nlmEqs %= (PostponedEquation k a u v:) type Sub = IntMap (Relevance, Term) @@ -260,6 +261,7 @@ type Sub = IntMap (Relevance, Term) -- the substitution computed by matching. data PostponedEquation = PostponedEquation { eqFreeVars :: Telescope -- ^ Telescope of free variables in the equation + , eqType :: Type -- ^ Type of the equation, living in same context as the rhs. , eqLhs :: Term -- ^ Term from pattern, living in pattern context. , eqRhs :: Term -- ^ Term from scrutinee, living in context where matching was invoked. } @@ -383,8 +385,7 @@ instance Match Type NLPat Term where case ok of Left b -> block b Right Nothing -> no "" - Right (Just v) -> tellSub r (i-n) $ teleLam tel $ renameP __IMPOSSIBLE__ perm v - + Right (Just v) -> tellSub r (i-n) t $ teleLam tel $ renameP __IMPOSSIBLE__ perm v _ | MetaV m es <- v -> matchingBlocked $ Blocked m () PDef f ps -> traceSDoc "rewriting.match" 60 ("matching a PDef: " <+> prettyTCM f) $ do @@ -453,7 +454,7 @@ instance Match Type NLPat Term where match r gamma k (ct, Con c ci []) (map Apply ps') (map Apply vs) _ -> no "" PTerm u -> traceSDoc "rewriting.match" 60 ("matching a PTerm" <+> addContext (gamma `abstract` k) (prettyTCM u)) $ - tellEq gamma k u v + tellEq gamma k t u v -- Checks if the given term contains any free variables that satisfy the -- given condition on their DBI, possibly reducing the term in the process. @@ -493,18 +494,18 @@ makeSubstitution gamma sub = Just (_ , v) -> Just v Nothing -> Nothing -checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m) +checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_) checkPostponedEquations sub eqs = forM' eqs $ - \ (PostponedEquation k lhs rhs) -> do + \ (PostponedEquation k a lhs rhs) -> do let lhs' = applySubst (liftS (size k) sub) lhs traceSDoc "rewriting.match" 30 (sep [ "checking postponed equality between" , addContext k (prettyTCM lhs') , " and " , addContext k (prettyTCM rhs) ]) $ do - addContext k $ equal lhs' rhs + addContext k $ equal a lhs' rhs -- main function -nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m, Match t a b) +nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution) nonLinMatch gamma t p v = do let no msg b = traceSDoc "rewriting.match" 10 (sep @@ -519,22 +520,20 @@ nonLinMatch gamma t p v = do Nothing -> return $ Right sub Just b -> no "checking of postponed equations" b --- | Untyped βη-equality, does not handle things like empty record types. +-- | Typed βη-equality, also handles empty record types. -- Returns `Nothing` if the terms are equal, or `Just b` if the terms are not -- (where b contains information about possible metas blocking the comparison) - --- TODO: implement a type-directed, lazy version of this function. -equal :: (MonadReduce m, HasConstInfo m) - => Term -> Term -> m (Maybe Blocked_) -equal u v = do - (u, v) <- etaContract =<< normalise (u, v) - let ok = u == v - block = caseMaybe (firstMeta (u, v)) - (NotBlocked ReallyNotBlocked ()) - (\ m -> Blocked m ()) - if ok then return Nothing else do - traceSDoc "rewriting.match" 10 (sep +equal :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m) + => Type -> Term -> Term -> m (Maybe Blocked_) +equal a u v = pureEqualTerm a u v >>= \case + True -> return Nothing + False -> traceSDoc "rewriting.match" 10 (sep [ "mismatch between " <+> prettyTCM u , " and " <+> prettyTCM v ]) $ do return $ Just block + + where + block = caseMaybe (firstMeta (u, v)) + (NotBlocked ReallyNotBlocked ()) + (\m -> Blocked m ())