Simple Intrinsically WellTyped MLIR programs

This module sets up a simple typesystem for MLIR programs, where the only terminator is "return a value".

In particular:

• This means there is no unstructured control flow (no jumping between basic blocks)
• The type system assumes all variable are defined prior to usage (i.e., no graph regions)
• We don't model dominance, only "closed from above" regions
• The type system is structural
• We define a concrete type for the context

We use VarName as the type of terminators, so that each terminator gives us exactly the variable we should return.

structure MLIR.SimplyTyped.RegionType (Ty : Type) : Type

The type of a region specifies the number and types of arguments to its entry block and the region return type

• arguments : List Ty
• returnType : Ty

structure MLIR.SimplyTyped.Signature (Ty : Type) : Type

The signature of a specific operation specifies:

• The number and types of its arguments,
• The number and types of its regions, and
• The type of it's return value

• arguments : List Ty
• regions : List (MLIR.SimplyTyped.RegionType Ty)
• returnType : Ty

class MLIR.SimplyTyped.OpSignature (Op : Type) (Ty : outParam Type) : Type

To implement OpSignature for a type of Operations, we specify the signature of each operation op : Op

• signature : Op → MLIR.SimplyTyped.Signature Ty

def MLIR.SimplyTyped.Lets.outContext {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (lets : MLIR.UnTyped.Lets Op MLIR.VarName) (Γ_in : MLIR.SimplyTyped.Context Ty) : MLIR.SimplyTyped.Context Ty

For each expression e in lets, add e.varName, (signature e).returnType to the context

Equations

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

@[simp]

theorem MLIR.SimplyTyped.Lets.outContext_cons {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {e : MLIR.UnTyped.Expr Op MLIR.VarName} (lets : List (MLIR.UnTyped.Expr Op MLIR.VarName)) (Γ_in : MLIR.SimplyTyped.Context Ty) : MLIR.SimplyTyped.Lets.outContext (MLIR.UnTyped.Lets.mk (e :: lets)) Γ_in = MLIR.SimplyTyped.Lets.outContext (MLIR.UnTyped.Lets.mk lets) (Γ_in.push e.varName (MLIR.SimplyTyped.OpSignature.signature e.op).returnType)

WellTyped

We define what it means for an untyped program to be well-formed under a specific context

@[irreducible]

def MLIR.SimplyTyped.Expr.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ : MLIR.SimplyTyped.Context Ty) : MLIR.UnTyped.Expr Op MLIR.VarName → Ty → Prop

Equations

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

@[irreducible]

def MLIR.SimplyTyped.Lets.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ_in : MLIR.SimplyTyped.Context Ty) : MLIR.UnTyped.Lets Op MLIR.VarName → MLIR.SimplyTyped.Context Ty → Prop

Equations

• One or more equations did not get rendered due to their size.
• MLIR.SimplyTyped.Lets.WellTyped Γ_in (MLIR.UnTyped.Lets.mk []) x = (x = Γ_in)

@[irreducible]

def MLIR.SimplyTyped.Body.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (Γ : MLIR.SimplyTyped.Context Ty) : MLIR.UnTyped.Body Op MLIR.VarName → Ty → Prop

Equations

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

@[irreducible]

def MLIR.SimplyTyped.BasicBlock.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] : MLIR.UnTyped.BasicBlock Op MLIR.VarName → MLIR.SimplyTyped.RegionType Ty → Prop

Equations

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

@[irreducible]

def MLIR.SimplyTyped.Region.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] : MLIR.UnTyped.Region Op MLIR.VarName → MLIR.SimplyTyped.RegionType Ty → Prop

Note that because we don't have branches between basic block, only the entry block to a region actually matters. Any other blocks, if specified, are unreachable and may be ignored. Also, regions are closed from above, so the well-formedness of a region does not depend on the context of the outer region

Equations

• MLIR.SimplyTyped.Region.WellTyped (MLIR.UnTyped.Region.mk entry blocks) = MLIR.SimplyTyped.BasicBlock.WellTyped entry

@[irreducible]

def MLIR.SimplyTyped.RegionList.WellTyped {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] : List (MLIR.UnTyped.Region Op MLIR.VarName) → List (MLIR.SimplyTyped.RegionType Ty) → Prop

RegionList.WellTyped regions regionTypes holds when regions and regionTypes are of the same length, and each region in the first list is welltyped according to the corresponing type of the second list. Morally, this can be expressed as regions.length = rgnTys.length ∧ ∀ r ∈ regions.zip rgnTys, Region.WellTyped r.fst r.snd However, we inline the definition to make the termination checker happy

Equations

• MLIR.SimplyTyped.RegionList.WellTyped [] [] = True
• MLIR.SimplyTyped.RegionList.WellTyped (r :: rgns) (rTy :: rgnTys) = (MLIR.SimplyTyped.Region.WellTyped r rTy ∧ MLIR.SimplyTyped.RegionList.WellTyped rgns rgnTys)
• MLIR.SimplyTyped.RegionList.WellTyped x✝ x = False

Theorems

theorem MLIR.SimplyTyped.Expr.WellTyped.exists_iff {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {e : MLIR.UnTyped.Expr Op MLIR.VarName} {Γ : MLIR.SimplyTyped.Context Ty} : (∃ (ty : Ty), MLIR.SimplyTyped.Expr.WellTyped Γ e ty) ↔ MLIR.SimplyTyped.Expr.WellTyped Γ e (MLIR.SimplyTyped.OpSignature.signature e.op).returnType

theorem MLIR.SimplyTyped.Lets.WellTyped.exists_iff {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {lets : MLIR.UnTyped.Lets Op MLIR.VarName} {Γ_in : MLIR.SimplyTyped.Context Ty} : (∃ (Γ_out : MLIR.SimplyTyped.Context Ty), MLIR.SimplyTyped.Lets.WellTyped Γ_in lets Γ_out) ↔ MLIR.SimplyTyped.Lets.WellTyped Γ_in lets (MLIR.SimplyTyped.Lets.outContext lets Γ_in)

There exists an output context for which a Lets is well-typed iff it is well-typed for Lets.outContext lets _. This justifies the choice of this particular context in Body.WellTyped

@[simp]

theorem MLIR.SimplyTyped.RegionList.WellTyped.iff {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] (regions : List (MLIR.UnTyped.Region Op MLIR.VarName)) (regionTypes : List (MLIR.SimplyTyped.RegionType Ty)) : MLIR.SimplyTyped.RegionList.WellTyped regions regionTypes ↔ regions.length = regionTypes.length ∧ ∀ (r : MLIR.UnTyped.Region Op MLIR.VarName × MLIR.SimplyTyped.RegionType Ty), r ∈ regions.zip regionTypes → MLIR.SimplyTyped.Region.WellTyped r.fst r.snd

Justify the RegionList.WellTyped definition

Congr

Show that well-typedness is preserved by extensionally equivalent contexts TODO: this is no longer true, now that we've switched Lets.WellTyped to use equality