From 2c2aa71fa0533dce4802bdfa949b3b09505d83ea Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 13:33:05 -0700 Subject: [PATCH 1/8] DDM: fix passthrough for fn rules with leading implicit Type params MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit translateSyntaxDef collapsed any single-ident syntax to .passthrough, but the parser path (Parser.opSyntaxParser) hardcodes the passthrough's target as argDecls[0]. For rules like fn matchExprArms_one (tp : Type, a : MatchExprArm tp) : MatchExprArms tp => a; the actual target is argDecls[1] (because tp is an implicit type parameter at index 0). Passthrough sent the parser to argDecls[0], which is the implicit Type slot, producing nonsensical syntax trees and triggering parsing-ambiguity panics in elabExpr. Fix: only enable passthrough when the single ident references argDecls[0]. Otherwise emit .std atoms prec — the parser will route through liftToKind with the correct ident index. --- Strata/DDM/Elab/DialectM.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Strata/DDM/Elab/DialectM.lean b/Strata/DDM/Elab/DialectM.lean index 54bd169f37..98101c2bfa 100644 --- a/Strata/DDM/Elab/DialectM.lean +++ b/Strata/DDM/Elab/DialectM.lean @@ -614,11 +614,16 @@ def translateSyntaxDef {argc} (argDecls : ArgDeclsMap argc) (mdTree tree : Tree) logError argDecls.decls[i].nameLoc s!"Argument is not elaborated." return default - -- Use passthrough for single-ident syntax without explicit precedence. - -- This runs after the argument-usage check so that polymorphic operators - -- with inferred type parameters are validated before simplification. + -- Passthrough only when the single ident is `argDecls[0]`: the + -- parser path hardcodes `[.ident 0 0]`, so other slots (e.g. when + -- leading args are implicit Type params) must take the `.std` path. if !hasExplicitPrec && singleAtomKind matches .ident then - return .passthrough + if h : atoms.size = 1 then + match atoms[0] with + | .ident 0 _ => return .passthrough + | _ => pure () + else + pure () return .std atoms prec From 85214ef4b276237ed05fd0a343ddb03ad986fede Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 13:33:46 -0700 Subject: [PATCH 2/8] DDM: fold result-type bvars into usedArgs translateSyntaxDef now also folds bound type variables in the result type into the implicit-arg map, so e.g. fn match_expr (dt : Type, tp : Type, scrut : dt, ..., body : tp) : tp => "match " scrut " { ... " body " ... }"; is accepted: `tp` is reachable through both `body : tp` (already worked) and the result `: tp` (new). Matches the existing convention that implicit type params must appear *somewhere* in the rule's signature. --- Strata/DDM/Elab/DialectM.lean | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/Strata/DDM/Elab/DialectM.lean b/Strata/DDM/Elab/DialectM.lean index 98101c2bfa..eabd8c3cb6 100644 --- a/Strata/DDM/Elab/DialectM.lean +++ b/Strata/DDM/Elab/DialectM.lean @@ -552,7 +552,8 @@ private def classifySyntaxArgs (args : Array Tree) : SingleAtomKind := | _ => .standard else .standard -def translateSyntaxDef {argc} (argDecls : ArgDeclsMap argc) (mdTree tree : Tree) : ElabM SyntaxDef := do +def translateSyntaxDef {argc} (argDecls : ArgDeclsMap argc) (mdTree tree : Tree) + (resultType? : Option PreType := none) : ElabM SyntaxDef := do let (syntaxMetadata, success) ← runChecked <| translateOptMetadata! argDecls mdTree if !success then return default @@ -608,6 +609,17 @@ def translateSyntaxDef {argc} (argDecls : ArgDeclsMap argc) (mdTree tree : Tree) if !success then return default + -- Type variables in the result type are inferable from invocation + -- context, so they count as used even when the production omits + -- them (e.g. `fn match_expr (... tp : Type, ...) : tp`). + match resultType? with + | some result => + usedArgs := result.foldBoundTypeVars usedArgs fun s idx => + if idx < argDecls.decls.size then + s.insert (argDecls.decls.size - 1 - idx) .implicit + else s + | none => pure () + -- Check every argument is used (including implicitly inferred type params). for i in Fin.range argDecls.decls.size do if i.val ∉ usedArgs then @@ -849,7 +861,9 @@ def elabFnCommand : DialectElab := fun tree => do let opMdTree := tree[4] let opStxTree := tree[5] - let (opStx, stxSuccess) ← runElab <| runChecked <| translateSyntaxDef argDeclsMap opMdTree opStxTree + let (opStx, stxSuccess) ← runElab <| runChecked <| + translateSyntaxDef argDeclsMap opMdTree opStxTree + (resultType? := if resultSuccess then some result else none) if !stxSuccess then return From bb56d7a632c208e73717bd19b5d413de835db356 Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 14:45:26 -0700 Subject: [PATCH 3/8] CoreMatch: add intermediate AST and Core lowering MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lays the programmatic foundation for the dialect. Two modules: * `Strata/Languages/CoreMatch/CoreMatch.lean` — the `MExpr` / `MArm` / `MStmt` / `MStmtArm` / `MFunction` / `MProcedure` / `MDecl` / `MProgram` types. Constructor arms carry a *pre-curried case function* `caseFn = λb₁:T₁. … λbₖ:Tₖ. body` in de Bruijn form, and statement-level arms carry pre-lowered bodies that already include the `var b : T := D..f(scrut);` binder inits. Both choices let the lowering pass collapse to a single straightforward translation. * `Strata/Languages/CoreMatch/ToCore.lean` — lowering an `MProgram` to a `Core.Program`. Expression-level matches lower to `D$Elim scrut case₁ … caseₙ` with cases reordered into the datatype's declaration order; constructors with no explicit arm fall through to the wildcard arm (padded with `λ_:T.` lambdas to match arity), or to a `__coreMatch_missing_` sentinel fvar when no wildcard is present (unreachable when the redundancy checker has run). Statement matches lower to a nested-if chain over the auto-generated testers `D..isCᵢ`; uncovered constructors fall through to the wildcard arm or to `assert false` with a `coreMatch_nonexhaustive` label. This commit is self-contained: no DDM grammar, no source parser, no verifier integration. The next commits add the redundancy checker (ArmCheck) and the source pipeline. --- Strata.lean | 2 + Strata/Languages/CoreMatch/CoreMatch.lean | 105 ++++++++++++++ Strata/Languages/CoreMatch/ToCore.lean | 169 ++++++++++++++++++++++ 3 files changed, 276 insertions(+) create mode 100644 Strata/Languages/CoreMatch/CoreMatch.lean create mode 100644 Strata/Languages/CoreMatch/ToCore.lean diff --git a/Strata.lean b/Strata.lean index ee70beef36..da0a7072cd 100644 --- a/Strata.lean +++ b/Strata.lean @@ -40,6 +40,8 @@ import Strata.Languages.Boole.Boole import Strata.Languages.Boole.Verify import Strata.Languages.C_Simp.C_Simp import Strata.Languages.C_Simp.Verify +import Strata.Languages.CoreMatch.CoreMatch +import Strata.Languages.CoreMatch.ToCore import Strata.Languages.Core.EntryPoint import Strata.Languages.Core.VerifierProofs import Strata.Languages.Dyn.Dyn diff --git a/Strata/Languages/CoreMatch/CoreMatch.lean b/Strata/Languages/CoreMatch/CoreMatch.lean new file mode 100644 index 0000000000..2ec8feaa83 --- /dev/null +++ b/Strata/Languages/CoreMatch/CoreMatch.lean @@ -0,0 +1,105 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.Core.Expressions +public import Strata.Languages.Core.Identifiers +public import Strata.Languages.Core.Statement +public import Strata.Languages.Core.Procedure +public import Strata.Languages.Core.Function +public import Strata.Languages.Core.TypeDecl +public import Strata.Languages.Core.Program + +/-! +CoreMatch's intermediate representation. The translator emits values +of these types; `ToCore` lowers them to plain `Core.Program`. +-/ + +namespace Strata.CoreMatch + +open Core Lambda + +public section + +mutual + +inductive MExpr where + | core (e : Core.Expression.Expr) + | matchE (scrut : MExpr) (dtName : String) (arms : List MArm) + deriving Inhabited + +/-- +Expression-level match arm. Constructor arms carry a pre-curried case +function `caseFn = λb₁:T₁. … λbₖ:Tₖ. body` in de Bruijn form, ready +to be passed straight to the eliminator. Wildcard arm bodies must be +closed; compilation pads them per uncovered constructor. +-/ +inductive MArm where + | ctor (ctor : String) (caseFn : MExpr) : MArm + | wild (body : MExpr) : MArm + deriving Inhabited + +end + +/-- +Statement-level match arm. The body already includes the +`var b : T := D..f(scrut);` binder-init statements; lowering only +threads the scrutinee through the testers. +-/ +inductive MStmtArm : Type where + | ctor (ctor : String) (body : List Core.Statement) : MStmtArm + | wild (body : List Core.Statement) : MStmtArm + deriving Inhabited + +inductive MStmt : Type where + | core (s : Core.Statement) : MStmt + | matchStmt (scrutinee : Core.Expression.Expr) + (dtName : String) + (arms : List MStmtArm) + : MStmt + +@[expose] abbrev MStmts := List MStmt + +@[expose] def MStmt.ofCore (s : Core.Statement) : MStmt := .core s + +@[expose] def MStmts.ofCore (ss : List Core.Statement) : MStmts := + ss.map MStmt.ofCore + +@[expose] def MExpr.ofCore (e : Core.Expression.Expr) : MExpr := .core e + +structure MFunction where + name : Core.Expression.Ident + typeArgs : List Lambda.TyIdentifier := [] + inputs : List (Core.CoreIdent × Lambda.LMonoTy) + output : Lambda.LMonoTy + body : Option MExpr := none + deriving Inhabited + +structure MProcedure where + header : Core.Procedure.Header + spec : Core.Procedure.Spec := default + body : List MStmt := [] + deriving Inhabited + +inductive MDecl where + | type (t : Core.TypeDecl) (md : Imperative.MetaData Core.Expression) + | ax (a : Core.Axiom) (md : Imperative.MetaData Core.Expression) + | distinct (name : Core.Expression.Ident) + (es : List Core.Expression.Expr) + (md : Imperative.MetaData Core.Expression) + | proc (d : MProcedure) (md : Imperative.MetaData Core.Expression) + | func (f : MFunction) (md : Imperative.MetaData Core.Expression) + deriving Inhabited + +@[expose] abbrev MDecls := List MDecl + +structure MProgram where + decls : MDecls := [] + deriving Inhabited + +end + +end Strata.CoreMatch diff --git a/Strata/Languages/CoreMatch/ToCore.lean b/Strata/Languages/CoreMatch/ToCore.lean new file mode 100644 index 0000000000..6ed921b118 --- /dev/null +++ b/Strata/Languages/CoreMatch/ToCore.lean @@ -0,0 +1,169 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.Core.Statement +public import Strata.Languages.Core.Expressions +public import Strata.Languages.Core.Procedure +public import Strata.Languages.Core.Function +public import Strata.Languages.Core.TypeDecl +public import Strata.Languages.Core.Program +public import Strata.DL.Lambda.LExpr +public import Strata.DL.Util.Map + +/-! +Lower CoreMatch's intermediate representation to plain `Core.Program`. +Expression-level matches lower to applications of the auto-generated +structural eliminator `D$Elim`; statement-level matches lower to a +nested `if` chain over the auto-generated testers `D..isCᵢ`. +-/ + +namespace Strata.CoreMatch.ToCore + +open Core Lambda Imperative +open Strata.CoreMatch + +public section + +@[expose] def elimName (datatype : String) : String := datatype ++ "$Elim" +@[expose] def testerName (datatype ctor : String) : String := datatype ++ "..is" ++ ctor +@[expose] def accessorName (datatype field : String) : String := datatype ++ ".." ++ field + +def opE (name : String) : Core.Expression.Expr := + LExpr.op () ⟨name, ()⟩ none + +def applyAll (head : Core.Expression.Expr) + (args : List Core.Expression.Expr) : Core.Expression.Expr := + args.foldl (fun acc a => LExpr.app () acc a) head + +@[expose] +def findDatatype (decls : List Core.Decl) (name : String) + : Option (LDatatype Unit) := Id.run do + for d in decls do + if let .type (.data block) _ := d then + for dt in block do + if dt.name == name then return some dt + return none + +/-- +Sentinel emitted in the case slot for a constructor that has no +matching arm. Unreachable when the redundancy checker has run; if +emitted it surfaces downstream as an unbound symbol. +-/ +def missingArmPlaceholder (ctor : String) : Core.Expression.Expr := + LExpr.fvar () ⟨"__coreMatch_missing_" ++ ctor, ()⟩ none + +def padToCtorArity (c : LConstr Unit) (body : Core.Expression.Expr) + : Core.Expression.Expr := + LExpr.absMulti () (c.args.map (·.2)) body + +@[expose] +partial def compileMExprWith + (lookup : String → Option (LDatatype Unit)) + (e : MExpr) : Core.Expression.Expr := + match e with + | .core e0 => e0 + | .matchE scrut dtName arms => + let scrutE := compileMExprWith lookup scrut + match lookup dtName with + | none => LExpr.fvar () ⟨"__coreMatch_unknown_dt_" ++ dtName, ()⟩ none + | some dt => + let ctorMap : Map String MExpr := Map.ofList <| arms.filterMap fun + | .ctor c f => some (c, f) | .wild _ => none + let wild? : Option MExpr := + arms.findSome? fun | .wild b => some b | _ => none + let caseFor (c : LConstr Unit) : Core.Expression.Expr := + match ctorMap.find? c.name.name with + | some f => compileMExprWith lookup f + | none => + match wild? with + | some b => padToCtorArity c (compileMExprWith lookup b) + | none => missingArmPlaceholder c.name.name + applyAll (opE (elimName dtName)) (scrutE :: dt.constrs.map caseFor) + +@[expose] +def compileMExpr (decls : List Core.Decl) (e : MExpr) : Core.Expression.Expr := + compileMExprWith (findDatatype decls) e + +def mkTesterApp (dtName ctor : String) + (scrut : Core.Expression.Expr) : Core.Expression.Expr := + LExpr.app () (opE (testerName dtName ctor)) scrut + +def stmtsBlockOrSingle : List Core.Statement → Core.Statement + | [s] => s + | ss => Imperative.Stmt.block "" ss {} + +def assertFalse (label : String) : Core.Statement := + Core.Statement.assert label (LExpr.const () (LConst.boolConst false)) {} + +@[expose] +def compileMatchArms + (scrut : Core.Expression.Expr) + (dtName : String) + (dt : LDatatype Unit) + (arms : List MStmtArm) : Core.Statement := + let armMap : Map String (List Core.Statement) := Map.ofList <| arms.filterMap fun + | .ctor c body => some (c, body) | .wild _ => none + let wildcard? := arms.findSome? fun | .wild body => some body | _ => none + let fallback := wildcard?.getD [assertFalse "coreMatch_nonexhaustive"] + dt.constrs.foldr (init := stmtsBlockOrSingle fallback) fun c acc => + Imperative.Stmt.ite + (Imperative.ExprOrNondet.det (mkTesterApp dtName c.name.name scrut)) + ((armMap.find? c.name.name).getD fallback) + [acc] {} + +@[expose] +def compileMStmt (decls : List Core.Decl) : MStmt → List Core.Statement + | .core c => [c] + | .matchStmt scrut dtName arms => + match findDatatype decls dtName with + | none => [assertFalse ("coreMatch_unknown_dt_" ++ dtName)] + | some dt => [compileMatchArms scrut dtName dt arms] + +@[expose] +def compileMStmts (decls : List Core.Decl) (ss : List MStmt) + : List Core.Statement := + ss.flatMap (compileMStmt decls) + +@[expose] +def compileFunction (decls : List Core.Decl) (f : MFunction) : Core.Function := + { name := f.name + typeArgs := f.typeArgs + inputs := f.inputs + output := f.output + body := f.body.map (compileMExpr decls) + attr := #[] + concreteEval := none + axioms := [] + preconditions := [] + isConstr := false } + +@[expose] +def compileProcedure (decls : List Core.Decl) (p : MProcedure) : Core.Procedure := + { header := p.header + spec := p.spec + body := compileMStmts decls p.body } + +@[expose] +def compileDecl (decls : List Core.Decl) (d : MDecl) : Core.Decl := + match d with + | .type t md => .type t md + | .ax a md => .ax a md + | .distinct n e md => .distinct n e md + | .proc p md => .proc (compileProcedure decls p) md + | .func f md => .func (compileFunction decls f) md + +@[expose] +def compileProgram (p : MProgram) : Core.Program := + let decls : List Core.Decl := + p.decls.foldl (init := []) fun acc d => + acc ++ [compileDecl acc d] + { decls := decls } + +end + +end Strata.CoreMatch.ToCore From ee4715848ae6bf2aa9f2ceb8b6189eca352271e4 Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 14:45:59 -0700 Subject: [PATCH 4/8] CoreMatch: add redundancy and exhaustiveness checker MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Strata/Languages/CoreMatch/ArmCheck.lean` — a small pure module that inspects a list of arm "keys" against a datatype's constructor list and reports any of: * `unknownConstructor` — constructor name not in the datatype * `duplicateConstructor` — same constructor named twice * `multipleWildcards` — more than one `_ => …` arm * `redundantWildcard` — wildcard appears though every constructor is already covered explicitly * `nonExhaustive` — at least one constructor has no arm and there's no wildcard `ArmKey = Option String` is a deliberately abstract view of an arm (`some ctor` or `none` for a wildcard) so the checker is shape- independent: both the expression-level `MArm` and statement-level `MStmtArm` project to it via `MArm.key` / `MStmtArm.key` and run through the same `checkAgainst`. The checker doesn't depend on the source pipeline; it can be called on hand-built `MProgram`s as well, which is why it lands separately from the DDM-side translator. --- Strata/Languages/CoreMatch/ArmCheck.lean | 82 ++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 Strata/Languages/CoreMatch/ArmCheck.lean diff --git a/Strata/Languages/CoreMatch/ArmCheck.lean b/Strata/Languages/CoreMatch/ArmCheck.lean new file mode 100644 index 0000000000..d6a775d8e3 --- /dev/null +++ b/Strata/Languages/CoreMatch/ArmCheck.lean @@ -0,0 +1,82 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.Core.TypeDecl +public import Strata.DL.Lambda.TypeFactory + +/-! +Redundancy and exhaustiveness checking for `match` arms. The check +is shared between expression-level and statement-level matches via +the `ArmKey` projection. +-/ + +namespace Strata.CoreMatch.ArmCheck + +open Strata.CoreMatch Lambda + +public section + +inductive ArmIssue where + | unknownConstructor (name : String) + | duplicateConstructor (name : String) + | multipleWildcards + | redundantWildcard + | nonExhaustive (missing : List String) + deriving Repr, BEq + +@[expose] +def ArmIssue.format : ArmIssue → String + | .unknownConstructor n => s!"unknown constructor '{n}' in match arm" + | .duplicateConstructor n => s!"duplicate match arm for constructor '{n}'" + | .multipleWildcards => "match has more than one wildcard arm" + | .redundantWildcard => "wildcard arm is redundant: every constructor is covered explicitly" + | .nonExhaustive missing => s!"non-exhaustive match: no arm for constructors: {missing}" + +/-- An arm projected to its identity for checking: `some ctor` for a +constructor arm, `none` for a wildcard. -/ +@[expose] abbrev ArmKey := Option String + +/-- Check a match's arms against the scrutinee datatype's +constructors. `ctorNames` must be in declaration order; `keys` in +source order. -/ +@[expose] +def checkAgainst (ctorNames : List String) (keys : List ArmKey) : List ArmIssue := Id.run do + let mut issues : List ArmIssue := [] + let mut seen : List String := [] + let mut wildcards : Nat := 0 + for key in keys do + match key with + | none => + wildcards := wildcards + 1 + if wildcards > 1 then issues := .multipleWildcards :: issues + | some n => + if !ctorNames.contains n then issues := .unknownConstructor n :: issues + else if seen.contains n then issues := .duplicateConstructor n :: issues + else seen := n :: seen + let missing := ctorNames.filter (!seen.contains ·) + if wildcards > 0 then + if missing.isEmpty then issues := .redundantWildcard :: issues + else + if !missing.isEmpty then issues := .nonExhaustive missing :: issues + return issues.reverse + +@[expose] +def check (dt : LDatatype Unit) (keys : List ArmKey) : List ArmIssue := + checkAgainst (dt.constrs.map (·.name.name)) keys + +@[expose] +def MArm.key : MArm → ArmKey + | .ctor c _ => some c | .wild _ => none + +@[expose] +def MStmtArm.key : MStmtArm → ArmKey + | .ctor c _ => some c | .wild _ => none + +end + +end Strata.CoreMatch.ArmCheck From 2e54b157a244b2ef17479167cc61cd6f88ecd934 Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 14:46:59 -0700 Subject: [PATCH 5/8] CoreMatch: add DDM grammar, source translator, and pipeline entry points MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The source-side of the dialect, on top of the AST, lowering, and ArmCheck modules from the previous two commits. * `DDMTransform/Grammar.lean` declares the `CoreMatch` dialect (which imports `Core`) and the surface syntax for `match`: - statement form `match scrut { Ctor(v:T,…) => { … } … }` for procedure bodies - expression form `match scrut { arm Ctor(v:T,…) => body; … }` for function bodies, with a head-arm body surfaced as a direct `tp`-typed argument so DDM's type inference fixes the result type from the user's first body, plus a tail-arm-list category whose bodies are typed `Expr` (re-checked by the translator) - the `arm` keyword anchors each tail arm against parser ambiguity with Core operators - both forms share the `match` keyword; the parser dispatches by category (Statement vs Expr) so the two never compete * `DDMTransform/StrataGen.lean` runs `#strata_gen CoreMatch` to produce the typed `CoreMatchDDM.*` AST. * `DDMTransform/Translate.lean` walks the typed `CoreMatchDDM.Program` and emits an `MProgram`. Tracks `bvars`, `tyBVars`, datatype ctor info, label counters, and a `currentRecFns` / `recRewrite` state used by the rec-call rewrite for natural-style structural recursion. Detects two arm shapes (`natural`, `cata`, `unknown`) via `classifyArm`, rewrites self-calls `f(field)` into sentinel fvars during arm body translation, then resolves the sentinels to the eliminator's rec-result bvars at the absMulti wrapping step. Non-structural self-references (bare references, calls on non-recursive arguments) are rejected with a clear diagnostic. * `Verify.lean` exposes `toCore` (programmatic) and `parseToCore` (source) entry points for the dialect. `Strata.lean` registers the three new modules. --- Strata.lean | 3 + .../CoreMatch/DDMTransform/Grammar.lean | 80 ++++++++ .../CoreMatch/DDMTransform/StrataGen.lean | 18 ++ .../CoreMatch/DDMTransform/Translate.lean | 19 ++ .../DDMTransform/Translate/Basic.lean | 143 ++++++++++++++ .../DDMTransform/Translate/Datatypes.lean | 78 ++++++++ .../DDMTransform/Translate/Decls.lean | 187 ++++++++++++++++++ .../DDMTransform/Translate/Expressions.lean | 137 +++++++++++++ .../DDMTransform/Translate/NaturalCata.lean | 113 +++++++++++ .../DDMTransform/Translate/Statements.lean | 132 +++++++++++++ .../DDMTransform/Translate/Types.lean | 69 +++++++ Strata/Languages/CoreMatch/Verify.lean | 40 ++++ 12 files changed, 1019 insertions(+) create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Grammar.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/StrataGen.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Basic.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Datatypes.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Decls.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Expressions.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/NaturalCata.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Statements.lean create mode 100644 Strata/Languages/CoreMatch/DDMTransform/Translate/Types.lean create mode 100644 Strata/Languages/CoreMatch/Verify.lean diff --git a/Strata.lean b/Strata.lean index da0a7072cd..9a1cdc6a8c 100644 --- a/Strata.lean +++ b/Strata.lean @@ -42,6 +42,9 @@ import Strata.Languages.C_Simp.C_Simp import Strata.Languages.C_Simp.Verify import Strata.Languages.CoreMatch.CoreMatch import Strata.Languages.CoreMatch.ToCore +import Strata.Languages.CoreMatch.Verify +import Strata.Languages.CoreMatch.DDMTransform.StrataGen +import Strata.Languages.CoreMatch.DDMTransform.Translate import Strata.Languages.Core.EntryPoint import Strata.Languages.Core.VerifierProofs import Strata.Languages.Dyn.Dyn diff --git a/Strata/Languages/CoreMatch/DDMTransform/Grammar.lean b/Strata/Languages/CoreMatch/DDMTransform/Grammar.lean new file mode 100644 index 0000000000..ec8417128b --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Grammar.lean @@ -0,0 +1,80 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.Core.DDMTransform.Grammar +meta import Strata.DDM.Integration.Lean + +namespace Strata + +set_option maxRecDepth 10000 +set_option maxHeartbeats 400000 + +#dialect +dialect CoreMatch; + +import Core; + +category MatchPatVar; +@[declare(v, tp)] +op matchPatVar_typed (v : Ident, tp : Type) : MatchPatVar => v " : " tp; + +category MatchPatVars; +op matchPatVars_nil () : MatchPatVars => ; +@[scope(v)] +op matchPatVars_one (v : MatchPatVar) : MatchPatVars => v; +@[scope(v)] +op matchPatVars_cons (vs : MatchPatVars, @[scope(vs)] v : MatchPatVar) : MatchPatVars => + vs ", " v; + +category MatchPat; +@[scope(vs)] +op matchPat_ctor (ctor : Ident, vs : MatchPatVars) : MatchPat => + ctor "(" vs ")"; +op matchPat_wild () : MatchPat => "_"; + +category MatchStmtArm; +op matchStmtArm_mk (p : MatchPat, @[scope(p)] body : Block) : MatchStmtArm => + p " => " body:0; + +category MatchStmtArms; +op matchStmtArms_nil () : MatchStmtArms => ; +op matchStmtArms_cons (arm : MatchStmtArm, arms : MatchStmtArms) : MatchStmtArms => + arm "\n " arms:0; + +op match_statement (dt : Type, scrutinee : dt, arms : MatchStmtArms) : Statement => + "match " scrutinee " {\n " arms "\n}"; + +// Expression-level match. The head arm is surfaced separately so its +// body type pins the result type `tp`; tail arms then carry untyped +// `Expr` bodies. The `arm` keyword anchors tail arms against +// ambiguity with Core operators. +category MatchExprTailArm; +category MatchExprTailArmList; + +op matchExprTailArm_mk (p : MatchPat, @[scope(p)] body : Expr) : MatchExprTailArm => + "arm " p " => " body:0 ";"; + +op matchExprTailArmList_nil () : MatchExprTailArmList => ; +op matchExprTailArmList_cons (a : MatchExprTailArm, as : MatchExprTailArmList) : + MatchExprTailArmList => + a "\n " as:0; + +// Shares the `match` keyword with `match_statement`; the parser +// dispatches by syntactic category (Statement vs Expr). +fn match_expr (dt : Type, tp : Type, scrut : dt, + headPat : MatchPat, @[scope(headPat)] headBody : tp, + tailArms : MatchExprTailArmList) : tp => + "match " scrut " {" "arm " headPat " => " headBody ";" tailArms "}"; + +category Program; +op prog (commands : SpacePrefixSepBy Command) : Program => + commands; + +#end + +end Strata + diff --git a/Strata/Languages/CoreMatch/DDMTransform/StrataGen.lean b/Strata/Languages/CoreMatch/DDMTransform/StrataGen.lean new file mode 100644 index 0000000000..56491f2596 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/StrataGen.lean @@ -0,0 +1,18 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Grammar +meta import Strata.DDM.Integration.Lean + +public section + +namespace Strata.CoreMatchDDM + +set_option maxHeartbeats 800000 in +#strata_gen CoreMatch + +end Strata.CoreMatchDDM diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate.lean new file mode 100644 index 0000000000..6289ef87b5 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate.lean @@ -0,0 +1,19 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Types +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Datatypes +public import Strata.Languages.CoreMatch.DDMTransform.Translate.NaturalCata +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Expressions +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Statements +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Decls + +/-! +Re-exports the public surface of the CoreMatch translator from the +sub-modules in `Translate/`. +-/ diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Basic.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Basic.lean new file mode 100644 index 0000000000..66a9bf89a7 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Basic.lean @@ -0,0 +1,143 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.DDM.AST +public import Strata.Languages.CoreMatch.DDMTransform.Grammar +public import Strata.Languages.CoreMatch.DDMTransform.StrataGen +public import Strata.Languages.Core.Expressions +public import Strata.DL.Lambda.LExpr + +/-! +Shared substrate for the rest of the translator: the `TransM` monad +and its state, scoped state combinators, and helpers that flatten +the DDM AST's cons-chain repetitions to plain `List`s. +-/ + +namespace Strata.CoreMatch.Translate + +open Std (HashMap) +open Strata +open Lambda Imperative +open Lean.Parser + +public section + +open Strata.CoreMatchDDM + +/-- Cached `(constructorName, [fieldName, …])` for one datatype. -/ +abbrev DatatypeInfo := List (String × List String) + +structure TransState where + /-- Source file name, threaded into diagnostic source ranges. -/ + fileName : String := "" + /-- DDM's flat symbol context, indexed by `FreeVarIndex`. -/ + gctx : GlobalContext := {} + /-- For each entry of `gctx.vars`: `true` if it resolves as + `LExpr.op` (function/constant), `false` for a term-level fvar. + Computed once by `initFVarIsOp`. -/ + fvarIsOp : Array Bool := #[] + /-- Type-level binders, innermost last. -/ + tyBVars : Array String := #[] + /-- Term-level binders, innermost last. A slot holds either a + pre-built reference (procedure input, let-bound variable) or an + `LExpr.bvar 0` placeholder for a match-arm binder; `getBVarExpr` + distinguishes the two cases. -/ + bvars : Array Core.Expression.Expr := #[] + /-- Datatypes accumulated during the declaration walk. -/ + datatypes : HashMap String DatatypeInfo := {} + /-- Counter for synthesised assert/assume/spec labels. -/ + labelCounter : Nat := 0 + /-- Names of functions in the enclosing `rec function` block. + Self-references in their match arms get rewritten via + `recRewrites`; empty outside such a block. -/ + recFns : List String := [] + /-- Maps `(recFnName, bottomRelativeFieldPos)` to the rec-result + slot index in the case lambda. Consulted by `tryRecRewrite` to + spot natural-style self-calls. -/ + recRewrites : HashMap (String × Nat) Nat := {} + deriving Inhabited + +abbrev TransM := StateT TransState (Except DiagnosticModel) + +def mkIdent (name : String) : Core.Expression.Ident := ⟨name, ()⟩ + +def throwAt (range : SourceRange) (msg : String) : TransM α := do + throw <| .withRange ⟨⟨(← StateT.get).fileName⟩, range⟩ msg + +/-- Run `k` after mutating the field selected by `(get, set)`, +restoring the original value whether or not `k` throws. -/ +def withSaved + (get : TransState → β) (set : TransState → β → TransState) (mutate : β → β) + (k : TransM α) : TransM α := do + let old := get (← StateT.get) + modify (set · (mutate old)) + try + let result ← k + modify (set · old) + return result + catch e => + modify (set · old) + throw e + +def withTypeBVars (xs : List String) : TransM α → TransM α := + withSaved (·.tyBVars) ({ · with tyBVars := · }) (· ++ xs.toArray) + +def withBVarExprs (xs : Array Core.Expression.Expr) : TransM α → TransM α := + withSaved (·.bvars) ({ · with bvars := · }) (· ++ xs) + +/-- Push binders that the body should reference as `LExpr.fvar`s +(procedure inputs, let-bound variables). -/ +def withBVars (xs : List String) : TransM α → TransM α := + withBVarExprs (xs.toArray.map fun n => .fvar () (mkIdent n) none) + +/-- Push binders that the body will reference as `LExpr.bvar`s, used +when the body will be wrapped in `absMulti` afterwards. The stored +`bvar 0` is just a tag; the real de Bruijn index is derived from the +slot's stack position by `getBVarExpr`. -/ +def withBoundBVars (xs : List String) : TransM α → TransM α := + withBVarExprs (xs.toArray.map fun _ => .bvar () 0) + +def withRecFns (fns : List String) : TransM α → TransM α := + withSaved (·.recFns) ({ · with recFns := · }) (fun _ => fns) + +def withRecRewrites (entries : List ((String × Nat) × Nat)) + : TransM α → TransM α := + withSaved (·.recRewrites) ({ · with recRewrites := · }) fun m => + entries.foldl (fun m (k, v) => m.insert k v) m + +def bindingsToList : Bindings SourceRange → List (Binding SourceRange) + | .mkBindings _ ⟨_, xs⟩ => xs.toList + +def bindingName : Binding SourceRange → String + | .mkBinding _ ⟨_, n⟩ _ + | .outBinding _ ⟨_, n⟩ _ + | .inoutBinding _ ⟨_, n⟩ _ + | .casesBinding _ ⟨_, n⟩ _ => n + +def constructorListToList : + ConstructorList SourceRange → List (Constructor SourceRange) + | .constructorListAtom _ c => [c] + | .constructorListPush _ cs c => constructorListToList cs ++ [c] + +def matchPatVarsToList : + MatchPatVars SourceRange → List (MatchPatVar SourceRange) + | .matchPatVars_nil _ => [] + | .matchPatVars_one _ v => [v] + | .matchPatVars_cons _ vs v => matchPatVarsToList vs ++ [v] + +def matchStmtArmsToList : + MatchStmtArms SourceRange → List (MatchStmtArm SourceRange) + | .matchStmtArms_nil _ => [] + | .matchStmtArms_cons _ a as => a :: matchStmtArmsToList as + +def ctorFields : Constructor SourceRange → List (Binding SourceRange) + | .constructor_mk _ _ ⟨_, none⟩ => [] + | .constructor_mk _ _ ⟨_, some ⟨_, fs⟩⟩ => fs.toList + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Datatypes.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Datatypes.lean new file mode 100644 index 0000000000..e435745cd1 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Datatypes.lean @@ -0,0 +1,78 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.Core.TypeDecl +public import Strata.DL.Lambda.TypeFactory + +/-! +Datatype cache, derived `LDatatype` synthesis, and symbol resolution +against `TransState.gctx`. +-/ + +namespace Strata.CoreMatch.Translate + +open Lambda + +public section + +def addDatatype (n : String) (info : DatatypeInfo) : TransM Unit := + modify fun s => { s with datatypes := s.datatypes.insert n info } + +def lookupDatatype (n : String) : TransM (Option DatatypeInfo) := do + return (← StateT.get).datatypes.get? n + +def lookupCtor (dtName ctor : String) : TransM (Option (List String)) := do + return ((← lookupDatatype dtName) >>= (·.find? (·.1 == ctor))).map (·.2) + +/-- Synthesise an `LDatatype Unit` from cached info. Field types are +stubbed with `.int`: lowering and `ArmCheck` only inspect constructor +names and field counts, and user-visible field types come from each +arm's pattern binders. -/ +private def synthLDatatype (n : String) (info : DatatypeInfo) + : Except String (LDatatype Unit) := + match info with + | [] => .error s!"datatype '{n}' has no constructors" + | c :: rest => + let toConstr : String × List String → LConstr Unit := fun (cname, fields) => + { name := mkIdent cname + args := fields.map fun fn => (mkIdent fn, .int) + testerName := s!"{n}..is{cname}" } + .ok { name := n, typeArgs := [], + constrs := toConstr c :: rest.map toConstr, + constrs_ne := by simp } + +def lookupLDatatype (n : String) : TransM (LDatatype Unit) := do + match (← lookupDatatype n) with + | none => throw <| .fromMessage s!"match: datatype '{n}' is not declared" + | some info => + match synthLDatatype n info with + | .ok dt => return dt + | .error msg => throw <| .fromMessage s!"match: {msg}" + +def getFVarIsOp (i : Nat) : TransM Bool := do + let s ← StateT.get + match s.fvarIsOp[i]? with + | some b => return b + | none => + -- Fall back to inspecting the GlobalContext when the symbol is + -- outside the precomputed range (e.g. inherited via a dialect import). + return s.gctx.vars[i]? |>.any (·.2 matches .expr _) + +/-- Resolve a DDM bound variable. A pattern-binder slot stores +`bvar 0` as a tag and the de Bruijn index is derived from the slot's +stack position; any other slot stores a pre-built reference. -/ +def getBVarExpr (m : SourceRange) (i : Nat) : TransM Core.Expression.Expr := do + let xs := (← StateT.get).bvars + match xs[xs.size - 1 - i]? with + | some (.bvar _ _) => return .bvar () i + | some e => return e + | none => throwAt m s!"unknown bound variable {i}" + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Decls.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Decls.lean new file mode 100644 index 0000000000..89dab490e9 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Decls.lean @@ -0,0 +1,187 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Datatypes +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Types +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Expressions +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Statements +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.CoreMatch.ToCore +public import Strata.Languages.Core.Procedure +public import Strata.Languages.Core.Function +public import Strata.Languages.Core.TypeDecl +public import Strata.Languages.Core.Program + +/-! +Top-level command translation and the public entry points +(`toMProgram`, `getProgram`, `toCoreProgram`) that drive the full +`Strata.Program → Core.Program` pipeline. +-/ + +namespace Strata.CoreMatch.Translate + +open Lambda +open Strata.CoreMatchDDM + +public section + +private def toCoreBinding (b : Binding SourceRange) + : TransM (Core.Expression.Ident × LMonoTy) := do + match b with + | .mkBinding _ ⟨_, n⟩ tp + | .outBinding _ ⟨_, n⟩ tp + | .inoutBinding _ ⟨_, n⟩ tp + | .casesBinding _ ⟨_, n⟩ tp => + match tp with + | .expr ty => return (mkIdent n, ← toCoreMonoType ty) + | .type m => throwAt m "unexpected Type parameter in term binding" + +private def toCoreSpec (procName : String) (spec? : Option (Spec SourceRange)) + : TransM Core.Procedure.Spec := do + let some (.spec_mk _ ⟨_, elts⟩) := spec? | return default + let mut requires : List (Core.CoreLabel × Core.Procedure.Check) := [] + let mut ensures : List (Core.CoreLabel × Core.Procedure.Check) := [] + for e in elts.toList do + match e with + | .requires_spec m ⟨_, l?⟩ ⟨_, free?⟩ cond => + let lbl ← freshLabel m s!"{procName}_requires" l? + let attr := if free?.isSome then Core.Procedure.CheckAttr.Free else .Default + requires := (lbl, { expr := ← toCoreExpr cond, attr }) :: requires + | .ensures_spec m ⟨_, l?⟩ ⟨_, free?⟩ cond => + let lbl ← freshLabel m s!"{procName}_ensures" l? + let attr := if free?.isSome then Core.Procedure.CheckAttr.Free else .Default + ensures := (lbl, { expr := ← toCoreExpr cond, attr }) :: ensures + return { preconditions := requires.reverse, postconditions := ensures.reverse } + +private def toCoreDatatype (dtName : String) (typeParams : List String) + (ctors : ConstructorList SourceRange) : TransM (LDatatype Unit) := do + let toLConstr (c : Constructor SourceRange) : TransM (LConstr Unit) := do + let .constructor_mk _ ⟨_, cname⟩ _ := c + return { name := mkIdent cname + args := ← (ctorFields c).mapM toCoreBinding + testerName := s!"{dtName}..is{cname}" } + match constructorListToList ctors with + | [] => throw <| .fromMessage s!"datatype {dtName} must have at least one constructor" + | c :: rest => + return { name := dtName + typeArgs := typeParams + constrs := (← toLConstr c) :: (← rest.mapM toLConstr) + constrs_ne := by simp } + +/-- Cache `(ctorName, fieldNames)` info for a datatype declaration so +later commands can resolve match arms against it. -/ +private def cacheDatatype : DatatypeDecl SourceRange → TransM Unit + | .datatype_decl _ ⟨_, dtName⟩ _ ctors => + let info := (constructorListToList ctors).map fun c => + let .constructor_mk _ ⟨_, cname⟩ _ := c + (cname, (ctorFields c).map bindingName) + addDatatype dtName info + +/-- Translate a function body in scope of its inputs. When `recFns` +is non-empty the body is translated under `withRecFns`, so +self-references in match arms get rewritten to rec-result slots. -/ +private def translateFnBody + (ins : Bindings SourceRange) (ret : CoreMatchType SourceRange) + (body : CoreMatchDDM.Expr SourceRange) (recFns : List String := []) + : TransM (List (Core.Expression.Ident × LMonoTy) × LMonoTy × Core.Expression.Expr) := do + let bs := bindingsToList ins + let inputs ← bs.mapM toCoreBinding + let outMTy ← toCoreMonoType ret + let translate := if recFns.isEmpty then toCoreExpr body + else withRecFns recFns (toCoreExpr body) + let bodyE ← withBVars (bs.map bindingName) translate + return (inputs, outMTy, bodyE) + +private def mkMFunction (name : String) + (inputs : List (Core.Expression.Ident × LMonoTy)) + (output : LMonoTy) (bodyExpr : Core.Expression.Expr) + : Strata.CoreMatch.MFunction := + { name := mkIdent name + typeArgs := [] + inputs + output + body := some (.core bodyExpr) } + +def toCoreDecls : Command SourceRange → TransM (List Strata.CoreMatch.MDecl) + | .command_procedure _ ⟨_, n⟩ _ ins ⟨_, spec?⟩ ⟨_, body?⟩ => do + let bs := bindingsToList ins + let inputs ← bs.mapM toCoreBinding + let names := bs.map bindingName + let spec ← withBVars names (toCoreSpec n spec?) + let body ← match body? with + | none => pure [] + | some b => withBVars names (toMBlock b) + let header : Core.Procedure.Header := + { name := mkIdent n, typeArgs := [], inputs, outputs := [] } + return [.proc { header, spec, body } {}] + | .command_datatypes _ ⟨_, decls⟩ => do + for d in decls do cacheDatatype d + let lds ← decls.toList.mapM fun + | .datatype_decl _ ⟨_, n⟩ _ ctors => toCoreDatatype n [] ctors + return [.type (.data lds) {}] + | .command_fndef _ ⟨_, n⟩ _ ins ret _ body _ => do + let (inputs, outMTy, e) ← translateFnBody ins ret body + return [.func (mkMFunction n inputs outMTy e) {}] + | .command_recfndefs _ ⟨_, fns⟩ => do + let allNames := fns.toList.filterMap fun + | .recfn_decl _ ⟨_, n⟩ _ _ _ _ _ => some n + fns.toList.mapM fun + | .recfn_decl _ ⟨_, n⟩ _ ins ret _ body => do + let (inputs, outMTy, e) ← translateFnBody ins ret body (recFns := allNames) + return .func (mkMFunction n inputs outMTy e) {} + | cmd => throw <| .fromMessage s!"unsupported CoreMatch top-level command: {repr cmd}" + +/-- Per command, list whether each symbol it introduces resolves as +an op (`true`) or a term-level fvar (`false`). Order must match the +order DDM pushes symbols into `GlobalContext`. Mirrors +`Boole.initFVarIsOp`. -/ +private def commandSymbolKinds : Command SourceRange → List Bool + | .command_typedecl _ _ _ => [false] + | .command_typesynonym _ _ _ _ _ => [false] + | .command_constdecl _ _ _ _ => [true] + | .command_fndecl _ _ _ _ _ => [true] + | .command_fndef _ _ _ _ _ _ _ _ => [true] + | .command_recfndefs _ ⟨_, fs⟩ => fs.toList.map fun _ => true + | .command_datatypes _ ⟨_, decls⟩ => decls.toList.map fun _ => false + | _ => [] + +def initFVarIsOp (cmds : Array (Command SourceRange)) : Array Bool := + (cmds.toList.flatMap commandSymbolKinds).toArray + +@[expose] +def toMProgram (p : CoreMatchDDM.Program SourceRange) (gctx : GlobalContext) + (fileName : String) : Except DiagnosticModel Strata.CoreMatch.MProgram := do + let .prog _ ⟨_, cmds⟩ := p + let init : TransState := { fileName, gctx, fvarIsOp := initFVarIsOp cmds } + let act : TransM Strata.CoreMatch.MProgram := do + let dss ← cmds.toList.mapM toCoreDecls + return { decls := dss.flatten } + Prod.fst <$> StateT.run act init + +@[expose] +def getProgram (p : Strata.Program) + : Except DiagnosticModel (CoreMatchDDM.Program SourceRange) := do + let cmds : Array Arg := p.commands.map ArgF.op + let progOp : Operation := + { ann := default + name := q`CoreMatch.prog + args := #[.seq default .spacePrefix cmds] } + match CoreMatchDDM.Program.ofAst progOp with + | .ok prog => return prog + | .error msg => throw <| .fromMessage msg + +@[expose] +def toCoreProgram (p : Strata.Program) (fileName : String := "") + : Except DiagnosticModel Core.Program := do + let typed ← getProgram p + let mprog ← toMProgram typed p.globalContext fileName + return Strata.CoreMatch.ToCore.compileProgram mprog + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Expressions.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Expressions.lean new file mode 100644 index 0000000000..a4fa4d8448 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Expressions.lean @@ -0,0 +1,137 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Datatypes +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Types +public import Strata.Languages.CoreMatch.DDMTransform.Translate.NaturalCata +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.CoreMatch.ToCore +public import Strata.Languages.CoreMatch.ArmCheck + +/-! +Translate `CoreMatchDDM.Expr` AST nodes into `Core.Expression.Expr`. +Mutually recursive with the match-arm translators because +`match_expr` walks back into its arm bodies. +-/ + +namespace Strata.CoreMatch.Translate + +open Lambda +open Strata.CoreMatchDDM + +public section + +mutual + +partial def toCoreExpr (e : CoreMatchDDM.Expr SourceRange) + : TransM Core.Expression.Expr := do + let bin (op : Core.Expression.Expr) (a b : CoreMatchDDM.Expr SourceRange) : + TransM Core.Expression.Expr := + return .app () (.app () op (← toCoreExpr a)) (← toCoreExpr b) + match e with + | .fvar m i => + let n ← getFVarName m i + if (← StateT.get).recFns.contains n then + throwAt m s!"non-structural use of recursive function '{n}': \ + must apply directly to a recursive constructor field" + return if (← getFVarIsOp i) then .op () (mkIdent n) none + else .fvar () (mkIdent n) none + | .bvar m i => getBVarExpr m i + | .app m f a => + -- Try the natural-recursion rewrite first; otherwise reject any + -- non-structural self-application before recursing into the args. + if let some rewritten ← tryRecRewrite f a then return rewritten + if let .fvar _ i := f then + let s ← StateT.get + if let some name := s.gctx.nameOf? i then + if s.recFns.contains name then + throwAt m s!"non-structural recursive call to '{name}': \ + argument must be a recursive constructor field \ + of the enclosing match" + return .app () (← toCoreExpr f) (← toCoreExpr a) + | .btrue _ => return LExpr.true () + | .bfalse _ => return LExpr.false () + | .natToInt _ ⟨_, n⟩ => return .intConst () (Int.ofNat n) + | .not _ a => return .app () Core.boolNotOp (← toCoreExpr a) + | .and _ a b => bin Core.boolAndOp a b + | .or _ a b => bin Core.boolOrOp a b + | .implies _ a b => bin Core.boolImpliesOp a b + | .equiv _ a b => bin Core.boolEquivOp a b + | .equal _ _ a b => return .eq () (← toCoreExpr a) (← toCoreExpr b) + | .not_equal _ _ a b => return .app () Core.boolNotOp + (.eq () (← toCoreExpr a) (← toCoreExpr b)) + | .le _ _ a b => bin Core.intLeOp a b + | .lt _ _ a b => bin Core.intLtOp a b + | .ge _ _ a b => bin Core.intGeOp a b + | .gt _ _ a b => bin Core.intGtOp a b + | .neg_expr _ _ a => return .app () Core.intNegOp (← toCoreExpr a) + | .add_expr _ _ a b => bin Core.intAddOp a b + | .sub_expr _ _ a b => bin Core.intSubOp a b + | .mul_expr _ _ a b => bin Core.intMulOp a b + | .if _ _ c t f => return .ite () (← toCoreExpr c) (← toCoreExpr t) (← toCoreExpr f) + | .match_expr m scrutTy resTy scrut headPat headBody tailArms => do + let scrutMTy ← toCoreMonoType scrutTy + let dtName ← expectDatatype m scrutMTy + let resultMTy ← toCoreMonoType resTy + let dt ← lookupLDatatype dtName + let scrutE ← toCoreExpr scrut + let headArm ← translateExprArm dtName resultMTy headPat headBody + let tailArms ← collectTailArms dtName resultMTy tailArms + let arms := headArm :: tailArms + let issues := ArmCheck.check dt (arms.map ArmCheck.MArm.key) + unless issues.isEmpty do + throw <| .fromMessage + s!"match on '{dtName}': {String.intercalate "; " (issues.map ArmCheck.ArmIssue.format)}" + return Strata.CoreMatch.ToCore.compileMExprWith + (fun n => if n == dtName then some dt else none) + (.matchE (.core scrutE) dtName arms) + | _ => throw <| .fromMessage s!"unsupported CoreMatch expression: {repr e}" + +/-- Translate one arm `pat => body` into the eliminator's case +lambda for this constructor. -/ +partial def translateExprArm + (dtName : String) (resultMTy : LMonoTy) + (pat : MatchPat SourceRange) (body : CoreMatchDDM.Expr SourceRange) + : TransM Strata.CoreMatch.MArm := do + match pat with + | .matchPat_wild _ => + return .wild (.core (← toCoreExpr body)) + | .matchPat_ctor _ ⟨_, ctor⟩ vs => + let binders ← (matchPatVarsToList vs).mapM fun + | .matchPatVar_typed _ ⟨_, n⟩ ty => return (n, ← toCoreMonoType ty) + let shape ← classifyArm dtName ctor (binders.map (·.2)) + let st ← StateT.get + -- Stage rec-rewrites for natural arms; cata/unknown arms run with + -- an empty map and translate verbatim. + let recRewrites := match shape with + | .natural recIdxs => + naturalRecRewrites st.recFns recIdxs st.bvars.size + | _ => [] + let bodyE ← withBoundBVars (binders.map (·.1)) <| + withRecRewrites recRewrites (toCoreExpr body) + let (caseBinders, caseBody) := match shape with + | .natural recIdxs => + desugarNaturalToCata resultMTy recIdxs.length binders bodyE + | _ => (binders, bodyE) + let caseFn := LExpr.absMulti () (caseBinders.map (·.2)) caseBody + return .ctor ctor (.core caseFn) + +partial def collectTailArms + (dtName : String) (resultMTy : LMonoTy) + : MatchExprTailArmList SourceRange → TransM (List Strata.CoreMatch.MArm) + | .matchExprTailArmList_nil _ => return [] + | .matchExprTailArmList_cons _ (.matchExprTailArm_mk _ pat body) rest => do + let arm ← translateExprArm dtName resultMTy pat body + let rest ← collectTailArms dtName resultMTy rest + return arm :: rest + +end + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/NaturalCata.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/NaturalCata.lean new file mode 100644 index 0000000000..8d14ac9f22 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/NaturalCata.lean @@ -0,0 +1,113 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Datatypes +public import Strata.DL.Lambda.LExpr +import Strata.DL.Lambda.LExprWF + +/-! +Desugar natural-style match arms to cata-style ones, so both surface +forms emit the same eliminator argument. + +The transformation runs in two passes. During body translation, +`tryRecRewrite` replaces each self-call `f(field)` with a sentinel +fvar carrying the rec-result slot index. After translation, +`desugarNaturalToCata` injects rec-result binders, lifts the body's +existing bvars past them, and substitutes each sentinel with the +matching `bvar`. +-/ + +namespace Strata.CoreMatch.Translate + +open Lambda +open Strata.CoreMatchDDM + +public section + +/-- Name of the placeholder fvar that stands in for a rec-result +reference until `desugarNaturalToCata` resolves it. -/ +def recSentinelName (slot : Nat) : String := + s!"$$coreMatch$rec${slot}" + +/-- If the application is a self-call `f(field)` that should lower to +a rec-result slot, return the matching sentinel; otherwise `none`. -/ +def tryRecRewrite (f a : CoreMatchDDM.Expr SourceRange) + : TransM (Option Core.Expression.Expr) := do + let .fvar _ fIdx := f | return none + let .bvar _ bIdx := a | return none + let s ← StateT.get + let some fName := s.gctx.nameOf? fIdx | return none + unless s.recFns.contains fName do return none + let stackSize := s.bvars.size + unless bIdx < stackSize do return none + let fieldPos := stackSize - 1 - bIdx + let some slot := s.recRewrites[(fName, fieldPos)]? | return none + return some <| .fvar () ⟨recSentinelName slot, ()⟩ none + +/-- The shape of an arm's pattern binders relative to its +constructor's declared fields. -/ +inductive ArmShape where + /-- One binder per declared field; the body's self-calls on + recursive fields will be rewritten. `recFieldIdxs` are the + positions of the recursive-typed fields. -/ + | natural (recFieldIdxs : List Nat) + /-- Field binders followed by one extra binder per recursive + field; the body is taken verbatim. -/ + | cata + /-- Datatype isn't cached; trust the user's binder count. -/ + | unknown + +def classifyArm (dtName ctor : String) + (binderTys : List LMonoTy) : TransM ArmShape := do + let isRecField : LMonoTy → Bool + | .tcons n _ => n == dtName + | _ => false + let userArity := binderTys.length + match (← lookupCtor dtName ctor) with + | none => return .unknown + | some fields => + let fc := fields.length + let recIdxs := binderTys.take fc |>.zipIdx.filterMap fun (ty, i) => + if isRecField ty then some i else none + if userArity == fc then return .natural recIdxs + if userArity == fc + recIdxs.length then return .cata + throw <| .fromMessage + s!"match arm '{ctor}': expected {fc} field binders \ + or {fc + recIdxs.length} (with rec-results), got {userArity}" + +/-- Build the rewrite-map entries for an arm: one +`(recFn, fieldStackPos) ↦ recResultIdx` per pairing of a current rec +function with a recursive field. Stack positions are bottom-relative +so they survive nested binders inside the body. -/ +def naturalRecRewrites + (recFns : List String) (recIdxs : List Nat) (baseDepth : Nat) + : List ((String × Nat) × Nat) := + let recCount := recIdxs.length + recFns.flatMap fun fn => + recIdxs.zipIdx.map fun (fieldIdx, i) => + ((fn, baseDepth + fieldIdx), recCount - 1 - i) + +/-- Resolve the sentinels left in a natural-style arm body, returning +the cata-shaped `(binders, body)` pair: appends one rec-result binder +per recursive field, lifts the body's existing bvars past them, and +substitutes each sentinel `$$coreMatch$rec$i` with `bvar i`. -/ +def desugarNaturalToCata + (resultMTy : LMonoTy) (recCount : Nat) + (binders : List (String × LMonoTy)) (body : Core.Expression.Expr) + : List (String × LMonoTy) × Core.Expression.Expr := + let injected := (List.range recCount).map fun i => + (s!"rec_{i}", resultMTy) + let subst : _root_.Map Core.Expression.Ident Core.Expression.Expr := + _root_.Map.ofList <| (List.range recCount).map fun i => + (⟨recSentinelName i, ()⟩, .bvar () i) + let lifted := LExpr.liftBVars recCount body + (binders ++ injected, LExpr.substFvarsLifting lifted subst) + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Statements.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Statements.lean new file mode 100644 index 0000000000..c3fb452206 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Statements.lean @@ -0,0 +1,132 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Datatypes +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Types +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Expressions +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.CoreMatch.ArmCheck +public import Strata.Languages.Core.Statement + +/-! +Translate statement-level forms. Statement-position `match` lowers +to a nested-if chain over the auto-generated testers, with pattern +binders prepended as `var b : T := D..fᵢ(scrut);` init statements. +-/ + +namespace Strata.CoreMatch.Translate + +open Lambda Imperative +open Strata.CoreMatchDDM + +public section + +def freshLabel (m : SourceRange) (prefix_ : String) + (l? : Option (Label SourceRange)) : TransM String := do + match l? with + | some (.label _ ⟨_, l⟩) => return l + | none => + let i := (← StateT.get).labelCounter + modify fun s => { s with labelCounter := i + 1 } + return s!"{prefix_}_{i}_{m.start}" + +private def toCoreCondBool (c : ExprOrNondet SourceRange) + : TransM (Imperative.ExprOrNondet Core.Expression) := do + match c with + | .condDet _ e => return .det (← toCoreExpr e) + | .condNondet _ => return .nondet + +/-- Build the binder-init statements for a constructor arm: +`var b₁ : T₁ := D..f₁(scrut); …`. Falls back to positional `f0, f1, +…` names when the cached field list disagrees with the binder count; +downstream type-checking surfaces the real problem. -/ +private def buildArmInits + (dtName ctor : String) (binders : List (String × LMonoTy)) + (scrut : Core.Expression.Expr) : TransM (List Core.Statement) := do + let cachedFields := (← lookupCtor dtName ctor).getD [] + let names := + if cachedFields.length == binders.length then cachedFields + else (List.range binders.length).map (s!"f{·}") + return (binders.zip names).map fun ((b, ty), fname) => + let acc : Core.Expression.Expr := + .app () (.op () ⟨dtName ++ ".." ++ fname, ()⟩ none) scrut + Core.Statement.init (mkIdent b) (.forAll [] ty) (.det acc) {} + +mutual + +partial def toMBlock : Block SourceRange → TransM (List Strata.CoreMatch.MStmt) + | .block _ ⟨_, ss⟩ => return (← ss.toList.mapM toMStmt).flatten + +/-- Translate a block to plain Core statements. Inner `matchStmt` +wrappers are dropped here; they are lowered by the procedure-level +pass that has access to the full declaration scope. -/ +partial def toCoreBlock (b : Block SourceRange) : TransM (List Core.Statement) := do + return (← toMBlock b).flatMap fun + | .core c => [c] + | .matchStmt _ _ _ => [] + +partial def matchArmToMStmtArm + (dtName : String) (scrut : Core.Expression.Expr) + : MatchStmtArm SourceRange → TransM Strata.CoreMatch.MStmtArm + | .matchStmtArm_mk _ (.matchPat_wild _) body => + return .wild (← toCoreBlock body) + | .matchStmtArm_mk _ (.matchPat_ctor _ ⟨_, ctor⟩ vs) body => do + let binders ← (matchPatVarsToList vs).mapM fun + | .matchPatVar_typed _ ⟨_, n⟩ ty => return (n, ← toCoreMonoType ty) + let inits ← buildArmInits dtName ctor binders scrut + let body ← withBVars (binders.map (·.1)) (toCoreBlock body) + return .ctor ctor (inits ++ body) + +partial def toMStmt : Statement SourceRange → TransM (List Strata.CoreMatch.MStmt) + | .initStatement _ ty ⟨_, n⟩ e => do + let mty ← toCoreMonoType ty + let rhs ← toCoreExpr e + -- Bring the new binder into scope for the rest of the enclosing block. + modify fun s => { s with bvars := s.bvars.push (.fvar () (mkIdent n) none) } + return [.core <| Core.Statement.init (mkIdent n) (.forAll [] mty) (.det rhs) {}] + | .assign _ _ lhs rhs => do + let n ← match lhs with + | .lhsIdent _ ⟨_, n⟩ => pure n + | .lhsArray _ _ _ _ => + throw <| .fromMessage "array assignment not yet supported in CoreMatch" + return [.core <| Core.Statement.set (mkIdent n) (← toCoreExpr rhs) {}] + | .assume m ⟨_, l?⟩ e => do + let lbl ← freshLabel m "assume" l? + return [.core <| Core.Statement.assume lbl (← toCoreExpr e) {}] + | .assert m _ ⟨_, l?⟩ e => do + let lbl ← freshLabel m "assert" l? + return [.core <| Core.Statement.assert lbl (← toCoreExpr e) {}] + | .if_statement _ c t f => do + let cond ← toCoreCondBool c + let thenBlk ← toCoreBlock t + let elseBlk ← match f with + | .else0 _ => pure [] + | .else1 _ b => toCoreBlock b + return [.core <| Imperative.Stmt.ite cond thenBlk elseBlk {}] + | .match_statement m scrutTy scrut arms => do + let scrutMTy ← toCoreMonoType scrutTy + let dtName ← expectDatatype m scrutMTy + let dt ← lookupLDatatype dtName + let scrutE ← toCoreExpr scrut + let mArms ← (matchStmtArmsToList arms).mapM (matchArmToMStmtArm dtName scrutE) + let issues := ArmCheck.check dt (mArms.map ArmCheck.MStmtArm.key) + unless issues.isEmpty do + throw <| .fromMessage + s!"match on '{dtName}': {String.intercalate "; " (issues.map ArmCheck.ArmIssue.format)}" + return [.matchStmt scrutE dtName mArms] + | .block_statement _ ⟨_, label⟩ b => do + let inner ← withBVars [] (toCoreBlock b) + return [.core <| Imperative.Stmt.block label inner {}] + | .varStatement _ _ => return [] + | s => throw <| .fromMessage s!"unsupported CoreMatch statement: {repr s}" + +end + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/DDMTransform/Translate/Types.lean b/Strata/Languages/CoreMatch/DDMTransform/Translate/Types.lean new file mode 100644 index 0000000000..d10ac4e331 --- /dev/null +++ b/Strata/Languages/CoreMatch/DDMTransform/Translate/Types.lean @@ -0,0 +1,69 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.DDMTransform.Translate.Basic + +/-! +DDM type expressions → `LMonoTy`. Used pervasively by the rest of +the translator for procedure bindings, function signatures, and +match scrutinee types. +-/ + +namespace Strata.CoreMatch.Translate + +open Strata +open Lambda +open Strata.CoreMatchDDM + +public section + +private def typeRange : CoreMatchType SourceRange → SourceRange + | .bvar m _ | .tvar m _ | .fvar m _ _ + | .arrow m _ _ + | .bool m | .int m | .string m | .regex m | .real m + | .bv1 m | .bv8 m | .bv16 m | .bv32 m | .bv64 m + | .Map m _ _ | .Sequence m _ => m + +private def getTypeBVar (m : SourceRange) (i : Nat) : TransM LMonoTy := do + let xs := (← StateT.get).tyBVars + match xs[xs.size - 1 - i]? with + | some n => return .ftvar n + | none => throwAt m s!"unknown type bvar {i}" + +def getFVarName (m : SourceRange) (i : Nat) : TransM String := do + match (← StateT.get).gctx.nameOf? i with + | some n => return n + | none => throwAt m s!"unknown free variable {i}" + +partial def toCoreMonoType : CoreMatchType SourceRange → TransM LMonoTy + | .int _ => return .int + | .bool _ => return .bool + | .string _ => return .string + | .real _ => return .real + | .bv1 _ => return .bitvec 1 + | .bv8 _ => return .bitvec 8 + | .bv16 _ => return .bitvec 16 + | .bv32 _ => return .bitvec 32 + | .bv64 _ => return .bitvec 64 + | .arrow _ a b => return .arrow (← toCoreMonoType a) (← toCoreMonoType b) + | .Map _ k v => return .tcons "Map" [← toCoreMonoType k, ← toCoreMonoType v] + | .Sequence _ a => return .tcons "Sequence" [← toCoreMonoType a] + | .tvar _ n => return .ftvar n + | .fvar m i args => return .tcons (← getFVarName m i) (← args.toList.mapM toCoreMonoType) + | .bvar m i => getTypeBVar m i + | t => throwAt (typeRange t) s!"unsupported type: {repr t}" + +/-- Strip a scrutinee's monomorphic type to a datatype name; fail +with a diagnostic if it isn't a `tcons`. -/ +def expectDatatype (range : SourceRange) (mty : LMonoTy) : TransM String := + match mty with + | .tcons n _ => return n + | _ => throwAt range s!"match scrutinee must be a datatype, got: {repr mty}" + +end + +end Strata.CoreMatch.Translate diff --git a/Strata/Languages/CoreMatch/Verify.lean b/Strata/Languages/CoreMatch/Verify.lean new file mode 100644 index 0000000000..d163d6dbb7 --- /dev/null +++ b/Strata/Languages/CoreMatch/Verify.lean @@ -0,0 +1,40 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.CoreMatch.CoreMatch +public import Strata.Languages.CoreMatch.ToCore +public import Strata.Languages.CoreMatch.DDMTransform.Translate +public import Strata.Languages.Core.Program +public import Strata.Languages.Core.Verifier +public import Strata.Languages.Core.EntryPoint + +/-! +Public entry points for the CoreMatch dialect's source-to-Core +pipeline. +-/ + +namespace Strata.CoreMatch.Verify + +open Core + +public section + +/-- Lower an already-translated `MProgram` to a `Core.Program`. -/ +@[expose] +def toCore (prog : Strata.CoreMatch.MProgram) : Core.Program := + Strata.CoreMatch.ToCore.compileProgram prog + +/-- Parse a `Strata.Program` against the CoreMatch dialect and lower +it all the way to a `Core.Program`. -/ +@[expose] +def parseToCore (prog : Strata.Program) (fileName : String := "") + : Except DiagnosticModel Core.Program := + Strata.CoreMatch.Translate.toCoreProgram prog fileName + +end + +end Strata.CoreMatch.Verify From 6972e19df8d8404f65eb1232834758033ffcef09 Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 13:35:45 -0700 Subject: [PATCH 6/8] CoreMatch: add pattern-matching examples and test suite MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `Examples/pattern_matching/`: nine `.coreMatch.st` programs covering non-recursive enums with wildcards, structural recursion (natural and cata-style), nested matches, mixed-type constructor fields, expression-tree evaluation, and constructor calls in arm bodies. README documents the conventions. * `StrataTest/Languages/CoreMatch/CompileTest.lean`: programmatic invariants on `MProgram → Core.Program` lowering plus ArmCheck diagnostics. * `StrataTest/Languages/CoreMatch/SourceTest.lean`: end-to-end source pipeline tests asserting `D$Elim` head, no self-references after natural-style rewrite, ite-shaped procedure bodies, and the redundancy / non-structural diagnostic surface. --- .../pattern_matching/01_option.coreMatch.st | 21 + .../pattern_matching/02_color.coreMatch.st | 34 + .../pattern_matching/03_peano.coreMatch.st | 29 + .../pattern_matching/04_list.coreMatch.st | 37 ++ .../pattern_matching/05_tree_dfs.coreMatch.st | 50 ++ .../pattern_matching/06_either.coreMatch.st | 29 + .../07_nested_match.coreMatch.st | 24 + .../08_expr_eval.coreMatch.st | 35 + .../09_constructor_calls.coreMatch.st | 31 + .../Languages/CoreMatch/ArmCheckTest.lean | 145 ++++ .../Languages/CoreMatch/CompileTest.lean | 234 +++++++ .../Languages/CoreMatch/NaturalCataTest.lean | 339 ++++++++++ .../Languages/CoreMatch/SourceTest.lean | 625 ++++++++++++++++++ .../CoreMatch/StatementsAndSpecsTest.lean | 534 +++++++++++++++ 14 files changed, 2167 insertions(+) create mode 100644 Examples/pattern_matching/01_option.coreMatch.st create mode 100644 Examples/pattern_matching/02_color.coreMatch.st create mode 100644 Examples/pattern_matching/03_peano.coreMatch.st create mode 100644 Examples/pattern_matching/04_list.coreMatch.st create mode 100644 Examples/pattern_matching/05_tree_dfs.coreMatch.st create mode 100644 Examples/pattern_matching/06_either.coreMatch.st create mode 100644 Examples/pattern_matching/07_nested_match.coreMatch.st create mode 100644 Examples/pattern_matching/08_expr_eval.coreMatch.st create mode 100644 Examples/pattern_matching/09_constructor_calls.coreMatch.st create mode 100644 StrataTest/Languages/CoreMatch/ArmCheckTest.lean create mode 100644 StrataTest/Languages/CoreMatch/CompileTest.lean create mode 100644 StrataTest/Languages/CoreMatch/NaturalCataTest.lean create mode 100644 StrataTest/Languages/CoreMatch/SourceTest.lean create mode 100644 StrataTest/Languages/CoreMatch/StatementsAndSpecsTest.lean diff --git a/Examples/pattern_matching/01_option.coreMatch.st b/Examples/pattern_matching/01_option.coreMatch.st new file mode 100644 index 0000000000..96281c2e2b --- /dev/null +++ b/Examples/pattern_matching/01_option.coreMatch.st @@ -0,0 +1,21 @@ +program CoreMatch; + +// Option-like enum: non-recursive datatype, simplest possible match. + +datatype OptInt () { None(), Some(val : int) }; + +function getOr(o : OptInt, dflt : int) : int +{ + match o { + arm None() => dflt; + arm Some(val : int) => val; + } +}; + +function isSome(o : OptInt) : bool +{ + match o { + arm None() => false; + arm Some(val : int) => true; + } +}; diff --git a/Examples/pattern_matching/02_color.coreMatch.st b/Examples/pattern_matching/02_color.coreMatch.st new file mode 100644 index 0000000000..d96dee4e69 --- /dev/null +++ b/Examples/pattern_matching/02_color.coreMatch.st @@ -0,0 +1,34 @@ +program CoreMatch; + +// Pure enum with wildcard arms covering uncovered constructors. + +datatype Color () { Red(), Green(), Blue(), Yellow() }; + +function isWarm(c : Color) : bool +{ + match c { + arm Red() => true; + arm Yellow() => true; + arm _ => false; + } +}; + +function isPrimary(c : Color) : bool +{ + match c { + arm Red() => true; + arm Green() => true; + arm Blue() => true; + arm _ => false; + } +}; + +function rank(c : Color) : int +{ + match c { + arm Red() => 1; + arm Green() => 2; + arm Blue() => 3; + arm Yellow() => 4; + } +}; diff --git a/Examples/pattern_matching/03_peano.coreMatch.st b/Examples/pattern_matching/03_peano.coreMatch.st new file mode 100644 index 0000000000..999d55120a --- /dev/null +++ b/Examples/pattern_matching/03_peano.coreMatch.st @@ -0,0 +1,29 @@ +program CoreMatch; + +// Peano naturals: natural-style recursion on the `pred` field. + +datatype Nat () { Zero(), Succ(pred : Nat) }; + +rec function toInt(n : Nat) : int +{ + match n { + arm Zero() => 0; + arm Succ(pred : Nat) => 1 + toInt(pred); + } +}; + +rec function isZero(n : Nat) : bool +{ + match n { + arm Zero() => true; + arm Succ(pred : Nat) => false; + } +}; + +rec function double(n : Nat) : Nat +{ + match n { + arm Zero() => Zero(); + arm Succ(pred : Nat) => Succ(Succ(double(pred))); + } +}; diff --git a/Examples/pattern_matching/04_list.coreMatch.st b/Examples/pattern_matching/04_list.coreMatch.st new file mode 100644 index 0000000000..47ca51f5c6 --- /dev/null +++ b/Examples/pattern_matching/04_list.coreMatch.st @@ -0,0 +1,37 @@ +program CoreMatch; + +// Monomorphic List of int: natural-style recursion on `tl`. + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function length(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + length(tl); + } +}; + +rec function sum(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => hd + sum(tl); + } +}; + +rec function allPositive(xs : List) : bool +{ + match xs { + arm Nil() => true; + arm Cons(hd : int, tl : List) => hd > 0 && allPositive(tl); + } +}; + +rec function containsZero(xs : List) : bool +{ + match xs { + arm Nil() => false; + arm Cons(hd : int, tl : List) => hd == 0 || containsZero(tl); + } +}; diff --git a/Examples/pattern_matching/05_tree_dfs.coreMatch.st b/Examples/pattern_matching/05_tree_dfs.coreMatch.st new file mode 100644 index 0000000000..aa8cd17583 --- /dev/null +++ b/Examples/pattern_matching/05_tree_dfs.coreMatch.st @@ -0,0 +1,50 @@ +program CoreMatch; + +// Binary tree DFS: natural-style recursion on `left` and `right`. + +datatype Tree () { Leaf(), Node(value : int, left : Tree, right : Tree) }; + +rec function treeSum(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + value + treeSum(left) + treeSum(right); + } +}; + +rec function nodeCount(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + 1 + nodeCount(left) + nodeCount(right); + } +}; + +rec function depth(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + 1 + (if depth(left) >= depth(right) then depth(left) else depth(right)); + } +}; + +rec function allNonNeg(t : Tree) : bool +{ + match t { + arm Leaf() => true; + arm Node(value : int, left : Tree, right : Tree) => + value >= 0 && allNonNeg(left) && allNonNeg(right); + } +}; + +rec function containsZero(t : Tree) : bool +{ + match t { + arm Leaf() => false; + arm Node(value : int, left : Tree, right : Tree) => + value == 0 || containsZero(left) || containsZero(right); + } +}; diff --git a/Examples/pattern_matching/06_either.coreMatch.st b/Examples/pattern_matching/06_either.coreMatch.st new file mode 100644 index 0000000000..500ce53fe4 --- /dev/null +++ b/Examples/pattern_matching/06_either.coreMatch.st @@ -0,0 +1,29 @@ +program CoreMatch; + +// Either with heterogeneously-typed constructor fields. + +datatype Either () { LeftI(v : int), RightB(b : bool) }; + +function isError(e : Either) : bool +{ + match e { + arm LeftI(v : int) => v < 0; + arm RightB(b : bool) => !b; + } +}; + +function describeKind(e : Either) : int +{ + match e { + arm LeftI(v : int) => 1; + arm RightB(b : bool) => 2; + } +}; + +function unwrapOr(e : Either, dflt : int) : int +{ + match e { + arm LeftI(v : int) => v; + arm RightB(b : bool) => dflt; + } +}; diff --git a/Examples/pattern_matching/07_nested_match.coreMatch.st b/Examples/pattern_matching/07_nested_match.coreMatch.st new file mode 100644 index 0000000000..942155f2e5 --- /dev/null +++ b/Examples/pattern_matching/07_nested_match.coreMatch.st @@ -0,0 +1,24 @@ +program CoreMatch; + +// Nested non-recursive matches: outer on `m`, inner on `s`. + +datatype Shape () { Circle(radius : int), Square(side : int), Triangle(base : int, height : int) }; +datatype Mode () { Area(), Perimeter() }; + +function compute(s : Shape, m : Mode) : int +{ + match m { + arm Area() => + match s { + arm Circle(radius : int) => 3 * radius * radius; + arm Square(side : int) => side * side; + arm Triangle(base : int, height : int) => base * height; + }; + arm Perimeter() => + match s { + arm Circle(radius : int) => 6 * radius; + arm Square(side : int) => 4 * side; + arm Triangle(base : int, height : int) => base + base + height; + }; + } +}; diff --git a/Examples/pattern_matching/08_expr_eval.coreMatch.st b/Examples/pattern_matching/08_expr_eval.coreMatch.st new file mode 100644 index 0000000000..1862b7b400 --- /dev/null +++ b/Examples/pattern_matching/08_expr_eval.coreMatch.st @@ -0,0 +1,35 @@ +program CoreMatch; + +// Expression-tree evaluator: natural-style recursion on `l` and `r`. + +datatype Op () { Plus(), Times(), Minus() }; +datatype Tree () { Lit(v : int), Bin(op : Op, l : Tree, r : Tree) }; + +rec function eval(t : Tree) : int +{ + match t { + arm Lit(v : int) => v; + arm Bin(op : Op, l : Tree, r : Tree) => + match op { + arm Plus() => eval(l) + eval(r); + arm Times() => eval(l) * eval(r); + arm Minus() => eval(l) - eval(r); + }; + } +}; + +rec function size(t : Tree) : int +{ + match t { + arm Lit(v : int) => 1; + arm Bin(op : Op, l : Tree, r : Tree) => 1 + size(l) + size(r); + } +}; + +rec function constantsOnly(t : Tree) : bool +{ + match t { + arm Lit(v : int) => true; + arm Bin(op : Op, l : Tree, r : Tree) => constantsOnly(l) && constantsOnly(r); + } +}; diff --git a/Examples/pattern_matching/09_constructor_calls.coreMatch.st b/Examples/pattern_matching/09_constructor_calls.coreMatch.st new file mode 100644 index 0000000000..a11308109a --- /dev/null +++ b/Examples/pattern_matching/09_constructor_calls.coreMatch.st @@ -0,0 +1,31 @@ +program CoreMatch; + +// Constructor calls in arm bodies plus natural-style recursion. + +datatype List () { Nil(), Cons(hd : int, tl : List) }; +datatype Pair () { MkPair(first : int, second : List) }; + +rec function map_inc(xs : List) : List +{ + match xs { + arm Nil() => Nil(); + arm Cons(hd : int, tl : List) => Cons(hd + 1, map_inc(tl)); + } +}; + +rec function filter_pos(xs : List) : List +{ + match xs { + arm Nil() => Nil(); + arm Cons(hd : int, tl : List) => + if hd > 0 then Cons(hd, filter_pos(tl)) else filter_pos(tl); + } +}; + +function head_or_zero_with_rest(xs : List) : Pair +{ + match xs { + arm Nil() => MkPair(0, Nil()); + arm Cons(hd : int, tl : List) => MkPair(hd, tl); + } +}; diff --git a/StrataTest/Languages/CoreMatch/ArmCheckTest.lean b/StrataTest/Languages/CoreMatch/ArmCheckTest.lean new file mode 100644 index 0000000000..6d65c71ca8 --- /dev/null +++ b/StrataTest/Languages/CoreMatch/ArmCheckTest.lean @@ -0,0 +1,145 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.CoreMatch.CoreMatch +import Strata.Languages.CoreMatch.ArmCheck + +/-! +Tests for the `ArmCheck` redundancy and exhaustiveness checker. They +cover every `ArmIssue` constructor plus the positive cases of full +constructor coverage and a wildcard covering the missing arms. +-/ + +open Strata.CoreMatch +open Strata.CoreMatch.ArmCheck +open Lambda + +namespace CoreMatchArmCheckTest + +private def colorCtors : List String := ["Red", "Green", "Blue"] + +private def hasIssue (issues : List ArmIssue) (target : ArmIssue) : Bool := + issues.contains target + +private def hasNonExhaustiveOf (issues : List ArmIssue) (missing : List String) : Bool := + issues.any fun + | .nonExhaustive m => m == missing + | _ => false + + +/-! Positive cases (no issues) -/ + +-- Full constructor cover, no wildcard. +#guard (checkAgainst colorCtors [some "Red", some "Green", some "Blue"]).isEmpty + +-- Wildcard covering exactly the missing ctor. +#guard (checkAgainst colorCtors [some "Red", some "Green", none]).isEmpty + +-- Wildcard covering all missing ctors at once. +#guard (checkAgainst colorCtors [some "Red", none]).isEmpty + +-- Single wildcard covering everything. +#guard (checkAgainst colorCtors [none]).isEmpty + + +/-! Non-exhaustive + +Missing constructors with no wildcard ⇒ `.nonExhaustive`. -/ + +#guard hasNonExhaustiveOf (checkAgainst colorCtors [some "Red"]) + ["Green", "Blue"] +#guard hasNonExhaustiveOf (checkAgainst colorCtors [some "Red", some "Green"]) + ["Blue"] +#guard hasNonExhaustiveOf (checkAgainst colorCtors []) colorCtors + + +/-! Duplicate constructor -/ + +#guard hasIssue (checkAgainst colorCtors [some "Red", some "Red"]) + (.duplicateConstructor "Red") +#guard hasIssue (checkAgainst colorCtors [some "Red", some "Red", some "Red"]) + (.duplicateConstructor "Red") + +-- Two distinct duplicates: both reported. +#guard let issues := checkAgainst colorCtors + [some "Red", some "Red", some "Green", some "Green"] + hasIssue issues (.duplicateConstructor "Red") + && hasIssue issues (.duplicateConstructor "Green") + + +/-! Unknown constructor -/ + +#guard hasIssue (checkAgainst colorCtors [some "Purple"]) + (.unknownConstructor "Purple") +#guard hasIssue (checkAgainst colorCtors [some "Red", some "NotAColor"]) + (.unknownConstructor "NotAColor") + + +/-! Multiple wildcards -/ + +#guard hasIssue (checkAgainst colorCtors [some "Red", none, none]) + .multipleWildcards +#guard hasIssue (checkAgainst colorCtors [none, none, none]) + .multipleWildcards + + +/-! Redundant wildcard -/ + +-- Wildcard arm where every constructor is already explicitly covered. +#guard hasIssue (checkAgainst colorCtors + [some "Red", some "Green", some "Blue", none]) + .redundantWildcard + + +/-! Multiple issues at once + +A single check can report multiple distinct issues. -/ + +#guard let issues := checkAgainst colorCtors + [some "Red", some "Red", some "Purple"] + hasIssue issues (.duplicateConstructor "Red") + && hasIssue issues (.unknownConstructor "Purple") + && hasNonExhaustiveOf issues ["Green", "Blue"] + + +/-! `check` against a real `LDatatype` -/ + +private def color : LDatatype Unit := + { name := "Color", typeArgs := [] + constrs := [ + { name := ⟨"Red", ()⟩, args := [] }, + { name := ⟨"Green", ()⟩, args := [] }, + { name := ⟨"Blue", ()⟩, args := [] }], + constrs_ne := by decide } + +#guard (check color [some "Red", some "Green", some "Blue"]).isEmpty +#guard hasNonExhaustiveOf (check color [some "Red"]) ["Green", "Blue"] + + +/-! `MArm.key` and `MStmtArm.key` projections + +The same checker drives expression-level and statement-level matches +through these abstract-key projections. -/ + +#guard MArm.key (.ctor "Red" (.core (.intConst () 0))) == some "Red" +#guard MArm.key (.wild (.core (.intConst () 0))) == none + +#guard MStmtArm.key (.ctor "Red" []) == some "Red" +#guard MStmtArm.key (.wild []) == none + + +/-! Issue formatting + +Each issue formats to a non-empty diagnostic string. -/ + +#guard !(ArmIssue.format (.unknownConstructor "X")).isEmpty +#guard !(ArmIssue.format (.duplicateConstructor "X")).isEmpty +#guard !(ArmIssue.format .multipleWildcards).isEmpty +#guard !(ArmIssue.format .redundantWildcard).isEmpty +#guard !(ArmIssue.format (.nonExhaustive ["X"])).isEmpty + + +end CoreMatchArmCheckTest diff --git a/StrataTest/Languages/CoreMatch/CompileTest.lean b/StrataTest/Languages/CoreMatch/CompileTest.lean new file mode 100644 index 0000000000..7ff66e314a --- /dev/null +++ b/StrataTest/Languages/CoreMatch/CompileTest.lean @@ -0,0 +1,234 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.CoreMatch.CoreMatch +import Strata.Languages.CoreMatch.ToCore + +/-! +Programmatic tests for `MProgram → Core.Program` lowering. Build +`MExpr` / `MStmt` values directly and assert on the resulting Core +shape: eliminator applications for expression-level matches, nested +ifs for statement-level matches, wildcard padding, arm reordering, +accessor calls in statement-arm prologues, and the unknown-datatype +and missing-arm fallbacks. +-/ + +open Strata.CoreMatch +open Lambda + +namespace CoreMatchCompileTest + + +/-! Helper datatypes -/ + +private def color : LDatatype Unit := + { name := "Color", typeArgs := [] + constrs := [ + { name := ⟨"Red", ()⟩, args := [] }, + { name := ⟨"Green", ()⟩, args := [] }, + { name := ⟨"Blue", ()⟩, args := [] }], + constrs_ne := by decide } + +private def colorDecl : Core.Decl := .type (.data [color]) {} + +private def list : LDatatype Unit := + { name := "List", typeArgs := [] + constrs := [ + { name := ⟨"Nil", ()⟩, args := [] }, + { name := ⟨"Cons", ()⟩, + args := [(⟨"hd", ()⟩, .int), (⟨"tl", ()⟩, .tcons "List" [])] }], + constrs_ne := by decide } + +private def listDecl : Core.Decl := .type (.data [list]) {} + +private def cId : Core.Expression.Expr := .fvar () ⟨"c", ()⟩ (some (.tcons "Color" [])) +private def xsId : Core.Expression.Expr := .fvar () ⟨"xs", ()⟩ (some (.tcons "List" [])) + + +/-! AST inspection helpers -/ + +private partial def appHead : Core.Expression.Expr → Option String + | .app _ f _ => appHead f + | .op _ ⟨n, _⟩ _ => some n + | _ => none + +private partial def appArgCount : Core.Expression.Expr → Nat + | .app _ f _ => appArgCount f + 1 + | _ => 0 + +private partial def appArgs : Core.Expression.Expr → List Core.Expression.Expr + | .app _ f a => appArgs f ++ [a] + | _ => [] + + +/-! Expression match: head and arity -/ + +private def colorRank : MExpr := + .matchE (.core cId) "Color" [ + .ctor "Red" (.core (.intConst () 1)), + .wild (.core (.intConst () 0))] + +private def lowered : Core.Expression.Expr := + Strata.CoreMatch.ToCore.compileMExpr [colorDecl] colorRank + +#guard appHead lowered == some "Color$Elim" + +-- `Color$Elim c `: 4 args. +#guard appArgCount lowered == 4 + +-- The first arg after the eliminator is the scrutinee. +#guard match appArgs lowered with + | scrut :: _ => scrut == cId + | _ => false + +-- The Red case is the explicit `1`; Green and Blue come from +-- wildcard expansion (also `0`, since the wildcard body is `0`). +#guard match appArgs lowered with + | _ :: red :: green :: blue :: [] => + red == .intConst () 1 + && green == .intConst () 0 + && blue == .intConst () 0 + | _ => false + + +/-! Arm reordering + +Cases must come out in the datatype's declaration order regardless of +the source order. -/ + +private def colorOutOfOrder : MExpr := + .matchE (.core cId) "Color" [ + .ctor "Blue" (.core (.intConst () 3)), + .ctor "Red" (.core (.intConst () 1)), + .ctor "Green" (.core (.intConst () 2))] + +private def reordered : Core.Expression.Expr := + Strata.CoreMatch.ToCore.compileMExpr [colorDecl] colorOutOfOrder + +-- After lowering, the case order must match `[Red, Green, Blue]`. +#guard match appArgs reordered with + | _ :: red :: green :: blue :: [] => + red == .intConst () 1 + && green == .intConst () 2 + && blue == .intConst () 3 + | _ => false + + +/-! Wildcard padding + +A wildcard arm for a constructor with arity > 0 must be wrapped in +λ-binders to match the ctor's arity. -/ + +private def listToInt : MExpr := + .matchE (.core xsId) "List" [ + .ctor "Nil" (.core (.intConst () 0)), + .wild (.core (.intConst () 1))] -- covers Cons + +private def loweredList : Core.Expression.Expr := + Strata.CoreMatch.ToCore.compileMExpr [listDecl] listToInt + +#guard appHead loweredList == some "List$Elim" +#guard appArgCount loweredList == 3 -- scrut + Nil case + Cons case + +-- Cons has arity 2; the wildcard expansion must wrap the body in +-- two `λ`s. +#guard match appArgs loweredList with + | _ :: _nilCase :: consCase :: [] => + match consCase with + | .abs _ _ _ (.abs _ _ _ (.intConst _ 1)) => true + | _ => false + | _ => false + + +/-! Statement match: nested-if compilation -/ + +private def colorStmt : MStmt := + .matchStmt cId "Color" [.ctor "Red" [], .ctor "Green" [], .wild []] + +private def loweredStmt : List Core.Statement := + Strata.CoreMatch.ToCore.compileMStmt [colorDecl] colorStmt + +-- Single statement — nested-if is a single ite at the top. +#guard loweredStmt.length == 1 + +#guard match loweredStmt with + | [.ite _ _ _ _] => true + | _ => false + +-- The outer ite's condition is `Color..isRed(c)`. +#guard match loweredStmt with + | [.ite (.det (.app _ (.op _ ⟨name, _⟩ _) _)) _ _ _] => + name == "Color..isRed" + | _ => false + + +/-! Statement match: missing-arm fallback to assert false -/ + +-- Match without a wildcard and without an arm for `Blue`: lowering +-- emits `assert false` (`coreMatch_nonexhaustive`) for the gap. +private def colorIncomplete : MStmt := + .matchStmt cId "Color" [.ctor "Red" [], .ctor "Green" []] + +private def loweredIncomplete : List Core.Statement := + Strata.CoreMatch.ToCore.compileMStmt [colorDecl] colorIncomplete + +-- The Blue arm body is the assert-false fallback. The exact shape +-- is one ite producing `Color$Elim` + `assert` for the missing case. +#guard loweredIncomplete.length == 1 + + +/-! Unknown-datatype fallback + +Lowering a match against a datatype not in the decl list emits a +distinctive sentinel rather than panicking — surfaces a clear error +downstream. -/ + +private def colorUnknown : MExpr := + .matchE (.core cId) "DoesNotExist" [.ctor "Foo" (.core (.intConst () 1))] + +private def loweredUnknown : Core.Expression.Expr := + Strata.CoreMatch.ToCore.compileMExpr [] colorUnknown -- empty decl list + +-- The lowered expression is a fvar with a `__coreMatch_unknown_dt_*` +-- name — visible at typecheck time as an unbound symbol. +#guard match loweredUnknown with + | .fvar _ ⟨n, _⟩ _ => n.startsWith "__coreMatch_unknown_dt_" + | _ => false + + +/-! Missing-arm placeholder + +`compileMExprWith` emits a `__coreMatch_missing_*` sentinel when a +constructor has no arm and no wildcard. This should never reach +production (the arm-checker rejects it), but if it does, the verifier +fails loudly on an unbound symbol rather than silently producing +garbage. -/ + +-- Build a malformed MExpr that's missing the Cons arm and has no +-- wildcard. Lowering should still complete and the placeholder +-- shows up where Cons would be. +private def badList : MExpr := + .matchE (.core xsId) "List" [.ctor "Nil" (.core (.intConst () 0))] + +private def loweredBadList : Core.Expression.Expr := + Strata.CoreMatch.ToCore.compileMExpr [listDecl] badList + +-- The Cons case slot should be the missing-arm placeholder. +#guard match appArgs loweredBadList with + | _ :: _nilCase :: consCase :: [] => + match consCase with + | .fvar _ ⟨n, _⟩ _ => n.startsWith "__coreMatch_missing_" + | _ => false + | _ => false + + +/-! `MStmts.ofCore` / `MStmt.ofCore` lifting helpers -/ + +#guard MStmt.ofCore (.assert "x" (LExpr.true ()) {}) matches .core _ +#guard (MStmts.ofCore [.assert "a" (LExpr.true ()) {}, .assume "b" (LExpr.true ()) {}]).length == 2 + + +end CoreMatchCompileTest diff --git a/StrataTest/Languages/CoreMatch/NaturalCataTest.lean b/StrataTest/Languages/CoreMatch/NaturalCataTest.lean new file mode 100644 index 0000000000..5c341b2915 --- /dev/null +++ b/StrataTest/Languages/CoreMatch/NaturalCataTest.lean @@ -0,0 +1,339 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.CoreMatch.CoreMatch +import Strata.Languages.CoreMatch.ToCore +import Strata.Languages.CoreMatch.DDMTransform.Translate.NaturalCata +import Strata.Languages.CoreMatch.Verify +import Strata.Languages.CoreMatch.DDMTransform.StrataGen + +/-! +Tests for the natural-style to cata-style desugaring. Combines direct +unit tests on the helpers in +`CoreMatch.DDMTransform.Translate.NaturalCata` with end-to-end +property checks confirming that natural-style and cata-style source +programs lower to identical Core expressions. +-/ + +open Strata Strata.CoreMatch Strata.CoreMatch.Translate +open Lambda + +namespace CoreMatchNaturalCataTest + + +/-! Sentinel naming -/ + +#guard recSentinelName 0 == "$$coreMatch$rec$0" +#guard recSentinelName 1 == "$$coreMatch$rec$1" +#guard recSentinelName 7 == "$$coreMatch$rec$7" + +-- Sentinel names are unguessable — `$$` prefix never appears in a +-- valid CoreMatch identifier. +#guard (recSentinelName 0).startsWith "$$coreMatch" + + +/-! `naturalRecRewrites` shape + +Test the bookkeeping that drives `tryRecRewrite`: keys are +`(fnName, baseDepth + fieldIdx)`, values are slot indices counted +from `recCount - 1` down to 0 in declaration order. -/ + +-- Single recursive field, single rec function: one entry, slot 0. +#guard naturalRecRewrites ["length"] [1] 0 + == [(("length", 1), 0)] + +-- Two recursive fields (binary tree `Node(value, left, right)` → +-- recIdxs = [1, 2]), one rec function: two entries, slots reversed +-- (left → 1, right → 0) so `right_rec` ends up at innermost +-- bvar 0 in the case lambda. +#guard naturalRecRewrites ["treeSum"] [1, 2] 0 + == [(("treeSum", 1), 1), (("treeSum", 2), 0)] + +-- Three recursive fields: slot indices recCount-1 down to 0. +#guard naturalRecRewrites ["f"] [0, 1, 2] 0 + == [(("f", 0), 2), (("f", 1), 1), (("f", 2), 0)] + +-- Non-zero baseDepth shifts every key by the same amount. +#guard naturalRecRewrites ["length"] [1] 5 + == [(("length", 6), 0)] + +-- Mutually recursive functions: each rec field appears once per +-- function, so two rec fns × two rec fields = four entries. +#guard naturalRecRewrites ["f", "g"] [0, 1] 0 + == [(("f", 0), 1), (("f", 1), 0), + (("g", 0), 1), (("g", 1), 0)] + +-- No rec functions in scope ⇒ no entries even with rec fields. +#guard naturalRecRewrites [] [0, 1] 0 == [] + +-- No rec fields ⇒ no entries even with rec functions. +#guard naturalRecRewrites ["f"] [] 0 == [] + + +/-! `desugarNaturalToCata` mechanics + +The transformation is pure: given `(resultType, recCount, binders, +body-with-sentinels)`, returns `(extendedBinders, body-with-bvars)`. +The injected binders are named `rec_0..rec_{n-1}`, typed as the +function's return type, and appended to the user's binders. -/ + +-- recCount = 0 is a no-op (cata/unknown shape would skip the call, +-- but the function should still be safe to invoke). +#guard let (b, _) := desugarNaturalToCata .int 0 [("hd", .int)] (.intConst () 0) + b == [("hd", .int)] + +-- recCount = 1: appends one rec_0 binder. +#guard let (b, _) := desugarNaturalToCata .int 1 [("tl", .tcons "List" [])] + (.intConst () 0) + b == [("tl", .tcons "List" []), ("rec_0", .int)] + +-- recCount = 2: appends rec_0 and rec_1 in order. +#guard let (b, _) := desugarNaturalToCata .int 2 + [("left", .tcons "Tree" []), ("right", .tcons "Tree" [])] + (.intConst () 0) + b == [("left", .tcons "Tree" []), ("right", .tcons "Tree" []), + ("rec_0", .int), ("rec_1", .int)] + +-- The injected binders are typed as the *result* type, regardless of +-- the user binders' types. +#guard let (b, _) := desugarNaturalToCata .bool 1 [] (.intConst () 0) + b == [("rec_0", .bool)] + + +/-! Sentinel substitution + +The body's sentinels become bvars; the existing bvars are lifted +past the new injection. -/ + +-- A body that's a single sentinel: should resolve to bvar 0. +#guard let (_, body) := desugarNaturalToCata .int 1 [] + (.fvar () ⟨recSentinelName 0, ()⟩ none) + body matches .bvar _ 0 + +-- Two sentinels, ordered by slot index. +#guard let (_, body) := desugarNaturalToCata .int 2 [] + (.app () (.fvar () ⟨recSentinelName 0, ()⟩ none) + (.fvar () ⟨recSentinelName 1, ()⟩ none)) + match body with + | .app _ (.bvar _ 0) (.bvar _ 1) => true + | _ => false + +-- A pre-existing bvar in the body gets lifted by recCount. Setup: +-- one user binder `hd` referenced as bvar 0, then recCount = 1 +-- injection. Expected: bvar 0 → bvar 1. +#guard let (_, body) := desugarNaturalToCata .int 1 [("hd", .int)] + (.bvar () 0) + body matches .bvar _ 1 + +-- recCount = 2 lift: bvar 0 → bvar 2, bvar 1 → bvar 3. +#guard let (_, body) := desugarNaturalToCata .int 2 + [("hd", .int), ("tl", .tcons "List" [])] + (.app () (.bvar () 1) (.bvar () 0)) + match body with + | .app _ (.bvar _ 3) (.bvar _ 2) => true + | _ => false + + +/-! End-to-end: natural and cata produce identical Core + +The strongest property: source programs that differ only in +natural-vs-cata style lower to byte-identical Core. -/ + +-- Helper: extract the body of the named function from a parsed program. +private def fnBody (p : Strata.Program) (name : String) : Option Core.Expression.Expr := + match Strata.CoreMatch.Verify.parseToCore p "test" with + | .error _ => none + | .ok prog => + prog.decls.findSome? fun + | .func f _ => if f.name.name == name then f.body else none + | _ => none + +private def pListNatural : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function length(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + length(tl); + } +}; +#end + +private def pListCata : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +function length(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List, lenTl : int) => 1 + lenTl; + } +}; +#end + +-- Both styles produce a body, both bodies are equal. +#guard fnBody pListNatural "length" |>.isSome +#guard fnBody pListCata "length" |>.isSome +#guard fnBody pListNatural "length" == fnBody pListCata "length" + + +/-! Multiple recursive fields + +Binary tree DFS: `Node(value, left, right)` → two rec-result binders +in declaration order at the *end* of the case-lambda binder list. -/ + +private def pTreeNatural : Strata.Program := +#strata +program CoreMatch; + +datatype Tree () { Leaf(), Node(value : int, left : Tree, right : Tree) }; + +rec function treeSum(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + value + treeSum(left) + treeSum(right); + } +}; +#end + +private def pTreeCata : Strata.Program := +#strata +program CoreMatch; + +datatype Tree () { Leaf(), Node(value : int, left : Tree, right : Tree) }; + +function treeSum(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree, leftR : int, rightR : int) => + value + leftR + rightR; + } +}; +#end + +#guard fnBody pTreeNatural "treeSum" |>.isSome +#guard fnBody pTreeCata "treeSum" |>.isSome +#guard fnBody pTreeNatural "treeSum" == fnBody pTreeCata "treeSum" + + +/-! Mutually recursive functions + +Both functions in the block are eligible self-call targets. -/ + +private def pMutual : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function length(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + length(tl); + } +}; + +rec function sum(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => hd + sum(tl); + } +}; +#end + +#guard fnBody pMutual "length" |>.isSome +#guard fnBody pMutual "sum" |>.isSome + + +/-! Non-structural recursion is rejected + +The natural-style rewrite only fires for `f(field)` where `field` +is a recursive constructor field of the enclosing match. All other +forms reject. -/ + +private def parseError? (p : Strata.Program) : Bool := + match Strata.CoreMatch.Verify.parseToCore p "test" with + | .ok _ => false + | .error _ => true + +-- f(non-recursive-field-of-other-binder). +private def pBadOtherParam : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function bad(xs : List, ys : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + bad(ys, tl); + } +}; +#end + +#guard parseError? pBadOtherParam + +-- f passed as a value (no argument applied). Note: this won't even +-- type-check at the source level since `f` has function type, but +-- it confirms the .fvar branch in toCoreExpr would reject it. +private def pBadValue : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function badValue(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + badValue(xs); + } +}; +#end + +-- xs is the function input, not a recursive *field*; rejected. +#guard parseError? pBadValue + + +/-! Wrong binder count is rejected with a clear error + +Neither natural (== fc) nor cata (== fc + recCount) shape ⇒ classify +fails. -/ + +private def pWrongArity : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +function bad(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int) => hd; + } +}; +#end + +-- Cons has 2 fields; user wrote 1 binder. Expected: 2 or 3 (cata +-- with one rec-result), got 1. Reject. +#guard parseError? pWrongArity + + +end CoreMatchNaturalCataTest diff --git a/StrataTest/Languages/CoreMatch/SourceTest.lean b/StrataTest/Languages/CoreMatch/SourceTest.lean new file mode 100644 index 0000000000..69018f966a --- /dev/null +++ b/StrataTest/Languages/CoreMatch/SourceTest.lean @@ -0,0 +1,625 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.CoreMatch.Verify +import Strata.Languages.CoreMatch.DDMTransform.StrataGen + +/-! +End-to-end source pipeline tests. Each program travels DDM parse → +typed AST → `MProgram` → `Core.Program` and is asserted on for +structural invariants in the lowered Core (eliminator-headed +function bodies, no self-references after natural-style rewrite, +ite-shaped procedure bodies) and for the diagnostic surface of the +redundancy and non-structural checks. +-/ + +open Strata Lambda + +namespace CoreMatchSourceTest + + +/-! Inspection helpers -/ + +private partial def headOpName + (e : LExpr ⟨⟨Unit, Unit⟩, LMonoTy⟩) : Option String := + match e with + | .app _ f _ => headOpName f + | .op _ ⟨n, _⟩ _ => some n + | _ => none + +private partial def hasFvar + (e : LExpr ⟨⟨Unit, Unit⟩, LMonoTy⟩) (name : String) : Bool := + match e with + | .fvar _ ⟨n, _⟩ _ => n == name + | .app _ f a => hasFvar f name || hasFvar a name + | .abs _ _ _ b => hasFvar b name + | .quant _ _ _ _ t b => hasFvar t name || hasFvar b name + | .ite _ c t f => hasFvar c name || hasFvar t name || hasFvar f name + | .eq _ a b => hasFvar a name || hasFvar b name + | _ => false + +private partial def opNames + (e : LExpr ⟨⟨Unit, Unit⟩, LMonoTy⟩) : List String := + match e with + | .op _ ⟨n, _⟩ _ => [n] + | .app _ f a => opNames f ++ opNames a + | .abs _ _ _ b => opNames b + | .quant _ _ _ _ t b => opNames t ++ opNames b + | .ite _ c t f => opNames c ++ opNames t ++ opNames f + | .eq _ a b => opNames a ++ opNames b + | _ => [] + +private def parseToCore (p : Strata.Program) + : Except DiagnosticModel Core.Program := + Strata.CoreMatch.Verify.parseToCore p "test" + +private def lookupFn (p : Strata.Program) (name : String) : Option Core.Function := + match parseToCore p with + | .error _ => none + | .ok prog => + prog.decls.findSome? fun + | .func f _ => if f.name.name == name then some f else none + | _ => none + +private def lookupProc (p : Strata.Program) (name : String) : Option Core.Procedure := + match parseToCore p with + | .error _ => none + | .ok prog => + prog.decls.findSome? fun + | .proc d _ => if d.header.name.name == name then some d else none + | _ => none + +private def declCount (p : Strata.Program) : Nat := + match parseToCore p with + | .ok prog => prog.decls.length + | .error _ => 0 + +private def parseError? (p : Strata.Program) : Bool := + match parseToCore p with + | .ok _ => false + | .error _ => true + +/-- Body is `D$Elim …`, no self-reference left, no termination + obligation: the catamorphism convention. -/ +private def isCataFn (dtName : String) (f : Core.Function) : Bool := + match f.body with + | none => false + | some b => + headOpName b == some (dtName ++ "$Elim") + && !hasFvar b f.name.name + && f.preconditions.isEmpty + && f.axioms.isEmpty + && f.attr.isEmpty + +/-- Procedure body lowered to a single ite (possibly wrapped in a + block), as a match-statement should produce. -/ +private def isIteHeadedProc (d : Core.Procedure) : Bool := + match d.body with + | [.block _ [.ite _ _ _ _] _] => true + | [.ite _ _ _ _] => true + | _ => false + + +/-! Non-recursive enum (option-like) -/ + +private def pOption : Strata.Program := +#strata +program CoreMatch; + +datatype OptInt () { None(), Some(val : int) }; + +function getOr(o : OptInt, dflt : int) : int +{ + match o { + arm None() => dflt; + arm Some(val : int) => val; + } +}; + +function isSome(o : OptInt) : bool +{ + match o { + arm None() => false; + arm Some(val : int) => true; + } +}; +#end + +#guard declCount pOption == 5 + +#guard match lookupFn pOption "getOr" with + | some f => headOpName f.body.get! == some "OptInt$Elim" + | none => false + +#guard match lookupFn pOption "isSome" with + | some f => headOpName f.body.get! == some "OptInt$Elim" + | none => false + + +/-! Pure enum with wildcard arms -/ + +private def pEnum : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue(), Yellow() }; + +function isWarm(c : Color) : bool +{ + match c { + arm Red() => true; + arm Yellow() => true; + arm _ => false; + } +}; + +function rank(c : Color) : int +{ + match c { + arm Red() => 1; + arm Green() => 2; + arm Blue() => 3; + arm Yellow() => 4; + } +}; +#end + +#guard declCount pEnum == 5 + +-- Both functions lower to Color$Elim head. +#guard match lookupFn pEnum "isWarm" with + | some f => headOpName f.body.get! == some "Color$Elim" + | none => false + +#guard match lookupFn pEnum "rank" with + | some f => headOpName f.body.get! == some "Color$Elim" + | none => false + + +/-! Unary recursion (Peano natural numbers) -/ + +private def pPeano : Strata.Program := +#strata +program CoreMatch; + +datatype Nat () { Zero(), Succ(pred : Nat) }; + +rec function toInt(n : Nat) : int +{ + match n { + arm Zero() => 0; + arm Succ(pred : Nat) => 1 + toInt(pred); + } +}; + +rec function isZero(n : Nat) : bool +{ + match n { + arm Zero() => true; + arm Succ(pred : Nat) => false; + } +}; +#end + +-- toInt: cata invariants hold. +#guard match lookupFn pPeano "toInt" with + | some f => isCataFn "Nat" f + | none => false + +-- isZero: doesn't actually recurse (the Succ arm returns false), but +-- the body is still eliminator-headed. +#guard match lookupFn pPeano "isZero" with + | some f => headOpName f.body.get! == some "Nat$Elim" + | none => false + + +/-! Binary-tree DFS (multiple recursive fields) -/ + +private def pTree : Strata.Program := +#strata +program CoreMatch; + +datatype Tree () { Leaf(), Node(value : int, left : Tree, right : Tree) }; + +rec function treeSum(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + value + treeSum(left) + treeSum(right); + } +}; + +rec function nodeCount(t : Tree) : int +{ + match t { + arm Leaf() => 0; + arm Node(value : int, left : Tree, right : Tree) => + 1 + nodeCount(left) + nodeCount(right); + } +}; +#end + +#guard match lookupFn pTree "treeSum" with + | some f => isCataFn "Tree" f + | none => false + +#guard match lookupFn pTree "nodeCount" with + | some f => isCataFn "Tree" f + | none => false + +-- The only ops appearing in `treeSum`'s body should be `Tree$Elim` +-- and `Int.Add` — no `treeSum` reference at all, confirming the +-- natural-style rewrite consumed both `treeSum(left)` and +-- `treeSum(right)`. +#guard match lookupFn pTree "treeSum" with + | some f => + match f.body with + | some b => (opNames b).all fun n => n == "Tree$Elim" || n == "Int.Add" + | none => false + | none => false + + +/-! Mutually recursive functions -/ + +private def pMutual : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function length(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + length(tl); + } +}; + +rec function sum(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => hd + sum(tl); + } +}; +#end + +#guard match lookupFn pMutual "length" with + | some f => isCataFn "List" f + | none => false + +#guard match lookupFn pMutual "sum" with + | some f => isCataFn "List" f + | none => false + + +/-! Heterogeneous constructor field types -/ + +private def pEither : Strata.Program := +#strata +program CoreMatch; + +datatype Either () { LeftI(v : int), RightB(b : bool) }; + +function isError(e : Either) : bool +{ + match e { + arm LeftI(v : int) => v < 0; + arm RightB(b : bool) => !b; + } +}; + +function describeKind(e : Either) : int +{ + match e { + arm LeftI(v : int) => 1; + arm RightB(b : bool) => 2; + } +}; +#end + +#guard match lookupFn pEither "isError" with + | some f => headOpName f.body.get! == some "Either$Elim" + | none => false + + +/-! Nested matches -/ + +private def pNested : Strata.Program := +#strata +program CoreMatch; + +datatype Shape () { Circle(radius : int), Square(side : int) }; +datatype Mode () { Area(), Perimeter() }; + +function compute(s : Shape, m : Mode) : int +{ + match m { + arm Area() => + match s { + arm Circle(radius : int) => 3 * radius * radius; + arm Square(side : int) => side * side; + }; + arm Perimeter() => + match s { + arm Circle(radius : int) => 6 * radius; + arm Square(side : int) => 4 * side; + }; + } +}; +#end + +-- Outer match is on `m`; body is `Mode$Elim`-headed. +#guard match lookupFn pNested "compute" with + | some f => headOpName f.body.get! == some "Mode$Elim" + | none => false + + +/-! Constructor calls in arm bodies -/ + +private def pBuilds : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function map_inc(xs : List) : List +{ + match xs { + arm Nil() => Nil(); + arm Cons(hd : int, tl : List) => Cons(hd + 1, map_inc(tl)); + } +}; +#end + +-- map_inc returns a List, calls Cons in its body, and uses natural +-- recursion: the cata invariant should still hold. +#guard match lookupFn pBuilds "map_inc" with + | some f => isCataFn "List" f + | none => false + + +/-! Statement-level match: ite-shaped procedure body -/ + +private def pProc : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; + +procedure rank(c: Color, out r: int) +spec { ensures r >= 0; ensures r <= 2; } +{ + match c { + Red() => { r := 0; } + Green() => { r := 1; } + Blue() => { r := 2; } + } +}; +#end + +#guard match lookupProc pProc "rank" with + | some d => isIteHeadedProc d + | none => false + +-- Spec is preserved: 2 `ensures` clauses. +#guard match lookupProc pProc "rank" with + | some d => d.spec.postconditions.length == 2 + | none => false + + +/-! Statement-level match: pattern binders → accessor inits -/ + +private def pProcWithBinder : Strata.Program := +#strata +program CoreMatch; + +datatype OptInt () { None(), Some(val : int) }; + +procedure unwrapOr(o: OptInt, dflt: int, out r: int) +{ + match o { + None() => { r := dflt; } + Some(val : int) => { r := val; } + } +}; +#end + +-- Body lowers to ite chain whose Some arm contains +-- `var val : int := OptInt..val(o); r := val;`. We just confirm +-- the procedure parses and lowers. +#guard match lookupProc pProcWithBinder "unwrapOr" with + | some d => isIteHeadedProc d + | none => false + + +/-! Diagnostics: redundancy / exhaustiveness -/ + +private def pNonExhaustive : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +function broken(xs : List) : int +{ + match xs { + arm Nil() => 0; + } +}; +#end + +private def pDuplicate : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; + +function broken(c : Color) : int +{ + match c { + arm Red() => 1; + arm Red() => 2; + arm Green() => 3; + arm Blue() => 4; + } +}; +#end + +private def pRedundantWild : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; + +function broken(c : Color) : int +{ + match c { + arm Red() => 1; + arm Green() => 2; + arm Blue() => 3; + arm _ => 4; + } +}; +#end + +private def pUnknownCtor : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; + +function broken(c : Color) : int +{ + match c { + arm Red() => 1; + arm Purple() => 2; + arm Green() => 3; + arm Blue() => 4; + } +}; +#end + +#guard parseError? pNonExhaustive +#guard parseError? pDuplicate +#guard parseError? pRedundantWild +#guard parseError? pUnknownCtor + + +/-! Diagnostics: non-structural recursion -/ + +private def pBadOtherParam : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function badCall(xs : List, ys : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + badCall(ys, tl); + } +}; +#end + +private def pBadSelfApply : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +rec function badSelf(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List) => 1 + badSelf(xs); + } +}; +#end + +#guard parseError? pBadOtherParam +#guard parseError? pBadSelfApply + + +/-! Diagnostics: wrong arm binder count -/ + +private def pTooFewBinders : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +function bad(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int) => hd; + } +}; +#end + +private def pTooManyBinders : Strata.Program := +#strata +program CoreMatch; + +datatype List () { Nil(), Cons(hd : int, tl : List) }; + +function bad(xs : List) : int +{ + match xs { + arm Nil() => 0; + arm Cons(hd : int, tl : List, x : int, y : int) => hd; + } +}; +#end + +#guard parseError? pTooFewBinders +#guard parseError? pTooManyBinders + + +/-! Multiple datatypes, multiple top-level commands -/ + +private def pMulti : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; +datatype Mode () { On(), Off() }; + +function isRed(c : Color) : bool +{ + match c { + arm Red() => true; + arm Green() => false; + arm Blue() => false; + } +}; + +function isOn(m : Mode) : bool +{ + match m { + arm On() => true; + arm Off() => false; + } +}; +#end + +-- Two datatypes plus two functions; the exact decl count includes +-- auto-generated companions, but it's well-defined and stable. +#guard declCount pMulti == 6 + +#guard match lookupFn pMulti "isRed" with + | some f => headOpName f.body.get! == some "Color$Elim" + | none => false + +#guard match lookupFn pMulti "isOn" with + | some f => headOpName f.body.get! == some "Mode$Elim" + | none => false + + +end CoreMatchSourceTest diff --git a/StrataTest/Languages/CoreMatch/StatementsAndSpecsTest.lean b/StrataTest/Languages/CoreMatch/StatementsAndSpecsTest.lean new file mode 100644 index 0000000000..6f57f66ed5 --- /dev/null +++ b/StrataTest/Languages/CoreMatch/StatementsAndSpecsTest.lean @@ -0,0 +1,534 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.CoreMatch.Verify +import Strata.Languages.CoreMatch.DDMTransform.StrataGen + +/-! +Tests for the statement-form translator and procedure spec +translation: the full statement repertoire, `buildArmInits` accessor +calls, requires/ensures handling (with the `free` attribute and +custom labels), and type-translation breadth across bv-widths, +strings, reals, `Map`, `Sequence`, and `arrow` forms. +-/ + +open Strata Lambda + +namespace CoreMatchStatementsAndSpecsTest + + +/-! Inspection helpers -/ + +private partial def hasOp (e : LExpr ⟨⟨Unit, Unit⟩, LMonoTy⟩) (name : String) : Bool := + match e with + | .op _ ⟨n, _⟩ _ => n == name + | .app _ f a => hasOp f name || hasOp a name + | .abs _ _ _ b => hasOp b name + | .quant _ _ _ _ t b => hasOp t name || hasOp b name + | .ite _ c t f => hasOp c name || hasOp t name || hasOp f name + | .eq _ a b => hasOp a name || hasOp b name + | _ => false + +private partial def stmtHasOp (s : Core.Statement) (name : String) : Bool := + match s with + | .init _ _ rhs _ => + match rhs with + | .det e => hasOp e name + | .nondet => false + | .set _ rhs _ => hasOp rhs name + | .assert _ e _ => hasOp e name + | .assume _ e _ => hasOp e name + | .ite cond t e _ => + let condHas := match cond with + | .det c => hasOp c name + | .nondet => false + condHas || (t.any (stmtHasOp · name)) || (e.any (stmtHasOp · name)) + | .block _ ss _ => ss.any (stmtHasOp · name) + | _ => false + +private def parseToCore (p : Strata.Program) + : Except DiagnosticModel Core.Program := + Strata.CoreMatch.Verify.parseToCore p "test" + +private def lookupProc (p : Strata.Program) (name : String) : Option Core.Procedure := + match parseToCore p with + | .error _ => none + | .ok prog => + prog.decls.findSome? fun + | .proc d _ => if d.header.name.name == name then some d else none + | _ => none + +private def parseError? (p : Strata.Program) : Bool := + match parseToCore p with + | .ok _ => false + | .error _ => true + + +/-! Full statement repertoire + +Build a procedure that uses every statement form CoreMatch translates, +then check the lowered procedure body has the right shape. This is +the only place these forms are exercised end-to-end. -/ + +private def pAssertions : Strata.Program := +#strata +program CoreMatch; + +procedure assertions(out r: int) +{ + assume true; + assert true; + r := 0; +}; +#end + +#guard match lookupProc pAssertions "assertions" with + | some d => + match d.body with + | [_, _, _] => true -- assume + assert + assignment + | _ => false + | none => false + +-- The body contains an assert and an assume statement. +#guard match lookupProc pAssertions "assertions" with + | some d => + d.body.any fun + | .assert _ _ _ => true + | _ => false + | none => false + +#guard match lookupProc pAssertions "assertions" with + | some d => + d.body.any fun + | .assume _ _ _ => true + | _ => false + | none => false + + +private def pIfs : Strata.Program := +#strata +program CoreMatch; + +procedure withIf(b : bool, out r: int) +{ + if (b) { + r := 1; + } else { + r := 0; + } +}; +#end + +-- The body lowers to a single ite. +#guard match lookupProc pIfs "withIf" with + | some d => + match d.body with + | [.ite _ _ _ _] => true + | _ => false + | none => false + + +private def pIfNoElse : Strata.Program := +#strata +program CoreMatch; + +procedure withIfNoElse(b : bool, out r: int) +{ + r := 0; + if (b) { + r := 1; + } +}; +#end + +-- if-without-else lowers to ite with an empty else block. +#guard match lookupProc pIfNoElse "withIfNoElse" with + | some d => + match d.body with + | [_, .ite _ _ [] _] => true + | _ => false + | none => false + + +private def pBlock : Strata.Program := +#strata +program CoreMatch; + +procedure withBlock(out r: int) +{ + lbl: { + r := 1; + } +}; +#end + +-- A labelled block statement lowers to `Stmt.block "lbl" [...]`. +#guard match lookupProc pBlock "withBlock" with + | some d => + d.body.any fun + | .block lbl _ _ => lbl == "lbl" + | _ => false + | none => false + + +/-! Statement-arm accessor inits + +`buildArmInits` prepends `var b : T := D..f(scrut);` to each arm +body that binds pattern variables. Verify the lowered procedure +references the accessor op. -/ + +private def pAccessor : Strata.Program := +#strata +program CoreMatch; + +datatype OptInt () { None(), Some(val : int) }; + +procedure unwrapOr(o : OptInt, dflt : int, out r: int) +{ + match o { + None() => { r := dflt; } + Some(val : int) => { r := val; } + } +}; +#end + +-- The Some arm's body should contain an accessor call to `OptInt..val`. +#guard match lookupProc pAccessor "unwrapOr" with + | some d => d.body.any (stmtHasOp · "OptInt..val") + | none => false + +-- The same procedure also threads testers `OptInt..isNone` and +-- `OptInt..isSome` through the ite chain. +#guard match lookupProc pAccessor "unwrapOr" with + | some d => d.body.any (stmtHasOp · "OptInt..isNone") + | none => false + + +/-! Procedure spec translation -/ + +private def pSpec : Strata.Program := +#strata +program CoreMatch; + +procedure clamp(x : int, out r: int) +spec { + requires x >= 0; + ensures r >= 0; + ensures r <= 100; +} +{ + r := 0; +}; +#end + +#guard match lookupProc pSpec "clamp" with + | some d => d.spec.preconditions.length == 1 + | none => false + +#guard match lookupProc pSpec "clamp" with + | some d => d.spec.postconditions.length == 2 + | none => false + +-- Default attribute on a non-`free` clause. +#guard match lookupProc pSpec "clamp" with + | some d => + match d.spec.preconditions with + | [(_, check)] => check.attr == .Default + | _ => false + | none => false + + +private def pSpecFree : Strata.Program := +#strata +program CoreMatch; + +procedure usingFree(x : int, out r: int) +spec { + free requires x >= 0; + free ensures r == x; +} +{ + r := x; +}; +#end + +-- `requires free` produces `CheckAttr.Free`. +#guard match lookupProc pSpecFree "usingFree" with + | some d => + match d.spec.preconditions with + | [(_, check)] => check.attr == .Free + | _ => false + | none => false + +#guard match lookupProc pSpecFree "usingFree" with + | some d => + match d.spec.postconditions with + | [(_, check)] => check.attr == .Free + | _ => false + | none => false + + +private def pSpecLabel : Strata.Program := +#strata +program CoreMatch; + +procedure named(out r : int) +spec { + ensures [outNonNeg]: r >= 0; +} +{ + r := 0; +}; +#end + +-- User-provided label is used verbatim. +#guard match lookupProc pSpecLabel "named" with + | some d => + match d.spec.postconditions with + | [(lbl, _)] => lbl == "outNonNeg" + | _ => false + | none => false + + +/-! Type translation breadth + +Procedures whose parameters and bodies exercise type forms beyond +the int/bool/datatype set the rest of the suite covers. -/ + +private def pTypeBreadth : Strata.Program := +#strata +program CoreMatch; + +procedure typeBreadth( + a : bv8, b : bv32, s : string, x : real, + m : Map int bool, q : Sequence int, + out r : int) +{ + r := 0; +}; +#end + +-- Just confirm the procedure parses and lowers without error. +#guard match lookupProc pTypeBreadth "typeBreadth" with + | some _ => true + | none => false + +-- The header carries every binding the procedure declares (including +-- the outparam): six inputs + one outparam = seven entries. +#guard match lookupProc pTypeBreadth "typeBreadth" with + | some d => d.header.inputs.length == 7 + | none => false + + +private def pBitvecs : Strata.Program := +#strata +program CoreMatch; + +procedure bitvecs(a : bv1, b : bv16, c : bv64, out r : int) +{ + r := 0; +}; +#end + +#guard match lookupProc pBitvecs "bitvecs" with + | some d => d.header.inputs.length == 4 + | none => false + + +private def pNestedTypes : Strata.Program := +#strata +program CoreMatch; + +procedure nestedTypes( + sm : Sequence (Map int bool), + ms : Map string (Sequence real), + out r : int) +{ + r := 0; +}; +#end + +#guard match lookupProc pNestedTypes "nestedTypes" with + | some d => d.header.inputs.length == 3 + | none => false + + +/-! Empty / minimal programs + +The translator should accept a program with no declarations, and a +program with only a datatype. -/ + +private def pEmpty : Strata.Program := +#strata +program CoreMatch; +#end + +#guard match parseToCore pEmpty with + | .ok p => p.decls.isEmpty + | .error _ => false + + +private def pOnlyDatatype : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; +#end + +#guard match parseToCore pOnlyDatatype with + | .ok p => !p.decls.isEmpty -- at least the datatype decl + | .error _ => false + + +/-! Bare `var n : T;` (varStatement) + +`toMStmt`'s `varStatement` branch returns `[]` — the variable is +introduced into the bvar stack only; no Core statement is emitted. -/ + +private def pBareVar : Strata.Program := +#strata +program CoreMatch; + +procedure bareVar(out r : int) +{ + var x : int; + r := 0; +}; +#end + +-- Body should have just the assignment, no init for `x`. +#guard match lookupProc pBareVar "bareVar" with + | some d => d.body.length == 1 + | none => false + + +/-! Non-deterministic `if (*)` + +`toCoreCondBool`'s `.condNondet` branch lowers to +`Imperative.ExprOrNondet.nondet`. -/ + +private def pNondetIf : Strata.Program := +#strata +program CoreMatch; + +procedure nondetIf(out r : int) +{ + if * { + r := 1; + } else { + r := 0; + } +}; +#end + +#guard match lookupProc pNondetIf "nondetIf" with + | some d => + match d.body with + | [.ite .nondet _ _ _] => true + | _ => false + | none => false + + +/-! Multiple datatypes in one block declaration + +`command_datatypes` accepts a comma-separated list of datatype decls +in one statement; the cache is populated for all of them and the +emitted `MDecl.type (.data lds)` carries every datatype. -/ + +private def pMultiDatatypes : Strata.Program := +#strata +program CoreMatch; + +datatype Color () { Red(), Green(), Blue() }; + +datatype Shape () { Circle(radius : int), Square(side : int) }; + +function dispatch(c : Color, s : Shape) : int +{ + match c { + arm Red() => + match s { + arm Circle(radius : int) => radius; + arm Square(side : int) => side; + }; + arm Green() => 0; + arm Blue() => 0; + } +}; +#end + +-- Both datatypes are usable from the same function — confirms the +-- cache survives across decls. +#guard match parseToCore pMultiDatatypes with + | .ok _ => true + | .error _ => false + + +/-! Custom labels on assert/assume + +A user-supplied label is preserved in the lowered Core statement. -/ + +private def pLabels : Strata.Program := +#strata +program CoreMatch; + +procedure withLabels(b : bool, out r : int) +{ + assert [precond]: b; + assume [postcond]: b; + r := 0; +}; +#end + +#guard match lookupProc pLabels "withLabels" with + | some d => + d.body.any fun + | .assert lbl _ _ => lbl == "precond" + | _ => false + | none => false + +#guard match lookupProc pLabels "withLabels" with + | some d => + d.body.any fun + | .assume lbl _ _ => lbl == "postcond" + | _ => false + | none => false + + +/-! Synthesised labels for unlabelled assertions + +`freshLabel` synthesises labels of the form `prefix_N_pos` when the +user doesn't provide one. We confirm the produced label is non-empty +and starts with the right prefix. -/ + +private def pUnlabelled : Strata.Program := +#strata +program CoreMatch; + +procedure unlabelled(b : bool, out r : int) +{ + assert b; + assume b; + r := 0; +}; +#end + +#guard match lookupProc pUnlabelled "unlabelled" with + | some d => + d.body.any fun + | .assert lbl _ _ => !lbl.isEmpty && lbl.startsWith "assert" + | _ => false + | none => false + +#guard match lookupProc pUnlabelled "unlabelled" with + | some d => + d.body.any fun + | .assume lbl _ _ => !lbl.isEmpty && lbl.startsWith "assume" + | _ => false + | none => false + + +end CoreMatchStatementsAndSpecsTest From 27de82beee3c410984c5a5a6083072f3e638849b Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 14:07:40 -0700 Subject: [PATCH 7/8] editors: add syntax highlighting for .coreMatch.st (VSCode + Emacs) * `editors/GenSyntax.lean` extended to emit a per-dialect highlighter: add `LangCfg`/`EmacsCfg` config records and a `DialectGenSpec` describing each language to write. The generator now produces highlighters for both `Core` (`.core.st`) and `CoreMatch` (`.coreMatch.st`). * Auto-generated mode files: `editors/emacs/coreMatch-st-mode.el`, `editors/vscode/syntaxes/coreMatch-st.tmLanguage.json`. * VSCode `package.json` and Emacs / VSCode README updates wire the new language entries. --- editors/GenSyntax.lean | 179 ++++++++++++------ editors/emacs/README.md | 22 ++- editors/emacs/core-st-mode.el | 2 +- editors/emacs/coreMatch-st-mode.el | 85 +++++++++ editors/vscode/README.md | 20 +- editors/vscode/package.json | 13 +- .../syntaxes/coreMatch-st.tmLanguage.json | 97 ++++++++++ 7 files changed, 347 insertions(+), 71 deletions(-) create mode 100644 editors/emacs/coreMatch-st-mode.el create mode 100644 editors/vscode/syntaxes/coreMatch-st.tmLanguage.json diff --git a/editors/GenSyntax.lean b/editors/GenSyntax.lean index 73d35ceed9..367154e28d 100644 --- a/editors/GenSyntax.lean +++ b/editors/GenSyntax.lean @@ -5,23 +5,24 @@ -/ import Strata.Languages.Core.DDMTransform.Grammar +import Strata.Languages.CoreMatch.DDMTransform.StrataGen /-! -# Auto-generate editor syntax highlighting from the Core DDM grammar +# Auto-generate editor syntax highlighting from Strata DDM grammars Usage: - lake env lean --run editors/GenSyntax.lean vscode # writes editors/vscode/syntaxes/core-st.tmLanguage.json - lake env lean --run editors/GenSyntax.lean emacs # writes editors/emacs/core-st-mode.el + lake env lean --run editors/GenSyntax.lean vscode # writes vscode TextMate grammars + lake env lean --run editors/GenSyntax.lean emacs # writes emacs major modes lake env lean --run editors/GenSyntax.lean all # writes both -The generator reads the `Core` dialect object (produced by `#strata_gen`) -and extracts types, keywords, operators, constants, and built-in function +The generator reads each dialect object produced by `#strata_gen` and +extracts types, keywords, operators, constants, and built-in function names from the structured `SyntaxDef` data. Static patterns (comments, strings, labels, attributes, identifiers, numbers) are hardcoded since they come from the DDM parser, not the dialect grammar. -/ -open Strata CoreDDM Strata.Elab +open Strata CoreDDM CoreMatchDDM Strata.Elab /-! ## Extract syntax tokens from the Dialect object -/ @@ -58,7 +59,8 @@ def extractSyntaxInfo (d : Dialect) : SyntaxInfo := | _ => none -- Function names with explicit classification (handled by dedicated branches below) let constantFnNames := ["btrue", "bfalse"] - let keywordFnNames := ["forall", "forallT", "exists", "existsT", "old"] + let keywordFnNames := ["forall", "forallT", "exists", "existsT", "old", + "match_expr", "matchExprArm_mk"] -- Auto-detect literal constructors by naming convention (*Lit suffix) let isLiteralCtor (name : String) : Bool := name.endsWith "Lit" -- Internal functions: not user-visible operators or keywords @@ -138,7 +140,13 @@ def escapeRegexForJson (s : String) : String := String.ofList <| s.toList.flatMap fun c => if special.contains c then ['\\', '\\', c] else [c] -def generateTextMate (info : SyntaxInfo) : String := +structure LangCfg where + langId : String + scopeName : String + displayName : String + generatorTarget : String + +def generateTextMate (cfg : LangCfg) (info : SyntaxInfo) : String := let typePattern := "\\\\b(" ++ "|".intercalate (info.types.map escapeRegexForJson) ++ ")\\\\b" let kwPattern := "\\\\b(" ++ "|".intercalate (info.keywords.map escapeRegexForJson) ++ ")\\\\b" let constPattern := "\\\\b(" ++ "|".intercalate (info.constants.map escapeRegexForJson) ++ ")\\\\b" @@ -154,9 +162,9 @@ def generateTextMate (info : SyntaxInfo) : String := let lines : List String := [ ob, s!" {q}$schema{q}: {q}https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json{q},", - s!" {q}_comment{q}: {q}AUTO-GENERATED from the Core DDM grammar. Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean vscode{q},", - s!" {q}name{q}: {q}Strata Core{q},", - s!" {q}scopeName{q}: {q}source.core-st{q},", + s!" {q}_comment{q}: {q}AUTO-GENERATED from the {cfg.generatorTarget} DDM grammar. Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean vscode{q},", + s!" {q}name{q}: {q}{cfg.displayName}{q},", + s!" {q}scopeName{q}: {q}source.{cfg.langId}{q},", s!" {q}patterns{q}: [", s!" {ob} {q}include{q}: {q}#comment{q} {cb},", s!" {ob} {q}include{q}: {q}#string{q} {cb},", @@ -172,67 +180,67 @@ def generateTextMate (info : SyntaxInfo) : String := " ],", s!" {q}repository{q}: {ob}", s!" {q}comment{q}: {ob}", - s!" {q}name{q}: {q}comment.line.double-slash.core-st{q},", + s!" {q}name{q}: {q}comment.line.double-slash.{cfg.langId}{q},", s!" {q}match{q}: {q}//.*${q}", s!" {cb},", s!" {q}string{q}: {ob}", - s!" {q}name{q}: {q}string.quoted.double.core-st{q},", + s!" {q}name{q}: {q}string.quoted.double.{cfg.langId}{q},", s!" {q}begin{q}: {q}\\{q}{q},", s!" {q}end{q}: {q}\\{q}{q},", s!" {q}patterns{q}: [", s!" {ob}", - s!" {q}name{q}: {q}constant.character.escape.core-st{q},", + s!" {q}name{q}: {q}constant.character.escape.{cfg.langId}{q},", s!" {q}match{q}: {q}\\\\\\\\.{q}", s!" {cb}", " ]", s!" {cb},", s!" {q}attribute{q}: {ob}", - s!" {q}name{q}: {q}meta.attribute.core-st{q},", + s!" {q}name{q}: {q}meta.attribute.{cfg.langId}{q},", s!" {q}match{q}: {q}@\\\\[[^\\\\]]*\\\\]{q},", s!" {q}captures{q}: {ob}", - s!" {q}0{q}: {ob} {q}name{q}: {q}entity.other.attribute-name.core-st{q} {cb}", + s!" {q}0{q}: {ob} {q}name{q}: {q}entity.other.attribute-name.{cfg.langId}{q} {cb}", s!" {cb}", s!" {cb},", s!" {q}label{q}: {ob}", - s!" {q}name{q}: {q}meta.label.core-st{q},", + s!" {q}name{q}: {q}meta.label.{cfg.langId}{q},", s!" {q}match{q}: {q}\\\\[([a-zA-Z_][a-zA-Z0-9_]*)\\\\]\\\\s*:{q},", s!" {q}captures{q}: {ob}", - s!" {q}0{q}: {ob} {q}name{q}: {q}entity.name.label.core-st{q} {cb},", - s!" {q}1{q}: {ob} {q}name{q}: {q}entity.name.tag.core-st{q} {cb}", + s!" {q}0{q}: {ob} {q}name{q}: {q}entity.name.label.{cfg.langId}{q} {cb},", + s!" {q}1{q}: {ob} {q}name{q}: {q}entity.name.tag.{cfg.langId}{q} {cb}", s!" {cb}", s!" {cb},", s!" {q}number{q}: {ob}", s!" {q}patterns{q}: [", s!" {ob}", - s!" {q}name{q}: {q}constant.numeric.decimal.core-st{q},", + s!" {q}name{q}: {q}constant.numeric.decimal.{cfg.langId}{q},", s!" {q}match{q}: {q}\\\\b[0-9]+(\\\\.[0-9]+)?\\\\b{q}", s!" {cb}", " ]", s!" {cb},", s!" {q}keyword{q}: {ob}", - s!" {q}name{q}: {q}keyword.core-st{q},", + s!" {q}name{q}: {q}keyword.{cfg.langId}{q},", s!" {q}match{q}: {q}{kwPattern}{q}", s!" {cb},", s!" {q}type{q}: {ob}", - s!" {q}name{q}: {q}support.type.core-st{q},", + s!" {q}name{q}: {q}support.type.{cfg.langId}{q},", s!" {q}match{q}: {q}{typePattern}{q}", s!" {cb},", s!" {q}constant{q}: {ob}", - s!" {q}name{q}: {q}constant.language.core-st{q},", + s!" {q}name{q}: {q}constant.language.{cfg.langId}{q},", s!" {q}match{q}: {q}{constPattern}{q}", s!" {cb},", s!" {q}operator{q}: {ob}", s!" {q}patterns{q}: [", s!" {ob}", - s!" {q}name{q}: {q}keyword.operator.assignment.core-st{q},", + s!" {q}name{q}: {q}keyword.operator.assignment.{cfg.langId}{q},", s!" {q}match{q}: {q}:={q}", s!" {cb},", s!" {ob}", - s!" {q}name{q}: {q}keyword.operator.word.core-st{q},", + s!" {q}name{q}: {q}keyword.operator.word.{cfg.langId}{q},", s!" {q}match{q}: {q}{wordOpPattern}{q}", s!" {cb},", s!" {ob}", - s!" {q}name{q}: {q}keyword.operator.symbol.core-st{q},", + s!" {q}name{q}: {q}keyword.operator.symbol.{cfg.langId}{q},", s!" {q}match{q}: {q}{symOpPattern}{q}", s!" {cb}", " ]", @@ -240,11 +248,11 @@ def generateTextMate (info : SyntaxInfo) : String := s!" {q}function-call{q}: {ob}", s!" {q}match{q}: {q}{builtinPattern}{q},", s!" {q}captures{q}: {ob}", - s!" {q}1{q}: {ob} {q}name{q}: {q}support.function.builtin.core-st{q} {cb}", + s!" {q}1{q}: {ob} {q}name{q}: {q}support.function.builtin.{cfg.langId}{q} {cb}", s!" {cb}", s!" {cb},", s!" {q}identifier{q}: {ob}", - s!" {q}name{q}: {q}variable.other.core-st{q},", + s!" {q}name{q}: {q}variable.other.{cfg.langId}{q},", s!" {q}match{q}: {q}\\\\b[a-zA-Z_$][a-zA-Z0-9_$]*\\\\b{q}", s!" {cb}", s!" {cb}", @@ -266,42 +274,49 @@ private def emacsWordList (items : List String) (indent : String := " ") : St let allLines := result.1 ++ [result.2] "\n".intercalate allLines -def generateEmacs (info : SyntaxInfo) : String := +structure EmacsCfg where + langId : String + modeLine : String + /-- Raw elisp regex string for `auto-mode-alist`; inserted verbatim. -/ + extRegex : String + displayName : String + +def generateEmacs (cfg : EmacsCfg) (info : SyntaxInfo) : String := let kwList := emacsWordList info.keywords let tyList := emacsWordList info.types let ctList := emacsWordList info.constants let opList := emacsWordList info.wordOperators let biList := emacsWordList info.builtinFunctions - -- Build the file as a list of lines to avoid escape nightmares + let id := cfg.langId let lines : List String := [ - ";;; core-st-mode.el --- Major mode for Strata Core (.core.st) files -*- lexical-binding: t; -*-", + s!";;; {id}-mode.el --- Major mode for {cfg.displayName} files -*- lexical-binding: t; -*-", "", - ";; AUTO-GENERATED from the Core DDM grammar.", + ";; AUTO-GENERATED from the Strata DDM grammar.", ";; Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean emacs", "", ";; Keywords", - "(defvar core-st-keywords", + s!"(defvar {id}-keywords", s!" '({kwList}))", "", - "(defvar core-st-types", + s!"(defvar {id}-types", s!" '({tyList}))", "", - "(defvar core-st-constants", + s!"(defvar {id}-constants", s!" '({ctList}))", "", - "(defvar core-st-operators", + s!"(defvar {id}-operators", s!" '({opList}))", "", - "(defvar core-st-builtins", + s!"(defvar {id}-builtins", s!" '({biList}))", "", ";; Font-lock rules", - "(defvar core-st-font-lock-keywords", - " (let ((kw-re (regexp-opt core-st-keywords 'symbols))", - " (ty-re (regexp-opt core-st-types 'symbols))", - " (ct-re (regexp-opt core-st-constants 'symbols))", - " (op-re (regexp-opt core-st-operators 'symbols))", - " (bi-re (regexp-opt core-st-builtins 'symbols)))", + s!"(defvar {id}-font-lock-keywords", + s!" (let ((kw-re (regexp-opt {id}-keywords 'symbols))", + s!" (ty-re (regexp-opt {id}-types 'symbols))", + s!" (ct-re (regexp-opt {id}-constants 'symbols))", + s!" (op-re (regexp-opt {id}-operators 'symbols))", + s!" (bi-re (regexp-opt {id}-builtins 'symbols)))", " `((,kw-re . font-lock-keyword-face)", " (,ty-re . font-lock-type-face)", " (,ct-re . font-lock-constant-face)", @@ -315,7 +330,7 @@ def generateEmacs (info : SyntaxInfo) : String := " (\"\\\\b[0-9]+\\\\(?:\\\\.[0-9]+\\\\)?\\\\b\" . font-lock-constant-face))))", "", ";; Syntax table", - "(defvar core-st-mode-syntax-table", + s!"(defvar {id}-mode-syntax-table", " (let ((st (make-syntax-table)))", " ;; // line comments", " (modify-syntax-entry ?/ \". 12\" st)", @@ -337,36 +352,82 @@ def generateEmacs (info : SyntaxInfo) : String := " st))", "", ";;;###autoload", - "(define-derived-mode core-st-mode prog-mode \"Core.st\"", - " \"Major mode for editing Strata Core (.core.st) files.\"", - " :syntax-table core-st-mode-syntax-table", - " (setq-local font-lock-defaults '(core-st-font-lock-keywords))", + s!"(define-derived-mode {id}-mode prog-mode \"{cfg.modeLine}\"", + s!" \"Major mode for editing {cfg.displayName} files.\"", + s!" :syntax-table {id}-mode-syntax-table", + s!" (setq-local font-lock-defaults '({id}-font-lock-keywords))", " (setq-local comment-start \"// \")", " (setq-local comment-end \"\"))", "", ";;;###autoload", - "(add-to-list 'auto-mode-alist '(\"\\\\.core\\\\.st\\\\'\" . core-st-mode))", + s!"(add-to-list 'auto-mode-alist '(\"{cfg.extRegex}\" . {id}-mode))", "", - "(provide 'core-st-mode)", - ";;; core-st-mode.el ends here", + s!"(provide '{id}-mode)", + s!";;; {id}-mode.el ends here", "" ] "\n".intercalate lines -/-! ## Main -/ +structure DialectGenSpec where + /-- Every dialect whose ops should appear in the highlighter. For + dialects that import others (e.g. `CoreMatch` imports `Core`), list + each one: `Dialect.declarations` only carries the locally-declared + ops, so imports must be extracted and merged separately. -/ + dialects : List Dialect + vscode : LangCfg + emacs : EmacsCfg -def main (args : List String) : IO Unit := do - let info := extractSyntaxInfo Core - let target := args.head?.getD "all" +def SyntaxInfo.merge (a b : SyntaxInfo) : SyntaxInfo := + { types := (a.types ++ b.types).eraseDups + keywords := (a.keywords ++ b.keywords).eraseDups + wordOperators := (a.wordOperators ++ b.wordOperators).eraseDups + constants := (a.constants ++ b.constants).eraseDups + builtinFunctions := (a.builtinFunctions ++ b.builtinFunctions).eraseDups + symbolOperators := (a.symbolOperators ++ b.symbolOperators).eraseDups } + +def SyntaxInfo.empty : SyntaxInfo := + { types := [], keywords := [], wordOperators := [], + constants := [], builtinFunctions := [], symbolOperators := [] } + +def coreSpec : DialectGenSpec := + { dialects := [Core] + vscode := { langId := "core-st" + scopeName := "source.core-st" + displayName := "Strata Core" + generatorTarget := "Core" } + emacs := { langId := "core-st" + modeLine := "Core.st" + extRegex := "\\\\.core\\\\.st\\\\'" + displayName := "Strata Core (.core.st)" } } + +def coreMatchSpec : DialectGenSpec := + { dialects := [Core, CoreMatch] + vscode := { langId := "coreMatch-st" + scopeName := "source.coreMatch-st" + displayName := "Strata CoreMatch" + generatorTarget := "CoreMatch" } + emacs := { langId := "coreMatch-st" + modeLine := "CoreMatch.st" + extRegex := "\\\\.coreMatch\\\\.st\\\\'" + displayName := "Strata CoreMatch (.coreMatch.st)" } } + +def writeForDialect (spec : DialectGenSpec) (target : String) : IO Unit := do + let info := spec.dialects.foldl (init := SyntaxInfo.empty) fun acc d => + SyntaxInfo.merge acc (extractSyntaxInfo d) let scriptDir := "editors" if target == "vscode" || target == "all" then - let path := s!"{scriptDir}/vscode/syntaxes/core-st.tmLanguage.json" - IO.FS.writeFile path (generateTextMate info) + let path := s!"{scriptDir}/vscode/syntaxes/{spec.vscode.langId}.tmLanguage.json" + IO.FS.writeFile path (generateTextMate spec.vscode info) IO.println s!"Wrote {path}" if target == "emacs" || target == "all" then - let path := s!"{scriptDir}/emacs/core-st-mode.el" - IO.FS.writeFile path (generateEmacs info) + let path := s!"{scriptDir}/emacs/{spec.emacs.langId}-mode.el" + IO.FS.writeFile path (generateEmacs spec.emacs info) IO.println s!"Wrote {path}" + +def main (args : List String) : IO Unit := do + let target := args.head?.getD "all" if target != "vscode" && target != "emacs" && target != "all" then IO.eprintln s!"Usage: lake env lean --run editors/GenSyntax.lean [vscode|emacs|all]" IO.Process.exit 1 + writeForDialect coreSpec target + writeForDialect coreMatchSpec target diff --git a/editors/emacs/README.md b/editors/emacs/README.md index 257220e710..1ad979210c 100644 --- a/editors/emacs/README.md +++ b/editors/emacs/README.md @@ -1,6 +1,8 @@ # Strata Syntax Highlighting for Emacs -Major mode for Strata Core (`.core.st`) files, providing syntax highlighting, comment support, and bracket matching. +Major modes for Strata Core (`.core.st`) and Strata CoreMatch +(`.coreMatch.st`) files, providing syntax highlighting, comment +support, and bracket matching. ## Installation @@ -8,20 +10,32 @@ Add the following to your Emacs config (e.g., `~/.emacs.d/init.el`): ```elisp (load-file "/path/to/Strata/editors/emacs/core-st-mode.el") +(load-file "/path/to/Strata/editors/emacs/coreMatch-st-mode.el") ``` -All `.core.st` files will now open in `core-st-mode` automatically. +`.core.st` files open in `core-st-mode`; `.coreMatch.st` open in +`coreMatch-st-mode`, which adds the `match` and `arm` keywords on top +of Core. Alternatively, if the directory is on your `load-path`: ```elisp (require 'core-st-mode) +(require 'coreMatch-st-mode) +``` + +## Regenerating after a grammar change + +```bash +lake env lean --run editors/GenSyntax.lean all ``` ## Adding support for other Strata dialects -Strata has other dialect extensions (e.g., `.laurel.st`). To add highlighting for another dialect, copy `core-st-mode.el` as a starting point, adjust the keyword lists and `auto-mode-alist` entry for the new extension, and load it the same way. +Add a `DialectGenSpec` in `editors/GenSyntax.lean` referencing the new +dialect (list any imported dialects in `dialects` so inherited ops show +up), then re-run the generator. ## Uninstall -Remove the line from your Emacs config. +Remove the line(s) from your Emacs config. diff --git a/editors/emacs/core-st-mode.el b/editors/emacs/core-st-mode.el index 6bcfb271d4..0956f48b16 100644 --- a/editors/emacs/core-st-mode.el +++ b/editors/emacs/core-st-mode.el @@ -1,6 +1,6 @@ ;;; core-st-mode.el --- Major mode for Strata Core (.core.st) files -*- lexical-binding: t; -*- -;; AUTO-GENERATED from the Core DDM grammar. +;; AUTO-GENERATED from the Strata DDM grammar. ;; Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean emacs ;; Keywords diff --git a/editors/emacs/coreMatch-st-mode.el b/editors/emacs/coreMatch-st-mode.el new file mode 100644 index 0000000000..cf7c52fbaa --- /dev/null +++ b/editors/emacs/coreMatch-st-mode.el @@ -0,0 +1,85 @@ +;;; coreMatch-st-mode.el --- Major mode for Strata CoreMatch (.coreMatch.st) files -*- lexical-binding: t; -*- + +;; AUTO-GENERATED from the Strata DDM grammar. +;; Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean emacs + +;; Keywords +(defvar coreMatch-st-keywords + '( "var" "assume" "assert" "cover" "if" "else" "havoc" "invariant" + "decreases" "while" "out" "inout" "call" "exit" "free" "ensures" + "requires" "spec" "procedure" "type" "const" "function" "inline" + "rec" "axiom" "distinct" "datatype" "old" "forall" "exists" + "program" "match" "arm")) + +(defvar coreMatch-st-types + '( "bool" "int" "string" "regex" "real" "bv1" "bv8" "bv16" "bv32" + "bv64" "Map" "Sequence")) + +(defvar coreMatch-st-constants + '( "true" "false" "null")) + +(defvar coreMatch-st-operators + '( "div" "mod" "sdiv" "smod" "safesdiv" "safesmod")) + +(defvar coreMatch-st-builtins + '( "Sequence.length" "Sequence.select" "Sequence.append" + "Sequence.build" "Sequence.update" "Sequence.contains" + "Sequence.take" "Sequence.drop" "str.len" "str.concat" "str.substr" + "str.to.re" "str.in.re" "str.prefixof" "str.suffixof" "re.allchar" + "re.all" "re.range" "re.concat" "re.*" "re.+" "re.loop" "re.union" + "re.inter" "re.comp" "re.none" "Int.DivT" "Int.ModT")) + +;; Font-lock rules +(defvar coreMatch-st-font-lock-keywords + (let ((kw-re (regexp-opt coreMatch-st-keywords 'symbols)) + (ty-re (regexp-opt coreMatch-st-types 'symbols)) + (ct-re (regexp-opt coreMatch-st-constants 'symbols)) + (op-re (regexp-opt coreMatch-st-operators 'symbols)) + (bi-re (regexp-opt coreMatch-st-builtins 'symbols))) + `((,kw-re . font-lock-keyword-face) + (,ty-re . font-lock-type-face) + (,ct-re . font-lock-constant-face) + (,op-re . font-lock-keyword-face) + (,bi-re . font-lock-builtin-face) + ;; Attributes: @[...] + ("@\\[[^]]*\\]" . font-lock-preprocessor-face) + ;; Labels: [name]: + ("\\[\\([a-zA-Z_][a-zA-Z0-9_]*\\)\\]\\s-*:" 1 font-lock-function-name-face) + ;; Numeric literals + ("\\b[0-9]+\\(?:\\.[0-9]+\\)?\\b" . font-lock-constant-face)))) + +;; Syntax table +(defvar coreMatch-st-mode-syntax-table + (let ((st (make-syntax-table))) + ;; // line comments + (modify-syntax-entry ?/ ". 12" st) + (modify-syntax-entry ?\n ">" st) + ;; String literals + (modify-syntax-entry ?\" "\"" st) + ;; Backslash escapes in strings + (modify-syntax-entry ?\\ "\\" st) + ;; Brackets + (modify-syntax-entry ?\( "()" st) + (modify-syntax-entry ?\) ")(" st) + (modify-syntax-entry ?\{ "(}" st) + (modify-syntax-entry ?\} "){" st) + (modify-syntax-entry ?\[ "(]" st) + (modify-syntax-entry ?\] ")[" st) + ;; Dot and underscore are symbol constituents + (modify-syntax-entry ?. "_" st) + (modify-syntax-entry ?_ "_" st) + st)) + +;;;###autoload +(define-derived-mode coreMatch-st-mode prog-mode "CoreMatch.st" + "Major mode for editing Strata CoreMatch (.coreMatch.st) files." + :syntax-table coreMatch-st-mode-syntax-table + (setq-local font-lock-defaults '(coreMatch-st-font-lock-keywords)) + (setq-local comment-start "// ") + (setq-local comment-end "")) + +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.coreMatch\\.st\\'" . coreMatch-st-mode)) + +(provide 'coreMatch-st-mode) +;;; coreMatch-st-mode.el ends here diff --git a/editors/vscode/README.md b/editors/vscode/README.md index d84b882e27..bff82014da 100644 --- a/editors/vscode/README.md +++ b/editors/vscode/README.md @@ -1,6 +1,7 @@ # Strata Syntax Highlighting for VSCode -Syntax highlighting for Strata Core (`.core.st`) files. +Syntax highlighting for Strata Core (`.core.st`) and Strata CoreMatch +(`.coreMatch.st`) files. ## Installation @@ -12,15 +13,22 @@ ln -s /path/to/Strata/editors/vscode ~/.vscode/extensions/strata-st Then reload VSCode via the Command Palette: **Developer: Reload Window**. -All `.core.st` files will now have syntax highlighting, bracket matching, auto-closing pairs, and comment toggling. +`.core.st` files use `core-st`; `.coreMatch.st` use `coreMatch-st`, +which adds the `match` and `arm` keywords on top of Core. ## Adding support for other Strata dialects -Strata has other dialect extensions (e.g., `.laurel.st`). To add highlighting for another dialect: +Grammar files in `syntaxes/` are auto-generated. Regenerate from the +repository root: -1. Add a new entry to the `"languages"` array in `package.json` with the appropriate extension. -2. Create a new TextMate grammar in `syntaxes/` if the dialect has different syntax, or reuse `core-st.tmLanguage.json` if it shares the same grammar. -3. Wire the language to its grammar in the `"grammars"` array in `package.json`. +```bash +lake env lean --run editors/GenSyntax.lean all +``` + +To add a new dialect: add a `DialectGenSpec` in `editors/GenSyntax.lean` +(list any imported dialects in `dialects` so inherited ops show up), +re-run the generator, then add `languages` and `grammars` entries in +`package.json` pointing at the new `syntaxes/.tmLanguage.json`. ## Uninstall diff --git a/editors/vscode/package.json b/editors/vscode/package.json index b9ea8d5454..df43ace62e 100644 --- a/editors/vscode/package.json +++ b/editors/vscode/package.json @@ -3,7 +3,7 @@ "displayName": "Strata", "publisher": "strata-org", "description": "Syntax highlighting for Strata dialect files", - "version": "0.1.0", + "version": "0.2.0", "engines": { "vscode": "^1.60.0" }, @@ -15,6 +15,12 @@ "aliases": ["Strata Core", "core-st"], "extensions": [".core.st"], "configuration": "./language-configuration.json" + }, + { + "id": "coreMatch-st", + "aliases": ["Strata CoreMatch", "coreMatch-st"], + "extensions": [".coreMatch.st"], + "configuration": "./language-configuration.json" } ], "grammars": [ @@ -22,6 +28,11 @@ "language": "core-st", "scopeName": "source.core-st", "path": "./syntaxes/core-st.tmLanguage.json" + }, + { + "language": "coreMatch-st", + "scopeName": "source.coreMatch-st", + "path": "./syntaxes/coreMatch-st.tmLanguage.json" } ] } diff --git a/editors/vscode/syntaxes/coreMatch-st.tmLanguage.json b/editors/vscode/syntaxes/coreMatch-st.tmLanguage.json new file mode 100644 index 0000000000..3595c23580 --- /dev/null +++ b/editors/vscode/syntaxes/coreMatch-st.tmLanguage.json @@ -0,0 +1,97 @@ +{ + "$schema": "https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json", + "_comment": "AUTO-GENERATED from the CoreMatch DDM grammar. Do not edit by hand; run: lake env lean --run editors/GenSyntax.lean vscode", + "name": "Strata CoreMatch", + "scopeName": "source.coreMatch-st", + "patterns": [ + { "include": "#comment" }, + { "include": "#string" }, + { "include": "#attribute" }, + { "include": "#label" }, + { "include": "#number" }, + { "include": "#keyword" }, + { "include": "#type" }, + { "include": "#constant" }, + { "include": "#operator" }, + { "include": "#function-call" }, + { "include": "#identifier" } + ], + "repository": { + "comment": { + "name": "comment.line.double-slash.coreMatch-st", + "match": "//.*$" + }, + "string": { + "name": "string.quoted.double.coreMatch-st", + "begin": "\"", + "end": "\"", + "patterns": [ + { + "name": "constant.character.escape.coreMatch-st", + "match": "\\\\." + } + ] + }, + "attribute": { + "name": "meta.attribute.coreMatch-st", + "match": "@\\[[^\\]]*\\]", + "captures": { + "0": { "name": "entity.other.attribute-name.coreMatch-st" } + } + }, + "label": { + "name": "meta.label.coreMatch-st", + "match": "\\[([a-zA-Z_][a-zA-Z0-9_]*)\\]\\s*:", + "captures": { + "0": { "name": "entity.name.label.coreMatch-st" }, + "1": { "name": "entity.name.tag.coreMatch-st" } + } + }, + "number": { + "patterns": [ + { + "name": "constant.numeric.decimal.coreMatch-st", + "match": "\\b[0-9]+(\\.[0-9]+)?\\b" + } + ] + }, + "keyword": { + "name": "keyword.coreMatch-st", + "match": "\\b(var|assume|assert|cover|if|else|havoc|invariant|decreases|while|out|inout|call|exit|free|ensures|requires|spec|procedure|type|const|function|inline|rec|axiom|distinct|datatype|old|forall|exists|program|match|arm)\\b" + }, + "type": { + "name": "support.type.coreMatch-st", + "match": "\\b(bool|int|string|regex|real|bv1|bv8|bv16|bv32|bv64|Map|Sequence)\\b" + }, + "constant": { + "name": "constant.language.coreMatch-st", + "match": "\\b(true|false|null)\\b" + }, + "operator": { + "patterns": [ + { + "name": "keyword.operator.assignment.coreMatch-st", + "match": ":=" + }, + { + "name": "keyword.operator.word.coreMatch-st", + "match": "\\b(div|mod|sdiv|smod|safesdiv|safesmod)\\b" + }, + { + "name": "keyword.operator.symbol.coreMatch-st", + "match": "(safe_neg|safe-|safe\\+|safe\\*|<==>|>=s|==>|>>s|<=s|/t|\\|\\||>=|%t|<<|>>|&&|<=|==|!=|s|>|\\^|\\+|\\*|/|%|!|-|~|&|<|\\|)" + } + ] + }, + "function-call": { + "match": "\\b(Sequence\\.length|Sequence\\.select|Sequence\\.append|Sequence\\.build|Sequence\\.update|Sequence\\.contains|Sequence\\.take|Sequence\\.drop|str\\.len|str\\.concat|str\\.substr|str\\.to\\.re|str\\.in\\.re|str\\.prefixof|str\\.suffixof|re\\.allchar|re\\.all|re\\.range|re\\.concat|re\\.\\*|re\\.\\+|re\\.loop|re\\.union|re\\.inter|re\\.comp|re\\.none|Int\\.DivT|Int\\.ModT|bvconcat\\{[0-9]+\\}\\{[0-9]+\\}|bvextract\\{[0-9]+\\}\\{[0-9]+\\}\\{[0-9]+\\})\\b", + "captures": { + "1": { "name": "support.function.builtin.coreMatch-st" } + } + }, + "identifier": { + "name": "variable.other.coreMatch-st", + "match": "\\b[a-zA-Z_$][a-zA-Z0-9_$]*\\b" + } + } +} \ No newline at end of file From ded45596cfe6b96e827b075cb6d71775237f095d Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 8 May 2026 14:07:51 -0700 Subject: [PATCH 8/8] CoreMatch: add `lake exe coreMatchCheck` for per-file iteration Quick CLI that loads the CoreMatch DDM dialect, parses a single `.coreMatch.st` file, runs the redundancy / exhaustiveness checker, and lowers it to a `Core.Program`. Prints `OK: decls` (with optional `--show-decls` summary) or `ERR: `. Useful for iterating on individual programs in `Examples/pattern_matching/` without rebuilding the full test suite. --- Scripts/CoreMatchCheck.lean | 72 +++++++++++++++++++++++++++++++++++++ lakefile.toml | 4 +++ 2 files changed, 76 insertions(+) create mode 100644 Scripts/CoreMatchCheck.lean diff --git a/Scripts/CoreMatchCheck.lean b/Scripts/CoreMatchCheck.lean new file mode 100644 index 0000000000..5e9674574c --- /dev/null +++ b/Scripts/CoreMatchCheck.lean @@ -0,0 +1,72 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import Strata.Languages.CoreMatch.Verify +import Strata.Languages.CoreMatch.DDMTransform.StrataGen +import Strata.DDM.Elab + +/-! +Per-file iteration helper for the CoreMatch dialect. Invoked as +`lake exe coreMatchCheck [--show-decls]`; prints +`OK: decls` on success or `ERR: ` on failure. +-/ + +open Strata +open Lambda + +private def declSummary (d : Core.Decl) : String := + match d with + | .type t _ => + match t with + | .data block => + let names := block.map (·.name) + s!" type (data) {names}" + | .con tc => s!" type {tc.name}" + | .syn ts => s!" type {ts.name} (synonym)" + | .ax a _ => s!" axiom {a.name}" + | .distinct n _ _ => s!" distinct {n.name}" + | .proc p _ => s!" procedure {p.header.name.name}" + | .func f _ => + let kind := if f.isRecursive then "rec function" else "function" + s!" {kind} {f.name.name}" + | .recFuncBlock fs _ => + let names := fs.map (·.name.name) + s!" rec block {names}" + +private def runOnFile (path : System.FilePath) (showDecls : Bool) : IO UInt32 := do + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := + Strata.Elab.LoadedDialects.ofDialects! + #[Strata.initDialect, Strata.Core, Strata.CoreMatch] + let leanEnv ← Lean.mkEmptyEnvironment 0 + let prog ← + match Strata.Elab.elabProgram dialects leanEnv input with + | .ok p => pure p + | .error errors => + let mut msg : String := "ERR: parse failed:" + for e in errors do + msg := msg ++ s!"\n {e.pos.line}:{e.pos.column}: {← e.data.toString}" + IO.eprintln msg + return (1 : UInt32) + match Strata.CoreMatch.Verify.parseToCore prog path.toString with + | .error e => + IO.eprintln s!"ERR: lowering failed: {e.format none}" + return (1 : UInt32) + | .ok cp => + IO.println s!"OK: {cp.decls.length} decls" + if showDecls then + for d in cp.decls do + IO.println (declSummary d) + return (0 : UInt32) + +def main (args : List String) : IO UInt32 := do + match args with + | [] | ["--help"] => + IO.println "Usage: lake exe coreMatchCheck [--show-decls]" + return (0 : UInt32) + | path :: rest => + let showDecls := rest.contains "--show-decls" + runOnFile path showDecls diff --git a/lakefile.toml b/lakefile.toml index b59a11c9e8..e040cd1dc4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -45,3 +45,7 @@ root = "Scripts.ImportStats" [[lean_exe]] name = "DiffTestCore" + +[[lean_exe]] +name = "coreMatchCheck" +root = "Scripts.CoreMatchCheck"