{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE GADTs #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Rewriting with arbitrary rules.
--
--   The user specifies a relation symbol by the pragma
--   @
--       {-\# BUILTIN REWRITE rel \#-}
--   @
--   where @rel@ should be of type @Δ → (lhs rhs : A) → Set i@.
--
--   Then the user can add rewrite rules by the pragma
--   @
--       {-\# REWRITE q \#-}
--   @
--   where @q@ should be a closed term of type @Γ → rel us lhs rhs@.
--
--   We then intend to add a rewrite rule
--   @
--       Γ ⊢ lhs ↦ rhs : B
--   @
--   to the signature where @B = A[us/Δ]@.
--
--   To this end, we normalize @lhs@, which should be of the form
--   @
--       f ts
--   @
--   for a @'Def'@-symbol f (postulate, function, data, record, constructor).
--   Further, @FV(ts) = dom(Γ)@.
--   The rule @q :: Γ ⊢ f ts ↦ rhs : B@ is added to the signature
--   to the definition of @f@.
--
--   When reducing a term @Ψ ⊢ f vs@ is stuck, we try the rewrites for @f@,
--   by trying to unify @vs@ with @ts@.
--   This is for now done by substituting fresh metas Xs for the bound
--   variables in @ts@ and checking equality with @vs@
--   @
--       Ψ ⊢ (f ts)[Xs/Γ] = f vs : B[Xs/Γ]
--   @
--   If successful (no open metas/constraints), we replace @f vs@ by
--   @rhs[Xs/Γ]@ and continue reducing.

module Agda.TypeChecking.Rewriting where

import Prelude hiding (null)

import Control.Monad

import Data.Foldable (toList)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Interaction.Options

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free
import Agda.TypeChecking.Conversion
import qualified Agda.TypeChecking.Positivity.Occurrence as Pos
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive ( getBuiltinName )
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.Rewriting.NonLinMatch
import Agda.TypeChecking.Rewriting.NonLinPattern
import Agda.TypeChecking.Warnings

import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet

import Agda.Utils.Impossible
import Agda.Utils.Either

requireOptionRewriting :: TCM ()
requireOptionRewriting :: TCM ()
requireOptionRewriting =
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optRewriting forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionRewriting

-- | Check that the name given to the BUILTIN REWRITE is actually
--   a relation symbol.
--   I.e., its type should be of the form @Δ → (lhs : A) (rhs : B) → Set ℓ@.
--   Note: we do not care about hiding/non-hiding of lhs and rhs.
verifyBuiltinRewrite :: Term -> Type -> TCM ()
verifyBuiltinRewrite :: Term -> Type -> TCM ()
verifyBuiltinRewrite Term
v Type
t = do
  TCM ()
requireOptionRewriting
  let failure :: TCMT IO Doc -> TCM ()
failure TCMT IO Doc
reason = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
       [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" does not have the right type for a rewriting relation"
       , TCMT IO Doc
reason
       ]
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCM (Maybe RelView)
relView Type
t)
    (TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because it should accept at least two arguments") forall a b. (a -> b) -> a -> b
$
    \ (RelView Tele (Dom Type)
tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
b Type
core) -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensHiding a => a -> Bool
visible Dom Type
a Bool -> Bool -> Bool
&& forall a. LensHiding a => a -> Bool
visible Dom Type
b) forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because its two final arguments are not both visible."
    case forall t a. Type'' t a -> a
unEl Type
core of
      Sort{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Con{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Level{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Lam{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Pi{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> TCMT IO Doc -> TCM ()
failure forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"because its type does not end in a sort, but in "
             forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core

-- | Deconstructing a type into @Δ → t → t' → core@.
data RelView = RelView
  { RelView -> Tele (Dom Type)
relViewTel   :: Telescope  -- ^ The whole telescope @Δ, t, t'@.
  , RelView -> [Dom (ArgName, Type)]
relViewDelta :: ListTel    -- ^ @Δ@.
  , RelView -> Dom Type
relViewType  :: Dom Type   -- ^ @t@.
  , RelView -> Dom Type
relViewType' :: Dom Type   -- ^ @t'@.
  , RelView -> Type
relViewCore  :: Type       -- ^ @core@.
  }

-- | Deconstructing a type into @Δ → t → t' → core@.
--   Returns @Nothing@ if not enough argument types.
relView :: Type -> TCM (Maybe RelView)
relView :: Type -> TCM (Maybe RelView)
relView Type
t = do
  TelV Tele (Dom Type)
tel Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let n :: Int
n                = forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
      ([Dom (ArgName, Type)]
delta, [Dom (ArgName, Type)]
lastTwo) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n forall a. Num a => a -> a -> a
- Int
2) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel
  if forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
lastTwo forall a. Ord a => a -> a -> Bool
< Int
2 then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else do
    let [Dom Type
a, Dom Type
b] = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom (ArgName, Type)]
lastTwo
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> [Dom (ArgName, Type)] -> Dom Type -> Dom Type -> Type -> RelView
RelView Tele (Dom Type)
tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
b Type
core

-- | Check the given rewrite rules and add them to the signature.
addRewriteRules :: [QName] -> TCM ()
addRewriteRules :: [QName] -> TCM ()
addRewriteRules [QName]
qs = do

  -- Check the rewrite rules
  RewriteRules
rews <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM RewriteRule
checkRewriteRule [QName]
qs

  -- Add rewrite rules to the signature
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RewriteRules
rews forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
    let f :: QName
f = RewriteRule -> QName
rewHead RewriteRule
rew
        matchables :: [QName]
matchables = forall a. GetMatchables a => a -> [QName]
getMatchables RewriteRule
rew
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"adding rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      TCMT IO Doc
"to the definition of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"matchable symbols: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
matchables
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor QName
f [RewriteRule
rew] [QName]
matchables

  -- Run confluence check for the new rules
  -- (should be done after adding all rules, see #3795)
  forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ \ConfluenceCheck
confChk -> do
    -- Warn if --cubical is enabled
    forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ \Cubical
_ -> forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning
      Doc
"Confluence checking for --cubical is not yet supported, confluence checking might be incomplete"
    -- Global confluence checker requires rules to be sorted
    -- according to the generality of their lhs
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConfluenceCheck
confChk forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> QName
rewHead RewriteRules
rews) QName -> TCM ()
sortRulesOfSymbol
    ConfluenceCheck -> RewriteRules -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk RewriteRules
rews
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"done checking confluence of rules" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) RewriteRules
rews)

-- Auxiliary function for checkRewriteRule.
-- | Get domain of rewrite relation.
rewriteRelationDom :: QName -> TCM (ListTel, Dom Type)
rewriteRelationDom :: QName -> TCM ([Dom (ArgName, Type)], Dom Type)
rewriteRelationDom QName
rel = do
  -- We know that the type of rel is that of a relation.
  Maybe RelView
relV <- Type -> TCM (Maybe RelView)
relView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
rel
  let RelView Tele (Dom Type)
_tel [Dom (ArgName, Type)]
delta Dom Type
a Dom Type
_a' Type
_core = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe RelView
relV
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ do
    TCMT IO Doc
"rewrite relation at type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
      forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Dom (ArgName, Type)] -> Tele (Dom Type)
telFromList [Dom (ArgName, Type)]
delta) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" |- " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Dom (ArgName, Type)]
delta forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
  forall (m :: * -> *) a. Monad m => a -> m a
