Generic traversals of reflected terms (#1294)

Using it to implement weakening, strengthening and free variable check.

Author: UlfNorell

CHANGELOG.md

@@ -21,6 +21,10 @@ Deprecated names
 New modules
 -----------
 
+* Added `Reflection.Traversal` for generic de Bruijn-aware traversals of reflected terms.
+* Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
+  on reflected terms.
+
 Other major changes
 -------------------
 

src/Reflection/DeBruijn.agda

@@ -0,0 +1,124 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Weakening, strengthening and free variable check for reflected terms.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Reflection.DeBruijn where
+
+open import Data.Bool using (Bool; true; false; _∨_; if_then_else_)
+open import Data.Nat as Nat using (ℕ; zero; suc; _+_; _<ᵇ_; _≡ᵇ_)
+open import Data.List using (List; []; _∷_; _++_)
+open import Data.Maybe using (Maybe; nothing; just)
+import Data.Maybe.Categorical as Maybe
+import Function.Identity.Categorical as Identity
+open import Category.Applicative using (RawApplicative)
+
+open import Reflection
+open import Reflection.Argument.Visibility using (Visibility)
+import Reflection.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 relevant) (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 (k , Γ) i with Nat.compare i k
+    ... | Nat.less _ _    = just i
+    ... | Nat.equal _     = nothing
+    ... | Nat.greater _ _ = just (Nat.pred i)
+
+    actions : Actions
+    actions = record defaultActions { onVar = strVar }
+
+  strengthenFrom′ : (Actions → Cxt → A → Maybe A) → (from : ℕ) → A → Maybe A
+  strengthenFrom′ trav from = trav actions (from , []) -- not using the context part
+
+  strengthenFrom : (from : ℕ) → Term → Maybe Term
+  strengthenFrom = strengthenFrom′ traverseTerm
+
+  strengthen : Term → Maybe Term
+  strengthen = strengthenFrom 0
+
+
+------------------------------------------------------------------------
+-- Free variable check
+
+module _ where
+
+  private
+    anyApplicative : RawApplicative (λ _ → Bool)
+    anyApplicative .RawApplicative.pure _ = false
+    anyApplicative .RawApplicative._⊛_    = _∨_
+
+  open Traverse anyApplicative
+
+  private
+    fvVar : ℕ → Cxt → ℕ → Bool
+    fvVar i (n , _) x = i + n ≡ᵇ x
+
+    actions : ℕ → Actions
+    actions i = record defaultActions { onVar = fvVar i }
+
+  _∈FV_ : ℕ → Term → Bool
+  i ∈FV t = traverseTerm (actions i) (0 , []) t

src/Reflection/Traversal.agda

@@ -0,0 +1,112 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- de Bruijn-aware generic traversal of reflected terms.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Category.Applicative using (RawApplicative)
+
+module Reflection.Traversal {F : Set → Set} (AppF : RawApplicative F) where
+
+open import Data.Nat     using (ℕ; zero; suc; _+_)
+open import Data.List    using (List; []; _∷_; _++_; reverse; length)
+open import Data.Product using (_×_; _,_)
+open import Data.String  using (String)
+open import Function     using (_∘_)
+open import Reflection
+
+open RawApplicative AppF
+
+------------------------------------------------------------------------
+-- Context representation
+
+-- Track both number of variables and actual context, to avoid having to
+-- compute the length of the context everytime it's needed.
+record Cxt : Set where
+  constructor _,_
+  field
+    len     : ℕ
+    context : List (String × Arg Term)
+
+private
+  _∷cxt_ : String × Arg Term → Cxt → Cxt
+  e ∷cxt (n , Γ) = (suc n , e ∷ Γ)
+
+  _++cxt_ : List (String × Arg Term) → Cxt → Cxt
+  es ++cxt (n , Γ) = (length es + n , es ++ Γ)
+
+------------------------------------------------------------------------
+-- Actions
+
+Action : Set → Set
+Action A = Cxt → A → F A
+
+-- A traversal gets to operate on variables, metas, and names.
+record Actions : Set where
+  field
+    onVar  : Action ℕ
+    onMeta : Action Meta
+    onCon  : Action Name
+    onDef  : Action Name
+
+-- Default action: do nothing.
+defaultActions : Actions
+defaultActions .Actions.onVar  _ = pure
+defaultActions .Actions.onMeta _ = pure
+defaultActions .Actions.onCon  _ = pure
+defaultActions .Actions.onDef  _ = pure
+
+------------------------------------------------------------------------
+-- Traversal functions
+
+module _ (actions : Actions) where
+
+  open Actions actions
+
+  private
+    patternTelescope : Args Pattern → List (String × Arg Term)
+    patternTelescope []       = []
+    patternTelescope (arg i (Pattern.var s)     ∷ ps) = (s , arg i unknown) ∷ patternTelescope ps
+    patternTelescope (arg _ (Pattern.con c ps₁) ∷ ps) = patternTelescope ps₁ ++ patternTelescope ps
+    patternTelescope (arg i Pattern.dot         ∷ ps) = patternTelescope ps
+    patternTelescope (arg i (Pattern.lit l)     ∷ ps) = patternTelescope ps
+    patternTelescope (arg i (Pattern.proj f)    ∷ ps) = patternTelescope ps
+    patternTelescope (arg i Pattern.absurd      ∷ ps) = patternTelescope ps
+
+  traverseTerm    : Action Term
+  traverseSort    : Action Sort
+  traverseArgs    : Action (List (Arg Term))
+  traverseArg     : Action (Arg Term)
+  traverseAbs     : Arg Term → Action (Abs Term)
+  traverseClauses : Action Clauses
+  traverseClause  : Action Clause
+
+  traverseTerm Γ (var x args)      = var       <$> onVar Γ x ⊛ traverseArgs Γ args
+  traverseTerm Γ (con c args)      = con       <$> onCon Γ c ⊛ traverseArgs Γ args
+  traverseTerm Γ (def f args)      = def       <$> onDef Γ f ⊛ traverseArgs Γ args
+  traverseTerm Γ (lam v t)         = lam v     <$> traverseAbs (arg (arg-info v relevant) unknown) Γ t
+  traverseTerm Γ (pat-lam cs args) = pat-lam   <$> traverseClauses Γ cs ⊛ traverseArgs Γ args
+  traverseTerm Γ (pi a b)          = pi        <$> traverseArg Γ a ⊛ traverseAbs a Γ b
+  traverseTerm Γ (agda-sort s)     = agda-sort <$> traverseSort Γ s
+  traverseTerm Γ (meta x args)     = meta      <$> onMeta Γ x ⊛ traverseArgs Γ args
+  traverseTerm Γ t@(lit _)         = pure t
+  traverseTerm Γ t@unknown         = pure t
+
+  traverseArg Γ (arg i t) = arg i <$> traverseTerm Γ t
+  traverseArgs Γ []       = pure []
+  traverseArgs Γ (a ∷ as) = _∷_ <$> traverseArg Γ a ⊛ traverseArgs Γ as
+
+  traverseAbs ty Γ (abs x t) = abs x <$> traverseTerm ((x , ty) ∷cxt Γ) t
+
+  traverseClauses Γ []       = pure []
+  traverseClauses Γ (c ∷ cs) = _∷_ <$> traverseClause Γ c ⊛ traverseClauses Γ cs
+
+  traverseClause Γ (Clause.clause ps t) =
+    Clause.clause ps <$> traverseTerm (patternTelescope ps ++cxt Γ) t
+  traverseClause Γ c@(Clause.absurd-clause ps) = pure c
+
+  traverseSort Γ (Sort.set t)   = Sort.set <$> traverseTerm Γ t
+  traverseSort Γ t@(Sort.lit _) = pure t
+  traverseSort Γ [email protected] = pure t