From 4e1768c331a076a1cc398652ecfe1ea9681ef4ea Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 24 Oct 2023 13:35:10 +0100 Subject: [PATCH] Remove all trailing whitespaces in SSA/ (#114) This makes sure other PRs are not polluted by whitespace noise. --- SSA/Core/Context.lean | 24 ++++---- SSA/Core/ErasedContext.lean | 58 +++++++++---------- SSA/Core/Framework.lean | 20 +++---- SSA/Core/Tactic.lean | 6 +- SSA/Core/Util/ConcreteOrMVar.lean | 10 ++-- .../Bugred/failed-to-generate-splitter-2.lean | 6 +- .../Bugred/failed-to-generate-splitter.lean | 10 ++-- ...low-dependent-pattern-matching-string.lean | 56 +++++++++--------- SSA/Experimental/FlatSSAEncoding.lean | 48 +++++++-------- .../FullyHomomorphicEncryption/Basic.lean | 26 ++++----- SSA/Projects/Holor/Holor.lean | 14 ++--- SSA/Projects/InstCombine/Base.lean | 12 ++-- SSA/Projects/InstCombine/ForStd.lean | 16 ++--- SSA/Projects/InstCombine/Test.lean | 38 ++++++------ SSA/Projects/InstCombine/Tests.lean | 6 +- SSA/Projects/MLIRSyntax/AST.lean | 18 +++--- SSA/Projects/MLIRSyntax/EDSL.lean | 2 +- SSA/Projects/Tensor1D/Tensor1D.lean | 2 +- SSA/Projects/Tensor2D/Tensor2D.lean | 24 ++++---- 19 files changed, 198 insertions(+), 198 deletions(-) diff --git a/SSA/Core/Context.lean b/SSA/Core/Context.lean index 6c3c5dfe9..85ade95fc 100644 --- a/SSA/Core/Context.lean +++ b/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 => diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 79607c1d2..7b1811100 100644 --- a/SSA/Core/ErasedContext.lean +++ b/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,7 +230,7 @@ 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 @@ -238,17 +238,17 @@ 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] diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index f25acb6f6..231f5e96e 100644 --- a/SSA/Core/Framework.lean +++ b/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,10 +464,10 @@ 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 @@ -475,20 +475,20 @@ structure DialectMorphism (Op Op' : Type) {Ty Ty' : Type} [OpSignature Op Ty] [O 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 diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean index 60ce0383b..64ca9adc5 100644 --- a/SSA/Core/Tactic.lean +++ b/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, diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 1cf6865a4..2c5f1e0c6 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/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` diff --git a/SSA/Experimental/Bugred/failed-to-generate-splitter-2.lean b/SSA/Experimental/Bugred/failed-to-generate-splitter-2.lean index b933dc11e..6d12bd594 100644 --- a/SSA/Experimental/Bugred/failed-to-generate-splitter-2.lean +++ b/SSA/Experimental/Bugred/failed-to-generate-splitter-2.lean @@ -5,12 +5,12 @@ inductive Ty def Ctxt : Type := Erased <| List Ty - + noncomputable def Ctxt.snoc (Γ : Ctxt) (t : Ty) : Ctxt := Erased.mk <| t :: Γ.out def Ctxt.Var (Γ : Ctxt) (t : Ty) : Type := - { i : Nat // Γ.out.get? i = some t } + { i : Nat // Γ.out.get? i = some t } inductive CtxtProp : Ctxt → Type | nil : CtxtProp (Erased.mk []) @@ -26,7 +26,7 @@ noncomputable def matchVar {t : Ty} {Δ : Ctxt} : CtxtProp Δ → Δ.Var t → O -- | _, _ => none -example {Δ : Ctxt} (d : CtxtProp Δ) {w : Δ.Var t} : +example {Δ : Ctxt} (d : CtxtProp Δ) {w : Δ.Var t} : matchVar d w = none := by unfold matchVar /- throws error: diff --git a/SSA/Experimental/Bugred/failed-to-generate-splitter.lean b/SSA/Experimental/Bugred/failed-to-generate-splitter.lean index d06e10505..e787652c1 100644 --- a/SSA/Experimental/Bugred/failed-to-generate-splitter.lean +++ b/SSA/Experimental/Bugred/failed-to-generate-splitter.lean @@ -10,13 +10,13 @@ inductive Ty def Ctxt : Type := List Ty - + def Ctxt.Var (Γ : Ctxt) (t : Ty) : Type := - { i : Nat // Γ.get? i = some t } + { i : Nat // Γ.get? i = some t } -def matchVar {t : Ty} : {Δ : Ctxt} → Δ.Var t → Option Bool +def matchVar {t : Ty} : {Δ : Ctxt} → Δ.Var t → Option Bool | _::Δ, ⟨w+1, h⟩ => -- w† = Var.toSnoc w let w : Ctxt.Var Δ t := ⟨w, by simp_all[List.get?]⟩ matchVar w @@ -24,10 +24,10 @@ def matchVar {t : Ty} : {Δ : Ctxt} → Δ.Var t → Option Bool none -example {Δ : Ctxt } {w : Δ.Var t} : +example {Δ : Ctxt } {w : Δ.Var t} : matchVar w = none := by - -- uncommenting the `unfold` triggers an infinite loop of sorts, + -- uncommenting the `unfold` triggers an infinite loop of sorts, -- consuming 100% CPU without being caught by `maxHeartbeats` timeout -- unfold matchVar sorry \ No newline at end of file diff --git a/SSA/Experimental/Bugred/slow-dependent-pattern-matching-string.lean b/SSA/Experimental/Bugred/slow-dependent-pattern-matching-string.lean index 9aabe6a60..4a61ea49a 100644 --- a/SSA/Experimental/Bugred/slow-dependent-pattern-matching-string.lean +++ b/SSA/Experimental/Bugred/slow-dependent-pattern-matching-string.lean @@ -1,7 +1,7 @@ import Mathlib.Data.Int.Basic import Mathlib.Data.Int.Lemmas open Mathlib -open Std +open Std open Int open Nat @@ -13,7 +13,7 @@ Kinds of values. We must have 'pair' to take multiple arguments. -/ inductive Kind where | int : Kind -| nat: Kind +| nat: Kind | float : Kind | tensor1d: Kind | tensor2d: Kind @@ -33,7 +33,7 @@ def Var.unit : Var := { name := "_", kind := .unit } inductive Op: Type where | op (ret : Var) (name : String) - (arg : List Var): Op + (arg : List Var): Op -- Lean type that corresponds to kind. @@ -44,7 +44,7 @@ def Kind.eval: Kind -> Type | .unit => Unit | .float => Float | .tensor1d => Nat → Int -| .tensor2d => Nat → Nat → Int +| .tensor2d => Nat → Nat → Int | .pair p q => p.eval × q.eval end AST @@ -57,16 +57,16 @@ structure Val where kind: Kind val: kind.eval - + def Val.unit : Val := { kind := Kind.unit, val := () } -- The retun value of an SSA operation, with a name, kind, and value of that kind. structure NamedVal extends Val where - name : String + name : String -- Given a 'Var' of kind 'kind', and a value of type 〚kind⟧, build a 'Val' -def AST.Var.toNamedVal (var: Var) (value: var.kind.eval): NamedVal := +def AST.Var.toNamedVal (var: Var) (value: var.kind.eval): NamedVal := { kind := var.kind, val := value, name := var.name } def NamedVal.var (nv: NamedVal): Var := @@ -76,7 +76,7 @@ def NamedVal.var (nv: NamedVal): Var := -- bindings of variables to values of type ⟦var.kind⟧ inductive Env where | empty: Env -| cons (var: Var) (val: var.kind.eval) (rest: Env): Env +| cons (var: Var) (val: var.kind.eval) (rest: Env): Env abbrev ErrorKind := String abbrev TopM (α : Type) : Type := StateT Env (Except ErrorKind) α @@ -85,35 +85,35 @@ abbrev TopM (α : Type) : Type := StateT Env (Except ErrorKind) α def Env.set (var: Var) (val: var.kind.eval): Env → Env | env => (.cons var val env) -def Env.get (var: Var): Env → Except ErrorKind NamedVal +def Env.get (var: Var): Env → Except ErrorKind NamedVal | .empty => Except.error s!"unknown var {var.name}" -| .cons var' val env' => +| .cons var' val env' => if H : var = var' - then pure <| var.toNamedVal (H ▸ val) - else env'.get var + then pure <| var.toNamedVal (H ▸ val) + else env'.get var -def TopM.get (var: Var): TopM NamedVal := do - let e ← StateT.get +def TopM.get (var: Var): TopM NamedVal := do + let e ← StateT.get Env.get var e -def TopM.set (nv: NamedVal) (k: TopM α): TopM α := do +def TopM.set (nv: NamedVal) (k: TopM α): TopM α := do let e ← StateT.get let e' := Env.set nv.var nv.val e StateT.set e' let out ← k - StateT.set e - return out + StateT.set e + return out def TopM.error (e: ErrorKind) : TopM α := Except.error e -- Runtime denotation of an Op, that has evaluated its arguments, --- and expects a return value of type ⟦retkind⟧ +-- and expects a return value of type ⟦retkind⟧ inductive Op' where | mk (name : String) (argval : List Val) -def AST.Op.denote - (sem: (o: Op') → TopM Val): Op → TopM NamedVal -| .op ret name args => do +def AST.Op.denote + (sem: (o: Op') → TopM Val): Op → TopM NamedVal +| .op ret name args => do let vals ← args.mapM TopM.get let op' : Op' := .mk name (vals.map NamedVal.toVal) let out ← sem op' @@ -122,7 +122,7 @@ def AST.Op.denote else TopM.error "unexpected return kind '{}', expected {}" def runOp (sem : (o: Op') → TopM Val) (Op: AST.Op) -(env : Env := Env.empty) : Except ErrorKind (NamedVal × Env) := +(env : Env := Env.empty) : Except ErrorKind (NamedVal × Env) := (Op.denote sem).run env @@ -135,21 +135,21 @@ def sem: (o: Op') → TopM Val | .mk "float2" [⟨.float, x⟩] => return ⟨.float, x + x⟩ | .mk "int2" [⟨.int, x⟩] => return ⟨.int, x + x⟩ | .mk "nat2" [⟨.nat, x⟩] => return ⟨.nat, x + x⟩ -| .mk "add" [⟨.int, x⟩, ⟨.int, y⟩] => +| .mk "add" [⟨.int, x⟩, ⟨.int, y⟩] => return ⟨.int, (x + y)⟩ -| .mk "sub" [⟨.int, x⟩, ⟨.int, y⟩] => +| .mk "sub" [⟨.int, x⟩, ⟨.int, y⟩] => return ⟨.int, (x - y)⟩ -| .mk "tensor1d" [⟨.tensor1d, t⟩, ⟨.nat, ix⟩] => - let i := t ix +| .mk "tensor1d" [⟨.tensor1d, t⟩, ⟨.nat, ix⟩] => + let i := t ix return ⟨.int, i + i⟩ -| .mk "tensor2d" [⟨.tensor2d, t⟩, ⟨.int, i⟩, ⟨.nat, j⟩] => +| .mk "tensor2d" [⟨.tensor2d, t⟩, ⟨.int, i⟩, ⟨.nat, j⟩] => let i := t 0 0 let j := t 1 1 return ⟨.int, i + i⟩ | op => TopM.error s!"unknown op" -open AST in +open AST in theorem Fail: runOp sem (Op.op Var.unit "float" []) = .ok output := by { -- ERROR: -- tactic 'simp' failed, nested error: diff --git a/SSA/Experimental/FlatSSAEncoding.lean b/SSA/Experimental/FlatSSAEncoding.lean index 741eeb425..091b4572a 100644 --- a/SSA/Experimental/FlatSSAEncoding.lean +++ b/SSA/Experimental/FlatSSAEncoding.lean @@ -32,7 +32,7 @@ def test : Op := .Add c1 c2 -- I want to replace 'c2' in test with '(.Add (.Constant 1) (.Constant 1))' - -- However, to lean / as far as we can tell by inspecting 'test', + -- However, to lean / as far as we can tell by inspecting 'test', -- test = Op.Add (Op.Constant 1) (Op.Constant 2) -- -- The names 'c1'/'c2' have vanished, since they are not part @@ -41,7 +41,7 @@ def test : Op := -- We are unable to study the notion of a "name", and all that comes -- with it (rewriting at names, dominance of names, etc.) #reduce test - + open Op @@ -53,7 +53,7 @@ def sem : Op → Nat /--- #define double(x) = x + x -int foo = double(printf("10")); +int foo = double(printf("10")); -/ /- @@ -77,16 +77,16 @@ inductive OffsetOp : Nat -> Type -- (v : OffsetOp 2) --- induction on (OffsetOp 2), you need to 'deduce' that Const can never happen, +-- induction on (OffsetOp 2), you need to 'deduce' that Const can never happen, -- v = Add -abbrev FinVec (n: Nat) (α : Type) := Fin n → α +abbrev FinVec (n: Nat) (α : Type) := Fin n → α structure BasicBlock where len : Nat -- | TODO: generalize index to k-tuples for nesting. insts : (ix: Fin len) -> Σ (noperands : Nat), OffsetOp noperands × FinVec noperands (Fin ix) - + def emptyBB : BasicBlock := { len := 0, insts := fun ix => Fin.elim0 ix @@ -99,35 +99,35 @@ def appendBB (bb: BasicBlock) (inst: OffsetOp noperands) insts := fun ix => if H : ix < bb.len then bb.insts ⟨ix.val, H⟩ - else - have H : Fin bb.len = Fin ix := by + else + have H : Fin bb.len = Fin ix := by have : ix = bb.len := by linarith[ix.isLt] simp [this] - ⟨noperands, inst, H ▸ v⟩ + ⟨noperands, inst, H ▸ v⟩ } -- 0 -> Const 2 -- 1 +1 / 2 -- (let x = v in e) <-> (fun x => e) v -open Lean in +open Lean in instance : Pure OpM where pure a := .Return_ a - + def OpM.bind (ma: OpM a) (a2mb: a -> OpM b): OpM b := match ma with | .Return_ a => a2mb a | .Random_ ka => .Random_ (fun r => bind (ka r) a2mb) | .Print_ v opa => .Print_ v (bind opa a2mb) -def OpM.map (f: a -> b) (ma: OpM a) : OpM b := +def OpM.map (f: a -> b) (ma: OpM a) : OpM b := match ma with | .Return_ a => .Return_ (f a) | .Random_ ka => .Random_ (fun r => OpM.map f (ka r)) | .Print_ v ma => .Print_ v (OpM.map f ma) instance : Seq OpM where - seq m_a2b unit2ma := + seq m_a2b unit2ma := let ma := unit2ma (); OpM.bind m_a2b (fun a2b => OpM.map a2b ma) -- seqLeft : {α β : Type u} → f α → (Unit → f β) → f α @@ -139,11 +139,11 @@ instance : SeqLeft OpM where instance : SeqRight OpM where seqRight ma unit2mb := OpM.bind ma (fun _ => unit2mb () ) instance : Functor OpM where - map := OpM.map + map := OpM.map -instance : Bind OpM where +instance : Bind OpM where bind := OpM.bind - + instance : Applicative OpM := ⟨⟩ instance : Monad OpM := ⟨⟩ @@ -185,7 +185,7 @@ def testRandom2 : OpM Unit := do print r print s return () - + #reduce testRandom2 -- OpM.Random_ fun r => OpM.Random_ fun s => OpM.Print_ r (OpM.Print_ s (OpM.Return_ PUnit.unit)) @@ -195,15 +195,15 @@ def testRandom3 : OpM Unit := do print r print r return () - + #reduce testRandom3 -def testPerverse : OpM Unit := +def testPerverse : OpM Unit := OpM.Random_ fun r => (if r == 10 then print 42 else print 100) - + #reduce testPerverse /- -def program : Foo Op := +def program : Foo Op := let c1 ← .Constant 1 return .Add c1 c1 -- /= .Add (.Constant 1) (.Constant 1) -/ @@ -212,15 +212,15 @@ def program : Foo Op := -- bit pattern leads to the ALU failing. def semBadALU : Op → Option Nat | .Constant c => if c == 42 then .none else .some c -| .Add a b => do +| .Add a b => do let va ← semBadALU a let vb ← semBadALU b return va + vb -| .Mul a b => do +| .Mul a b => do let vb ← semBadALU b let va ← semBadALU a return va * vb - + #reduce semBadALU -- Follows trivially from commutativity of addition. diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean index 703466d63..bef519c67 100644 --- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean +++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean @@ -33,7 +33,7 @@ variable (q t : Nat) [Fact (q > 1)] (n : Nat) theorem WithBot.npow_coe_eq_npow (n : Nat) (x : ℕ) : (WithBot.some x : WithBot ℕ) ^ n = WithBot.some (x ^ n) := by induction n with | zero => simp - | succ n ih => + | succ n ih => rw [pow_succ'', ih, ← WithBot.coe_mul] rw [← WithBot.some_eq_coe, WithBot.some] apply Option.some_inj.2 @@ -65,7 +65,7 @@ theorem f_deg_eq : (f q n).degree = 2^n := by done /-- Charaterizing `f`: `f` is monic -/ -theorem f_monic : Monic (f q n) := by +theorem f_monic : Monic (f q n) := by have hn : 2^n = (2^n - 1) + 1 := by rw [Nat.sub_add_cancel (Nat.one_le_two_pow n)] have hn_minus_1 : degree 1 ≤ ↑(2^n - 1) := by rw [Polynomial.degree_one (R := (ZMod q))]; simp @@ -102,7 +102,7 @@ noncomputable def R.representative : R q n → (ZMod q)[X] := fun x => R.represe -/ @[simp] theorem R.fromPoly_representative : forall a : R q n, (R.fromPoly (n:=n) (R.representative q n a)) = a := by - intro a + intro a simp [R.representative] rw [Polynomial.modByMonic_eq_sub_mul_div _ (f_monic q n)] rw [RingHom.map_sub (R.fromPoly (q := q) (n:=n)) _ _] @@ -125,7 +125,7 @@ is just `a + i` for some `i ∈ (Ideal.span {f q n})`. -/ theorem R.fromPoly_rep'_eq : forall a : (ZMod q)[X], ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) a).representative' = a + i := by intro a - exists (R.fromPoly (n:=n) a).representative' - a + exists (R.fromPoly (n:=n) a).representative' - a constructor · apply Ideal.Quotient.eq.1 simp [R.representative', Function.surjInv_eq] @@ -134,7 +134,7 @@ theorem R.fromPoly_rep'_eq : forall a : (ZMod q)[X], ∃ i ∈ Ideal.span {f q n /-- Characterization theorem for the representative. -Taking the representative of the equivalence class of a polynomial `a : (ZMod q)[X]` is +Taking the representative of the equivalence class of a polynomial `a : (ZMod q)[X]` is the same as taking the remainder of `a` modulo `f q n`. -/ theorem R.representative_fromPoly : forall a : (ZMod q)[X], (R.fromPoly (n:=n) a).representative = a %ₘ (f q n) := by @@ -158,12 +158,12 @@ theorem R.rep_degree_lt_n : forall a : R q n, (R.representative q n a).degree < exact f_monic q n /-- -This function gets the `i`th coefficient of the polynomial representative -(with degree `< 2^n`) of an element `a : R q n`. Note that this is not +This function gets the `i`th coefficient of the polynomial representative +(with degree `< 2^n`) of an element `a : R q n`. Note that this is not invariant under the choice of representative. -/ -noncomputable def R.coeff (a : R q n) (i : Nat) : ZMod q := - Polynomial.coeff a.representative i +noncomputable def R.coeff (a : R q n) (i : Nat) : ZMod q := + Polynomial.coeff a.representative i /-- `R.monomial i c` is the equivalence class of the monomial `c * X^i` in `R q n`. @@ -172,9 +172,9 @@ noncomputable def R.monomial {q n : Nat} (i : Nat) (c : ZMod q) : R q n := R.fromPoly (Polynomial.monomial i c) /-- -Given an equivalence class of polynomials `a : R q n` with representative +Given an equivalence class of polynomials `a : R q n` with representative `p = p_0 + p_1 X + ... + p_{2^n - 1} X^{2^n - 1}`, `R.slice a startIdx endIdx` yields -the equivalence class of the polynomial +the equivalence class of the polynomial `p_{startIdx}*X^{startIdx} + p_{startIdx + 1} X^{startIdx + 1} + ... + p_{endIdx - 1} X^{endIdx - 1}` Note that this is not invariant under the choice of representative. -/ @@ -186,7 +186,7 @@ noncomputable def R.slice {q n : Nat} (a : R q n) (startIdx endIdx : Nat) : R q coeffs.zip coeffIdxs |>.foldl accum R.zero /-- -We define the base type of the representation, which encodes both natural numbers +We define the base type of the representation, which encodes both natural numbers and elements in the ring `R q n` (which in FHE are sometimes called 'polynomials' in allusion to `R.representative`). -/ @@ -202,7 +202,7 @@ toType := fun | .poly q n => (R q n) /-- -The operation type of the `Poly` dialect. Operations are parametrized by the +The operation type of the `Poly` dialect. Operations are parametrized by the two parameters `p` and `n` that characterize the ring `R q n`. -/ inductive Op diff --git a/SSA/Projects/Holor/Holor.lean b/SSA/Projects/Holor/Holor.lean index 3965a4706..5e395f48e 100644 --- a/SSA/Projects/Holor/Holor.lean +++ b/SSA/Projects/Holor/Holor.lean @@ -29,31 +29,31 @@ def Holor.pointwise_mul [Mul α] (h₁ h₂ : Holor α ds) : Holor α ds := fun instance [Mul α] : Mul (Holor α ds) where mul := Holor.pointwise_mul -theorem Holor.pointwise_mul_index [Mul α] (h₁ h₂ : Holor α ds) : +theorem Holor.pointwise_mul_index [Mul α] (h₁ h₂ : Holor α ds) : (h₁ * h₂) i = h₁ i * h₂ i := rfl /-- Holor inherits algebraic structures --/ -instance [Semiring α] : Semiring (Holor α ds) := +instance [Semiring α] : Semiring (Holor α ds) := by delta Holor; infer_instance -instance [CommSemiring α] : CommSemiring (Holor α ds) := +instance [CommSemiring α] : CommSemiring (Holor α ds) := by delta Holor; infer_instance -instance [Ring α] : Ring (Holor α ds) := +instance [Ring α] : Ring (Holor α ds) := by delta Holor; infer_instance -instance [CommRing α] : CommRing (Holor α ds) := +instance [CommRing α] : CommRing (Holor α ds) := by delta Holor; infer_instance -instance [SMul M A] : SMul M (Holor A ds) := by +instance [SMul M A] : SMul M (Holor A ds) := by delta Holor; infer_instance /-- Fill a holor with a constant value 'a'. -/ def Holor.fill (a : α) : Holor α ds := fun _ => a -- @chrishughes24: --- given the map ralg : R -> Z(A), +-- given the map ralg : R -> Z(A), -- I want to declare the map (r : R) -> (fill (ralg R) : Holor A ds). -- This will be the map that turns (Holor A ds) into an R-algebra. -- I'm not sure how to define this. diff --git a/SSA/Projects/InstCombine/Base.lean b/SSA/Projects/InstCombine/Base.lean index fb25e3588..5481f7a92 100644 --- a/SSA/Projects/InstCombine/Base.lean +++ b/SSA/Projects/InstCombine/Base.lean @@ -15,7 +15,7 @@ import SSA.Projects.InstCombine.ForMathlib or `1`, indicating there is exactly one distinct width meta-variable. In particular, we only define a denotational semantics for concrete programs (i.e., where `φ = 0`) - + see https://releases.llvm.org/14.0.0/docs/LangRef.html#bitwise-binary-operations -/ @@ -43,8 +43,8 @@ inductive MTy (φ : Nat) abbrev Ty := MTy 0 -instance : Repr (MTy φ) where - reprPrec +instance : Repr (MTy φ) where + reprPrec | .bitvec (.concrete w), _ => "i" ++ repr w | .bitvec (.mvar ⟨i, _⟩), _ => f!"i$\{%{i}}" @@ -55,7 +55,7 @@ def Ty.width : Ty → Nat | .bitvec (.concrete w) => w @[simp] -theorem Ty.width_eq (ty : Ty) : .bitvec (ty.width) = ty := by +theorem Ty.width_eq (ty : Ty) : .bitvec (ty.width) = ty := by rcases ty with ⟨w|i⟩ · rfl · exact i.elim0 @@ -128,7 +128,7 @@ instance : ToString Op where @[simp, reducible] def MOp.sig : MOp φ → List (MTy φ) | .and w | .or w | .xor w | .shl w | .lshr w | .ashr w -| .add w | .mul w | .sub w | .udiv w | .sdiv w +| .add w | .mul w | .sub w | .udiv w | .sdiv w | .srem w | .urem w | .icmp _ w => [.bitvec w, .bitvec w] | .not w | .neg w | .copy w => [.bitvec w] @@ -145,7 +145,7 @@ def MOp.outTy : MOp φ → MTy φ | .icmp _ _ => .bitvec 1 | .const width _ => .bitvec width -instance : OpSignature (MOp φ) (MTy φ) where +instance : OpSignature (MOp φ) (MTy φ) where signature op := ⟨op.sig, [], op.outTy⟩ @[simp] diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean index 736a140a0..e7a48df1f 100644 --- a/SSA/Projects/InstCombine/ForStd.lean +++ b/SSA/Projects/InstCombine/ForStd.lean @@ -7,7 +7,7 @@ def ofBool : (Bool) -> Std.BitVec 1 notation:50 x " ≤ᵤ " y => BitVec.ule x y notation:50 x " <ᵤ " y => BitVec.ult x y -notation:50 x " ≥ᵤ " y => BitVec.ult y x +notation:50 x " ≥ᵤ " y => BitVec.ult y x notation:50 x " >ᵤ " y => BitVec.ule y x notation:50 x " ≤ₛ " y => BitVec.sle x y @@ -44,7 +44,7 @@ theorem refl {α: Type u} : ∀ x : Option α, Refinement x x := by theorem trans {α : Type u} : ∀ x y z : Option α, Refinement x y → Refinement y z → Refinement x z := by intro x y z h₁ h₂ cases h₁ <;> cases h₂ <;> try { apply Refinement.noneAny } ; try {apply Refinement.bothSome; assumption} - rename_i x y hxy y h + rename_i x y hxy y h rw [hxy, h]; apply refl instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by @@ -55,7 +55,7 @@ instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by { apply isFalse; intro h; cases h } { rename_i val val' cases (decEq val val') - { apply isFalse; intro h; cases h; contradiction } + { apply isFalse; intro h; cases h; contradiction } { apply isTrue; apply Refinement.bothSome; assumption } } @@ -79,10 +79,10 @@ Note that signed integer division and unsigned integer division are distinct ope Division by zero is undefined behavior. Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1. -/ -def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w := - if y.toInt = 0 +def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w := + if y.toInt = 0 then none - else + else let div := (x.toInt / y.toInt) if div < Int.ofNat (2^w) then some $ BitVec.ofInt w div @@ -91,9 +91,9 @@ def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w := /-- This instruction returns the unsigned integer remainder of a division. This instruction always performs an unsigned division to get the remainder. Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’. -Taking the remainder of a division by zero is undefined behavior. +Taking the remainder of a division by zero is undefined behavior. -/ -def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w := +def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w := if y.toNat = 0 then none else some $ BitVec.ofNat w (x.toNat % y.toNat) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index d750e5502..44bb67198 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -7,10 +7,10 @@ open MLIR AST TODO: infer the number of meta-variables in an AST, so that we can remove the `Op 0` annotation in the following -/ -def add_mask : Op 0 := [mlir_op| +def add_mask : Op 0 := [mlir_op| "module"() ( { "llvm.func"() ( { - ^bb0(%arg0: i32): + ^bb0(%arg0: i32): %0 = "llvm.mlir.constant"() {value = 8 : i32} : () -> i32 %1 = "llvm.mlir.constant"() {value = 31 : i32} : () -> i32 %2 = "llvm.ashr"(%arg0, %1) : (i32, i32) -> i32 @@ -19,7 +19,7 @@ def add_mask : Op 0 := [mlir_op| "llvm.return"(%4) : (i32) -> () }) : () -> () "llvm.func"() ( { - ^bb0(%arg0: i32): + ^bb0(%arg0: i32): %0 = "llvm.mlir.constant"() {value = 8 : i32} : () -> i32 %1 = "llvm.mlir.constant"() {value = 31 : i32} : () -> i32 %2 = "llvm.ashr"(%arg0, %1) : (i32, i32) -> i32 @@ -30,22 +30,22 @@ def add_mask : Op 0 := [mlir_op| }) : () -> () ] -def bb0 : Region 0 := [mlir_region| +def bb0 : Region 0 := [mlir_region| { - ^bb0(%arg0: i32): + ^bb0(%arg0: i32): %0 = "llvm.mlir.constant"() {value = 8 : i32} : () -> i32 %1 = "llvm.mlir.constant"() {value = 31 : i32} : () -> i32 %2 = "llvm.ashr"(%arg0, %1) : (i32, i32) -> i32 %3 = "llvm.and"(%2, %0) : (i32, i32) -> i32 %4 = "llvm.add"(%3, %2) : (i32, i32) -> i32 "llvm.return"(%4) : (i32) -> () - }] + }] #print bb0 #eval bb0 - + open InstCombine -def Γn (n : Nat) : Context φ := +def Γn (n : Nat) : Context φ := Ctxt.ofList <| .replicate n (.bitvec 32) def op0 : Op 0 := [mlir_op| %0 = "llvm.mlir.constant"() {value = 8 : i32} : () -> i32] @@ -67,7 +67,7 @@ def opRet : Op 0 := [mlir_op| "llvm.return"(%4) : (i32) -> ()] #eval mkExpr (Γn 5) op4 ["3", "2", "1", "0", "arg0"] #eval mkReturn (Γn 6) opRet ["4", "3", "2", "1", "0", "arg0"] -def ops : List (Op 0) := [mlir_ops| +def ops : List (Op 0) := [mlir_ops| %0 = "llvm.mlir.constant"() {value = 8 : i32} : () -> i32 %1 = "llvm.mlir.constant"() {value = 31 : i32} : () -> i32 %2 = "llvm.ashr"(%arg0, %1) : (i32, i32) -> i32 @@ -96,9 +96,9 @@ def com := mkCom bb0 |>.toOption |>.get (by rfl) theorem com_Γ : com.1 = (Γn 1) := by rfl theorem com_ty : com.2.1 = .bitvec 32 := by rfl -def bb0IcomConcrete := [mlir_icom| +def bb0IcomConcrete := [mlir_icom| { - ^bb0(%arg0: i32): + ^bb0(%arg0: i32): %0 = "llvm.mlir.constant"() {value = 1 : i32} : () -> i32 %1 = "llvm.mlir.constant"() {value = 31 : i32} : () -> i32 %2 = "llvm.ashr"(%arg0, %1) : (i32, i32) -> i32 @@ -108,16 +108,16 @@ def bb0IcomConcrete := [mlir_icom| }] /-- A simple example of a family of programs, generic over some bitwidth `w` -/ -def GenericWidth (w : Nat) := [mlir_icom (w)| +def GenericWidth (w : Nat) := [mlir_icom (w)| { ^bb0(): %0 = "llvm.mlir.constant"() {value = 0 : _} : () -> _ "llvm.return"(%0) : (_) -> () }] -def bb0IcomGeneric (w : Nat) := [mlir_icom (w)| +def bb0IcomGeneric (w : Nat) := [mlir_icom (w)| { - ^bb0(%arg0: _): + ^bb0(%arg0: _): %0 = "llvm.mlir.constant"() {value = 1 : _} : () -> _ %1 = "llvm.mlir.constant"() {value = 31 : _} : () -> _ %2 = "llvm.ashr"(%arg0, %1) : (_, _) -> _ @@ -129,13 +129,13 @@ def bb0IcomGeneric (w : Nat) := [mlir_icom (w)| /-- Indeed, the concrete program is an instantiation of the generic program -/ example : bb0IcomGeneric 32 = bb0IcomConcrete := by rfl -/-- +/-- Simple example of the denotation of `GenericWidth`. - Note that we only have semantics (in the sense of "an implementation of `OpSemantics`") - for concrete programs. We thus need to instantiate `GenericWidth` with some width `w` before we - can use `denote`. In this way, we indirectly give semantics to the family of programs that + Note that we only have semantics (in the sense of "an implementation of `OpSemantics`") + for concrete programs. We thus need to instantiate `GenericWidth` with some width `w` before we + can use `denote`. In this way, we indirectly give semantics to the family of programs that `GenericWidth` represents. -/ example (w Γv) : (GenericWidth w).denote Γv = some (Bitvec.ofNat w 0) := by rfl - + diff --git a/SSA/Projects/InstCombine/Tests.lean b/SSA/Projects/InstCombine/Tests.lean index 2e35d4168..41392abce 100644 --- a/SSA/Projects/InstCombine/Tests.lean +++ b/SSA/Projects/InstCombine/Tests.lean @@ -3,9 +3,9 @@ import SSA.Projects.InstCombine.Base -- TODO: move this to new EDSL, once generic bitwidth syntax works namespace InstCombine -def test1 (_params : Nat × Nat × Nat) : IO Bool := do +def test1 (_params : Nat × Nat × Nat) : IO Bool := do -- let (w, A, B) := params - -- let E : EnvC ∅ := EnvC.empty + -- let E : EnvC ∅ := EnvC.empty -- let out : Option (Bitvec w) := TSSA.eval -- [dsl_bb| -- ^bb @@ -20,7 +20,7 @@ def test1 (_params : Nat × Nat × Nat) : IO Bool := do -- %v8 := pair:%v1 %v7; -- %v9 := op:or w %v8 -- dsl_ret %v9 - -- ] E + -- ] E -- IO.println (repr out) -- return true throw <| .userError "test1 not implemented yet!" diff --git a/SSA/Projects/MLIRSyntax/AST.lean b/SSA/Projects/MLIRSyntax/AST.lean index c72250abb..7c235f9cc 100644 --- a/SSA/Projects/MLIRSyntax/AST.lean +++ b/SSA/Projects/MLIRSyntax/AST.lean @@ -53,9 +53,9 @@ abbrev Width.mvar : Fin φ → Width φ := ConcreteOrMVar.mvar inductive MLIRType (φ : Nat) : Type _ := | int: Signedness -> Width φ -> MLIRType φ | float: Nat -> MLIRType φ - | tensor1d: MLIRType φ -- tensor of int values. - | tensor2d: MLIRType φ -- tensor of int values. - | tensor4d: MLIRType φ -- tensor of int values. + | tensor1d: MLIRType φ -- tensor of int values. + | tensor2d: MLIRType φ -- tensor of int values. + | tensor4d: MLIRType φ -- tensor of int values. | index: MLIRType φ | undefined: String → MLIRType φ deriving Repr, DecidableEq @@ -192,7 +192,7 @@ instance : Coe (String × MLIRType φ) (AttrEntry φ) where coe v := AttrEntry.mk v.fst (AttrValue.type v.snd) instance : Coe (AttrEntry φ) (String × AttrValue φ) where - coe + coe | AttrEntry.mk key val => (key, val) instance : Coe (List (AttrEntry φ)) (AttrDict φ) where @@ -200,7 +200,7 @@ instance : Coe (List (AttrEntry φ)) (AttrDict φ) where | v => AttrDict.mk v instance : Coe (AttrDict φ) (List (AttrEntry φ)) where - coe + coe | AttrDict.mk as => as def Region.name (region : Region φ) : BBName := @@ -276,12 +276,12 @@ partial def op_to_format {φ} : Op φ → Format doc_res ++ " := " ++ doc_name ++ doc_args ++ doc_rgns ++ repr attrs partial def rgn_to_format {φ} : Region φ → Format - | Region.mk name args ops => + | Region.mk name args ops => let doc_args := if args.isEmpty then f!"" else f!"({args.map (fun (v, t) => f!"{repr v} : {repr t}") |>.intersperse "," |> Format.join})" - let doc_ops := + let doc_ops := ops.map (Format.align true ++ op_to_format ·) |> Format.join f!"^{name}{doc_args} : " ++ doc_ops end @@ -327,12 +327,12 @@ def AttrDict.find {φ} (attrs : AttrDict φ) (name : String) : Option (AttrValue | some v => v.value | none => none -def AttrDict.find_nat {φ} (attrs : AttrDict φ) (name : String) : Option Nat := +def AttrDict.find_nat {φ} (attrs : AttrDict φ) (name : String) : Option Nat := match attrs.find name with | .some (AttrValue.nat i) => .some i | _ => .none -def AttrDict.find_int {φ} (attrs : AttrDict φ) +def AttrDict.find_int {φ} (attrs : AttrDict φ) (name : String): Option (Int × MLIRType φ) := match attrs.find name with | .some (AttrValue.int i ty) => .some (i, ty) diff --git a/SSA/Projects/MLIRSyntax/EDSL.lean b/SSA/Projects/MLIRSyntax/EDSL.lean index 833bd15b6..4adce42e6 100644 --- a/SSA/Projects/MLIRSyntax/EDSL.lean +++ b/SSA/Projects/MLIRSyntax/EDSL.lean @@ -736,7 +736,7 @@ syntax mlir_op_operand "=" macro_rules | `([mlir_op| $resName:mlir_op_operand = $name:str ( $operandsNames,* ) $[ ( $rgns,* ) ]? $[ $attrDict ]? - : ( $operandsTypes,* ) -> $resType:mlir_type + : ( $operandsTypes,* ) -> $resType:mlir_type ]) => do let results ← `([([mlir_op_operand| $resName], [mlir_type| $resType])]) -- TODO: Needs a consistency check that `operandsNames.length = operandsTypes.length` diff --git a/SSA/Projects/Tensor1D/Tensor1D.lean b/SSA/Projects/Tensor1D/Tensor1D.lean index dc44204b8..043a37b9f 100644 --- a/SSA/Projects/Tensor1D/Tensor1D.lean +++ b/SSA/Projects/Tensor1D/Tensor1D.lean @@ -319,7 +319,7 @@ inductive Op deriving DecidableEq inductive Ty -| /-- values held in tensors -/ int : Ty +| /-- values held in tensors -/ int : Ty | /-- shapes and indexes of tensors -/ ix : Ty | /-- tensor type -/ tensor1d : Ty deriving DecidableEq, Inhabited diff --git a/SSA/Projects/Tensor2D/Tensor2D.lean b/SSA/Projects/Tensor2D/Tensor2D.lean index 843c4cf9f..d1656ffe1 100644 --- a/SSA/Projects/Tensor2D/Tensor2D.lean +++ b/SSA/Projects/Tensor2D/Tensor2D.lean @@ -87,7 +87,7 @@ inductive Op | sub | map2d | fill2d -| extract2d +| extract2d inductive Ty | int : Ty @@ -106,7 +106,7 @@ instance : Goedel Ty where toType := Ty.toType def Op.outTy : Op → Ty | .add => .int | .sub => .int - | .constIx _ => .ix + | .constIx _ => .ix | .constTensor _ => .tensor2d | .constInt _ => .int | .map2d | .fill2d => .tensor2d @@ -130,8 +130,8 @@ def Op.regSig : Op → RegionSignature Ty @[reducible] instance : OpSignature Op Ty where - signature op := ⟨op.sig, op.regSig, op.outTy⟩ - + signature op := ⟨op.sig, op.regSig, op.outTy⟩ + /- -- error: unknown free variable: _kernel_fresh.97 @@ -141,7 +141,7 @@ instance : OpDenote Op Ty where | .constIx v, _, _ => v | .constTensor v, _, _ => v | .constInt v, _, _ => v - | .add, (.cons x (.cons y nil)), _ => + | .add, (.cons x (.cons y nil)), _ => let x : Int := x; let y : Int := y; x + y @@ -150,14 +150,14 @@ instance : OpDenote Op Ty where let y : Int := y; let out : Int := x - y out - | .map2d, (.cons t .nil), (.cons r .nil) => + | .map2d, (.cons t .nil), (.cons r .nil) => let t : Tensor2d' Int := t -- Is there a cleaner way to build the data below? let f : Int → Int := fun v => r (Ctxt.Valuation.ofHVector <| (.cons v .nil)) t.map f - | .fill2d, (.cons v (.cons t nil)), _ => + | .fill2d, (.cons v (.cons t nil)), _ => t.fill v - | .extract2d, (.cons δ₁ (.cons δ₂ (.cons sz₁ (.cons sz₂ (.cons t .nil))))), _ => + | .extract2d, (.cons δ₁ (.cons δ₂ (.cons sz₁ (.cons sz₂ (.cons t .nil))))), _ => t.extract δ₁ δ₂ sz₁ sz₂ -- NOTE: there is no way in MLIR to talk about composition of functions, so `map . map` is out @@ -169,20 +169,20 @@ instance : OpDenote Op Ty where -- naively leads to errors about incorrect types: -- https://github.com/bollu/ssa/issues/28 open SSA EDSL2 in -theorem map_fill_2d +theorem map_fill_2d (t : Tensor2d' Int) - (sz₀ sz₁ ix₀ ix₁: Index) + (sz₀ sz₁ ix₀ ix₁: Index) (i : Int): TSSA.eval (e := e) (Op := Op) [dsl_bb2| - return op:fill2d (op:constInt(i) (), + return op:fill2d (op:constInt(i) (), op:extract2d ( ((op:constIx(sz₀) () , op:constIx(sz₁) ()), (op:constIx(ix₀) (), op:constIx(ix₁) ())), op:constTensor(t) ())) ] = TSSA.eval (e := e) (Op := Op) [dsl_bb2| - return op:extract2d + return op:extract2d (((op:constIx(sz₀) (), op:constIx(sz₁) ()), (op:constIx(ix₀) (), op:constIx(ix₁) ())), op:fill2d (op:constInt(i) (), op:constTensor(t) ()))