{-# OPTIONS --safe #-}
-- {-# OPTIONS -v tactic.premises:100 #-}
module Prelude.STS.GenPremises where

-- FIXME: upstream this
open import Prelude.Init
  hiding (Type; pred; _∷_)
  renaming (_∈_ to _∈ˡ_)

open import Prelude.InferenceRules
open import Class.Show
open import Class.Foldable
open import Class.Decidable
open import Class.DecEq.Instances
open import Class.Monad
open import Class.Functor
open import Class.Semigroup

open import Meta.Init
  renaming (TC to TCI)
  hiding (Monad-TC; MonadError-TC)
open import Agda.Builtin.Reflection
  using (withReduceDefs)
open import Reflection
  using (TC; Name; Meta; extendContext; withNormalisation)
open import Reflection.Utils
  hiding (mkRecord)
open import Reflection.Debug
open import Reflection.Utils.Debug
  hiding (error)
open import Class.MonadTC
  hiding (extendContext)
open MonadTC ⦃...⦄
open import Class.MonadError
  using (MonadError; MonadError-TC)
open MonadError ⦃...⦄
  using (error; catch)
open import Meta.Prelude

open Debug ("tactic.premises", 100)
open import Reflection using ()

open import Data.List using (_∷_; [])

instance
  iTC  = MonadTC-TC
  iTCE = MonadError-TC

-- N-ary extension of the TC context.
-- TODO: use `MonadTC.extendContext'` once it includes names
extendContextTel : Telescope → TC A → TC A
extendContextTel = λ where
  [] → id
  ((x , t) ∷ tel) → extendContext x t ∘ extendContextTel tel

-- -- N-ary extension of the TCI context.
-- extendContextTel′ : Telescope → TCI A → TCI A
-- extendContextTel′ = λ where
--   [] m → m
--   ((x , ty) ∷ tys) m → extendContext x ty ∘ extendContextTel′ tys m

-- Reducing only definitions.
reduceDef : Type → TC Type
reduceDef = λ where
  t@(def _ _) → reduce t
  t           → return t

-- Constructing list of quoted names without having to use `quote`.
macro
  infixr 4 _`∷_
  _`∷_ : Name → List Name → Hole → TC ⊤
  (x `∷ y) hole = do
    `x ← quoteTC x
    `y ← quoteTC y
    unify hole $ con (quote _∷_) (vArg `x ∷ vArg `y ∷ [])

-- Calculating all free variables of a term.
freeVars : Term → List ℕ
freeVars = go 0 where mutual
  go : ℕ → Term → _
  go bound = λ where
    (var x as) → if bound Nat.≤ᵇ x then [ x ∸ bound ] else []
    (def _ as) → goArgs bound as
    (con _ as) → goArgs bound as
    (lam _ t̂) → goAbs (suc bound) t̂
    (pat-lam cs as) → goCls bound cs ++ goArgs bound as
    (pi at t̂) → goArg bound at ++ goAbs (suc bound) t̂
    (meta _ as) → goArgs bound as
    _ → []

  goArg : ℕ → Arg Term → _
  goArg b (arg _ t) = go b t

  goAbs : ℕ → Abs Term → _
  goAbs b (abs _ t) = go b t

  goArgs : ℕ → Args Term → _
  goArgs b = λ where [] → []; (a ∷ as) → goArg b a ++ goArgs b as

  goCl : ℕ → Clause → _
  goCl b = λ where
    (clause tel _ t) → go (length tel + b) t
    (absurd-clause _ _) → []

  goCls : ℕ → List Clause → _
  goCls b = λ where [] → []; (c ∷ cs) → goCl b c ++ goCls b cs

module _ x y z where
  _ = freeVars (quoteTerm (λ x → x + 1))
    ≡ []
    ∋ refl
  _ = freeVars (quoteTerm (λ x → x + y))
    ≡ [ 1 ]
    ∋ refl
  _ = freeVars (quoteTerm (λ x y → x + y + z))
    ≡ [ 0 ]
    ∋ refl
  _ = freeVars (quoteTerm (λ x → x + y + z))
    ≡ (1 ∷ 0 ∷ [])
    ∋ refl
  _ = freeVars (quoteTerm (x + y + z))
    ≡ (2 ∷ 1 ∷ 0 ∷ [])
    ∋ refl
  _ = freeVars (quote _,_ ◆⟦ ♯ 0 ∣ `λ "y" ⇒ ♯ 1 ⟧)
    ≡ (0 ∷ 0 ∷ [])
    ∋ refl

-- ** Telescopes providing names via `Abs` instead of products.

AbsTelescope = List (Abs (Arg Type))

absTelescope : AbsTelescope → Telescope
absTelescope = map λ where (abs x t) → x , t

telescopeAbs : Telescope → AbsTelescope
telescopeAbs = map $ uncurry abs

showAbsTel = show ⦃ Show-Tel ⦄ ∘ absTelescope

-- Check that a type has an instance.
hasInstance : Type → TC Bool
hasInstance = isSuccessful ∘ checkType (quote it ∙)

{-
** Extracting the hypotheses of an STS rule.

Constructors should be formulated in the STS syntax for inference rules, i.e.

    rule : ∀ <IMPLICIT_ARGUMENTS + LET_EXPRESSIONS>
      ∙ <HYPOTHESIS#1>
      ∙ <HYPOTHESIS#2>
      ⋮
      ∙ <HYPOTHESIS#n-1>
      ∙ <HYPOTHESIS#n>
        ────────────────────────────────
        <CONCLUSION>

This meta-program then generates the type of the (decidable) hypotheses of the rule,
as well as a proof that it is in fact decidable, i.e.

    rule-premises : ∀ ⋯ → Set
    rule-premises ⋯ =
      ∙ <HYPOTHESIS#1>
      ∙ <HYPOTHESIS#3>
      ⋮
      ∙ <HYPOTHESIS#n-1>

    rule-premises? : ∀ ⋯ → Dec (rule-premises ⋯)
    rule-premises? = it

where ⋯ stands for the subset of implicit arguments that are relevant for the
selected subset of decidable hypotheses.

To be precise, we generate both definitions above under a single name, as well as
wrapping the decidability proof in the _⁇ typeclass from `Class.Decidable`, i.e.

    unquoteDecl rule-premises = genPremises rule-premises (quote rule)
    -- rule-premises        : ∀ ⋯ → ∃ _⁇
    -- rule-premises .proj₁ : ∀ ⋯ → Set
    -- rule-premises .proj₂ : ∀ ⋯ → (rule-premises .proj₁ ⋯) ⁇
-}

whitelist : List Name
whitelist =
    quote _∙_
  ∷ quote ∙_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────────_
  ∷ quote _──────────────────────────────────────────_
  ∷ quote _─────────────────────────────────────────_
  ∷ quote _────────────────────────────────────────_
  ∷ quote _───────────────────────────────────────_
  ∷ quote _──────────────────────────────────────_
  ∷ quote _─────────────────────────────────────_
  ∷ quote _────────────────────────────────────_
  ∷ quote _───────────────────────────────────_
  ∷ quote _──────────────────────────────────_
  ∷ quote _─────────────────────────────────_
  ∷ quote _────────────────────────────────_
  ∷ quote _───────────────────────────────_
  ∷ quote _──────────────────────────────_
  ∷ quote _─────────────────────────────_
  ∷ quote _────────────────────────────_
  ∷ quote _───────────────────────────_
  ∷ quote _──────────────────────────_
  ∷ quote _─────────────────────────_
  ∷ quote _────────────────────────_
  ∷ quote _───────────────────────_
  ∷ quote _──────────────────────_
  ∷ quote _─────────────────────_
  ∷ quote _────────────────────_
  ∷ quote _───────────────────_
  ∷ quote _──────────────────_
  ∷ quote _─────────────────_
  ∷ quote _────────────────_
  ∷ quote _───────────────_
  ∷ quote _──────────────_
  ∷ quote _─────────────_
  ∷ quote _────────────_
  ∷ quote _───────────_
  ∷ quote _──────────_
  ∷ quote _─────────_
  ∷ quote _────────_
  ∷ quote _───────_
  ∷ quote _──────_
  ∷ quote _─────_
  ∷ quote _────_
  ∷ quote _───_
  -- ^ include all syntactic sugar for inference rules here
  ∷ []

genPremises : Name → Name → TC ⊤
genPremises f n = do
  print $ "*** Generating premises for constructor:" <+> show n <+> "***"
  ty ← reduceRuleSyntax =<< getType n             -- (1)
  let is , hs = breakImplicits $ viewTy ty .proj₁ -- (2)
  hs ← fmap unbundleHypotheses                     -- (3)
     $ extendContextTel (absTelescope is)
     $ mapM reduceRuleSyntax hs -- reducing again to work around Agda issue #6951
  dhs ← filterM (isDecidable? is) hs              -- (4)
  let dhs = bundleHypotheses dhs                  -- (5)
  is , premise ← removeUnusedImplicits is dhs     -- (6)
  let premiseTy  = tyView (is , quote ∃⁇ ∙)
      premiseTel = absTelescope is
      premisePs  = map (λ (i , x) → arg (argInfo $ unAbs x) (` i))
                       (uncurry L.zip $ map₁ reverse $ unzip $ enumerate is)
      ∃premise?  = quote _,_ ◆⟦ premise ∣ quote it ∙ ⟧
      cl         = clause premiseTel premisePs ∃premise?
  print $ "```\n" <> show f <+> ":" <+> show premiseTy <> "\n"
       -- <> show f <+> "⋯ =" <+> show premise <> " , it\n```\n"
       -- TOO EXPENSIVE FOR LARGE RULES (even without `-v` flag)
  declareDef (vArg f) premiseTy
  defineFun f [ cl ]
  where
  -- (1) unfold syntactic sugar from Interface.STS
  reduceRuleSyntax : Type → TC Type
  reduceRuleSyntax ty = do
    withReduceDefs (true , whitelist) $ normalise ty

  -- (2) separate implicit arguments from visible hypotheses
  breakImplicits : AbsTelescope → AbsTelescope × List Type
  breakImplicits = map₂  (unArgs ∘ map unAbs)
                 ∘ break (isVisible? ∘ unAbs)

  -- (3) unbundle hypotheses (always a single product due to `∙`)
  --     * TODO: generalise to curried rules (which use `→`)
  unbundleHypotheses : List Type → List Type
  unbundleHypotheses = concatMap go where go = λ where
    (def (quote _×_) (hArg _ ∷ hArg _ ∷ vArg x ∷ vArg ys ∷ [])) →
      x ∷ go ys
    t → [ t ]

  -- (4) select only the hypotheses that are decidable
  isDecidable? : AbsTelescope → Type → TC Bool
  isDecidable? tel ty =
    isSuccessful $ checkType (quote it ∙) (tyView (tel , quote _⁇ ∙⟦ ty ⟧))

  -- (5) bundle the (decidable) hypotheses back together in a single product
  bundleHypotheses : List Type → Type
  bundleHypotheses []       = quote ⊤ ∙
  bundleHypotheses (x ∷ []) = x
  bundleHypotheses (x ∷ xs) = quote _×_ ∙⟦ x ∣ bundleHypotheses xs ⟧

  -- (6) minimize the implicit arguments to only the ones that are actually used in (5)
  removeUnusedImplicits : AbsTelescope → Type → TC (AbsTelescope × Type)
  removeUnusedImplicits is ty = go (pred $ length is) is ty
    where
    fvs = freeVars ty

    go : ℕ → AbsTelescope → Type → TC (AbsTelescope × Type)
    go _ []       t = return ([] , t)
    go n (i ∷ is) t =
      ifᵈ n ∈ˡ fvs then -- relevant hypothesis
        map₁ (i ∷_) <$> go (pred n) is t
      else -- irrelevant hypothesis
        go (pred n) is (mapFreeVars pred n t)

-- ** Tests.
private

  -- * The tactics works for one or zero hypotheses.
  data ℝ : ℕ → ℕ → Set where
    base :
      ────────────────────────────────
      ℝ 0 0

    step : ∀ {n m} →
      ∙ ℝ n m
      ────────────────────────────────
      ℝ (suc n) (suc m)

  module _ ⦃ _ : ℝ ⁇² ⦄ where
    unquoteDecl ℝ-base-premises = genPremises ℝ-base-premises (quote ℝ.base)
    unquoteDecl ℝ-step-premises = genPremises ℝ-step-premises (quote ℝ.step)

    _ : ℝ-base-premises .proj₁
    _ = tt

    _ : ℝ-base-premises .proj₂ .dec ≡ yes tt
    _ = refl

    module _ (n m : ℕ) (𝕣 : ℝ n m) where
      _ : ℝ-step-premises .proj₁
      _ = 𝕣

      _ : (ℝ n m) ⁇
      _ = ℝ-step-premises .proj₂

  open import Class.Monoid

  -- * The tactic works for multiple *decidable* hypotheses.
  data ℚ {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ : A → A → Set where
    base :
      ────────────────────────────────
      ℚ ε ε

    step : ∀ {n m n′ m′} →
      ∙ ℚ n m
      ∙ ℚ n′ m′
      ────────────────────────────────
      ℚ (n ◇ n′) (m ◇ m′)

  module _ ⦃ _ : ∀ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ → ℚ {A} ⁇² ⦄ where
    unquoteDecl ℚ-base-premises = genPremises ℚ-base-premises (quote ℚ.base)
    unquoteDecl ℚ-step-premises = genPremises ℚ-step-premises (quote ℚ.step)

    _ : ℚ-base-premises .proj₁
    _ = tt

    module _ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ (n m n′ m′ : A) (𝕢ˡ : ℚ n m) (𝕢ʳ : ℚ n′ m′) where
      _ : ℚ-step-premises .proj₁
      _ = 𝕢ˡ , 𝕢ʳ

  -- * The tactic omits *undecidable* hypotheses.
  data ℝ′ : ℕ → ℕ → Set where
    base :
      ────────────────────────────────
      ℝ′ 0 0

    step : ∀ {n m} {T T′ : ℕ → ℕ} →
      ∙ ℝ′ n m
      ∙ T ≡ T′
      ────────────────────────────────
      ℝ′ (suc n) (suc m)

  module _ ⦃ _ : ℝ′ ⁇² ⦄ where
    unquoteDecl ℝ′-base-premises = genPremises ℝ′-base-premises (quote ℝ′.base)
    unquoteDecl ℝ′-step-premises = genPremises ℝ′-step-premises (quote ℝ′.step)

    _ : ℝ′-base-premises .proj₁
    _ = tt

    module _ (n m : ℕ) (𝕣 : ℝ′ n m) where
      _ : ℝ′-step-premises .proj₁
      _ = 𝕣

  -- * The tactic works under module contexts.
  module _ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ ⦃ _ : ℚ {A} ⁇² ⦄ ⦃ _ : ℝ ⁇² ⦄ where

    data 𝕎 : A → ℕ → Set where
      base :
        ────────────────────────────────
        𝕎 ε 0

      step : ∀ {x y n n′} →
        ∙ ℝ n n′
        ∙ ℚ x y
        ∙ 𝕎 (x ◇ y) n
        ────────────────────────────────
        𝕎 (x ◇ y) n′

    unquoteDecl 𝕎-base-premises = genPremises 𝕎-base-premises (quote 𝕎.base)

    _ : 𝕎-base-premises .proj₁
    _ = tt

    unquoteDecl 𝕎-step-premises = genPremises 𝕎-step-premises (quote 𝕎.step)

    module _ (n n′ : ℕ) (x y : A) (𝕣 : ℝ n n′) (𝕢 : ℚ x y) where
      _ : 𝕎-step-premises .proj₁
      _ = 𝕣 , 𝕢

  -- * Irrelevant free variable `z` is not included in the premise type,
  --   since it only appears in the conclusion.
  data 𝕍 {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ : A → A → Set where
    base :
      ────────────────────────────────
      𝕍 ε ε

    step : ∀ {n m n′ m′ z} ⦃ _ : Show A ⦄ →
      ∙ 𝕍 n m
      ∙ 𝕍 n′ m′
      ────────────────────────────────
      𝕍 (n ◇ n′ ◇ m ◇ m′) z

  module _ ⦃ _ : ∀ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ → 𝕍 {A} ⁇² ⦄ where
    unquoteDecl 𝕍-base-premises = genPremises 𝕍-base-premises (quote 𝕍.base)
    unquoteDecl 𝕍-step-premises = genPremises 𝕍-step-premises (quote 𝕍.step)

    _ : 𝕍-base-premises .proj₁
    _ = tt

    module _ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄
             (n m n′ m′ : A) (𝕢ˡ : 𝕍 n m) (𝕢ʳ : 𝕍 n′ m′) where
      _ : 𝕍-step-premises .proj₁
      _ = 𝕢ˡ , 𝕢ʳ

  -- * Irrelevant free variable `T` is not included in the premise type,
  --   since it only appears in an undecidable hypothesis.
  data 𝕍′ {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ : A → A → Set where
    base :
      ────────────────────────────────
      𝕍′ ε ε

    step : ∀ {n m n′ m′} ⦃ _ : Show A ⦄ {T : Type} →
      ∙ 𝕍′ n m
      ∙ 𝕍′ n′ m′
      ∙ (∀ T′ → T ≡ T′)
      ────────────────────────────────
      𝕍′ (n ◇ n′) (m ◇ m′)

  module _ ⦃ _ : ∀ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ → 𝕍′ {A} ⁇² ⦄ where
    unquoteDecl 𝕍′-base-premises = genPremises 𝕍′-base-premises (quote 𝕍′.base)
    unquoteDecl 𝕍′-step-premises = genPremises 𝕍′-step-premises (quote 𝕍′.step)

    _ : 𝕍′-base-premises .proj₁
    _ = tt

    module _ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄
             (n m n′ m′ : A) (𝕢ˡ : 𝕍′ n m) (𝕢ʳ : 𝕍′ n′ m′) where
      _ : 𝕍′-step-premises .proj₁
      _ = 𝕢ˡ , 𝕢ˡ

  -- * Irrelevant instance `⦃ Show A ⦄` is not included in the premise type.
  data ℚ′ {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ : A → A → Set where
    base :
      ────────────────────────────────
      ℚ′ ε ε

    step : ∀ {n m n′ m′} ⦃ _ : Show A ⦄ →
      ∙ ℚ′ n m
      ∙ ℚ′ n′ m′
      ────────────────────────────────
      ℚ′ (n ◇ n′) (m ◇ m′)

  module _ ⦃ _ : ∀ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄ → ℚ′ {A} ⁇² ⦄ where
    unquoteDecl ℚ′-base-premises = genPremises ℚ′-base-premises (quote ℚ′.base)
    unquoteDecl ℚ′-step-premises = genPremises ℚ′-step-premises (quote ℚ′.step)

    _ : ℚ′-base-premises .proj₁
    _ = tt

    module _ {A} ⦃ _ : Semigroup A ⦄ ⦃ _ : Monoid A ⦄
             (n m n′ m′ : A) (𝕢ˡ : ℚ′ n m) (𝕢ʳ : ℚ′ n′ m′) where
      _ : ℚ′-step-premises .proj₁
      _ = 𝕢ˡ , 𝕢ʳ