Define substitutions on core expressions

agda/Core/Syntax.agda

@@ -1,9 +1,11 @@
 module Core.Syntax where
 
+open import Agda.Builtin.Bool
 open import Agda.Builtin.List public
 open import Agda.Builtin.String
-open import Data.Nat.Base public
+open import Data.Bool using (if_then_else_ ; _∨_)
 open import Data.Fin public using (Fin)
+open import Data.Nat.Base public
 open import Data.Product public using (_×_)
 open import Data.Product using (_,_)
 open import Data.Vec.Base
@@ -17,6 +19,11 @@ record Var : Set where
   field
     var : String
 
+open Var
+
+var-eq : Var → Var → Bool
+var-eq x₁ x₂ = primStringEquality (var x₁) (var x₂)
+
 ADTCons : ℕ → Set
 CaseBranches : ℕ → Set
 
@@ -63,7 +70,37 @@ variable
   Γ Γ' Δ : Ctx
   x x' x₁ x₂ y ν ν₁ ν₂ : Var
   τ τ' τ₁ τ₂ τ₁' τ₂' τᵢ τⱼ σ : CExpr
-  ε ε' ε₁ ε₂ ε₁' ε₂' : CExpr
+  ε ε' ε₁ ε₂ ε₃ ε₁' ε₂' ϖ : CExpr
   b b' b₁ b₂ : CExpr
   n : ℕ
-  s : Sort
+  s s₁ s₂ : Sort
+
+
+substCons : Var → CExpr → ADTCons n → ADTCons n
+
+infix 30 [_↦_]_
+[_↦_]_ : Var → CExpr → CExpr → CExpr
+[ x ↦ ε ] CVar var = if var-eq x var then ε else CVar var
+[ x ↦ ε ] CSort s = CSort s
+[ x ↦ ε ] CPi var ε₁ ε₂ = let ε₁' = [ x ↦ ε ] ε₁
+                              ε₂' = if var-eq x var then ε₂ else [ x ↦ ε ] ε₂
+                           in CPi var ε₁' ε₂'
+[ x ↦ ε ] CLam var ε₁ ε₂ = let ε₁' = [ x ↦ ε ] ε₁
+                               ε₂' = if var-eq x var then ε₂ else [ x ↦ ε ] ε₂
+                            in CLam var ε₁' ε₂'
+[ x ↦ ε ] CApp ε₁ ε₂ = CApp ([ x ↦ ε ] ε₁) ([ x ↦ ε ] ε₂)
+[ x ↦ ε ] Cunit = Cunit
+[ x ↦ ε ] CUnit = CUnit
+[ x ↦ ε ] CADT cons = CADT (substCons x ε cons)
+[ x ↦ ε ] CCon idx ε' cons = CCon idx ([ x ↦ ε ] ε') (substCons x ε cons)
+[ x ↦ ε ] CCase ε' branches = CCase ([ x ↦ ε ] ε') (go branches)
+  where
+    go : CaseBranches n → CaseBranches n
+    go [] = []
+    go (b@(MkCaseBranch x' π body) ∷ bs) = let b = if var-eq x x' ∨ var-eq x π
+                                                    then b
+                                                    else MkCaseBranch x' π ([ x ↦ ε ] body)
+                                            in b ∷ go bs
+
+substCons x ε [] = []
+substCons x ε (con ∷ cons) = [ x ↦ ε ] con ∷ substCons x ε cons