Merge branch 'main' into paper-examples

.github/workflows/doc.yml

@@ -4,8 +4,11 @@ on:
     branches:
       - "main"
 
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
-  contents: write
+  contents: read
+  pages: write
+  id-token: write
 
 jobs:
   build:

SSA/Experimental/ExtrinsicAsymptotics.lean

@@ -106,10 +106,10 @@ example : (mk_com' 1000).WF [] .nat := check_ok (by native_decide)
 -- This would be more problematic in the intrinsic type as we would have to make sure the incremental
 -- array values in it do not actually exist at run time (see `Erased`).
 
-def ICom (Γ : Ctxt) (ty : Ty) := { c : Com // c.WF Γ ty }
-def transform : ICom [] ty → ICom [] ty := sorry
-def denote : ICom [] ty → ty.toType := sorry
-def print : ICom [] ty → String := sorry
+def Com (Γ : Ctxt) (ty : Ty) := { c : Com // c.WF Γ ty }
+def transform : Com [] ty → Com [] ty := sorry
+def denote : Com [] ty → ty.toType := sorry
+def print : Com [] ty → String := sorry
 
 theorem td : denote (transform c) = denote c := sorry
 

SSA/Experimental/ExtrinsicAsymptoticsArrays.lean

@@ -105,10 +105,10 @@ example : (mk_com' 1000).WF Array.empty .nat := check_ok (by native_decide)
 -- This would be more problematic in the intrinsic type as we would have to make sure the incremental
 -- array values in it do not actually exist at run time (see `Erased`).
 
-def ICom (Γ : Ctxt) (ty : Ty) := { c : Com // c.WF Γ ty }
-def transform : ICom Array.empty ty → ICom [] ty := sorry
-def denote : ICom Array.empty ty → ty.toType := sorry
-def print : ICom Array.empty ty → String := sorry
+def Com (Γ : Ctxt) (ty : Ty) := { c : Com // c.WF Γ ty }
+def transform : Com Array.empty ty → Com [] ty := sorry
+def denote : Com Array.empty ty → ty.toType := sorry
+def print : Com Array.empty ty → String := sorry
 
 theorem td : denote (transform c) = denote c := sorry
 

SSA/Projects/DCE/DCE.lean

@@ -234,18 +234,18 @@ def arglistDeleteVar? {Γ: Ctxt Ty} {delv : Γ.Var α} {Γ' : Ctxt Ty} {ts : Lis
           apply has'
         ⟩
 
-/- Try to delete a variable from an IExpr -/
-def IExpr.deleteVar? (DEL : Deleted Γ delv Γ') (e: IExpr Op Γ t) :
-  Option { e' : IExpr Op Γ' t // ∀ (V : Γ.Valuation), e.denote V = e'.denote (DEL.pushforward_Valuation V) } :=
+/- Try to delete a variable from an Expr -/
+def Expr.deleteVar? (DEL : Deleted Γ delv Γ') (e: Expr Op Γ t) :
+  Option { e' : Expr Op Γ' t // ∀ (V : Γ.Valuation), e.denote V = e'.denote (DEL.pushforward_Valuation V) } :=
   match e with
   | .mk op ty_eq args regArgs =>
     match arglistDeleteVar? DEL args with
     | .none => .none
     | .some args' =>
       .some ⟨.mk op ty_eq args' regArgs, by
         intros V
-        rw[IExpr.denote_unfold]
-        rw[IExpr.denote_unfold]
+        rw[Expr.denote_unfold]
+        rw[Expr.denote_unfold]
         simp
         congr 1
         apply args'.property
@@ -306,25 +306,25 @@ theorem Deleted.pushforward_Valuation_snoc {Γ Γ' : Ctxt Ty} {ω : Ty} {delv :
           case neg =>
             rfl
 
-/-- Delete a variable from an ICom. -/
-def ICom.deleteVar? (DEL : Deleted Γ delv Γ') (com : ICom Op Γ t) :
-  Option { com' : ICom Op Γ' t // ∀ (V : Γ.Valuation), com.denote V = com'.denote (DEL.pushforward_Valuation V) } :=
+/-- Delete a variable from an Com. -/
+def Com.deleteVar? (DEL : Deleted Γ delv Γ') (com : Com Op Γ t) :
+  Option { com' : Com Op Γ' t // ∀ (V : Γ.Valuation), com.denote V = com'.denote (DEL.pushforward_Valuation V) } :=
   match com with
   | .ret v =>
     match Var.tryDelete? DEL v with
     | .none => .none
     | .some ⟨v, hv⟩ =>
       .some ⟨.ret v, hv⟩
   | .lete (α := ω) e body =>
-    match ICom.deleteVar? (Deleted.snoc DEL) body with
+    match Com.deleteVar? (Deleted.snoc DEL) body with
     | .none => .none
     | .some ⟨body', hbody'⟩ =>
-      match IExpr.deleteVar? DEL e with
+      match Expr.deleteVar? DEL e with
         | .none => .none
         | .some ⟨e', he'⟩ =>
           .some ⟨.lete  e' body', by
             intros V
-            simp[ICom.denote]
+            simp[Com.denote]
             rw[← he']
             rw[hbody']
             congr
@@ -335,20 +335,20 @@ def ICom.deleteVar? (DEL : Deleted Γ delv Γ') (com : ICom Op Γ t) :
    This is necessary so that we can mark the DCE implementation as a `partial def` and ensure that Lean
    does not freak out on us, since it's indeed unclear to Lean that the output type of `dce` is always inhabited.
 -/
-def DCEType [OpSignature Op Ty] [OpDenote Op Ty] {Γ : Ctxt Ty} {t : Ty} (com : ICom Op Γ t) : Type :=
+def DCEType [OpSignature Op Ty] [OpDenote Op Ty] {Γ : Ctxt Ty} {t : Ty} (com : Com Op Γ t) : Type :=
   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ),
-    { com' : ICom Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)}
+    { com' : Com Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)}
 
 /-- Show that DCEType in inhabited. -/
-instance [SIG : OpSignature Op Ty] [DENOTE : OpDenote Op Ty] {Γ : Ctxt Ty} {t : Ty} (com : ICom Op Γ t) : Inhabited (DCEType com) where
+instance [SIG : OpSignature Op Ty] [DENOTE : OpDenote Op Ty] {Γ : Ctxt Ty} {t : Ty} (com : Com Op Γ t) : Inhabited (DCEType com) where
   default :=
     ⟨Γ, Ctxt.Hom.id, com, by intros V; rfl⟩
 
 /-- walk the list of bindings, and for each `let`, try to delete the variable defined by the `let` in the body/
 Note that this is `O(n^2)`, for an easy proofs, as it is written as a forward pass.
 The fast `O(n)` version is a backward pass. 
 -/
-partial def dce_ [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : ICom Op Γ t) : DCEType com :=
+partial def dce_ [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : Com Op Γ t) : DCEType com :=
     match HCOM: com with
     | .ret v => -- If we have a `ret`, return it.
       ⟨Γ, Ctxt.Hom.id, ⟨.ret v, by
@@ -358,29 +358,29 @@ partial def dce_ [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (
     | .lete (α := α) e body =>
       let DEL := Deleted.deleteSnoc Γ α
         -- Try to delete the variable α in the body.
-        match ICom.deleteVar? DEL body with
+        match Com.deleteVar? DEL body with
         | .none => -- we don't succeed, so DCE the child, and rebuild the same `let` binding.
           let ⟨Γ', hom', ⟨body', hbody'⟩⟩
-            :   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' (Ctxt.snoc Γ α)), { body' : ICom Op Γ' t //  ∀ (V : (Γ.snoc α).Valuation), body.denote V = body'.denote (V.comap hom)} :=
+            :   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' (Ctxt.snoc Γ α)), { body' : Com Op Γ' t //  ∀ (V : (Γ.snoc α).Valuation), body.denote V = body'.denote (V.comap hom)} :=
             (dce_ body)
-          let com' := ICom.lete (α := α) e (body'.changeVars hom')
+          let com' := Com.lete (α := α) e (body'.changeVars hom')
           ⟨Γ, Ctxt.Hom.id, com', by
             intros V
-            simp[ICom.denote]
+            simp[Com.denote]
             rw[hbody']
             rfl
           ⟩
         | .some ⟨body', hbody⟩ =>
           let ⟨Γ', hom', ⟨com', hcom'⟩⟩
-          : Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ), { com' : ICom Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
+          : Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ), { com' : Com Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
             ⟨Γ, Ctxt.Hom.id, ⟨body', by -- NOTE: we deleted the `let` binding.
               simp[HCOM]
               intros V
-              simp[ICom.denote]
+              simp[Com.denote]
               apply hbody
             ⟩⟩
           let ⟨Γ'', hom'', ⟨com'', hcom''⟩⟩
-            :   Σ (Γ'' : Ctxt Ty) (hom: Ctxt.Hom Γ'' Γ'), { com'' : ICom Op Γ'' t //  ∀ (V' : Γ'.Valuation), com'.denote V' = com''.denote (V'.comap hom)} :=
+            :   Σ (Γ'' : Ctxt Ty) (hom: Ctxt.Hom Γ'' Γ'), { com'' : Com Op Γ'' t //  ∀ (V' : Γ'.Valuation), com'.denote V' = com''.denote (V'.comap hom)} :=
             dce_ com' -- recurse into `com'`, which contains *just* the `body`, not the `let`, and return this.
           ⟨Γ'', hom''.comp hom', com'', by
             intros V
@@ -397,15 +397,15 @@ decreasing_by {
 
 /-- This is the real entrypoint to `dce` which unfolds the type of `dce_`, where we play the `DCEType` trick
 to convince Lean that the output type is in fact inhabited. -/
-def dce [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : ICom Op Γ t) :
+def dce [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : Com Op Γ t) :
   Σ (Γ' : Ctxt Ty) (hom: Ctxt.Hom Γ' Γ),
-    { com' : ICom Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
+    { com' : Com Op Γ' t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom)} :=
   dce_ com
 
 /-- A version of DCE that returns an output program with the same context. It uses the context
    morphism of `dce` to adapt the result of DCE to work with the original context -/
-def dce' [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : ICom Op Γ t) :
-    { com' : ICom Op Γ t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote V} :=
+def dce' [OpSignature Op Ty] [OpDenote Op Ty]  {Γ : Ctxt Ty} {t : Ty} (com : Com Op Γ t) :
+    { com' : Com Op Γ t //  ∀ (V : Γ.Valuation), com.denote V = com'.denote V} :=
   let ⟨ Γ', hom, com', hcom'⟩ := dce_ com
   ⟨com'.changeVars hom, by
     intros V
@@ -445,33 +445,33 @@ instance : OpDenote ExOp ExTy where
     | .add, .cons (a : Nat) (.cons b .nil), _ => a + b
     | .beq, .cons (a : Nat) (.cons b .nil), _ => a == b
 
-def cst {Γ : Ctxt _} (n : ℕ) : IExpr ExOp Γ .nat  :=
-  IExpr.mk
+def cst {Γ : Ctxt _} (n : ℕ) : Expr ExOp Γ .nat  :=
+  Expr.mk
     (op := .cst n)
     (ty_eq := rfl)
     (args := .nil)
     (regArgs := .nil)
 
-def add {Γ : Ctxt _} (e₁ e₂ : Ctxt.Var Γ .nat) : IExpr ExOp Γ .nat :=
-  IExpr.mk
+def add {Γ : Ctxt _} (e₁ e₂ : Ctxt.Var Γ .nat) : Expr ExOp Γ .nat :=
+  Expr.mk
     (op := .add)
     (ty_eq := rfl)
     (args := .cons e₁ <| .cons e₂ .nil)
     (regArgs := .nil)
 
 attribute [local simp] Ctxt.snoc
 
-def ex1_pre_dce : ICom ExOp ∅ .nat :=
-  ICom.lete (cst 1) <|
-  ICom.lete (cst 2) <|
-  ICom.ret ⟨0, by simp [Ctxt.snoc]⟩
+def ex1_pre_dce : Com ExOp ∅ .nat :=
+  Com.lete (cst 1) <|
+  Com.lete (cst 2) <|
+  Com.ret ⟨0, by simp [Ctxt.snoc]⟩
 
 /-- TODO: how do we evaluate 'ex1_post_dce' within Lean? :D -/
-def ex1_post_dce : ICom ExOp ∅ .nat := (dce' ex1_pre_dce).val
+def ex1_post_dce : Com ExOp ∅ .nat := (dce' ex1_pre_dce).val
 
-def ex1_post_dce_expected : ICom ExOp ∅ .nat :=
-  ICom.lete (cst 1) <|
-  ICom.ret ⟨0, by simp [Ctxt.snoc]⟩
+def ex1_post_dce_expected : Com ExOp ∅ .nat :=
+  Com.lete (cst 1) <|
+  Com.ret ⟨0, by simp [Ctxt.snoc]⟩
 
 
 end Examples

SSA/Projects/InstCombine/LLVM/EDSL.lean

@@ -25,4 +25,4 @@ elab "[mlir_icom (" mvars:term,* ")| " reg:mlir_region "]" : term => do
         throwError "Translation failed with error:\n\t{repr err}"
     | e => throwError "Translation failed to reduce, possibly too generic syntax\n\t{e}"
 
-macro "[mlir_icom| " reg:mlir_region "]" : term => `([mlir_icom ()| $reg])
+macro "[mlir_icom| " reg:mlir_region "]" : term => `([mlir_icom ()| $reg])

SSA/Projects/InstCombine/LLVM/Transform.lean

@@ -14,12 +14,12 @@ open Std (BitVec)
 
 abbrev Context (φ) := List (MTy φ)
 
-abbrev Expr (Γ : Context φ) (ty : MTy φ)  := IExpr (MOp φ) Γ ty
-abbrev Com (Γ : Context φ) (ty : MTy φ)   := ICom (MOp φ) Γ ty
-abbrev Var (Γ : Context φ) (ty : MTy φ)   := Ctxt.Var Γ ty
+abbrev Expr (Γ : Context φ) (ty : MTy φ)  := _root_.Expr (MOp φ) Γ ty
+abbrev Com (Γ : Context φ) (ty : MTy φ)   := _root_.Com (MOp φ) Γ ty
+abbrev Var (Γ : Context φ) (ty : MTy φ)   := _root_.Ctxt.Var Γ ty
 
 abbrev Com.lete (body : Expr Γ ty₁) (rest : Com (ty₁::Γ) ty₂) : Com Γ ty₂ :=
-  ICom.lete body rest
+  _root_.Com.lete body rest
 
 inductive TransformError
   | nameAlreadyDeclared (var : String)
@@ -446,7 +446,7 @@ def mkReturn (Γ : Context φ) (opStx : Op φ) : ReaderM (Σ ty, Com Γ ty) :=
   then match opStx.args with
   | vStx::[] => do
     let ⟨ty, v⟩ ← vStx.mkVal Γ
-    return ⟨ty, ICom.ret v⟩
+    return ⟨ty, _root_.Com.ret v⟩
   | _ => throw <| .generic s!"Ill-formed return statement (wrong arity, expected 1, got {opStx.args.length})"
   else throw <| .generic s!"Tried to build return out of non-return statement {opStx.name}"
 
@@ -477,8 +477,8 @@ def mkCom (reg : Region φ) : ExceptM (Σ (Γ : Context φ) (ty : MTy φ), Com 
   | [] => throw <| .generic "Ill-formed region (empty)"
   | coms => BuilderM.runWithNewMapping <| do
     let Γ ← declareBindings ∅ reg.args
-    let icom ← mkComHelper Γ coms
-    return ⟨Γ, icom⟩
+    let com ← mkComHelper Γ coms
+    return ⟨Γ, com⟩
 
 /-!
   ## Instantiation
@@ -524,9 +524,9 @@ def MOp.instantiateCom (vals : Vector Nat φ) : DialectMorphism (MOp φ) (InstCo
 
 open InstCombine (Op Ty) in
 def mkComInstantiate (reg : Region φ) :
-    ExceptM (Vector Nat φ → Σ (Γ : Ctxt Ty) (ty : Ty), ICom InstCombine.Op Γ ty) := do
-  let ⟨Γ, ty, icom⟩ ← mkCom reg
+    ExceptM (Vector Nat φ → Σ (Γ : Ctxt Ty) (ty : Ty), _root_.Com InstCombine.Op Γ ty) := do
+  let ⟨Γ, ty, com⟩ ← mkCom reg
   return fun vals =>
-    ⟨Γ.instantiate vals, ty.instantiate vals, icom.map (MOp.instantiateCom vals)⟩
+    ⟨Γ.instantiate vals, ty.instantiate vals, com.map (MOp.instantiateCom vals)⟩
 
 end MLIR.AST

SSA/Projects/InstCombine/Refinement.lean

@@ -3,7 +3,7 @@ import SSA.Projects.InstCombine.AliveStatements
 
 open MLIR AST
 
-abbrev ICom.Refinement (src tgt : Com (φ:=0) Γ t) (h : Goedel.toType t = Option α := by rfl) : Prop :=
+abbrev Com.Refinement (src tgt : Com (φ:=0) Γ t) (h : Goedel.toType t = Option α := by rfl) : Prop :=
   ∀ Γv, (h ▸ src.denote Γv) ⊑ (h ▸ tgt.denote Γv)
 
-infixr:90 " ⊑ "  => ICom.Refinement
+infixr:90 " ⊑ "  => Com.Refinement

SSA/Projects/InstCombine/Tactic.lean

@@ -6,7 +6,7 @@ open MLIR AST
 open Std (BitVec)
 
 /--
-- We first simplify `ICom.refinement` to see the context `Γv`.
+- We first simplify `Com.refinement` to see the context `Γv`.
 - We `simp_peephole Γv` to simplify context accesses by variables.
 - We simplify the translation overhead.
 - Then we introduce variables, `cases` on the variables to eliminate the `none` cases.
@@ -16,7 +16,7 @@ open Std (BitVec)
 macro "simp_alive_peephole" : tactic =>
   `(tactic|
       (
-        dsimp only [ICom.Refinement]
+        dsimp only [Com.Refinement]
         intros Γv
         simp_peephole at Γv
         /- note that we need the `HVector.toPair`, `HVector.toSingle` lemmas since it's used in `InstCombine.Op.denote`