    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Weakening, strengthening and free variable check for reflected terms.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Reflection.AST.DeBruijn where

    open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
    open import Data.Nat.Base using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
    open import Data.List.Base  using (List; []; _∷_; _++_)
    open import Data.Maybe.Base using (Maybe; nothing; just)
    import Data.Maybe.Effectful as Maybe using (applicative)
    import Function.Identity.Effectful as Identity using (applicative)
    open import Effect.Applicative using (RawApplicative; mkRawApplicative)
    open import Reflection
    open import Reflection.AST.Argument.Visibility using (Visibility)
    import Reflection.AST.Traversal as Traverse

    private
      variable A : Set

    ------------------------------------------------------------------------
    -- Weakening

    module _ where

      open Traverse Identity.applicative

      private

        wkVar : ℕ → Cxt → ℕ → ℕ
        wkVar by (from , _) i = if i <ᵇ from then i else i + by

        actions : ℕ → Actions
        actions k = record defaultActions { onVar = wkVar k }

      weakenFrom′ : (Actions → Cxt → A → A) → (from by : ℕ) → A → A
      weakenFrom′ trav from by = trav (actions by) (from , []) -- not using the context part

      weakenFrom : (from by : ℕ) → Term → Term
      weakenFrom = weakenFrom′ traverseTerm

      weaken : (by : ℕ) → Term → Term
      weaken = weakenFrom 0

      weakenArgs : (by : ℕ) → Args Term → Args Term
      weakenArgs = weakenFrom′ traverseArgs 0

      weakenClauses : (by : ℕ) → Clauses → Clauses
      weakenClauses = weakenFrom′ traverseClauses 0

    ------------------------------------------------------------------------
    -- η-expansion

    private
      η : Visibility → (Args Term → Term) → Args Term → Term
      η h f args =
        lam h (abs "x" (f (weakenArgs 1 args ++
                           arg (arg-info h defaultModality) (var 0 []) ∷
                           [])))

    η-expand : Visibility → Term → Term
    η-expand h (var x      args) = η h (var (suc x)) args
    η-expand h (con c      args) = η h (con c) args
    η-expand h (def f      args) = η h (def f) args
    η-expand h (pat-lam cs args) = η h (pat-lam (weakenClauses 1 cs)) args
    η-expand h (meta x     args) = η h (meta x) args
    η-expand h t@(lam _ _)       = t
    η-expand h t@(pi _ _)        = t
    η-expand h t@(agda-sort _)   = t
    η-expand h t@(lit _)         = t
    η-expand h t@unknown         = t

    ------------------------------------------------------------------------
    -- Strengthening

    module _ where

      open Traverse Maybe.applicative

      private
        strVar : ℕ → Cxt → ℕ → Maybe ℕ
        strVar by (from , Γ) i with i <ᵇ from | i <ᵇ from + by
        ... | true | _    = just i
        ... | _    | true = nothing
        ... | _    | _    = just (i ∸ by)

        actions : ℕ → Actions
        actions by = record defaultActions { onVar = strVar by }

      strengthenFromBy′ : (Actions → Cxt → A → Maybe A) → (from by : ℕ) → A → Maybe A
      strengthenFromBy′ trav from by = trav (actions by) (from , []) -- not using the context part

      strengthenFromBy : (from by : ℕ) → Term → Maybe Term
      strengthenFromBy = strengthenFromBy′ traverseTerm

      strengthenBy : (by : ℕ) → Term → Maybe Term
      strengthenBy = strengthenFromBy 0

      strengthenFrom : (from : ℕ) → Term → Maybe Term
      strengthenFrom from = strengthenFromBy from 1

      strengthen : Term → Maybe Term
      strengthen = strengthenFromBy 0 1

    ------------------------------------------------------------------------
    -- Free variable check

    module _ where

      private
        anyApplicative : ∀ {ℓ} → RawApplicative {ℓ} (λ _ → Bool)
        anyApplicative = mkRawApplicative _ (λ _ → false)  _∨_

      open Traverse anyApplicative

      private
        fvVar : ℕ → Cxt → ℕ → Bool
        fvVar i (n , _) x = i + n ≡ᵇ x

        actions : ℕ → Actions
        actions i = record defaultActions { onVar = fvVar i }

      infix 4 _∈FV_

      _∈FV_ : ℕ → Term → Bool
      i ∈FV t = traverseTerm (actions i) (0 , []) t