return ([Dom (ArgName, Type)]
delta, Dom Type
a)

-- | Check the validity of @q : Γ → rel us lhs rhs@ as rewrite rule
--   @
--       Γ ⊢ lhs ↦ rhs : B
--   @
--   where @B = A[us/Δ]@.
--   Remember that @rel : Δ → A → A → Set i@, so
--   @rel us : (lhs rhs : A[us/Δ]) → Set i@.
--   Returns the checked rewrite rule to be added to the signature.
checkRewriteRule :: QName -> TCM RewriteRule
checkRewriteRule :: QName -> TCM RewriteRule
checkRewriteRule QName
q = do
  TCM ()
requireOptionRewriting
  let failNoBuiltin :: TCMT IO a
failNoBuiltin = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
        ArgName
"Cannot add rewrite rule without prior BUILTIN REWRITE"
  Set QName
rels <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM forall {a}. TCMT IO a
failNoBuiltin forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting.relations" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Rewrite relations:"
    , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set QName
rels
    ]
  Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  -- Issue 1651: Check that we are not adding a rewrite rule
  -- for a type signature whose body has not been type-checked yet.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Defn -> Bool
isEmptyFunction forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
      [ TCMT IO Doc
"Rewrite rule from function "
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
      , TCMT IO Doc
" cannot be added before the function definition"
      ]
  -- Get rewrite rule (type of q).
  TelV Tele (Dom Type)
