Remove all trailing whitespaces in SSA/ (#114)

This makes sure other PRs are not polluted by whitespace noise.

SSA/Core/Context.lean

@@ -30,7 +30,7 @@ def Var (Γ : Ctxt) (t : Ty) : Type :=
 
 namespace Var
 
-instance : DecidableEq (Var Γ t) := 
+instance : DecidableEq (Var Γ t) :=
   fun ⟨i, ih⟩ ⟨j, jh⟩ => match inferInstanceAs (Decidable (i = j)) with
     | .isTrue h => .isTrue <| by simp_all
     | .isFalse h => .isFalse <| by intro hc; apply h; apply Subtype.mk.inj hc
@@ -46,19 +46,19 @@ in context `Γ.snoc t`. This is marked as a coercion. -/
 @[coe]
 def toSnoc {Γ : Ctxt} {t t' : Ty} (var : Ctxt.Var Γ t) : Ctxt.Var (Ctxt.snoc Γ t') t  :=
   ⟨var.1+1, by cases var; simp_all [snoc]⟩
-  
-/-- This is an induction principle that case splits on whether or not a variable 
+
+/-- This is an induction principle that case splits on whether or not a variable
 is the last variable in a context. -/
 @[elab_as_elim]
-def casesOn 
+def casesOn
     {motive : (Γ : Ctxt) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt} {t t' : Ty} (v : (Γ.snoc t').Var t)
