DeBruijn.agda

------------------------------------------------------------------------
-- 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