gamma1 Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"attempting to add rewrite rule of type "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
gamma1
    , TCMT IO Doc
" |- " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
core
    ]
  let failureWrongTarget :: TCM a
      failureWrongTarget :: forall {a}. TCMT IO a
failureWrongTarget = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" does not target rewrite relation" ]
  let failureBlocked :: Blocker -> TCM a
      failureBlocked :: forall a. Blocker -> TCM a
failureBlocked Blocker
b
        | Bool -> Bool
not (forall a. Null a => a -> Bool
null Set MetaId
ms) = TCMT IO Doc -> TCMT IO a
err forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"it contains the unsolved meta variable(s)" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set MetaId
ms)
        | Bool -> Bool
not (forall a. Null a => a -> Bool
null Set ProblemId
ps) = TCMT IO Doc -> TCMT IO a
err forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"it is blocked on problem(s)" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set ProblemId
ps)
        | Bool -> Bool
not (forall a. Null a => a -> Bool
null Set QName
qs) = TCMT IO Doc -> TCMT IO a
err forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"it requires the definition(s) of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set QName
qs)
        | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
        where
          err :: TCMT IO Doc -> TCMT IO a
err TCMT IO Doc
reason = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
            [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since" , TCMT IO Doc
reason ]
          ms :: Set MetaId
ms = Blocker -> Set MetaId
allBlockingMetas Blocker
b
          ps :: Set ProblemId
ps = Blocker -> Set ProblemId
allBlockingProblems Blocker
b
          qs :: Set QName
qs = Blocker -> Set QName
allBlockingDefs Blocker
b
  let failureNotDefOrCon :: TCM a
      failureNotDefOrCon :: forall {a}. TCMT IO a
failureNotDefOrCon = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
  let failureFreeVars :: IntSet -> TCM a
      failureFreeVars :: forall a. IntSet -> TCM a
failureFreeVars IntSet
xs = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the following variables are not bound by the left hand side: " , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
xs) ]
  let failureNonLinearPars :: IntSet -> TCM a
      failureNonLinearPars :: forall a. IntSet -> TCM a
failureNonLinearPars IntSet
xs = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not a legal rewrite rule, since the following parameters are bound more than once on the left hand side: "
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a. a -> [a] -> [a]
List.intersperse TCMT IO Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
xs))
          forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
". Perhaps you can use a postulate instead of a constructor as the head symbol?"
  let failureIllegalRule :: TCM a -- TODO:: Defined but not used
      failureIllegalRule :: forall {a}. TCMT IO a
failureIllegalRule = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule" ]

  -- Check that type of q targets rel.
  case forall t a. Type'' t a -> a
unEl Type
core of
    Def QName