-    (base : {t t' : Ty} → 
+    (base : {t t' : Ty} →
         {Γ : Ctxt} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
       motive Γ t t' v :=
   match v with
-    | ⟨0, h⟩ => 
+    | ⟨0, h⟩ =>
         cast (by cases h; simp only [Var.last]) <| @last Γ t
     | ⟨i+1, h⟩ =>
         base ⟨i, h⟩
@@ -68,7 +68,7 @@ def casesOn
 def casesOn_last
     {motive : (Γ : Ctxt) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt} {t : Ty}
-    (base : {t t' : Ty} → 
+    (base : {t t' : Ty} →
         {Γ : Ctxt} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
     Ctxt.Var.casesOn (motive := motive)
@@ -78,10 +78,10 @@ def casesOn_last
 /-- `Ctxt.Var.casesOn` behaves in the expected way when applied to a previous variable,
 that is not the last one. -/
 @[simp]
-def casesOn_toSnoc 
+def casesOn_toSnoc
     {motive : (Γ : Ctxt) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt} {t t' : Ty} (v : Γ.Var t)
-    (base : {t t' : Ty} → 
+    (base : {t t' : Ty} →
         {Γ : Ctxt} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
       Ctxt.Var.casesOn (motive := motive) (Ctxt.Var.toSnoc (t' := t') v) base last = base v :=
@@ -98,9 +98,9 @@ def append : Ctxt → Ctxt → Ctxt :=
 
 theorem append_empty (Γ : Ctxt) : append Γ ∅ = Γ := by
   simp[append, EmptyCollection.emptyCollection, empty]
-
 
-theorem append_snoc (Γ Γ' : Ctxt) (t : Ty) : 
+
+theorem append_snoc (Γ Γ' : Ctxt) (t : Ty) :
     append Γ (Ctxt.snoc Γ' t) = (append Γ Γ').snoc t := by
   simp[append, snoc]
 
@@ -115,7 +115,7 @@ def Var.inl {Γ Γ' : Ctxt} {t : Ty} : Var Γ t → Var (Ctxt.append Γ Γ') t
   | ⟨v, h⟩ => ⟨v + Γ'.length, by simp[←h, append, List.get?_append_add]⟩
 
 def Var.inr {Γ Γ' : Ctxt} {t : Ty} : Var Γ' t → Var (append Γ Γ') t
-  | ⟨v, h⟩ => ⟨v, by 
+  | ⟨v, h⟩ => ⟨v, by
       simp[append]
       induction Γ' generalizing v
       case nil =>

SSA/Core/ErasedContext.lean

@@ -2,7 +2,7 @@ import Mathlib.Data.Erased
 import Mathlib.Data.Finset.Basic
 import SSA.Core.HVector
 
-/-- 
+/--
   Typeclass for a `baseType` which is a Gödel code of Lean types.
 
   Intuitively, each `b : β` represents a Lean `Type`, but using `β` instead of `Type` directly
@@ -39,7 +39,7 @@ def snoc : Ctxt Ty → Ty → Ctxt Ty :=
 @[coe, simp]
 def ofList : List Ty → Ctxt Ty :=
   -- Erased.mk
-  fun Γ => Γ 
+  fun Γ => Γ
 
 -- Why was this noncomutable? (removed it to make transformation computable)
 @[simp]
@@ -72,7 +72,7 @@ def last (Γ : Ctxt Ty) (t : Ty) : Ctxt.Var (Ctxt.snoc Γ t) t :=
   ⟨0, by simp [snoc, List.get?]⟩
 
 def emptyElim {α : Sort _} {t : Ty} : Ctxt.Var ∅ t → α :=
-  fun ⟨_, h⟩ => by 
+  fun ⟨_, h⟩ => by
     simp [EmptyCollection.emptyCollection, empty] at h
 
 
@@ -95,27 +95,27 @@ theorem succ_eq_toSnoc {Γ : Ctxt Ty} {t : Ty} {w} (h : (Γ.snoc t).get? (w+1) =
 /-- Transport a variable from `Γ` to any mapped context `Γ.map f` -/
 @[coe]
 def toMap : Var Γ t → Var (Γ.map f) (f t)
-  | ⟨i, h⟩ => ⟨i, by 
+  | ⟨i, h⟩ => ⟨i, by
       simp only [get?, map, List.get?_map, Option.map_eq_some']
       exact ⟨t, h, rfl⟩
     ⟩
 
 def cast {Γ : Ctxt Op} (h_eq : ty₁ = ty₂) : Γ.Var ty₁ → Γ.Var ty₂
   | ⟨i, h⟩ => ⟨i, h_eq ▸ h⟩
-  
-/-- This is an induction principle that case splits on whether or not a variable 
+
+/-- This is an induction principle that case splits on whether or not a variable
 is the last variable in a context. -/
 @[elab_as_elim]
-def casesOn 
+def casesOn
     {motive : (Γ : Ctxt Ty) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt Ty} {t t' : Ty} (v : (Γ.snoc t').Var t)
-    (toSnoc : {t t' : Ty} → 
+    (toSnoc : {t t' : Ty} →
         {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
       motive Γ t t' v :=
   match v with
-    | ⟨0, h⟩ => 
-        _root_.cast (by 
+    | ⟨0, h⟩ =>
+        _root_.cast (by
           simp [snoc] at h
           subst h
           simp [Ctxt.Var.last]
@@ -128,7 +128,7 @@ def casesOn
 def casesOn_last
     {motive : (Γ : Ctxt Ty) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt Ty} {t : Ty}
-    (base : {t t' : Ty} → 
+    (base : {t t' : Ty} →
         {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
     Ctxt.Var.casesOn (motive := motive)
@@ -138,18 +138,18 @@ def casesOn_last
 /-- `Ctxt.Var.casesOn` behaves in the expected way when applied to a previous variable,
 that is not the last one. -/
 @[simp]
-def casesOn_toSnoc 
+def casesOn_toSnoc
     {motive : (Γ : Ctxt Ty) → (t t' : Ty) → Ctxt.Var (Γ.snoc t') t → Sort _}
     {Γ : Ctxt Ty} {t t' : Ty} (v : Γ.Var t)
-    (base : {t t' : Ty} → 
+    (base : {t t' : Ty} →
         {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' v.toSnoc)
     (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
       Ctxt.Var.casesOn (motive := motive) (Ctxt.Var.toSnoc (t' := t') v) base last = base v :=
   rfl
 
 end Var
-  
-theorem toSnoc_injective {Γ : Ctxt Ty} {t t' : Ty} : 
+
+theorem toSnoc_injective {Γ : Ctxt Ty} {t t' : Ty} :
     Function.Injective (@Ctxt.Var.toSnoc Ty Γ t t') := by
   let ofSnoc : (Γ.snoc t').Var t → Option (Γ.Var t) :=
     fun v => Ctxt.Var.casesOn v some none
@@ -167,16 +167,16 @@ abbrev Hom.id {Γ : Ctxt Ty} : Γ.Hom Γ :=
    * `v₁` now maps to `v₂`
    * all other variables `v` still map to `map v` as in the original map
 -/
-def Hom.with [DecidableEq Ty] {Γ₁ Γ₂ : Ctxt Ty} (f : Γ₁.Hom Γ₂) {t : Ty} 
+def Hom.with [DecidableEq Ty] {Γ₁ Γ₂ : Ctxt Ty} (f : Γ₁.Hom Γ₂) {t : Ty}
     (v₁ : Γ₁.Var t) (v₂ : Γ₂.Var t) : Γ₁.Hom Γ₂ :=
   fun t' w =>
-    if h : ∃ ty_eq : t = t', ty_eq ▸ w = v₁ then 
+    if h : ∃ ty_eq : t = t', ty_eq ▸ w = v₁ then
       h.fst ▸ v₂
     else
       f w
 
 
-def Hom.snocMap {Γ Γ' : Ctxt Ty} (f : Hom Γ Γ') {t : Ty} : 
+def Hom.snocMap {Γ Γ' : Ctxt Ty} (f : Hom Γ Γ') {t : Ty} :
     (Γ.snoc t).Hom (Γ'.snoc t) := by
   intro t' v
   cases v using Ctxt.Var.casesOn with
@@ -198,10 +198,10 @@ variable [Goedel Ty] -- for a valuation, we need to evaluate the Lean `Type` cor
 def Valuation (Γ : Ctxt Ty) : Type :=
   ⦃t : Ty⦄ → Γ.Var t → (toType t)
 
-instance : Inhabited (Ctxt.Valuation (∅ : Ctxt Ty)) := ⟨fun _ v => v.emptyElim⟩ 
+instance : Inhabited (Ctxt.Valuation (∅ : Ctxt Ty)) := ⟨fun _ v => v.emptyElim⟩
 
 /-- Make a valuation for `Γ.snoc t` from a valuation for `Γ` and an element of `t.toType`. -/
-def Valuation.snoc {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : toType t) : 
+def Valuation.snoc {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : toType t) :
     (Γ.snoc t).Valuation := by
   intro t' v
   revert s x
@@ -211,7 +211,7 @@ def Valuation.snoc {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : toType t) :
 
 @[simp]
 theorem Valuation.snoc_last {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : toType t) :
-    (s.snoc x) (Ctxt.Var.last _ _) = x := by 
+    (s.snoc x) (Ctxt.Var.last _ _) = x := by
   simp [Ctxt.Valuation.snoc]
 
 @[simp]
@@ -230,25 +230,25 @@ end Valuation
 /- ## VarSet -/
 
 /-- A `Ty`-indexed family of sets of variables in context `Γ` -/
-abbrev VarSet (Γ : Ctxt Ty) : Type := 
+abbrev VarSet (Γ : Ctxt Ty) : Type :=
   Finset (Σ t, Γ.Var t)
 
 namespace VarSet
 
 /-- A `VarSet` with exactly one variable `v` -/
 @[simp]
 def ofVar {Γ : Ctxt Ty} (v : Γ.Var t) : VarSet Γ :=
-  {⟨_, v⟩} 
+  {⟨_, v⟩}
 
 end VarSet
 
 namespace Var
 
-@[simp] 
-theorem val_last {Γ : Ctxt Ty} {t : Ty} : (last Γ t).val = 0 := 
+@[simp]
+theorem val_last {Γ : Ctxt Ty} {t : Ty} : (last Γ t).val = 0 :=
   rfl
 
-@[simp] 
+@[simp]
 theorem val_toSnoc {Γ : Ctxt Ty} {t t' : Ty} (v : Γ.Var t) : (@toSnoc _ _ _ t' v).val = v.val + 1 :=
   rfl
 
@@ -266,7 +266,7 @@ abbrev Diff.Valid (Γ₁ Γ₂ : Ctxt Ty) (d : Nat) : Prop :=
   ∀ {i t}, Γ₁.get? i = some t → Γ₂.get? (i+d) = some t
 
 /--
-  If `Γ₁` is a prefix of `Γ₂`, 
+  If `Γ₁` is a prefix of `Γ₂`,
   then `d : Γ₁.Diff Γ₂` represents the number of elements that `Γ₂` has more than `Γ₁`
 -/
 def Diff (Γ₁ Γ₂ : Ctxt Ty) : Type :=
@@ -280,7 +280,7 @@ def zero (Γ : Ctxt Ty) : Diff Γ Γ :=
 
 /-- Adding a new type to the right context corresponds to incrementing the difference by 1 -/
 def toSnoc (d : Diff Γ₁ Γ₂) : Diff Γ₁ (Γ₂.snoc t) :=
-  ⟨d.val + 1, by 
+  ⟨d.val + 1, by
     intro i _ h_get_snoc
     rcases d with ⟨d, h_get_d⟩
     simp[←h_get_d h_get_snoc, snoc, List.get?]
@@ -336,7 +336,7 @@ theorem toHom_zero {Γ : Ctxt Ty} {h : Valid Γ Γ 0} :
   rfl
 
 @[simp]
-theorem toHom_unSnoc {Γ₁ Γ₂ : Ctxt Ty} (d : Diff (Γ₁.snoc t) Γ₂) : 
+theorem toHom_unSnoc {Γ₁ Γ₂ : Ctxt Ty} (d : Diff (Γ₁.snoc t) Γ₂) :
     toHom (unSnoc d) = fun _ v => (toHom d) v.toSnoc := by
   simp only [unSnoc, toHom, Var.toSnoc, Nat.add_assoc, Nat.add_comm 1]
 

SSA/Core/Framework.lean

@@ -56,7 +56,7 @@ inductive IExpr : (Γ : Ctxt Ty) → (ty : Ty) → Type :=
     (args : HVector (Ctxt.Var Γ) <| OpSignature.sig op)
     (regArgs : HVector (fun t : Ctxt Ty × Ty => ICom t.1 t.2)
       (OpSignature.regSig op)) : IExpr Γ ty
-  
+
 /-- A very simple intrinsically typed program: a sequence of let bindings. -/
 inductive ICom : Ctxt Ty → Ty → Type where
   | ret (v : Γ.Var t) : ICom Γ t
@@ -68,7 +68,7 @@ section
 open Std (Format)
 variable {Op Ty : Type} [OpSignature Op Ty] [Repr Op] [Repr Ty]
 
-mutual 
+mutual
   def IExpr.repr (prec : Nat) : IExpr Op Γ t → Format
     | ⟨op, _, args, _regArgs⟩ => f!"{repr op}{repr args}"
 
@@ -464,31 +464,31 @@ instance : Functor RegionSignature where
   map f := List.map fun (tys, ty) => (f <$> tys, f ty)
 
 instance : Functor Signature where
-  map := fun f ⟨sig, regSig, outTy⟩ => 
+  map := fun f ⟨sig, regSig, outTy⟩ =>
     ⟨f <$> sig, f <$> regSig, f outTy⟩
 
-/-- A dialect morphism consists of a map between operations and a map between types, 
+/-- A dialect morphism consists of a map between operations and a map between types,
   such that the signature of operations is respected
 -/
 structure DialectMorphism (Op Op' : Type) {Ty Ty' : Type} [OpSignature Op Ty] [OpSignature Op' Ty'] where
   mapOp : Op → Op'
   mapTy : Ty → Ty'
   preserves_signature : ∀ op, signature (mapOp op) = mapTy <$> (signature op)
 
-variable {Op Op' Ty Ty : Type} [OpSignature Op Ty] [OpSignature Op' Ty'] 
+variable {Op Op' Ty Ty : Type} [OpSignature Op Ty] [OpSignature Op' Ty']
   (f : DialectMorphism Op Op')
 
-def DialectMorphism.preserves_sig (op : Op) : 
+def DialectMorphism.preserves_sig (op : Op) :
     OpSignature.sig (f.mapOp op) = f.mapTy <$> (OpSignature.sig op) := by
   simp only [OpSignature.sig, Function.comp_apply, f.preserves_signature, List.map_eq_map]; rfl
 
-def DialectMorphism.preserves_regSig (op : Op) : 
+def DialectMorphism.preserves_regSig (op : Op) :
     OpSignature.regSig (f.mapOp op) = (OpSignature.regSig op).map (
       fun ⟨a, b⟩ => ⟨f.mapTy <$> a, f.mapTy b⟩
     ) := by
   simp only [OpSignature.regSig, Function.comp_apply, f.preserves_signature, List.map_eq_map]; rfl
 
-def DialectMorphism.preserves_outTy (op : Op) : 
+def DialectMorphism.preserves_outTy (op : Op) :
     OpSignature.outTy (f.mapOp op) = f.mapTy (OpSignature.outTy op) := by
   simp only [OpSignature.outTy, Function.comp_apply, f.preserves_signature]; rfl
 
@@ -502,12 +502,12 @@ mutual
         f.mapOp op,
         (f.preserves_outTy _).symm,
         f.preserves_sig _ ▸ args.map' f.mapTy fun _ => Var.toMap (f:=f.mapTy),
-        f.preserves_regSig _ ▸ 
+        f.preserves_regSig _ ▸
           HVector.mapDialectMorphism regs
       ⟩
 
   /-- Inline of `HVector.map'` for the termination checker -/
-  def HVector.mapDialectMorphism : ∀ {regSig : RegionSignature Ty}, 
+  def HVector.mapDialectMorphism : ∀ {regSig : RegionSignature Ty},
       HVector (fun t => ICom Op t.fst t.snd) regSig
       → HVector (fun t => ICom Op' t.fst t.snd) (f.mapTy <$> regSig : RegionSignature _)
     | _, .nil        => .nil

SSA/Core/Tactic.lean

@@ -1,9 +1,9 @@
 import SSA.Core.WellTypedFramework
 
-open SSA 
+open SSA
 
-macro "simp_mlir": tactic => 
-  `(tactic| 
+macro "simp_mlir": tactic =>
+  `(tactic|
       (
        simp (config := {decide := false}) only [TSSA.eval, Function.comp,
          id.def, TypedUserSemantics, TypedUserSemantics.eval, Context.Var,

SSA/Core/Util/ConcreteOrMVar.lean

@@ -3,7 +3,7 @@ import Mathlib.Data.Vector.Basic
 -- import Mathlib.Tactic
 
 
-/-- 
+/--
   A general type that is either a concrete known value of type `α`, or one of `φ` metavariables
  -/
 inductive ConcreteOrMVar (α : Type u) (φ : Nat)
@@ -17,22 +17,22 @@ instance : Coe α (ConcreteOrMVar α φ) := ⟨.concrete⟩
 /- In the specific case of `α := Nat`, we'd like to be able to use nat literals -/
 instance : OfNat (ConcreteOrMVar Nat φ) n := ⟨.concrete n⟩
 
-namespace ConcreteOrMVar 
+namespace ConcreteOrMVar
 
 /-- If there are no meta-variables, `ConcreteOrMVar` is just the concrete type `α` -/
-def toConcrete : ConcreteOrMVar α 0 → α 
+def toConcrete : ConcreteOrMVar α 0 → α
   | .concrete a => a
 
 @[simp]
 theorem toConcrete_concrete : toConcrete (.concrete a) = a := rfl
 
-/-- 
+/--
   Provide a value for one of the metavariables.
   Specifically, the metavariable with the maximal index `φ` out of `φ+1` total metavariables.
   All other metavariables indices' are left as-is, but cast to `Fin φ` -/
 def instantiateOne (a : α) : ConcreteOrMVar α (φ+1) → ConcreteOrMVar α φ
   | .concrete w => .concrete w
-  | .mvar i => i.lastCases 
+  | .mvar i => i.lastCases
       (.concrete a)       -- `i = Fin.last`
       (fun j => .mvar j)  -- `i = Fin.castSucc j`