From a19f9fa148aa5e195bd31674f4c85866ba94f639 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 9 Aug 2026 17:38:56 -0500 Subject: [PATCH] Get rid of Tagged --- lean/Spa.lean | 5 - lean/Spa/Language/Base.lean | 10 +- lean/Spa/Language/Tagged/Basic.lean | 18 - lean/Spa/Language/Tagged/Derive.lean | 509 ----------------------- lean/Spa/Language/Tagged/Graphs.lean | 104 ----- lean/Spa/Language/Tagged/Id.lean | 9 - lean/Spa/Language/Tagged/Properties.lean | 29 -- 7 files changed, 7 insertions(+), 677 deletions(-) delete mode 100644 lean/Spa/Language/Tagged/Basic.lean delete mode 100644 lean/Spa/Language/Tagged/Derive.lean delete mode 100644 lean/Spa/Language/Tagged/Graphs.lean delete mode 100644 lean/Spa/Language/Tagged/Id.lean delete mode 100644 lean/Spa/Language/Tagged/Properties.lean diff --git a/lean/Spa.lean b/lean/Spa.lean index bb2bcd9..3bc5711 100644 --- a/lean/Spa.lean +++ b/lean/Spa.lean @@ -19,10 +19,5 @@ import Spa.Showable import Spa.Analysis.Utils import Spa.Analysis.Sign import Spa.Analysis.Constant -import Spa.Language.Tagged.Id -import Spa.Language.Tagged.Derive -import Spa.Language.Tagged.Basic -import Spa.Language.Tagged.Properties -import Spa.Language.Tagged.Graphs import Spa.Analysis.Reaching import Spa.Transformation.Licm diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean index 8038004..1da64ea 100644 --- a/lean/Spa/Language/Base.lean +++ b/lean/Spa/Language/Base.lean @@ -5,9 +5,13 @@ 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. +transformation. It's a very basic imperative language. + +Program points are identified by their node in the control flow graph rather than +by an identifier stored in the AST: a recursion over a `Stmt` threads a +`Spa.GGraph.Embed` of the subtree's CFG into the whole program's (starting from +`Spa.Program.rootEmbed`), which yields the CFG index of each basic statement +along with a proof that the node carries it. -/ diff --git a/lean/Spa/Language/Tagged/Basic.lean b/lean/Spa/Language/Tagged/Basic.lean deleted file mode 100644 index ee61b20..0000000 --- a/lean/Spa/Language/Tagged/Basic.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Spa.Language.Base -import Spa.Language.Tagged.Id -import Spa.Language.Tagged.Derive - -derive_tagged Spa.Expr Spa.BasicStmt Spa.Stmt - -namespace Spa - -def tagStmt (s : Stmt) : Stmt.Tagged RawId := (s.tag 0).1 - -def Stmt.Tagged.subtreeIds {τ : Type} (s : Stmt.Tagged τ) : List τ := - s.foldTags (· :: ·) [] - -def Stmt.Tagged.isInLoopBody {τ : Type} [DecidableEq τ] - (body : Stmt.Tagged τ) (id : τ) : Bool := - decide (id ∈ body.subtreeIds) - -end Spa diff --git a/lean/Spa/Language/Tagged/Derive.lean b/lean/Spa/Language/Tagged/Derive.lean deleted file mode 100644 index b021a93..0000000 --- a/lean/Spa/Language/Tagged/Derive.lean +++ /dev/null @@ -1,509 +0,0 @@ -import Lean -import Mathlib.Tactic.DeriveTraversable -import Spa.Language.Base -import Spa.Language.Tagged.Id - -/-! -# The `derive_tagged` command - -`derive_tagged T₁ T₂ … Tₙ` takes a family of (possibly mutually recursive) -inductive types and generates, for each `Tᵢ`: - -* a *tagged* mirror inductive `Tᵢ.Tagged (τ : Type)`, in which every constructor - carries a leading `tag : τ` field and every field whose type is a family - member is retyped to its `.Tagged τ` counterpart; -* `Tᵢ.Tagged.erase : Tᵢ.Tagged τ → Tᵢ`, forgetting all tags; -* `Tᵢ.tag : Tᵢ → ℕ → Tᵢ.Tagged RawId × ℕ`, assigning every node a unique - `RawId` (its postorder index) by a single unified traversal that threads a - counter; the whole family shares one counter, so identifiers are unique across - types. - -The generated declarations have exactly the shape of the hand-written reference; -see `Spa/Language/Tagged/Basic.lean` (which invokes this command) and the proofs -in `Spa/Language/Tagged/Properties.lean`. - -Scope: the generator handles non-indexed inductives whose constructor fields are -either scalars or *direct* references to a family member (which covers the object -language). Nested occurrences such as `List Tᵢ` are not supported. --/ - -open Lean Elab Command Meta - -namespace Spa.DeriveTagged - -/-- One constructor field, classified as a recursive family reference or a scalar -(whose type syntax we keep verbatim for the mirror inductive). -/ -structure FieldData where - isRec : Bool - recType : Name - typeStx : Term - -/-- A constructor: its original (full) name, short name, and fields. -/ -structure CtorData where - origName : Name - shortName : Name - fields : Array FieldData - -/-- A family member together with its constructors. -/ -structure TypeData where - name : Name - ctors : Array CtorData - -def taggedOf (n : Name) : Name := n ++ `Tagged -def eraseOf (n : Name) : Name := n ++ `Tagged ++ `erase -def rootTagOf (n : Name) : Name := n ++ `Tagged ++ `rootTag -def tagOf (n : Name) : Name := n ++ `tag -def foldTagsOf (n : Name) : Name := n ++ `Tagged ++ `foldTags -def wfOf (n : Name) : Name := n ++ `Tagged ++ `WF -def narrowOf (n : Name) : Name := n ++ `Tagged ++ `narrow -def narrowEraseOf (n : Name) : Name := n ++ `Tagged ++ `narrow_erase -def tagLeOf (n : Name) : Name := n ++ `tag_le -def tagRootTagPostOf (n : Name) : Name := n ++ `tag_rootTag_post -def tagWfOf (n : Name) : Name := n ++ `tag_wf - -/-- Project the `i`-th conjunct (1-based) out of `hyp`, which has type a -right-nested `And` of `total` conjuncts, e.g. `hyp |>.2 |>.2 |>.1`. -/ -def projAnd {m : Type → Type} [Monad m] [MonadQuotation m] - (hyp : Term) (i total : Nat) : m Term := do - let mut t := hyp - for _ in [0:i-1] do - t ← `($t |>.2) - if i < total then - t ← `($t |>.1) - return t - -/-- Combine a non-empty array of propositions into a right-nested conjunction. -/ -def mkAndR {m : Type → Type} [Monad m] [MonadQuotation m] - (cs : Array Term) : m Term := do - let mut t := cs.back! - for c in cs.pop.reverse do - t ← `($c ∧ $t) - return t - -/-- For a constructor, return one entry per *recursive* field: its argument -identifier, the family member it references, and the start-counter expression at -which it is tagged (`n`, then `(a.tag n).2`, …) — the same threading `mkTag` -uses. -/ -def recChildren (cd : CtorData) (argNames : Array Ident) (nStart : Term) : - CommandElabM (Array (Ident × Name × Term)) := do - let mut res : Array (Ident × Name × Term) := #[] - let mut cur := nStart - for (f, a) in cd.fields.zip argNames do - if f.isRec then - res := res.push (a, f.recType, cur) - cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2) - return res - -/-- Inspect the family, classifying each constructor field. -/ -def gather (family : Array Name) (τ : Ident) : TermElabM (Array TypeData) := do - let famSet : NameSet := family.foldl (·.insert ·) {} - family.mapM fun tn => do - let iv ← getConstInfoInduct tn - let ctors ← iv.ctors.toArray.mapM fun cn => do - let cv ← getConstInfoCtor cn - let fields ← forallTelescopeReducing cv.type fun args _ => do - let fieldArgs := args.extract iv.numParams args.size - fieldArgs.mapM fun a => do - let ty ← inferType a - match ty.getAppFn.constName? with - | some hn => - if famSet.contains hn then - return { isRec := true, recType := hn, typeStx := ← `($(mkIdent (taggedOf hn)) $τ) } - else - return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty } - | none => - return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty } - return { origName := cn, shortName := cn.componentsRev.head!, fields } - return { name := tn, ctors } - -/-- The arrow type `τ → → Self τ` of a tagged constructor. -/ -def ctorArrow (cd : CtorData) (self : Term) (τ : Ident) : TermElabM Term := do - let mut t := self - for f in cd.fields.reverse do - t ← `($(f.typeStx) → $t) - `($τ → $t) - -/-- The tagged mirror inductives, one per family member. The family is a DAG -(`Expr ← BasicStmt ← Stmt`), not genuinely mutual, so they are emitted as -separate inductives in dependency order rather than a `mutual` block. - -`Functor`/`Traversable` instances are derived separately by `mkDeriveInstances` -below rather than via an inline `deriving` clause. -/ -def mkInductives (tds : Array TypeData) (τ : Ident) : - CommandElabM (Array (TSyntax `command)) := do - tds.mapM fun td => do - let self ← `($(mkIdent (taggedOf td.name)) $τ) - let ctors ← td.ctors.mapM fun cd => do - let aty ← Command.liftTermElabM (ctorArrow cd self τ) - `(Lean.Parser.Command.ctor| | $(mkIdent cd.shortName):ident : $aty) - `(command| inductive $(mkIdent (taggedOf td.name)):ident ($τ : Type) where $ctors*) - -/-- A `deriving instance Functor, Traversable for Tᵢ.Tagged` command per family -member. Since every tagged type is a single-parameter, direct-recursive -inductive in `τ`, Mathlib's deriving handler produces clean (`sorry`-free) -instances, giving `map`, `traverse`, and the `Traversable.foldr`/`toList` folds -for free. - -These are emitted as *separate* commands in dependency order (rather than an -inline `deriving` clause on each inductive) for two reasons: deriving -`Stmt.Tagged` needs the `Expr.Tagged`/`BasicStmt.Tagged` instances already in -scope, and — because every member's type name ends in `.Tagged` — the handler's -auto-generated instance name (`instFunctorTagged`, built from the type's last -component) collides across the family unless each derive sees the environment -the previous one updated; separate commands give it that, so the names -disambiguate to `instFunctorTagged`, `instFunctorTagged_1`, …. - -The hand-written `foldTags` is retained alongside these: it is a -structural-recursion fold that `simp`/`decide` reduce cleanly, unlike the -abstract `Traversable.foldr` (defined via the `FreeMonoid`/`Const` applicative), -which reduces under `decide`/`rfl` but not naive `simp` unfolding. -/ -def mkDeriveInstances (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - tds.mapM fun td => - `(command| deriving instance Functor, Traversable for $(mkIdent (taggedOf td.name))) - -/-- The `erase` functions, one per family member (separate defs in dependency -order — each calls only already-defined lower members). -/ -def mkErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - tds.mapM fun td => do - let mut pats : Array Term := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}")) - let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) _ $argNames*) - let eraseArgs ← (cd.fields.zip argNames).mapM fun (f, a) => - if f.isRec then `($(mkIdent (eraseOf f.recType)) $a) else pure a - let rhs ← `($(mkIdent cd.origName) $eraseArgs*) - pats := pats.push pat - rhss := rhss.push rhs - `(command| def $(mkIdent (eraseOf td.name)) {τ : Type} : - $(mkIdent (taggedOf td.name)) τ → $(mkIdent td.name) := - fun x => match x with $[| $pats => $rhss]*) - -/-- The `rootTag` accessors (one non-recursive `def` per type). -/ -def mkRootTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let tIdent := mkIdent `t - tds.mapM fun td => do - let mut pats : Array Term := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let hole ← `(_) - let wilds := Array.mkArray cd.fields.size hole - pats := pats.push (← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tIdent $wilds*)) - rhss := rhss.push tIdent - `(command| def $(mkIdent (rootTagOf td.name)) {τ : Type} : - $(mkIdent (taggedOf td.name)) τ → τ := - fun x => match x with $[| $pats => $rhss]*) - -/-- The postorder `tag` functions, one per family member (separate defs in -dependency order). -/ -def mkTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let nId := mkIdent ``Spa.RawId - tds.mapM fun td => do - let mut pats : Array Term := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}")) - let pat ← `($(mkIdent cd.origName) $argNames*) - let mut cur : Term ← `(n) - let mut lets : Array (Ident × Term) := #[] - let mut taggedArgs : Array Term := #[] - let mut ri := 0 - for (f, a) in cd.fields.zip argNames do - if f.isRec then - let rName := mkIdent (.mkSimple s!"r{ri}") - let rhsCall ← `($(mkIdent (tagOf f.recType)) $a $cur) - lets := lets.push (rName, rhsCall) - taggedArgs := taggedArgs.push (← `($rName |>.1)) - cur ← `($rName |>.2) - ri := ri + 1 - else - taggedArgs := taggedArgs.push a - let last := cur - let tagged ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) - (⟨$last⟩ : $nId) $taggedArgs*) - let mut body ← `(($tagged, $last + 1)) - for (rName, rhs) in lets.reverse do - body ← `(let $rName := $rhs; $body) - pats := pats.push pat - rhss := rhss.push body - `(command| def $(mkIdent (tagOf td.name)) : - $(mkIdent td.name) → Nat → $(mkIdent (taggedOf td.name)) $nId × Nat := - fun e n => match e with $[| $pats => $rhss]*) - -/-- The tag-fold functions: `foldTags f acc t` applies `f` to every tag in `t`, -right-to-left, threading `acc`. This is the `Foldable`/`foldr`-over-tags the -hand-written collectors (e.g. `subtreeIds`) reduce to. One separate def per -family member (the family is a DAG, so no `mutual` block is needed). -/ -def mkFoldTags (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let τ := mkIdent `τ - let m := mkIdent `M - let fId := mkIdent `f - let accId := mkIdent `acc - let tagId := mkIdent `t - tds.mapM fun td => do - let mut pats : Array Term := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}")) - let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagId $argNames*) - let mut body : Term := accId - for (fld, a) in (cd.fields.zip argNames).reverse do - if fld.isRec then - body ← `($(mkIdent (foldTagsOf fld.recType)) $fId $body $a) - body ← `($fId $tagId $body) - pats := pats.push pat - rhss := rhss.push body - `(command| def $(mkIdent (foldTagsOf td.name)) {$τ:ident : Type} {$m:ident : Type} - ($fId : $τ → $m → $m) ($accId : $m) : - $(mkIdent (taggedOf td.name)) $τ → $m := - fun x => match x with $[| $pats => $rhss]*) - -/-- The well-formedness predicate `T.Tagged.WF : T.Tagged RawId → Prop`: every -recursive child's root tag has a strictly smaller postorder index than the node's -own tag, and each child is itself well-formed. Leaf constructors are `True`. -/ -def mkWF (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let tId := mkIdent `t - let rawId := mkIdent ``Spa.RawId - tds.mapM fun td => do - let mut pats : Array Term := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let hasRec := cd.fields.any (·.isRec) - let mut patArgs : Array Term := #[] - let mut recArgs : Array Ident := #[] - let mut i := 0 - for f in cd.fields do - if f.isRec then - let a := mkIdent (.mkSimple s!"a{i}") - patArgs := patArgs.push a - recArgs := recArgs.push a - else - patArgs := patArgs.push (← `(_)) - i := i + 1 - let tagBind : Term ← if hasRec then `($tId) else `(_) - let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagBind $patArgs*) - let rhs ← if recArgs.isEmpty then `(True) else do - let bounds ← recArgs.mapM fun a => `($(a).rootTag.post < $(tId).post) - let wfs ← recArgs.mapM fun a => `($(a).WF) - mkAndR (bounds ++ wfs) - pats := pats.push pat - rhss := rhss.push rhs - `(command| def $(mkIdent (wfOf td.name)) : - $(mkIdent (taggedOf td.name)) $rawId → Prop := - fun x => match x with $[| $pats => $rhss]*) - -/-- The `narrow` coercion `T.Tagged RawId → T.Tagged (Fin N)`, given a bound on -the root tag and a well-formedness proof. Each node's tag becomes the `Fin N` -built from its postorder index, and recursion threads the bound through `lt_trans` -and the (definitionally unfolded) `WF` conjunction. -/ -def mkNarrow (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let rawId := mkIdent ``Spa.RawId - let tId := mkIdent `t - let nId := mkIdent `N - let hId := mkIdent `h - let hwfId := mkIdent `hwf - let tgId := mkIdent `tg - tds.mapM fun td => do - let self ← `($(mkIdent (taggedOf td.name)) $rawId) - let mut patss : Array (Array Term) := #[] - let mut rhss : Array Term := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}") - let ctorPat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tgId $argNames*) - let k := (cd.fields.filter (·.isRec)).size - let mut newArgs : Array Term := #[] - let mut ri := 0 - for (f, a) in cd.fields.zip argNames do - if f.isRec then - let bound ← projAnd hwfId (ri + 1) (2 * k) - let wf ← projAnd hwfId (k + ri + 1) (2 * k) - newArgs := newArgs.push (← `($(a).narrow (lt_trans $bound $hId) $wf)) - ri := ri + 1 - else - newArgs := newArgs.push a - let built ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) ⟨$(tgId).post, $hId⟩ $newArgs*) - let nPat ← `(_) - let hPat ← `($hId) - let hwfPat : Term ← if k == 0 then `(_) else `($hwfId) - patss := patss.push #[ctorPat, nPat, hPat, hwfPat] - rhss := rhss.push built - `(command| def $(mkIdent (narrowOf td.name)) : ($tId : $self) → {$nId : ℕ} → - $(tId).rootTag.post < $nId → $(tId).WF → $(mkIdent (taggedOf td.name)) (Fin $nId) - $[| $[$patss],* => $rhss]*) - -/-- `T.tag_rootTag_post`: the root tag of a freshly tagged node is exactly one -below the threaded-out counter, i.e. the node itself is numbered last (postorder). -A uniform `cases <;> simp` discharges every constructor. -/ -def mkTagRootTagPost (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let eId := mkIdent `e - let nId := mkIdent `n - tds.mapM fun td => - `(command| theorem $(mkIdent (tagRootTagPostOf td.name)) - ($eId : $(mkIdent td.name)) ($nId : ℕ) : - ($(eId).tag $nId).1.rootTag.post + 1 = ($(eId).tag $nId).2 := by - cases $eId:ident <;> - simp [$(mkIdent (tagOf td.name)):ident, $(mkIdent (rootTagOf td.name)):ident]) - -/-- `T.tag_le`: tagging only ever advances the counter (`n ≤ (e.tag n).2`). -Proved by induction; each arm threads the counter through its recursive children -(using the relevant `tag_le`/induction hypothesis) and closes with `omega`. -/ -def mkTagLe (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let eId := mkIdent `e - let nId := mkIdent `n - tds.mapM fun td => do - let mut ctorLabels : Array Ident := #[] - let mut binderss : Array (Array Ident) := #[] - let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}") - let mut ihBinders : Array Ident := #[] - let mut haveTacs : Array (TSyntax `tactic) := #[] - let mut cur : Term ← `($nId) - let mut i := 0 - for (f, a) in cd.fields.zip argNames do - if f.isRec then - let fact ← if f.recType == td.name then - `($(mkIdent (.mkSimple s!"ih{i}")) $cur) - else - `($(mkIdent (tagLeOf f.recType)) $a $cur) - if f.recType == td.name then - ihBinders := ihBinders.push (mkIdent (.mkSimple s!"ih{i}")) - haveTacs := haveTacs.push (← `(tactic| have := $fact)) - cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2) - i := i + 1 - let simpTac ← `(tactic| simp only [$(mkIdent (tagOf td.name)):ident]) - let omegaTac ← `(tactic| omega) - let allTacs := #[simpTac] ++ haveTacs ++ #[omegaTac] - ctorLabels := ctorLabels.push (mkIdent cd.shortName) - binderss := binderss.push (argNames ++ ihBinders) - tacs := tacs.push (← `(tacticSeq| $[$allTacs]*)) - `(command| theorem $(mkIdent (tagLeOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) : - $nId ≤ ($(eId).tag $nId).2 := by - induction $eId:ident generalizing $nId:ident with - $[| $ctorLabels:ident $binderss* => $tacs]*) - -/-- `T.tag_wf`: a freshly tagged term is well-formed. Each recursive child's -bound conjunct is closed by `omega` from that child's `tag_rootTag_post` plus the -`tag_le` of every later child (which bounds the threaded-out counter), and each -well-formedness conjunct is the child's induction hypothesis / `tag_wf`. -/ -def mkTagWf (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let eId := mkIdent `e - let nId := mkIdent `n - tds.mapM fun td => do - let mut ctorLabels : Array Ident := #[] - let mut binderss : Array (Array Ident) := #[] - let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}") - -- recursive children: (arg, recType, startCounter, sameType?, fieldIndex) - let mut recs : Array (Ident × Name × Term × Bool × Nat) := #[] - let mut cur : Term ← `($nId) - let mut i := 0 - for (f, a) in cd.fields.zip argNames do - if f.isRec then - recs := recs.push (a, f.recType, cur, f.recType == td.name, i) - cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2) - i := i + 1 - let k := recs.size - let ihBinders := (recs.filter (·.2.2.2.1)).map fun r => mkIdent (.mkSimple s!"ih{r.2.2.2.2}") - let tac : TSyntax ``Lean.Parser.Tactic.tacticSeq ← if k == 0 then - `(tacticSeq| exact True.intro) - else do - let mut comps : Array Term := #[] - -- bound conjuncts - for idx in [0:k] do - let (a, rt, s, _, _) := recs[idx]! - let mut bHaves : Array (TSyntax `tactic) := - #[← `(tactic| have := $(mkIdent (tagRootTagPostOf rt)) $a $s)] - for j in [idx+1:k] do - let (aj, rtj, sj, _, _) := recs[j]! - bHaves := bHaves.push (← `(tactic| have := $(mkIdent (tagLeOf rtj)) $aj $sj)) - bHaves := bHaves.push (← `(tactic| omega)) - comps := comps.push (← `(by $(← `(tacticSeq| $[$bHaves]*)))) - -- well-formedness conjuncts - for idx in [0:k] do - let (a, rt, s, same, fi) := recs[idx]! - comps := comps.push <| ← if same then `($(mkIdent (.mkSimple s!"ih{fi}")) $s) - else `($(mkIdent (tagWfOf rt)) $a $s) - let simpTac ← `(tactic| simp only - [$(mkIdent (tagOf td.name)):ident, $(mkIdent (wfOf td.name)):ident]) - let exactTac ← `(tactic| exact ⟨$comps,*⟩) - `(tacticSeq| $[$(#[simpTac, exactTac])]*) - ctorLabels := ctorLabels.push (mkIdent cd.shortName) - binderss := binderss.push (argNames ++ ihBinders) - tacs := tacs.push tac - `(command| theorem $(mkIdent (tagWfOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) : - ($(eId).tag $nId).1.WF := by - induction $eId:ident generalizing $nId:ident with - $[| $ctorLabels:ident $binderss* => $tacs]*) - -/-- `T.Tagged.narrow_erase`: narrowing the tag type does not change the erased -(untagged) term. A per-constructor `simp` with the local `narrow`/`erase` -equations, the lower members' `narrow_erase`, and the induction hypotheses. -/ -def mkNarrowErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do - let rawId := mkIdent ``Spa.RawId - let tId := mkIdent `t - let nId := mkIdent `N - let hId := mkIdent `h - let hwfId := mkIdent `hwf - let tgId := mkIdent `tg - tds.mapM fun td => do - let mut ctorLabels : Array Ident := #[] - let mut binderss : Array (Array Ident) := #[] - let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[] - for cd in td.ctors do - let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}") - let mut lemmas : Array Term := - #[← `($(mkIdent (narrowOf td.name))), ← `($(mkIdent (eraseOf td.name)))] - let mut ihBinders : Array Ident := #[] - let mut seenLower : Array Name := #[] - let mut i := 0 - for f in cd.fields do - if f.isRec then - if f.recType == td.name then - let ih := mkIdent (.mkSimple s!"ih{i}") - ihBinders := ihBinders.push ih - lemmas := lemmas.push (← `($ih)) - else if !seenLower.contains f.recType then - seenLower := seenLower.push f.recType - lemmas := lemmas.push (← `($(mkIdent (narrowEraseOf f.recType)))) - i := i + 1 - let introTac ← `(tactic| intro $nId $hId $hwfId) - let simpTac ← `(tactic| simp [$[$lemmas:term],*]) - ctorLabels := ctorLabels.push (mkIdent cd.shortName) - binderss := binderss.push (#[tgId] ++ argNames ++ ihBinders) - tacs := tacs.push (← `(tacticSeq| $[$(#[introTac, simpTac])]*)) - `(command| theorem $(mkIdent (narrowEraseOf td.name)) : - ($tId : $(mkIdent (taggedOf td.name)) $rawId) → ∀ {$nId : ℕ} - ($hId : $(tId).rootTag.post < $nId) ($hwfId : $(tId).WF), - ($(tId).narrow $hId $hwfId).erase = $(tId).erase := by - intro $tId:ident - induction $tId:ident with - $[| $ctorLabels:ident $binderss* => $tacs]*) - -/-- `derive_tagged T₁ … Tₙ` — generate tagged mirrors, `erase`, and `tag` for the -given family of inductives. -/ -syntax (name := deriveTaggedCmd) "derive_tagged " ident+ : command - -@[command_elab deriveTaggedCmd] -def elabDeriveTagged : CommandElab := fun stx => do - match stx with - | `(derive_tagged $ids*) => - let family ← ids.mapM fun i => Command.liftCoreM (realizeGlobalConstNoOverload i) - let τ := mkIdent `τ - let tds ← Command.liftTermElabM (gather family τ) - for d in (← mkInductives tds τ) do elabCommand d - for d in (← mkDeriveInstances tds) do elabCommand d - for d in (← mkRootTag tds) do elabCommand d - for d in (← mkErase tds) do elabCommand d - for d in (← mkTag tds) do elabCommand d - for d in (← mkFoldTags tds) do elabCommand d - for d in (← mkWF tds) do elabCommand d - for d in (← mkNarrow tds) do elabCommand d - for d in (← mkTagRootTagPost tds) do elabCommand d - for d in (← mkTagLe tds) do elabCommand d - for d in (← mkTagWf tds) do elabCommand d - for d in (← mkNarrowErase tds) do elabCommand d - | _ => throwUnsupportedSyntax - -end Spa.DeriveTagged diff --git a/lean/Spa/Language/Tagged/Graphs.lean b/lean/Spa/Language/Tagged/Graphs.lean deleted file mode 100644 index 88353b1..0000000 --- a/lean/Spa/Language/Tagged/Graphs.lean +++ /dev/null @@ -1,104 +0,0 @@ -import Spa.Language -import Spa.Language.Graphs -import Spa.Language.Tagged.Basic -import Spa.Language.Tagged.Properties - -namespace Spa - -open GGraph - -def Stmt.Tagged.cfg {τ : Type} : Stmt.Tagged τ → GGraph (Option (BasicStmt.Tagged τ)) - | .basic _ bs => GGraph.singleton (some bs) - | .andThen _ s₁ s₂ => s₁.cfg ⤳ s₂.cfg - | .ifElse _ _ s₁ s₂ => s₁.cfg ∙ s₂.cfg - | .whileLoop _ _ s => GGraph.loop s.cfg - -theorem Stmt.Tagged.cfg_graph {τ : Type} : ∀ (t : Stmt.Tagged τ), - (Option.map BasicStmt.Tagged.erase) <$> t.cfg = t.erase.cfg - | .basic _ bs => by simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, BasicStmt.Tagged.erase] - | .andThen _ s₁ s₂ => by - simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂] - | .ifElse _ _ s₁ s₂ => by - simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂] - | .whileLoop _ _ s => by - simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s] - -def GGraph.nodeLabel {τ : Type} (g : GGraph (Option (BasicStmt.Tagged τ))) (i : g.Index) : - Option τ := - (g.nodes i).map BasicStmt.Tagged.rootTag - -def GGraph.stateOf {τ : Type} [DecidableEq τ] (g : GGraph (Option (BasicStmt.Tagged τ))) - (id : τ) : Option g.Index := - g.indices.find? (fun i => decide (g.nodeLabel i = some id)) - -theorem GGraph.stateOf_label {τ : Type} [DecidableEq τ] - {g : GGraph (Option (BasicStmt.Tagged τ))} {id : τ} - {i : g.Index} (h : g.stateOf id = some i) : g.nodeLabel i = some id := by - rw [GGraph.stateOf] at h - simpa using List.find?_some h - -namespace Program - -variable (p : Program) - -def tagged : Stmt.Tagged RawId := tagStmt p.rootStmt - -def size : ℕ := p.tagged.rootTag.post + 1 - -theorem size_pos : 0 < p.size := Nat.succ_pos _ - -abbrev NodeId : Type := Fin p.size - -theorem tagged_wf : p.tagged.WF := Stmt.tag_wf p.rootStmt 0 - -def taggedFin : Stmt.Tagged p.NodeId := - p.tagged.narrow (Nat.lt_succ_self _) p.tagged_wf - -def taggedCfg : GGraph (Option (BasicStmt.Tagged p.NodeId)) := - GGraph.wrap p.taggedFin.cfg - -theorem taggedCfg_erase : - (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = p.cfg := by - rw [taggedCfg, GGraph.map_wrap, Stmt.Tagged.cfg_graph, taggedFin, - Stmt.Tagged.narrow_erase, tagged, erase_tagStmt] - rfl - -theorem taggedCfg_size : p.taggedCfg.size = p.cfg.size := by - conv_rhs => rw [← p.taggedCfg_erase] - rfl - -def nodeIdOf (s : p.State) : Option p.NodeId := - p.taggedCfg.nodeLabel (Fin.cast p.taggedCfg_size.symm s) - -def stateOfNodeId (id : p.NodeId) : Option p.State := - (p.taggedCfg.stateOf id).map (Fin.cast p.taggedCfg_size) - -theorem cfg_nodes_eq (s : p.State) : - p.cfg.nodes s = Option.map BasicStmt.Tagged.erase - (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) := by - have key : ∀ (g : Graph) (hsz : p.taggedCfg.size = g.size), - (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = g → - ∀ i : Fin g.size, - g.nodes i = Option.map BasicStmt.Tagged.erase - (p.taggedCfg.nodes (Fin.cast hsz.symm i)) := by - intro g hsz hg i - subst hg - rfl - exact key p.cfg p.taggedCfg_size p.taggedCfg_erase s - -theorem nodeIdOf_isSome_of_code {s : p.State} {bs : BasicStmt} - (h : p.code s = some bs) : (p.nodeIdOf s).isSome = true := by - have hc : Option.map BasicStmt.Tagged.erase - (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) = some bs := by - rw [← p.cfg_nodes_eq s]; exact h - unfold Program.nodeIdOf GGraph.nodeLabel - cases hcase : p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s) with - | none => rw [hcase] at hc; simp at hc - | some tbs => simp - -def nodeIdOfNonempty (s : p.State) {bs : BasicStmt} (h : p.code s = some bs) : p.NodeId := - (p.nodeIdOf s).get (p.nodeIdOf_isSome_of_code h) - -end Program - -end Spa diff --git a/lean/Spa/Language/Tagged/Id.lean b/lean/Spa/Language/Tagged/Id.lean deleted file mode 100644 index 06b658a..0000000 --- a/lean/Spa/Language/Tagged/Id.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Mathlib.Data.Nat.Notation - -namespace Spa - -structure RawId where - post : ℕ - deriving DecidableEq, Repr - -end Spa diff --git a/lean/Spa/Language/Tagged/Properties.lean b/lean/Spa/Language/Tagged/Properties.lean deleted file mode 100644 index efe7d94..0000000 --- a/lean/Spa/Language/Tagged/Properties.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Spa.Language.Tagged.Basic - -namespace Spa - -@[simp] theorem Expr.erase_tag (e : Expr) (n : ℕ) : (e.tag n).1.erase = e := by - induction e generalizing n with - | add a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb] - | sub a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb] - | var x => simp [Expr.tag, Expr.Tagged.erase] - | num k => simp [Expr.tag, Expr.Tagged.erase] - -@[simp] theorem BasicStmt.erase_tag (bs : BasicStmt) (n : ℕ) : - (bs.tag n).1.erase = bs := by - cases bs with - | assign x e => simp [BasicStmt.tag, BasicStmt.Tagged.erase] - | noop => simp [BasicStmt.tag, BasicStmt.Tagged.erase] - -@[simp] theorem Stmt.erase_tag (s : Stmt) (n : ℕ) : (s.tag n).1.erase = s := by - induction s generalizing n with - | basic bs => simp [Stmt.tag, Stmt.Tagged.erase] - | andThen a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb] - | ifElse e a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb] - | whileLoop e s ih => simp [Stmt.tag, Stmt.Tagged.erase, ih] - -/-- Erasing a freshly tagged program recovers it. -/ -theorem erase_tagStmt (s : Stmt) : (tagStmt s).erase = s := by - simp [tagStmt] - -end Spa