rel es :: Elims
es@(Elim' Term
_:Elim' Term
_:Elims
_) | QName
rel forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
rels -> do
      ([Dom (ArgName, Type)]
delta, Dom Type
a) <- QName -> TCM ([Dom (ArgName, Type)], Dom Type)
rewriteRelationDom QName
rel
      -- Because of the type of rel (Γ → sort), all es are applications.
      let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      -- The last two arguments are lhs and rhs.
          n :: Int
n  = forall a. Sized a => a -> Int
size [Term]
vs
          ([Term]
us, [Term
lhs, Term
rhs]) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n forall a. Num a => a -> a -> a
- Int
2) [Term]
vs
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
delta forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Term]
us) forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
lhs <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
lhs
      Term
rhs <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
rhs
      Dom Type
b   <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Term]
us) Dom Type
a

      Tele (Dom Type)
gamma0 <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      Tele (Dom Type)
gamma1 <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Tele (Dom Type)
gamma1
      let gamma :: Tele (Dom Type)
gamma = Tele (Dom Type)
gamma0 forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
gamma1

      -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
      -- This is necessary to replace copies created by imports by their
      -- original definition.
      Term
lhs <- forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. SmallSetElement a => a -> SmallSet a
SmallSet.singleton AllowedReduction
InlineReductions) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
lhs

      -- Find head symbol f of the lhs, its type, its parameters (in case of a constructor), and its arguments.
      (QName
f , Elims -> Term
hd , Type
t , [Int]
pars , Elims
es) <- case Term
lhs of
        Def QName
f Elims
es -> do
          Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          QName -> Definition -> TCM ()
checkAxFunOrCon QName
f Definition
def
          forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f , QName -> Elims -> Term
Def QName
f , Definition -> Type
defType Definition
def , [] , Elims
es)
        Con ConHead
c ConInfo
ci Elims
vs -> do
          let hd :: Elims -> Term
hd = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci
          ~(Just ((QName
_ , Type
_ , [Arg Term]
pars) , Type
t)) <- forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
getFullyAppliedConType ConHead
c forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
b
          [Int]
pars <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ ConHead -> [Arg Term] -> TCMT IO [Int]
checkParametersAreGeneral ConHead
c [Arg Term]
pars
          forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> QName
conName ConHead
c , Elims -> Term
hd , Type
t , [Int]
pars , Elims
vs)
        Term
_        -> forall {a}. TCMT IO a
failureNotDefOrCon

      QName -> TCM RewriteRule -> TCM RewriteRule
ifNotAlreadyAdded QName
f forall a b. (a -> b) -> a -> b
$ do

      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
gamma1 forall a b. (a -> b) -> a -> b
$ do

        QName -> (Elims -> Term) -> Elims -> TCM ()
checkNoLhsReduction QName
f Elims -> Term
hd Elims
es

        PElims
ps <- forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr forall a. Blocker -> TCM a
failureBlocked forall a b. (a -> b) -> a -> b
$
          forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
Relevant Int
0 (Type
t , QName -> Elims -> Term
Def QName
f []) Elims
es

        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Pattern generated from lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> PElims -> NLPat
PDef QName
f PElims
ps)

        -- We need to check two properties on the variables used in the rewrite rule
        -- 1. For actually being able to apply the rewrite rule, we need
        --    that all variables that occur in the rule (on the left or the right)
        --    are bound in a pattern position on the left.
        -- 2. To preserve soundness, we need that all the variables that are used
        --    in the *proof* of the rewrite rule are bound in the lhs.
        --    For rewrite rules on constructors, we consider parameters to be bound
        --    even though they don't appear in the lhs, since they can be reconstructed.
        --    For postulated or abstract rewrite rules, we consider all arguments
        --    as 'used' (see #5238).
        let boundVars :: IntSet
boundVars = forall a. NLPatVars a => a -> IntSet
nlPatVars PElims
ps
            freeVars :: IntSet
freeVars  = forall t. Free t => t -> IntSet
allFreeVars (PElims
ps,Term
rhs)
            allVars :: IntSet
allVars   = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma
            usedVars :: IntSet
usedVars  = case Definition -> Defn
theDef Definition
def of
              Function{}     -> Definition -> IntSet
usedArgs Definition
def
              Axiom{}        -> IntSet
allVars
              AbstractDefn{} -> IntSet
allVars
              Defn
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"variables bound by the pattern: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
boundVars)
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"variables free in the rewrite rule: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
freeVars)
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"variables used by the rewrite rule: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IntSet
usedVars)
        forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (IntSet
freeVars IntSet -> IntSet -> IntSet
IntSet.\\ IntSet
boundVars) forall a. IntSet -> TCM a
failureFreeVars
        forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (IntSet
usedVars IntSet -> IntSet -> IntSet
IntSet.\\ (IntSet
boundVars IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int]
pars)) forall a. IntSet -> TCM a
failureFreeVars

        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
