/usr/share/agda-stdlib/Data/Fin/Substitution.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Substitutions
------------------------------------------------------------------------
-- Uses a variant of Conor McBride's technique from "Type-Preserving
-- Renaming and Substitution".
-- See Data.Fin.Substitution.Example for an example of how this module
-- can be used: a definition of substitution for the untyped
-- λ-calculus.
module Data.Fin.Substitution where
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec
open import Function as Fun using (flip)
open import Data.Star as Star using (Star; ε; _◅_)
------------------------------------------------------------------------
-- General functionality
-- A Sub T m n is a substitution which, when applied to something with
-- at most m variables, yields something with at most n variables.
Sub : (ℕ → Set) → ℕ → ℕ → Set
Sub T m n = Vec (T n) m
-- A /reversed/ sequence of matching substitutions.
Subs : (ℕ → Set) → ℕ → ℕ → Set
Subs T = flip (Star (flip (Sub T)))
-- Some simple substitutions.
record Simple (T : ℕ → Set) : Set where
infix 10 _↑
infixl 10 _↑⋆_ _↑✶_
field
var : ∀ {n} → Fin n → T n -- Takes variables to Ts.
weaken : ∀ {n} → T n → T (suc n) -- Weakens Ts.
-- Lifting.
_↑ : ∀ {m n} → Sub T m n → Sub T (suc m) (suc n)
ρ ↑ = var zero ∷ map weaken ρ
_↑⋆_ : ∀ {m n} → Sub T m n → ∀ k → Sub T (k + m) (k + n)
ρ ↑⋆ zero = ρ
ρ ↑⋆ suc k = (ρ ↑⋆ k) ↑
_↑✶_ : ∀ {m n} → Subs T m n → ∀ k → Subs T (k + m) (k + n)
ρs ↑✶ k = Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) ρs
-- The identity substitution.
id : ∀ {n} → Sub T n n
id {zero} = []
id {suc n} = id ↑
-- Weakening.
wk⋆ : ∀ k {n} → Sub T n (k + n)
wk⋆ zero = id
wk⋆ (suc k) = map weaken (wk⋆ k)
wk : ∀ {n} → Sub T n (suc n)
wk = wk⋆ 1
-- A substitution which only replaces the first variable.
sub : ∀ {n} → T n → Sub T (suc n) n
sub t = t ∷ id
-- Application of substitutions.
record Application (T₁ T₂ : ℕ → Set) : Set where
infixl 8 _/_ _/✶_
infixl 9 _⊙_
-- Post-application of substitutions to things.
field _/_ : ∀ {m n} → T₁ m → Sub T₂ m n → T₁ n
-- Reverse composition. (Fits well with post-application.)
_⊙_ : ∀ {m n k} → Sub T₁ m n → Sub T₂ n k → Sub T₁ m k
ρ₁ ⊙ ρ₂ = map (λ t → t / ρ₂) ρ₁
-- Application of multiple substitutions.
_/✶_ : ∀ {m n} → T₁ m → Subs T₂ m n → T₁ n
_/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero}
-- A combination of the two records above.
record Subst (T : ℕ → Set) : Set where
field
simple : Simple T
application : Application T T
open Simple simple public
open Application application public
-- Composition of multiple substitutions.
⨀ : ∀ {m n} → Subs T m n → Sub T m n
⨀ ε = id
⨀ (ρ ◅ ε) = ρ -- Convenient optimisation; simplifies some proofs.
⨀ (ρ ◅ ρs) = ⨀ ρs ⊙ ρ
------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations
-- Liftings from T₁ to T₂.
record Lift (T₁ T₂ : ℕ → Set) : Set where
field
simple : Simple T₁
lift : ∀ {n} → T₁ n → T₂ n
open Simple simple public
-- Variable substitutions (renamings).
module VarSubst where
subst : Subst Fin
subst = record
{ simple = record { var = Fun.id; weaken = suc }
; application = record { _/_ = lookup }
}
open Subst subst public
-- "Term" substitutions.
record TermSubst (T : ℕ → Set) : Set₁ where
field
var : ∀ {n} → Fin n → T n
app : ∀ {T′} → Lift T′ T → ∀ {m n} → T m → Sub T′ m n → T n
module Lifted {T′} (lift : Lift T′ T) where
application : Application T T′
application = record { _/_ = app lift }
open Lift lift public
open Application application public
varLift : Lift Fin T
varLift = record { simple = VarSubst.simple; lift = var }
infix 8 _/Var_
_/Var_ : ∀ {m n} → T m → Sub Fin m n → T n
_/Var_ = app varLift
simple : Simple T
simple = record
{ var = var
; weaken = λ t → t /Var VarSubst.wk
}
termLift : Lift T T
termLift = record { simple = simple; lift = Fun.id }
subst : Subst T
subst = record
{ simple = simple
; application = Lifted.application termLift
}
open Subst subst public hiding (var; simple)
|