def MLIR.UnTyped.Substitution : Type

Equations

• MLIR.UnTyped.Substitution = List (MLIR.VarName × MLIR.VarName)

def MLIR.UnTyped.Substitution.removeMappingFor (σ : MLIR.UnTyped.Substitution) (v : MLIR.VarName) : MLIR.UnTyped.Substitution

Remove all substitutions of variable v (i.e., where v is the variable being replaced) from the substitution σ

Equations

• σ.removeMappingFor v = List.filter (fun (x : MLIR.VarName × MLIR.VarName) => x.fst != v) σ

def MLIR.UnTyped.Substitution.apply (σ : MLIR.UnTyped.Substitution) (v : MLIR.VarName) : MLIR.VarName

Apply a substution σ to a variable v, returning the v unchanged if the σ does not define a mapping for v

Equations

• σ.apply v = match List.lookup v σ with | some w => w | none => v

class MLIR.UnTyped.SubstituteableTerminator (T : Type u) : Type u

• substituteTerminator : (MLIR.VarName → MLIR.VarName) → T → T

def MLIR.UnTyped.Expr.substitute {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : MLIR.UnTyped.Expr Op T → MLIR.UnTyped.Expr Op T

Equations

• One or more equations did not get rendered due to their size.

def MLIR.UnTyped.Expr.substitute.subRegions {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ' : MLIR.UnTyped.Substitution) : List (MLIR.UnTyped.Region Op T) → List (MLIR.UnTyped.Region Op T)

Equations

• MLIR.UnTyped.Expr.substitute.subRegions σ' [] = []
• MLIR.UnTyped.Expr.substitute.subRegions σ' (r :: rs) = MLIR.UnTyped.Region.substitute σ' r :: MLIR.UnTyped.Expr.substitute.subRegions σ' rs

def MLIR.UnTyped.Lets.substitute {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : MLIR.UnTyped.Lets Op T → MLIR.UnTyped.Lets Op T

Equations

• MLIR.UnTyped.Lets.substitute σ (MLIR.UnTyped.Lets.mk ls) = MLIR.UnTyped.Lets.mk (MLIR.UnTyped.Lets.substitute.go σ ls)

def MLIR.UnTyped.Lets.substitute.go {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : List (MLIR.UnTyped.Expr Op T) → List (MLIR.UnTyped.Expr Op T)

Equations

• MLIR.UnTyped.Lets.substitute.go σ [] = []
• MLIR.UnTyped.Lets.substitute.go σ (l :: ls) = MLIR.UnTyped.Expr.substitute σ l :: MLIR.UnTyped.Lets.substitute.go σ ls

def MLIR.UnTyped.Body.substitute {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : MLIR.UnTyped.Body Op T → MLIR.UnTyped.Body Op T

Equations

• One or more equations did not get rendered due to their size.

def MLIR.UnTyped.BasicBlock.substitute {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : MLIR.UnTyped.BasicBlock Op T → MLIR.UnTyped.BasicBlock Op T

Equations

• One or more equations did not get rendered due to their size.

def MLIR.UnTyped.Region.substitute {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : MLIR.UnTyped.Region Op T → MLIR.UnTyped.Region Op T

Equations

• MLIR.UnTyped.Region.substitute σ (MLIR.UnTyped.Region.mk entry blocks) = MLIR.UnTyped.Region.mk entry (MLIR.UnTyped.Region.substitute.subBlocks σ blocks)

def MLIR.UnTyped.Region.substitute.subBlocks {Op : Type} {T : Type} [MLIR.UnTyped.SubstituteableTerminator T] (σ : MLIR.UnTyped.Substitution) : List (MLIR.UnTyped.BasicBlock Op T) → List (MLIR.UnTyped.BasicBlock Op T)

Equations

• MLIR.UnTyped.Region.substitute.subBlocks σ [] = []
• MLIR.UnTyped.Region.substitute.subBlocks σ (b :: bs) = MLIR.UnTyped.BasicBlock.substitute σ b :: MLIR.UnTyped.Region.substitute.subBlocks σ bs