From a5235f6fbc4b6a8255a23234274759b74d5bf927 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 15:39:51 -0500 Subject: [PATCH] Add documentation to some modules. --- lean/Spa/Interp.lean | 10 ++++++++++ lean/Spa/Language/Base.lean | 19 +++++++++++++++++++ lean/Spa/Lattice.lean | 26 +++++++++++++++++++++++--- 3 files changed, 52 insertions(+), 3 deletions(-) diff --git a/lean/Spa/Interp.lean b/lean/Spa/Interp.lean index 97f0e24..62fb922 100644 --- a/lean/Spa/Interp.lean +++ b/lean/Spa/Interp.lean @@ -1,7 +1,17 @@ import Mathlib.Tactic.TypeStar +/-! + +Interpretation to a semantic domain. + +This file serves to introduce the double-angle-bracket "denotation" +notation by prodiving a class instance `Interp`, whose single +method `interp` is what the double brackets map to. -/ + namespace Spa +/-- A type `α` that implements this class has denotation / meaning + in the semantic domain `dom`. -/ class Interp (α : Type*) (dom : outParam Type*) where interp : α → dom diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean index 78e68b7..5fcdc72 100644 --- a/lean/Spa/Language/Base.lean +++ b/lean/Spa/Language/Base.lean @@ -1,7 +1,19 @@ import Mathlib.Data.Finset.Basic +/-! + +Base language. + +This file defines the core object language for the program analysis and +transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean` +file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data +types with unique IDs per condtructor, enabling in-AST pointers. + +-/ + namespace Spa +/-- A value-producing expression. Currently, this cannot have side effects. -/ inductive Expr where | add (e₁ e₂ : Expr) | sub (e₁ e₂ : Expr) @@ -9,11 +21,15 @@ inductive Expr where | num (n : ℕ) deriving DecidableEq +/-- A statement that cannot alter control flow (and thus, can be part of a basic block). + + This differs from, e.g., a loop, which can cause execution to jump to its top several times. -/ inductive BasicStmt where | assign (x : String) (e : Expr) | noop deriving DecidableEq +/-- Any statements, which may or may not change program state (variable assignments). -/ inductive Stmt where | basic (bs : BasicStmt) | andThen (s₁ s₂ : Stmt) @@ -21,16 +37,19 @@ inductive Stmt where | whileLoop (e : Expr) (s : Stmt) deriving DecidableEq +/-- Variables mentioned in this expression. -/ def Expr.vars : Expr → Finset String | .add l r => l.vars ∪ r.vars | .sub l r => l.vars ∪ r.vars | .var s => {s} | .num _ => ∅ +/-- Variables assigned or mentioned in this basic statement. -/ def BasicStmt.vars : BasicStmt → Finset String | .assign x e => {x} ∪ e.vars | .noop => ∅ +/-- Variables assigned or mentioned in this statement. -/ def Stmt.vars : Stmt → Finset String | .basic bs => bs.vars | .andThen s₁ s₂ => s₁.vars ∪ s₂.vars diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index d6ef43b..5c59215 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -1,8 +1,20 @@ import Mathlib.Order.Lattice import Mathlib.Order.RelSeries +/-! + +Lattice Definitions. + +This file provides some definitions for lattices. It used to be more critical +when this was an Agda project, since it defined (semi)lattices, the ordering +relation, etc. However, these have been lifted into `Mathlib.Order.Lattice` +etc.. What remains are a couple of theorems about folds, as well +as `FiniteHeightLattice`, the core concept of lattice-based static +program analyses. See the documentation on that class for more information. -/ + namespace Spa +/-- Predicate for binary functions independently monotone in both their arguments. -/ def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) : Prop := (∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·)) @@ -11,18 +23,20 @@ section Folds variable {α β : Type*} [Preorder α] [Preorder β] +/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/ lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β} (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂) - (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) : + (hf₁ : ∀ b, Monotone (f · b)) (hf₂ : ∀ a, Monotone (f a ·)) : l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by induction hl with | nil => exact hb | cons hxy _ ih => exact le_trans (hf₁ _ hxy) (hf₂ _ ih) +/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/ lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β} (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂) - (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) : + (hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f b ·)) : l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by induction hl generalizing b₁ b₂ with | nil => exact hb @@ -30,14 +44,16 @@ lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β} exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy)) omit [Preorder α] in +/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/ lemma foldr_mono' (l : List α) (f : α → β → β) - (hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by + (hf : ∀ a, Monotone (f a ·)) : Monotone (l.foldr f ·) := by intro b₁ b₂ hb induction l with | nil => exact hb | cons x xs ih => exact hf x ih omit [Preorder α] in +/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/ lemma foldl_mono' (l : List α) (f : β → α → β) (hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by intro b₁ b₂ hb @@ -47,15 +63,18 @@ lemma foldl_mono' (l : List α) (f : β → α → β) end Folds +/-- Predicate on types with `Preorder` that claims all $<$ chains in the type have at most `n` comparisons. -/ def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop := ∀ c : LTSeries α, c.length ≤ n +/-- Wrapper over `LTSeries` that exposes its beginning and end points, as well as its length, as part of the type. -/ structure PointedLTSeries (α : Type*) (f t : α) (n : ℕ) [Preorder α] where series : LTSeries α head_series : series.head = f last_series : series.last = t length_series : series.length = n +/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/ class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where height : ℕ longestChain : PointedLTSeries α ⊥ ⊤ height @@ -65,6 +84,7 @@ namespace FiniteHeightLattice variable (α : Type*) [Lattice α] [FiniteHeightLattice α] +/-- The bottom element `⊥` of a finite height lattice is _actually_ the least element. -/ lemma bot_le (a : α) : (⊥ : α) ≤ a := by by_cases heq : ⊥ ⊓ a = ⊥ · exact inf_eq_left.mp heq