70 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"variables bound in (erased) parameter position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show [Int]
pars)
        forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (IntSet
boundVars IntSet -> IntSet -> IntSet
`IntSet.intersection` [Int] -> IntSet
IntSet.fromList [Int]
pars) forall a. IntSet -> TCM a
failureNonLinearPars

        let rew :: RewriteRule
rew = QName
-> Tele (Dom Type)
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
q Tele (Dom Type)
gamma QName
f PElims
ps Term
rhs (forall t e. Dom' t e -> e
unDom Dom Type
b) Bool
False

        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"checked rewrite rule" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew ]
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
90 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"checked rewrite rule" , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show RewriteRule
rew) ]

        forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew

    Term
_ -> forall {a}. TCMT IO a
failureWrongTarget

  where
    checkNoLhsReduction :: QName -> (Elims -> Term)  -> Elims -> TCM ()
    checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> TCM ()
checkNoLhsReduction QName
f Elims -> Term
hd Elims
es = do
      -- Skip this check when global confluence check is enabled, as
      -- redundant rewrite rules may be required to prove confluence.
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just ConfluenceCheck
GlobalConfluenceCheck) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
      let v :: Term
v = Elims -> Term
hd Elims
es
      Term
v' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      let fail :: TCM a
          fail :: forall {a}. TCMT IO a
fail = do
            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Term
v)
            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Term
