Skip to content

Commit

Permalink
Reduction rewrite
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Jun 27, 2024
1 parent 54d38f3 commit a991488
Show file tree
Hide file tree
Showing 5 changed files with 119 additions and 47 deletions.
8 changes: 4 additions & 4 deletions DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,8 +181,8 @@ def WfD.CongD.right {P : Ctx α ε → LCtx α → Region φ → Region φ → S

inductive TStepD : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Type _
-- TODO: do we need to require r.WfD for rw?
| step {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r r' → TStepD Γ L r r'
| step_op {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r' r → TStepD Γ L r r'
| step {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → FStepD Γ.effect r r' → TStepD Γ L r r'
| step_op {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → FStepD Γ.effect r' r → TStepD Γ L r r'
| initial {Γ L} : Γ.IsInitial → r.WfD Γ L → r'.WfD Γ L → TStepD Γ L r r'
| terminal {Γ L} : e.WfD Γ ⟨Ty.unit, ⊥⟩ → e'.WfD Γ ⟨Ty.unit, ⊥⟩ → r.WfD (⟨Ty.unit, ⊥⟩::Γ) L
→ TStepD Γ L (let1 e r) (let1 e' r)
Expand All @@ -194,8 +194,8 @@ def TStepD.symm {Γ L} {r r' : Region φ} : TStepD Γ L r r' → TStepD Γ L r'
| terminal e e' d => terminal e' e d

inductive TStep : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Prop
| step {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r r' → TStep Γ L r r'
| step_op {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r' r → TStep Γ L r r'
| step {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → FStep Γ.effect r r' → TStep Γ L r r'
| step_op {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → FStep Γ.effect r' r → TStep Γ L r r'
| initial {Γ L} : Γ.IsInitial → r.Wf Γ L → r'.Wf Γ L → TStep Γ L r r'
| terminal {Γ L} : e.Wf Γ ⟨Ty.unit, ⊥⟩ → e'.Wf Γ ⟨Ty.unit, ⊥⟩ → r.Wf (⟨Ty.unit, ⊥⟩::Γ) L
→ TStep Γ L (let1 e r) (let1 e' r)
Expand Down
4 changes: 2 additions & 2 deletions DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,8 +247,8 @@ def RewriteD.lsubst_alpha {r₀ r₀'}
exact hρ
rw [Subst.vlift_liftn_comm]
rfl
| let2_eta r => by
apply cast_src _ (let2_eta _)
| let2_eta e r => by
apply cast_src _ (let2_eta _ _)
simp only [lsubst]
congr
simp only [vlift_alpha, vwk_vwk, vliftn_alpha, <-Nat.liftWk_comp, vwk1_lsubst_alpha]
Expand Down
51 changes: 51 additions & 0 deletions DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,33 @@ theorem Term.wk_comp (ρ σ)

def Term.wk1 : Term φ → Term φ := wk (Nat.liftWk Nat.succ)

theorem Term.wk_wk1 (r : Term φ) : r.wk1.wk ρ = r.wk (ρ ∘ Nat.liftWk Nat.succ)
:= by simp only [wk1, wk_wk, <-Nat.liftWk_comp]

theorem Term.wk_liftWk₂_wk1_to_wk (r : Term φ)
: r.wk1.wk (Nat.liftWk (Nat.liftWk ρ)) = r.wk (Nat.liftWk (Nat.succ ∘ ρ))
:= by rw [wk_wk1, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]

theorem Term.wk_liftWk₂_wk1 (r : Term φ)
: r.wk1.wk (Nat.liftWk (Nat.liftWk ρ)) = (r.wk (Nat.liftWk ρ)).wk1
:= by rw [wk_liftWk₂_wk1_to_wk, wk1, wk_wk, Nat.liftWk_comp]

theorem Term.wk_liftnWk₂_wk1 (r : Term φ)
: r.wk1.wk (Nat.liftnWk 2 ρ) = (r.wk (Nat.liftWk ρ)).wk1
:= by rw [Nat.liftnWk_two, <-wk_liftWk₂_wk1]; rfl

theorem Term.wk1_wk_liftWk (r : Term φ)
: (r.wk (Nat.liftWk ρ)).wk1 = r.wk1.wk (Nat.liftnWk 2 ρ)
:= r.wk_liftnWk₂_wk1.symm

theorem Term.wk_liftWk_wk_succ (r : Term φ)
: (r.wk Nat.succ).wk (Nat.liftWk ρ) = (r.wk ρ).wk Nat.succ
:= by simp only [wk_wk, Nat.liftWk_comp_succ]

theorem Term.wk_liftnWk_wk_add (r : Term φ) (n : ℕ)
: (r.wk (· + n)).wk (Nat.liftnWk n ρ) = (r.wk ρ).wk (· + n)
:= by simp only [wk_wk, Nat.liftnWk_comp_add]

def Term.wkn (n : ℕ) : Term φ → Term φ := wk (Nat.liftWk (· + n))

theorem Body.wk_id (b : Body φ) : b.wk id = b := by induction b <;> simp [*]
Expand Down Expand Up @@ -663,6 +690,30 @@ theorem Region.vwk_comp (ρ σ)

def Region.vwk1 : Region φ → Region φ := vwk (Nat.liftWk Nat.succ)

theorem Region.vwk_vwk1 (r : Region φ) : r.vwk1.vwk ρ = r.vwk (ρ ∘ Nat.liftWk Nat.succ)
:= by simp only [vwk1, vwk_vwk, <-Nat.liftWk_comp]

theorem Region.vwk_liftWk₂_vwk1_to_vwk (r : Region φ)
: r.vwk1.vwk (Nat.liftWk (Nat.liftWk ρ)) = r.vwk (Nat.liftWk (Nat.succ ∘ ρ))
:= by rw [vwk_vwk1, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]

theorem Region.vwk_liftWk₂_vwk1 (r : Region φ)
: r.vwk1.vwk (Nat.liftWk (Nat.liftWk ρ)) = (r.vwk (Nat.liftWk ρ)).vwk1
:= by rw [vwk_liftWk₂_vwk1_to_vwk, vwk1, vwk_vwk, Nat.liftWk_comp]

theorem Region.vwk_liftnWk₂_vwk1 (r : Region φ)
: r.vwk1.vwk (Nat.liftnWk 2 ρ) = (r.vwk (Nat.liftWk ρ)).vwk1
:= by rw [Nat.liftnWk_two, <-vwk_liftWk₂_vwk1]; rfl

theorem Region.vwk1_vwk_liftWk (r : Region φ)
: (r.vwk (Nat.liftWk ρ)).vwk1 = r.vwk1.vwk (Nat.liftnWk 2 ρ)
:= r.vwk_liftnWk₂_vwk1.symm

theorem Region.vwk_liftnWk₂_liftWk_vwk2 (r : Region φ)
: (r.vwk (Nat.liftnWk 2 Nat.succ)).vwk (Nat.liftnWk 2 (Nat.liftWk ρ))
= (r.vwk (Nat.liftnWk 2 ρ)).vwk (Nat.liftnWk 2 Nat.succ)
:= by simp only [vwk_vwk, <-Nat.liftnWk_comp, Nat.liftWk_comp_succ]

def Region.vwkn (n : ℕ) : Region φ → Region φ := vwk (Nat.liftWk (· + n))

theorem Region.lwk_id (r : Region φ) : r.lwk id = r := by induction r <;> simp [*]
Expand Down
95 changes: 58 additions & 37 deletions DeBruijnSSA/BinSyntax/Syntax/Rewrite/Definitions.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,22 +281,20 @@ inductive RewriteD : Region φ → Region φ → Type _
| cfg_let1 (a β n G) :
RewriteD (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G))
| cfg_let2 (a β n G) :
RewriteD (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
RewriteD (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
| cfg_case (e r s n G) :
RewriteD (cfg (case e r s) n G)
(case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
(case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
| cfg_cfg (β n G n' G') :
RewriteD (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
| cfg_zero (β G) : RewriteD (cfg β 0 G) β
| cfg_fuse (β n G k) (ρ : Fin k → Fin n) (hρ : Function.Surjective ρ) :
RewriteD
(cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
(cfg β k (G ∘ ρ))
| let2_eta (r : Region φ) :
RewriteD (let2 (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
(let1 (Term.var 0) r)
-- | let1_eta r :
-- RewriteD (let1 (Term.var 0) r.vwk1) r
| let2_eta (e) (r : Region φ) :
RewriteD (let2 e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
(let1 e r)

def RewriteD.cast_src {r₀ r₀' r₁ : Region φ} (h : r₀ = r₀') (p : RewriteD r₀ r₁)
: RewriteD r₀' r₁ := h ▸ p
Expand Down Expand Up @@ -365,9 +363,7 @@ theorem RewriteD.effect {Γ : ℕ → ε} {r r' : Region φ} (p : RewriteD r r')
apply congrArg
apply congrArg
funext i
rw [
Nat.liftnBot_two_apply, <-Nat.liftnBot_two_apply, Function.comp_apply, effect_liftnBot_vwk_add
]
simp [Nat.liftnBot_two]
| cfg_case => simp [sup_assoc]
| cfg_cfg =>
simp only [effect_cfg, sup_assoc]
Expand Down Expand Up @@ -428,20 +424,20 @@ inductive Rewrite : Region φ → Region φ → Prop
| cfg_let1 (a β n G) :
Rewrite (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G))
| cfg_let2 (a β n G) :
Rewrite (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
Rewrite (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
| cfg_case (e r s n G) :
Rewrite (cfg (case e r s) n G)
(case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
(case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
| cfg_cfg (β n G n' G') :
Rewrite (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
| cfg_zero (β G) : Rewrite (cfg β 0 G) β
| cfg_fuse (β n G k) (ρ : Fin k → Fin n) (hρ : Function.Surjective ρ) :
Rewrite
(cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
(cfg β k (G ∘ ρ))
| let2_eta (r : Region φ) :
Rewrite (let2 (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
(let1 (Term.var 0) r)
| let2_eta (e) (r : Region φ) :
Rewrite (let2 e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
(let1 e r)

theorem RewriteD.rewrite {r r' : Region φ} (p : RewriteD r r') : Rewrite r r'
:= by cases p <;> constructor; assumption
Expand Down Expand Up @@ -543,12 +539,12 @@ theorem eqv_cfg_let1 {a β n G}
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_let1 a β n G

theorem eqv_cfg_let2 {a β n G}
: @cfg φ (let2 a β) n G ≈ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
: @cfg φ (let2 a β) n G ≈ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_let2 a β n G

theorem eqv_cfg_case {e r s n G}
: @cfg φ (case e r s) n G
≈ case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
≈ case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_case e r s n G

theorem eqv_cfg_cfg {β n G n' G'}
Expand All @@ -560,10 +556,35 @@ theorem eqv_cfg_fuse {β n G k} (ρ : Fin k → Fin n) (hρ : Function.Surjectiv
≈ cfg β k (G ∘ ρ)
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_fuse β n G k ρ hρ

theorem eqv_let2_eta {r : Region φ}
: @let2 φ (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1)
≈ let1 (Term.var 0) r
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.let2_eta r
theorem eqv_let2_eta {e} {r : Region φ}
: @let2 φ e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1)
≈ let1 e r
:= EqvGen.rel _ _ $ Cong.rel $ Rewrite.let2_eta e r

def RewriteD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.vwk ρ) (r'.vwk ρ)
:= by cases d with
| let2_pair a b r =>
simp only [
Region.vwk, wk, Nat.liftWk, vwk_liftWk₂_vwk1, wk_liftWk_wk_succ, Nat.liftnWk_two]
constructor
| cfg_cfg β n G n' G' =>
simp only [Region.vwk, wk, Fin.comp_addCases_apply]
rw [<-Function.comp.assoc, Region.vwk_comp_lwk, Function.comp.assoc]
constructor
| cfg_fuse β n G k σ hσ =>
simp only [Region.vwk, Region.vwk_lwk, Function.comp_apply]
constructor
assumption
| let2_eta e r =>
simp only [Region.vwk, wk, Nat.liftnWk, Nat.lt_succ_self, ↓reduceIte, Nat.zero_lt_succ,
Nat.liftWk_comm_liftnWk_apply, vwk_liftnWk₂_vwk1, vwk_liftWk₂_vwk1]
constructor
| _ =>
simp only [
Region.vwk, wk, Nat.liftWk,
vwk_liftWk₂_vwk1, wk_liftWk_wk_succ, vwk_liftnWk₂_liftWk_vwk2, vwk_liftnWk₂_vwk1,
wk_liftnWk_wk_add, Nat.liftWk_comm_liftnWk_apply, Function.comp_apply]
constructor

inductive ReduceD : Region φ → Region φ → Type _
| case_inl (e r s) : ReduceD (case (inl e) r s) (let1 e r)
Expand Down Expand Up @@ -818,25 +839,25 @@ def StepD.cfg_let1_op {Γ : ℕ → ε} (a : Term φ) (β n G)

@[match_pattern]
def StepD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G)
: StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
: StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
:= StepD.rw $ RewriteD.cfg_let2 a β n G

@[match_pattern]
def StepD.cfg_let2_op {Γ : ℕ → ε} (a : Term φ) (β n G)
: StepD Γ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
: StepD Γ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
(cfg (let2 a β) n G)
:= StepD.rw_op $ RewriteD.cfg_let2 a β n G

@[match_pattern]
def StepD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G)
: StepD Γ (cfg (case e r s) n G)
(case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
(case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
)
:= StepD.rw $ RewriteD.cfg_case e r s n G

@[match_pattern]
def StepD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
: StepD Γ (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
: StepD Γ (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
(cfg (case e r s) n G)
:= StepD.rw_op $ RewriteD.cfg_case e r s n G

Expand All @@ -860,14 +881,14 @@ def StepD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
: StepD Γ β (cfg β 0 G) := StepD.rw_op $ RewriteD.cfg_zero β G

@[match_pattern]
def StepD.let2_eta {Γ : ℕ → ε} (r : Region φ)
: StepD Γ (let2 (var 0) (let1 ((var 1).pair (var 0)) r.vwk1.vwk1)) (let1 (var 0) r)
:= StepD.rw $ RewriteD.let2_eta r
def StepD.let2_eta {Γ : ℕ → ε} (e) (r : Region φ)
: StepD Γ (let2 e (let1 ((var 1).pair (var 0)) r.vwk1.vwk1)) (let1 e r)
:= StepD.rw $ RewriteD.let2_eta e r

@[match_pattern]
def StepD.let2_eta_op {Γ : ℕ → ε} (r : Region φ)
: StepD Γ (let1 (var 0) r) (let2 (var 0) (let1 ((var 1).pair (var 0)) r.vwk1.vwk1))
:= StepD.rw_op $ RewriteD.let2_eta r
: StepD Γ (let1 e r) (let2 e (let1 ((var 1).pair (var 0)) r.vwk1.vwk1))
:= StepD.rw_op $ RewriteD.let2_eta e r

-- @[match_pattern]
-- def StepD.let1_eta {Γ : ℕ → ε} (r : Region φ)
Expand Down Expand Up @@ -1115,22 +1136,22 @@ def RWD.cfg_let1_op {Γ : ℕ → ε} (a : Term φ) (β n G)
:= single $ BCongD.rel $ StepD.cfg_let1_op a β n G

def RWD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G)
: RWD StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
: RWD StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
:= single $ BCongD.rel $ StepD.cfg_let2 a β n G

def RWD.cfg_let2_op {Γ : ℕ → ε} (a : Term φ) (β n G)
: RWD StepD Γ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
: RWD StepD Γ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
(cfg (let2 a β) n G)
:= single $ BCongD.rel $ StepD.cfg_let2_op a β n G

def RWD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G)
: RWD StepD Γ (cfg (case e r s) n G)
(case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
(case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
)
:= single $ BCongD.rel $ StepD.cfg_case e r s n G

def RWD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
: RWD StepD Γ (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
: RWD StepD Γ (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
(cfg (case e r s) n G)
:= single $ BCongD.rel $ StepD.cfg_case_op e r s n G

Expand Down Expand Up @@ -1218,10 +1239,10 @@ def RWD.let1V0_id {Γ : ℕ → ε} (r : Region φ) (hΓ : Γ 0 = ⊥)

def RWD.let2_eta {Γ : ℕ → ε} (r : Region φ)
: RWD StepD Γ
(let2 (Term.var 0) $
(let2 e $
let1 ((Term.var 1).pair (Term.var 0)) $
r.vwk1.vwk1) (let1 (Term.var 0) r)
:= single $ BCongD.rel $ StepD.let2_eta r
r.vwk1.vwk1) (let1 e r)
:= single $ BCongD.rel $ StepD.let2_eta e r

def RWD.let2_eta_op {Γ : ℕ → ε} (r : Region φ)
: RWD StepD Γ (let1 (Term.var 0) r)
Expand Down
8 changes: 4 additions & 4 deletions lake-manifest.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
"rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -22,7 +22,7 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
"rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand Down Expand Up @@ -58,7 +58,7 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "97a63f4b46b5d410cc6b973bf51519d33110dd9c",
"rev": "e446b83b26b1782b8b43647db9f99595678e09b4",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
Expand All @@ -67,7 +67,7 @@
{"url": "https://github.com/imbrem/discretion.git",
"type": "git",
"subDir": null,
"rev": "fd860c182549cd06c1944d483dcd519fe6f1c53d",
"rev": "c69652d9f40f94ee481926e0582359b0b0116968",
"name": "discretion",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down

0 comments on commit a991488

Please sign in to comment.