v')
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
              [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not a legal rewrite rule, since the left-hand side "
              , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" reduces to " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' ]
      Elims
es' <- case Term
v' of
        Def QName
f' Elims
es'   | QName
f forall a. Eq a => a -> a -> Bool
== QName
f'         -> forall (m :: * -> *) a. Monad m => a -> m a
return Elims
es'
        Con ConHead
c' ConInfo
_ Elims
es' | QName
f forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c' -> forall (m :: * -> *) a. Monad m => a -> m a
return Elims
es'
        Term
_                              -> forall {a}. TCMT IO a
fail
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Elims
es Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Elims
es') forall a b. (a -> b) -> a -> b
$ do
        Type
a   <- forall (m :: * -> *).
MonadConversion m =>
QName -> Elims -> Elims -> m Type
computeElimHeadType QName
f Elims
es Elims
es'
        [Polarity]
pol <- forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
f
        Bool
ok  <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$
                 forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pol [] Type
a (QName -> Elims -> Term
Def QName
f []) Elims
es Elims
es'
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall {a}. TCMT IO a
fail

    checkAxFunOrCon :: QName -> Definition -> TCM ()
    checkAxFunOrCon :: QName -> Definition -> TCM ()
checkAxFunOrCon QName
f Definition
def = case Definition -> Defn
theDef Definition
def of
      Axiom{}        -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      def :: Defn
def@Function{} -> forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (forall a b. Either a b -> Maybe b
maybeRight (Defn -> Either ProjectionLikenessMissing Projection
funProjection Defn
def)) forall a b. (a -> b) -> a -> b
$ \Projection
proj ->
        case Projection -> Maybe QName
projProper Projection
proj of
          Just{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
            [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the head symbol"
            , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f , TCMT IO Doc
"is a projection"
            ]
          Maybe QName
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
            [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the head symbol"
            , TCMT IO Doc
hd , TCMT IO Doc
"is a projection-like function."
            , TCMT IO Doc
"You can turn off the projection-like optimization for", TCMT IO Doc
hd
            , TCMT IO Doc
"with the pragma {-# NOT_PROJECTION_LIKE", TCMT IO Doc
hd, TCMT IO Doc
"#-}"
            , TCMT IO Doc
"or globally with the flag --no-projection-like"
            ]
            where hd :: TCMT IO Doc
hd = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
      Constructor{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      AbstractDefn{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Primitive{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: is this fine?
      Defn
_              -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
" is not a legal rewrite rule, since the head symbol"
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f , TCMT IO Doc
"is not a postulate, a function, or a constructor"
        ]

    ifNotAlreadyAdded :: QName -> TCM RewriteRule -> TCM RewriteRule
    ifNotAlreadyAdded :: QName -> TCM RewriteRule -> TCM RewriteRule
ifNotAlreadyAdded QName
f TCM RewriteRule
cont = do
      RewriteRules
rews <- forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
f
      -- check if q is already an added rewrite rule
      case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((QName
q forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) RewriteRules
rews of
        Just RewriteRule
rew -> do
          forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            TCMT IO Doc
"Rewrite rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has already been added"
          forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule
rew
        Maybe RewriteRule
Nothing -> TCM RewriteRule
cont

    usedArgs :: Definition -> IntSet
    usedArgs :: Definition -> IntSet
usedArgs Definition
def = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ [(Occurrence, Int)]
usedIxs
      where
        occs :: [Occurrence]
occs = Definition -> [Occurrence]
defArgOccurrences Definition
def
        allIxs :: [(Occurrence, Int)]
allIxs = forall a b. [a] -> [b] -> [(a, b)]
zip [Occurrence]
occs forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size [Occurrence]
occs
        usedIxs :: [(Occurrence, Int)]
usedIxs = forall a. (a -> Bool) -> [a] -> [a]
filter (Occurrence -> Bool
used forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Occurrence, Int)]
allIxs
        used :: Occurrence -> Bool
used Occurrence
Pos.Unused = Bool
False
        used Occurrence
_          = Bool
True

    checkParametersAreGeneral :: ConHead -> Args -> TCM [Int]
    checkParametersAreGeneral :: ConHead -> [Arg Term] -> TCMT IO [Int]
checkParametersAreGeneral ConHead
c [Arg Term]
vs = do
        [Int]
is <- [Arg Term] -> TCMT IO [Int]
loop [Arg Term]
vs
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => [a] -> Bool
fastDistinct [Int]
is) forall a b. (a -> b) -> a -> b
$ forall {a}. TCMT IO a
errorNotGeneral
        forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
is
      where
        loop :: [Arg Term] -> TCMT IO [Int]
loop []       = forall (m :: * -> *) a. Monad m => a -> m a
return []
        loop (Arg Term
v : [Arg Term]
vs) = case forall e. Arg e -> e
unArg Arg Term
v of
          Var Int
i [] -> (Int
i forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TCMT IO [Int]
loop [Arg Term]
vs
          Term
_        -> forall {a}. TCMT IO a
errorNotGeneral

        errorNotGeneral :: TCM a
        errorNotGeneral :: forall {a}. TCMT IO a
errorNotGeneral = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
" is not a legal rewrite rule, since the constructor parameters are not fully general:"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Constructor: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
            ]

-- | @rewriteWith t f es rew@ where @f : t@
--   tries to rewrite @f es@ with @rew@, returning the reduct if successful.
rewriteWith :: Type
            -> (Elims -> Term)
            -> RewriteRule
            -> Elims
            -> ReduceM (Either (Blocked Term) Term)
rewriteWith :: Type
-> (Elims -> Term)
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type
t Elims -> Term
hd rew :: RewriteRule
rew@(RewriteRule QName
q Tele (Dom Type)
gamma QName
_ PElims
ps Term
rhs Type
b Bool
isClause) Elims
es
 | Bool
isClause = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd Elims
es
 | Bool
otherwise = do
  forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"{ attempting to rewrite term " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
    , TCMT IO Doc
" having head " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    , TCMT IO Doc
" with rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew
    ]) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
90 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"raw: attempting to rewrite term " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) (Elims -> Term
hd Elims
es)
    , TCMT IO Doc
" having head " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Type
t
    , TCMT IO Doc
" with rule " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) RewriteRule
rew
    ]) forall a b. (a -> b) -> a -> b
$ do
  Either Blocked_ Substitution
result <- forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
Tele (Dom Type) -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Tele (Dom Type)
gamma (Type
t,Elims -> Term
hd) PElims
ps Elims
es
  case Either Blocked_ Substitution
result of
    Left Blocked_
block -> forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 TCMT IO Doc
"}" forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Blocked_
block forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd Elims
es -- TODO: remember reductions
    Right Substitution
sub  -> do
      let v' :: Term
v' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub Term
rhs
      forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
50 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"rewrote " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
        , TCMT IO Doc
" to " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"}"
        ]) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Term
v'

-- | @rewrite b v rules es@ tries to rewrite @v@ applied to @es@ with the
--   rewrite rules @rules@. @b@ is the default blocking tag.
rewrite :: Blocked_ -> (Elims -> Term) -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
rewrite :: Blocked_
-> (Elims -> Term)
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked_
block Elims -> Term
hd RewriteRules
rules Elims
es = do
  Bool
rewritingAllowed <- PragmaOptions -> Bool
optRewriting forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  if (Bool
rewritingAllowed Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null RewriteRules
rules)) then do
    (QName
_ , Type
t) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead (Elims -> Term
hd [])
    Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t RewriteRules
rules forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Elims
es -- TODO: remove instantiateFull?
  else
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction (Blocked_
block forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd Elims
es)
  where
    loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
    loop :: Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t [] Elims
es =
      forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc ArgName
"rewriting.rewrite" Int
20 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"failed to rewrite " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
        , TCMT IO Doc
"blocking tag" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Blocked_
block)
        ]) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ Blocked_
block forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd Elims
es
    loop Blocked_
block Type
t (RewriteRule
rew:RewriteRules
rews) Elims
es
     | let n :: Int
n = RewriteRule -> Int
rewArity RewriteRule
rew, forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es forall a. Ord a => a -> a -> Bool
>= Int
n = do
          let (Elims
es1, Elims
es2) = forall i a. Integral i => i -> [a] -> ([a], [a])
List.genericSplitAt Int
n Elims
es
          Either (Blocked Term) Term
result <- Type
-> (Elims -> Term)
-> RewriteRule
-> Elims
-> ReduceM (Either (Blocked Term) Term)
rewriteWith Type
t Elims -> Term
hd RewriteRule
rew Elims
es1
          case Either (Blocked Term) Term
result of
            Left (Blocked Blocker
m Term
u)    -> Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block forall a. Monoid a => a -> a -> a
`mappend` forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
m ()) Type
t RewriteRules
rews Elims
es
            Left (NotBlocked NotBlocked' Term
_ Term
_) -> Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop Blocked_
block Type
t RewriteRules
rews Elims
es
            Right Term
w               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification forall a b. (a -> b) -> a -> b
$ Term
w forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2
     | Bool
otherwise = Blocked_
-> Type
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
loop (Blocked_
block forall a. Monoid a => a -> a -> a
`mappend` forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
Underapplied ()) Type
t RewriteRules
rews Elims
es

    rewArity :: RewriteRule -> Int
    rewArity :: RewriteRule -> Int
rewArity = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> PElims
rewPats