From f2841d8d4d88b0bf46c4b1e659c52a0387929e9a Mon Sep 17 00:00:00 2001 From: Michael Hicks Date: Wed, 8 Jul 2026 13:41:09 +0000 Subject: [PATCH 1/5] Support structure-parameterized output types in the constrained deriver Teach derive_generator / derive_mutual to produce values of an inductive relation whose output type is parameterized by a structure (rather than a plain Sort/type parameter), as in Strata's LExpr T / LExpr.HasTypeA. Three coordinated, strictly-additive changes: 1. Don't lift fixed, ungeneratable subterms during conclusion flattening. Utils.lean gains allFVarsFixed / isFixedUngenerable and threads a fixed set of input fvars through collectUnmatchable{,Proper}Subterms; a subterm determined entirely by fixed inputs whose type has no Arbitrary instance (e.g. a structure parameter projection T.mono) is left in place instead of lifted into a generated unknown. DeriveConstrainedProducer.lean adds the fixedFVars parameter to linearizeAndFlatten and computes it from the conclusion's non-output bare-fvar arguments. 2. Emit per-field producer-instance binders for structure parameters. MakeConstrainedProducerInstance.lean gains expandStructInstBinders (which recursively walks a structure-typed parameter, emitting [className proj] for each Type-valued leaf) and mkProducerParamInstBinders, threaded through both the single-instance and mutual-def emission paths (struct-field binders innermost in the latter) and all wrapper instance commands. 3. Drop implicit constructor arguments from conclusion outputs. MExp.lean gains dropImplicitCtorArgsExpr and makes scheduleToMExp monadic, so implicit args (e.g. an output type's structure parameter) are omitted and re-inferred by Lean rather than mis-placed positionally. Also add the missing Enum Unit primitive instance alongside Enum Bool, and the generatableVars -> generableVars rename in SearchTree.lean. Regression: SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean derives a generator and an enumerator together for a two-field (one nested) structure-parameterized STLC typing relation over the genuine abstract Tm P. --- Specimen/DeriveConstrainedProducer.lean | 26 ++- Specimen/Enumerators.lean | 4 + Specimen/MExp.lean | 48 +++++- Specimen/MakeConstrainedProducerInstance.lean | 104 +++++++++++- Specimen/SearchTree.lean | 4 +- Specimen/Utils.lean | 49 +++++- SpecimenTest.lean | 1 + .../DeriveStructParamGenerator.lean | 159 ++++++++++++++++++ 8 files changed, 372 insertions(+), 23 deletions(-) create mode 100644 SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean index 4455630..6ce46ea 100644 --- a/Specimen/DeriveConstrainedProducer.lean +++ b/Specimen/DeriveConstrainedProducer.lean @@ -265,10 +265,14 @@ def getScheduleSort (conclusion : HypothesisExpr) - Note: it is the caller's responsibility to check that `conclusion` does indeed contain a non-trivial function application (e.g. by using `containsNonTrivialFuncApp`) -/ def linearizeAndFlatten - (hypotheses : Array Expr) (conclusion : Expr) (outputIndices : List Nat) (localCtx : LocalContext) : + (hypotheses : Array Expr) (conclusion : Expr) (outputIndices : List Nat) (localCtx : LocalContext) + (fixedFVars : Std.HashSet FVarId := {}) : UnifyM (Array Expr × Expr × List (Name × Expr) × LocalContext) := do - -- Phase 1: flatten function calls into fresh unknowns with equality hypotheses - let funcAppExprs ← collectUnmatchableProperSubterms conclusion + -- Phase 1: flatten function calls into fresh unknowns with equality hypotheses. + -- `fixedFVars` are the producer's fixed inputs; a subterm determined entirely + -- by them (e.g. a type parameter `T.mono` where `T` is an input) is left in + -- place rather than lifted into a generated unknown. + let funcAppExprs ← collectUnmatchableProperSubterms fixedFVars conclusion trace[plausible.deriving.arbitrary] m!"Unmatchable exprs: {funcAppExprs} In conclusion: {conclusion}" withLCtx' localCtx do @@ -473,8 +477,22 @@ def getScheduleForInductiveRelationConstructor -- equal to the result of the function call, and adding an extra hypothesis asserting equality -- between the function call and the variable. -- `freshNamesAndTypes` is a list containing the names & types of the fresh variables produced during this procedure. + -- Identify fixed inputs as fvars, so flattening can leave subterms that are + -- determined entirely by the inputs (e.g. an output type's structure + -- parameter `T.mono`) in place instead of trying to generate them. The + -- conclusion's arguments at non-output (input) positions that are bare + -- variables are exactly those inputs (e.g. the inductive's parameter `T`). + let curLCtx ← getLCtx + let conclArgs := conclusion.getAppArgs + let fixedFVars : Std.HashSet FVarId := Id.run do + let mut s : Std.HashSet FVarId := {} + for h : i in [:conclArgs.size] do + if i ∉ outputIndices then + if let .fvar fid := conclArgs[i] then + s := s.insert fid + return s let (updatedHypotheses, updatedConclusion, freshNamesAndTypes, updatedLocalCtx) ← - linearizeAndFlatten hypotheses conclusion outputIndices (← getLCtx) + linearizeAndFlatten hypotheses conclusion outputIndices curLCtx fixedFVars -- Enter the updated `LocalContext` containing the fresh variable that was created when rewriting the conclusion withLCtx' updatedLocalCtx (do let hypothesisExprs := (← monadLift (updatedHypotheses.toList.mapM (exprToHypothesisExpr ctorName))).toArray diff --git a/Specimen/Enumerators.lean b/Specimen/Enumerators.lean index 8dc3fe9..d498950 100644 --- a/Specimen/Enumerators.lean +++ b/Specimen/Enumerators.lean @@ -128,6 +128,10 @@ end EnumeratorCombinators -- Some simple `Enum` instances +/-- `Enum` instance for `Unit` (its single value) -/ +instance : Enum Unit where + enum := pureEnum () + /-- `Enum` instance for `Bool` -/ instance : Enum Bool where enum := pureEnum false <|> pureEnum true diff --git a/Specimen/MExp.lean b/Specimen/MExp.lean index e76d84f..112b4fe 100644 --- a/Specimen/MExp.lean +++ b/Specimen/MExp.lean @@ -177,6 +177,38 @@ partial def constructorExprToMExp (exp : Explicit) (expr : ConstructorExpr) : ME | .Lit l => .MLit l | .CSort lvl => .MSort lvl +/-- Recursively drop the arguments of every *data constructor* application in a + `ConstructorExpr` that sit at implicit / instance-implicit positions. + + A conclusion output is emitted in implicit-allowing form, so a constructor's + implicit arguments — most importantly an output inductive's structure + type-parameter, e.g. `LExpr.const`'s `T` in `LExpr.const (T.mono) m c`, but + also ordinary ones like `Option.some`'s `α` — must be omitted and left for + Lean to infer from the explicit arguments. Constructors whose argument count + does not match their arity are left unchanged. `FuncApp`/`TyCtor` nodes are + traversed but their own argument lists are not filtered (function/type-former + applications are emitted implicit-allowing already). -/ +partial def dropImplicitCtorArgsExpr (ce : ConstructorExpr) : MetaM ConstructorExpr := do + match ce with + | .Ctor c args => + let args ← args.mapM dropImplicitCtorArgsExpr + -- Only genuine data constructors have implicit-position args to drop; some + -- `.Ctor` nodes are actually abbreviations/defs (e.g. `LExprParams.mono`). + unless (← getEnv).isConstructor c do return .Ctor c args + let ctorType := (← getConstInfoCtor c).type + let argsArr := args.toArray + let kept ← Meta.forallTelescopeReducing ctorType fun bvars _ => do + if bvars.size ≠ argsArr.size then return args + let mut result := #[] + for h : i in [:argsArr.size] do + if (← bvars[i]!.fvarId!.getDecl).binderInfo.isExplicit then + result := result.push argsArr[i]! + return result.toList + return .Ctor c kept + | .TyCtor c args => return .TyCtor c (← args.mapM dropImplicitCtorArgsExpr) + | .FuncApp f args => return .FuncApp f (← args.mapM dropImplicitCtorArgsExpr) + | other => return other + partial def mexpToConstructorExpr (m : MExp) : Option ConstructorExpr := match m with | .MId u => return .Unknown u @@ -475,7 +507,7 @@ def scheduleStepToMExp (step : ScheduleStep) (defFuel : MExp) (k : MExp) (output for the function we are deriving (these correspond to `size` and `initSize` in the QuickChick code for the derived functions) - `targetInductive` is the inductive we're generating for (used to detect same-type deps) -/ -def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recType : Expr) (fuelPrimeName : Name := `fuel') (sizePrimeName : Name := `size') (targetInductive : Name := `_unknown) : CompileScheduleM MExp := +def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recType : Expr) (fuelPrimeName : Name := `fuel') (sizePrimeName : Name := `size') (targetInductive : Name := `_unknown) : CompileScheduleM MExp := do let (scheduleSteps, scheduleSort) := schedule -- Compute the size expression: split budget across all size-consuming calls -- (self-recursive, mutual, and non-recursive calls to the same inductive) @@ -485,17 +517,19 @@ def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recTyp else .MApp .allExplicit (.MConst ``Nat.div) [.MId sizePrimeName, .MLit (.natVal numSizeCalls)] -- Determine the *epilogue* of the schedule (i.e. what happens after we -- have finished executing all the `scheduleStep`s) - let epilogue := + let epilogue ← do match scheduleSort with | .ProducerSchedule _ conclusionOutputs => - -- Convert all the outputs in the conclusion to `mexp`s + -- Drop implicit constructor arguments (e.g. an output type's structure + -- parameter), then convert all the outputs in the conclusion to `mexp`s. + let conclusionOutputs ← conclusionOutputs.mapM (fun ce => (monadLift (dropImplicitCtorArgsExpr ce) : CompileScheduleM _)) let conclusionMExps := constructorExprToMExp .allowImplicit <$> conclusionOutputs -- If there are multiple outputs, wrap them in a tuple match conclusionMExps with | [] => panic! "No outputs being returned in producer schedule" - | [output] => MExp.MRet output - | outputs => MExp.MRet (tupleOfList (fun e1 e2 => .MApp .allowImplicit (.MConst ``Prod.mk) [e1, e2]) outputs outputs[0]?) - | .CheckerSchedule => okTrue + | [output] => pure (MExp.MRet output) + | outputs => pure (MExp.MRet (tupleOfList (fun e1 e2 => .MApp .allowImplicit (.MConst ``Prod.mk) [e1, e2]) outputs outputs[0]?)) + | .CheckerSchedule => pure okTrue | .TheoremSchedule conclusion typeClassUsed => -- Create a pattern-match on the result of hte checker -- on the conclusion, returning `.ok true` or `.ok false` accordingly @@ -503,7 +537,7 @@ def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recTyp let scrutinee := if typeClassUsed then decOptChecker conclusionMExp mfuel else conclusionMExp - matchExceptBool scrutinee okTrue okFalse + pure (matchExceptBool scrutinee okTrue okFalse) -- Fold over the `scheduleSteps` and convert each of them to a functional `MExp` -- Note that the fold composes the `MExp`, and we use `foldr` since -- we want the `epilogue` to be the base-case of the fold diff --git a/Specimen/MakeConstrainedProducerInstance.lean b/Specimen/MakeConstrainedProducerInstance.lean index 9ac375a..498ee31 100644 --- a/Specimen/MakeConstrainedProducerInstance.lean +++ b/Specimen/MakeConstrainedProducerInstance.lean @@ -53,6 +53,62 @@ def mkTypeClassInstanceBinders (typeParams : Array Name) (typeClasses : Array Na `(Lean.Elab.Deriving.instBinderF| [$(mkIdent tc) $(mkIdent param)]) return TSyntaxArray.mk instances +open TSyntax.Compat in +/-- Recursively expand a *structure-typed* parameter into `[className proj]` + instance binders for each leaf field of type `Type u`. Mirrors + `expandStructBinders` in `Specimen.DeriveArbitrary` (the unconstrained + `deriving Arbitrary` path), which is what lets `Arbitrary (LExpr T)` be + derived for a structure parameter `T`: the constrained producer instance + needs the same per-field binders (e.g. `[Arbitrary T.base.Metadata]`) so the + metadata fields carried by each constructor can be generated. + + `ty` is the type being walked (the parameter's type, or a field's type as we + recurse) and `syn` is the matching surface syntax (the parameter identifier, + or a projection chain into it). A leaf `Type u` field yields `[className syn]`; + a structure field recurses into its own fields. Returns `#[]` for fields that + are neither Types nor structures-of-Types — the conservative, + behavior-preserving choice for the constrained path. -/ +partial def expandStructInstBinders (className : Name) (ty : Expr) (syn : TSyntax `term) : + TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + if ty.isSort then + -- A `Type u` leaf: emit `[className syn]`. + return #[← `(Lean.Elab.Deriving.instBinderF| [$(mkCIdent className):ident $syn])] + let env ← getEnv + let some sName := ty.constName? | return #[] + let some sInfo := getStructureInfo? env sName | return #[] + let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + -- The field's declared type, read as the codomain of the projection's + -- signature `∀ (_ : sName ..), fieldType`. Structure fields here are the + -- metadata-configuration types, whose field types do not depend on the value. + -- Limitation: `mkConst projName` is built without universe-level arguments, so + -- for a *universe-polymorphic* structure parameter `projType` would be computed + -- at the wrong universe. We don't support such parameters (they are rare in + -- practice; all current Strata params are `Type 0`); supporting them would mean + -- extracting `ty`'s universe levels and passing them to `mkConst` here. + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + let projSyn ← `($(mkIdent projName) $syn) + result := result ++ (← expandStructInstBinders className projType projSyn) + return result + +/-- Build the unconstrained-producer instance binders for a list of + non-target inductive parameters. For a `Sort`-typed parameter `α`, emits + `[className α] [DecidableEq α]` (the existing behavior). For a *structure* + parameter `T`, expands it into per-field binders via `expandStructInstBinders` + (e.g. `[className T.base.Metadata]` …) so the structure's metadata fields can + be generated. Parameters of other types contribute no binders. -/ +def mkProducerParamInstBinders (className : Name) + (params : Array (Name × Expr)) : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] + for (paramName, paramType) in params do + if paramType.isSort then + result := result ++ (← mkTypeClassInstanceBinders #[paramName] #[className, ``DecidableEq]) + else + result := result ++ (← expandStructInstBinders className paramType (mkIdent paramName)) + return result + /-- Finds the index of the argument in the inductive application for the value we wish to generate (i.e. finds `i` s.t. `args[i] == targetVar`) -/ def findTargetVarIndex (targetVar : FVarId) (args : Array Expr) : (Option Nat) := do @@ -135,6 +191,10 @@ def mkConstrainedProducerTypeClassInstance let mut outerParams := #[] let mut outputTypeSyntaxes : Array (TSyntax `term) := #[] let mut typeParams := #[] + -- Non-target, non-sort *structure* parameters (e.g. `T : LExprParams`): we + -- need per-field unconstrained-producer instances for these (see + -- `mkProducerParamInstBinders`). + let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do -- Only add a function parameter if the argument to the inductive relation is not a target variable -- (We skip the target variables since those are the values we wish to generate) @@ -152,6 +212,8 @@ def mkConstrainedProducerTypeClassInstance `(Term.letIdBinder| ($innerParamIdent : $paramTypeSyntax)) innerParams := innerParams.push innerParam + if !paramType.isSort then + structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -203,7 +265,11 @@ def mkConstrainedProducerTypeClassInstance | .Generator => ``Plausible.Arbitrary | .Enumerator => ``Enum - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + -- Per-field unconstrained-producer instances for structure parameters (e.g. + -- `[Arbitrary T.base.Metadata]`), so their fields can be generated. + let structParamInstances ← mkProducerParamInstBinders producerUnconstrainedClass structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structParamInstances let fuelVal := Lean.Option.get (← getOptions) specimen.fuel let fuelLit := Syntax.mkNumLit (toString fuelVal) @@ -264,6 +330,8 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($initSizeIdent : $natIdent))) innerParamBinders := innerParamBinders.push (← `(($sizeIdent : $natIdent))) + -- Non-target, non-sort structure parameters needing per-field producer instances. + let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do if paramType.isSort then typeParams := typeParams.push paramName @@ -274,6 +342,7 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : Sort _))) else innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : $paramTypeSyntax))) + structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -325,11 +394,23 @@ def mkConstrainedProducerMutualPieces | .Enumerator => ``Enum #[producerUnconstrainedClass, ``DecidableEq] let defTypeParamInstances ← mkTypeClassInstanceBinders typeParams typeClasses + -- Per-field producer instances for structure parameters (e.g. + -- `[Arbitrary T.base.Metadata]`). These reference value params (`T`), so they + -- are placed *innermost* — after all value params — where those are in scope. + -- The `def` itself always builds the underlying producer, so it uses the + -- producer-based unconstrained class regardless of `deriveSort`. + let structParamClass := match producerSort with + | .Generator => ``Plausible.Arbitrary + | .Enumerator => ``Enum + let structParamInstances ← mkProducerParamInstBinders structParamClass structParams -- Emit the def with ∀ type (supports instance binders inline) let defIdent := mkIdent globalDefName -- Build ∀ type with instance binders interleaved after Sort-typed params let mut defType ← pure optionTProducerType + -- Innermost: structure-parameter field instances (all value params in scope). + for instBinder in structParamInstances.reverse do + defType ← `(∀ $instBinder:bracketedBinder, $defType) -- Add non-Sort value params (from right) let insertIdx := 3 + typeParams.size for (name, ty) in allParamNamesAndTypes[insertIdx:].toArray.reverse do @@ -340,9 +421,12 @@ def mkConstrainedProducerMutualPieces -- Add Sort-typed params + fuel/initSize/size (from right) for (name, ty) in allParamNamesAndTypes[:insertIdx].toArray.reverse do defType ← `(($name : $ty) → $defType) - -- Lambda includes instance binders at the same position + -- Lambda includes instance binders at the same positions as the ∀ type: + -- sort-param instances after the sort params, struct-field instances innermost. let instParams : Array (TSyntax `term) := defTypeParamInstances.map (fun b => ⟨b.raw⟩) - let allInnerParams := innerParamBinders[:insertIdx].toArray ++ instParams ++ innerParamBinders[insertIdx:].toArray + let structInstParams : Array (TSyntax `term) := structParamInstances.map (fun b => ⟨b.raw⟩) + let allInnerParams := innerParamBinders[:insertIdx].toArray ++ instParams + ++ innerParamBinders[insertIdx:].toArray ++ structInstParams let lambdaBody ← `(fun $allInnerParams* => $matchExpr) let defCmd ← `(command| def $defIdent : $defType := $lambdaBody) @@ -360,7 +444,10 @@ def mkConstrainedProducerMutualPieces | .Enumerator => #[``Enum, ``DecidableEq] let instCmd ← match deriveSort with | .Checker | .Theorem => do - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams instTypeClasses + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses + -- Per-field struct-param instances for the wrapper (Checker/Theorem → `Enum`). + let structInsts ← mkProducerParamInstBinders ``Enum structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $decOptTypeclass (@$(mkIdent inductiveName) $args*) where $unqualifiedDecOptFn:ident := fun $freshSizeIdent => $callExpr) @@ -371,7 +458,14 @@ def mkConstrainedProducerMutualPieces let producerTypeClassFunction := match producerSort with | .Generator => unqualifiedArbitrarySizedSTFn | .Enumerator => unqualifiedEnumSizedSTFn - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams instTypeClasses + let producerUnconstrainedClass := match producerSort with + | .Generator => ``Plausible.Arbitrary + | .Enumerator => ``Enum + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses + -- Per-field struct-param instances for the wrapper (Generator/Enumerator + -- → `Arbitrary`/`Enum`). + let structInsts ← mkProducerParamInstBinders producerUnconstrainedClass structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $producerTypeClass $targetTypeSyntax (fun $targetVarPattern => @$(mkIdent inductiveName) $args*) where $producerTypeClassFunction:ident := fun $freshSizeIdent => $callExpr) diff --git a/Specimen/SearchTree.lean b/Specimen/SearchTree.lean index cc68531..a010cbe 100644 --- a/Specimen/SearchTree.lean +++ b/Specimen/SearchTree.lean @@ -262,8 +262,8 @@ def lowerBoundScore {α v} [BEq α] [BEq v] (currentOrder : List α) (remaining vars.all (currentEnv.contains ·)) -- All vars already bound let guaranteedChecks := forcedChecks.filter (fun (_, vars) => - let generatableVars := vars -- For simple case, all vars are generatable - generatableVars.any (!arbitraryVars.contains ·)) -- Can't be arbitrary + let generableVars := vars -- For simple case, all vars are generable + generableVars.any (!arbitraryVars.contains ·)) -- Can't be arbitrary let primaryScore := currentScore + guaranteedChecks.length let secondaryScore := countGuaranteedArbitraries currentOrder remaining hypVarMap diff --git a/Specimen/Utils.lean b/Specimen/Utils.lean index 5465682..fdf927f 100644 --- a/Specimen/Utils.lean +++ b/Specimen/Utils.lean @@ -1,5 +1,6 @@ import Lean +import Plausible.Arbitrary open Lean Meta LocalContext Std @@ -245,12 +246,50 @@ partial def collectFVarOccurrences (e : Expr) (skipArgIndices : List Nat := []) | _ => acc aux e {} true +/-- True if every free variable of `e` is a fixed input (member of `fixed`). + Such a subterm is fully determined by the producer's inputs. -/ +def allFVarsFixed (fixed : Std.HashSet FVarId) (e : Expr) : Bool := + let fvarIds := (collectFVarOccurrences e).toList.map Prod.fst + !fvarIds.isEmpty && fvarIds.all fixed.contains + +/-- Whether a subterm should be left in place during flattening rather than + lifted into a generated unknown. This holds when the subterm is determined + entirely by fixed inputs (`allFVarsFixed`) *and* its type has no `Arbitrary` + instance — i.e. it could not be generated anyway, so it must stay fixed. + + The motivating case is an output inductive's structure type-parameter such as + `T.mono : LExprParamsT` (where `T` is a fixed input): `LExprParamsT` carries + metadata-configuration types and has no `Arbitrary` instance. Crucially, an + ordinary fixed value-level subterm like `n * n : Nat` is *not* skipped (since + `Arbitrary Nat` exists), so checker/derivation behavior for those is + unchanged. -/ +def isFixedUngenerable (fixed : Std.HashSet FVarId) (e : Expr) : MetaM Bool := do + if !allFVarsFixed fixed e then return false + let ty ← inferType e + -- Be conservative if the type isn't fully determined: only the original + -- (universe-mismatch) behavior is preserved by *not* skipping such subterms. + if ty.hasExprMVar || ty.hasLevelMVar then return false + -- The subterm is a candidate for an `Arbitrary` instance; if none can be + -- synthesized, keep the subterm fixed rather than lifting it to a generator. + let some cls ← (try some <$> Meta.mkAppM ``Plausible.Arbitrary #[ty] catch _ => pure none) + | return false + let inst ← (try Meta.synthInstance? cls catch _ => pure none) + return inst.isNone + /-`collectUnmatchableSubterms` traverses an expression from top down until it finds anything except a constructor application or a variable or an inductive. It collects all such subterms. These subterms we cannot match on during unifications so we -turn them later into equality constraints. -/ -partial def collectUnmatchableSubterms (e : Expr) : MetaM (List Expr) := do +turn them later into equality constraints. + +`fixed` is the set of fixed-input fvars: a subterm all of whose free variables +are fixed is determined by the inputs (e.g. a type parameter `T.mono` where `T` +is an input), so we leave it in place rather than lifting it into a generated +unknown. -/ +partial def collectUnmatchableSubterms (fixed : Std.HashSet FVarId) (e : Expr) : MetaM (List Expr) := do let eType ← inferType e if eType.isSort then return [] + -- A fixed subterm whose type has no `Arbitrary` instance (e.g. an output + -- type's structure parameter `T.mono`) cannot be generated; keep it in place. + if ← isFixedUngenerable fixed e then return [] match e with | .app .. | .const .. => do let (f, args) := e.getAppFnArgs @@ -258,7 +297,7 @@ partial def collectUnmatchableSubterms (e : Expr) : MetaM (List Expr) := do if inf.isDefinition then return [e] else - args.foldlM (fun acc arg => (· ++ acc) <$> collectUnmatchableSubterms arg) [] + args.foldlM (fun acc arg => (· ++ acc) <$> collectUnmatchableSubterms fixed arg) [] | .fvar .. => return [] | _ => return [e] -- If it is not an application or a const, it is also not matchable, so we -- should also flatten it out. @@ -266,11 +305,11 @@ partial def collectUnmatchableSubterms (e : Expr) : MetaM (List Expr) := do /-`collectUnmatchableProperSubterms` traverses an expression from top down (ignoring the head, which is a hypothesis that does not need to be matched on) until it finds anything except a constructor application or a variable or an inductive. It collects all such subterms. These subterms we cannot match on during unifications so we turn them later into equality constraints.-/ -partial def collectUnmatchableProperSubterms (e : Expr) : MetaM (List Expr) := +partial def collectUnmatchableProperSubterms (fixed : Std.HashSet FVarId) (e : Expr) : MetaM (List Expr) := match e with | .app .. => do let args := e.getAppArgs - args.foldlM (fun acc arg => (· ++ acc) <$> collectUnmatchableSubterms arg) [] + args.foldlM (fun acc arg => (· ++ acc) <$> collectUnmatchableSubterms fixed arg) [] | _ => return [] /-- Looks up a key in a list and returns the value along with the list without that entry -/ diff --git a/SpecimenTest.lean b/SpecimenTest.lean index 75af422..cfa1ffa 100644 --- a/SpecimenTest.lean +++ b/SpecimenTest.lean @@ -43,6 +43,7 @@ import SpecimenTest.DeriveArbitrary.MissingNonRecursiveConstructorTest import SpecimenTest.DeriveArbitrary.ParameterizedTypeTest import SpecimenTest.DeriveArbitrary.MutuallyRecursiveTypeTest import SpecimenTest.DeriveArbitrarySuchThat.DeriveSTLCGenerator +import SpecimenTest.DeriveArbitrarySuchThat.DeriveStructParamGenerator import SpecimenTest.DeriveArbitrarySuchThat.NonLinearPatternsTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputSTLCTest diff --git a/SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean b/SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean new file mode 100644 index 0000000..b20b11e --- /dev/null +++ b/SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean @@ -0,0 +1,159 @@ +import Plausible.Gen +import Plausible.Arbitrary +import Specimen.Enumerators +import Specimen.EnumeratorCombinators +import Specimen.ArbitrarySizedSuchThat +import Specimen.DeriveConstrainedProducer +import Specimen.DeriveArbitrary +import Specimen.DeriveEnum + +/-! # Deriving producers for a *structure-parameterized* STLC + +A small, self-contained regression witness for Specimen's support of inductive +relations whose output type is parameterized by a **structure** (rather than a +plain `Sort`/type parameter). The full-scale motivating case is Strata's +`LExpr T` / `LExpr.HasTypeA`; this reproduces the shape in miniature. + +The two ingredients Strata relies on, distilled: + +* A **structure parameter** `P : ExprParams` bundles the configuration types for + the expression language. Here it has **two** fields, one of which is **itself a + structure** — so the constructor fields are reached by projection chains like + `P.info.Metadata` (nested) and `P.VarId` (direct). Exercising both is what + checks the *recursive* field expansion in `expandStructInstBinders`. +* The typing relation `HasType` is stated over the genuine abstract `Tm P` (**no + monomorphization**), so those projections ride along as implicit arguments of + every constructor in the conclusion. + +Deriving for this shape needs all three coordinated deriver changes: don't lift +the fixed, ungeneratable parameter projections; emit `[Arbitrary P.info.Metadata]` +/ `[Arbitrary P.VarId]` field binders (recursively); and drop the implicit +parameter from constructor outputs so Lean re-infers it. + +The witness is simply that `derive_mutual` **elaborates** producers for this +relation. We ask it for both producer sorts at once — a generator and an +enumerator — so the struct-param field binders are exercised on both emission +paths (`[Arbitrary P.info.Metadata]` for the generator, the `[Enum …]` +counterparts for the enumerator). Tiny `#eval`s then draw from each derived +producer to confirm they actually run. -/ + +open Plausible +open ArbitrarySizedSuchThat + +set_option guard_msgs.diff true +set_option specimen.autoDeriveDeps true +set_option specimen.multiOutput true + +namespace StructParamSTLC + +/-- Object-language types: naturals and functions. -/ +inductive Ty where + | nat : Ty + | arrow : Ty → Ty → Ty + deriving Repr, BEq, DecidableEq, Inhabited + +/-- A nested single-field structure, used as one field of `ExprParams`. Reaching + its field from the parameter requires a **two-step** projection chain + (`P.info.Metadata`), which is what checks the recursion in the field walk. -/ +structure NodeInfo : Type 1 where + /-- The type of metadata carried by each expression node. -/ + Metadata : Type + deriving Inhabited + +/-- The **structure parameter** bundling the language's configuration types. Two + fields: a *nested structure* `info` (so metadata is `P.info.Metadata`) and a + *direct* type field `VarId` (so variable labels are `P.VarId`). Lives in + `Type 1` because it quantifies over `Type`. -/ +structure ExprParams : Type 1 where + /-- Per-node metadata configuration (itself a structure). -/ + info : NodeInfo + /-- The type of the opaque label attached to variable occurrences. -/ + VarId : Type + deriving Inhabited + +/-- Expressions, parameterized by the structure `P`. Every constructor carries a + metadata field `(m : P.info.Metadata)` — a *nested* projection — and `var` + additionally carries a `(name : P.VarId)` — a *direct* projection — so both + fields of the parameter appear in generated values. -/ +inductive Tm (P : ExprParams) : Type where + /-- A numeric literal. -/ + | lit (m : P.info.Metadata) (n : Nat) + /-- A de-Bruijn–indexed bound variable, tagged with an opaque `name`. -/ + | var (m : P.info.Metadata) (name : P.VarId) (idx : Nat) + /-- Addition of two naturals. -/ + | add (m : P.info.Metadata) (e1 e2 : Tm P) + /-- A lambda abstraction annotated with its argument type. -/ + | lam (m : P.info.Metadata) (dom : Ty) (body : Tm P) + /-- A function application. -/ + | app (m : P.info.Metadata) (fn arg : Tm P) + +/-- Context lookup as an *invertible* inductive relation (de-Bruijn indexing). + Keeping this a relation rather than `Γ[i]? = some τ` lets the deriver invert + it to produce in-scope variables directly, so this example needs no + hand-written delegated producer. -/ +inductive Lookup : List Ty → Nat → Ty → Prop where + | here : Lookup (τ :: Γ) 0 τ + | there : Lookup Γ n τ → Lookup (τ' :: Γ) (n + 1) τ + +/-- The typing relation over the genuine abstract `Tm P` (no monomorphization). + `Γ` is the de-Bruijn context (head = most recently bound variable). -/ +inductive HasType {P : ExprParams} : List Ty → Tm P → Ty → Prop where + | lit : HasType Γ (.lit m n) .nat + | var : Lookup Γ i τ → HasType Γ (.var m x i) τ + | add : HasType Γ e1 .nat → + HasType Γ e2 .nat → + HasType Γ (.add m e1 e2) .nat + | lam : HasType (dom :: Γ) body cod → + HasType Γ (.lam m dom body) (.arrow dom cod) + | app : HasType Γ fn (.arrow dom cod) → + HasType Γ arg dom → + HasType Γ (.app m fn arg) cod + +/-- Shallow, terminating unconstrained producers for `Ty` (the `lam` binder + annotation). Auto-derived ones could recurse without bound through `arrow`; + a small fixed selection is enough for the constrained producers. -/ +instance : Arbitrary Ty where + arbitrary := do + let choices : List Ty := [.nat, .arrow .nat .nat, .arrow .nat (.arrow .nat .nat)] + let n ← Plausible.Gen.chooseNatLt 0 choices.length (by decide) + return choices[n.val]! + +instance : Enum Ty where + enum := EnumeratorCombinators.oneOfWithDefault + (pure .nat) (pure <$> [Ty.nat, .arrow .nat .nat, .arrow .nat (.arrow .nat .nat)]) + +/-! ## Deriving a generator and an enumerator together (abstract `P`) + +One `derive_mutual` asks for both producer sorts from the same relation. Each +derived instance is universally quantified over `P` with the field binders +synthesized by walking the structure — `[Arbitrary P.info.Metadata] +[Arbitrary P.VarId]` for the generator, and the `[Enum …]` counterparts for the +enumerator. That this elaborates at all is the core regression witness. -/ +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : ExprParams) (Γ : List Ty) (τ : Ty) => ∃ e : Tm P, @HasType P Γ e τ), + enumerator (fun (P : ExprParams) (Γ : List Ty) (τ : Ty) => ∃ e : Tm P, @HasType P Γ e τ) + +/-! ## The derived producers actually run + +Monomorphize the parameter (both fields to `Unit`) and draw from each derived +producer, confirming they run and yield at least one term. -/ +abbrev P0 : ExprParams := ⟨⟨Unit⟩, Unit⟩ + +#guard_msgs(drop info) in +#eval show IO Unit from do + let mut n := 0 + for (Γ, τ) in [([], Ty.nat), ([.nat], .nat), ([], .arrow .nat .nat)] do + for s in List.range 6 do + let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun e => @HasType P0 Γ e τ) 4) (s * 7 + 1) + n := n + 1 + IO.println s!"derived generator produced {n} well-typed terms" + +#guard_msgs(drop info) in +#eval do + let results ← runSizedEnum + (EnumSizedSuchThat.enumSizedST (fun e => @HasType P0 [] e .nat)) 3 + IO.println s!"derived enumerator produced {results.length} results at [] ⊢ _ : nat" + +end StructParamSTLC From 7e60e252ee89703b3cae23aea122ccbfcbf511c2 Mon Sep 17 00:00:00 2001 From: Michael Hicks Date: Wed, 8 Jul 2026 15:59:11 +0000 Subject: [PATCH 2/5] updated Strata LExpr generation to use structure parameter capability --- SpecimenTest/StrataDefs/LambdaCore.lean | 49 ++++++ SpecimenTest/StrataLexprGen.lean | 190 ++++++++---------------- 2 files changed, 112 insertions(+), 127 deletions(-) diff --git a/SpecimenTest/StrataDefs/LambdaCore.lean b/SpecimenTest/StrataDefs/LambdaCore.lean index b23ab83..3490369 100644 --- a/SpecimenTest/StrataDefs/LambdaCore.lean +++ b/SpecimenTest/StrataDefs/LambdaCore.lean @@ -132,6 +132,12 @@ instance : DecidableEq LMonoTy := @[match_pattern] def LMonoTy.arrow (t1 t2 : LMonoTy) : LMonoTy := .tcons "arrow" [t1, t2] +/-- Return `some (dom, cod)` if the type is an arrow, `none` otherwise. +(`Strata/DL/Lambda/LTy.lean`) -/ +def LMonoTy.isArrow : LMonoTy → Option (LMonoTy × LMonoTy) + | .tcons "arrow" [dom, cod] => some (dom, cod) + | _ => none + /-! ## `Identifiers.lean` — identifiers (slice) -/ /-- Identifiers with a name and additional metadata. -/ @@ -244,4 +250,47 @@ inductive LExpr.HasTypeA {T : LExprParams} : List LMonoTy → LExpr T.mono → L HasTypeA Δ e2 τ → HasTypeA Δ (.eq m e1 e2) .bool +/-- Typecheck an annotated `LExpr`, returning `some τ` if well-typed, `none` +otherwise. `ctx` maps de Bruijn indices to their types from enclosing binders. +(`Strata/DL/Lambda/Denote/LExprAnnotated.lean`.) + +`LExpr.typeCheck` is proved equivalent to `HasTypeA` upstream, so it serves as +the authoritative soundness oracle for sampled terms. -/ +@[expose] +def LExpr.typeCheck {T : LExprParams} (ctx : List LMonoTy) : LExpr T.mono → Option LMonoTy + | .const _ c => some c.ty + | .op _ _ (some ty) => some ty + | .op _ _ none => none + | .fvar _ _ (some ty) => some ty + | .fvar _ _ none => none + | .bvar _ i => ctx[i]? + | .abs _ _ (some aty) body => do + let rty ← typeCheck (aty :: ctx) body + some (.arrow aty rty) + | .abs _ _ none _ => none + | .quant _ _ _ (some qty) tr body => do + let _ ← typeCheck (qty :: ctx) tr + let bty ← typeCheck (qty :: ctx) body + guard (bty == .bool) + some .bool + | .quant _ _ _ none _ _ => none + | .app _ fn arg => do + let fty ← typeCheck ctx fn + let aty ← typeCheck ctx arg + let (dom, cod) ← fty.isArrow + guard (dom == aty) + some cod + | .ite _ c t e => do + let cty ← typeCheck ctx c + let tty ← typeCheck ctx t + let ety ← typeCheck ctx e + guard (cty == .bool) + guard (tty == ety) + some tty + | .eq _ e1 e2 => do + let ty1 ← typeCheck ctx e1 + let ty2 ← typeCheck ctx e2 + guard (ty1 == ty2) + some .bool + end Lambda diff --git a/SpecimenTest/StrataLexprGen.lean b/SpecimenTest/StrataLexprGen.lean index 25e4445..5ef7eaa 100644 --- a/SpecimenTest/StrataLexprGen.lean +++ b/SpecimenTest/StrataLexprGen.lean @@ -12,30 +12,27 @@ import Specimen.DeriveEnum Goal: produce a Specimen constrained generator for Strata `LExpr` values that satisfy the `LExpr.HasTypeA` annotated-typing relation (for a given bound-variable context `Δ` and result type `τ`). The faithful `LExpr`, -`LMonoTy`, etc. are vendored in `SpecimenTest/StrataDefs/LambdaCore.lean`. - -This file demonstrates that, with two Specimen changes in place — (1) the -classifier tolerating function-application premises such as the `bvar` rule's -`Δ[i]? = some t` de-Bruijn lookup, and (2) the delegated-producer path that -routes such an equality premise to a user-supplied `ArbitrarySizedSuchThat` -instance — the full annotated-typing relation derives a *good* generator, given -one hand-written instance for the lookup. - -## On the expression parameters - -The real `LExpr` is parameterized by a *structure* `T : LExprParamsT` (the -metadata/identifier/type-annotation types), and that `Type 1` parameter rides -along as an argument of every constructor (`@LExpr.const T.mono m c`). The -constrained deriver does not yet handle such a structure parameter — it tries to -*generate* it — which is a separate, orthogonal limitation independent of the -two changes exercised here. - -To keep this example focused on the typing relation, we use `LExprU`: the -*verbatim* shape of `LExpr` with that parameter inlined at its trivial, -fully-monomorphic instantiation (`Unit` expression metadata, `Unit` identifier -metadata, `LMonoTy` type annotations). I.e. `LExprU ≃ LExpr ⟨⟨Unit, Unit⟩, LMonoTy⟩`, -with the parameter erased so no `Type 1` argument appears in the constructors. -Likewise `HasTypeAU` is `LExpr.HasTypeA` transcribed verbatim over `LExprU`. -/ +`LMonoTy`, `HasTypeA`, and the soundness oracle `LExpr.typeCheck` are vendored +verbatim in `SpecimenTest/StrataDefs/LambdaCore.lean`. + +This file derives over the **genuine, structure-parameterized** relation — no +monomorphization. It exercises three Specimen capabilities together: + +1. the classifier tolerating a function-application premise (the `bvar` rule's + `Δ[i]? = some t` de-Bruijn lookup); +2. the **delegated-producer** path routing that equality to the hand-written + `lookupProducer` below (and a synthesis-direction companion); +3. the **structure-parameter** handling: `LExpr` is parameterized by a + *structure* `T : LExprParamsT` (metadata / identifier / type-annotation + configuration types), and that `Type 1` parameter rides along as an implicit + argument of every constructor (`@LExpr.const T.mono m c`). The constrained + deriver keeps that fixed parameter in place rather than trying to generate + it, and emits the per-field `[Arbitrary …]` binders the constructors need. + +We derive with `T : LExprParams` kept abstract; the derived instances are +universally quantified over `T` with the structure-field binders synthesized by +the deriver. The soundness `#eval` then instantiates `T := ⟨Unit, Unit⟩` and +type-checks every sampled term with the vendored `LExpr.typeCheck` oracle. -/ open Plausible open ArbitrarySizedSuchThat @@ -45,27 +42,7 @@ set_option guard_msgs.diff true set_option specimen.autoDeriveDeps true set_option specimen.multiOutput true -/-- Identifiers at `Unit` metadata (as in `LExpr` specialized to `⟨Unit, Unit⟩`). -/ -abbrev IdentU := Identifier Unit - -/-- The shape of Strata's `LExpr` with the `LExprParamsT` parameter inlined at - `⟨⟨Unit, Unit⟩, LMonoTy⟩`: expression metadata is `Unit`, identifier metadata - is `Unit`, and user type annotations are `LMonoTy`. A verbatim transcription - of `Lambda.LExpr` (see `LambdaCore.lean`). -/ -inductive LExprU : Type where - | const (m : Unit) (c : LConst) - | op (m : Unit) (o : IdentU) (ty : Option LMonoTy) - | bvar (m : Unit) (deBruijnIndex : Nat) - | fvar (m : Unit) (name : IdentU) (ty : Option LMonoTy) - | abs (m : Unit) (prettyName : String) (ty : Option LMonoTy) (e : LExprU) - | quant (m : Unit) (k : QuantifierKind) (prettyName : String) (ty : Option LMonoTy) - (trigger : LExprU) (e : LExprU) - | app (m : Unit) (fn e : LExprU) - | ite (m : Unit) (c t e : LExprU) - | eq (m : Unit) (e1 e2 : LExprU) - deriving Repr - -/-! ## Unconstrained producers for the value types carried by `LExprU` -/ +/-! ## Unconstrained producers for the value types carried by `LExpr` -/ /-- `Rat` is carried by `LConst.realConst`; Plausible ships no `Arbitrary Rat`. -/ instance : Arbitrary Rat where @@ -89,14 +66,17 @@ instance : Arbitrary LMonoTy where let n ← Plausible.Gen.chooseNatLt 0 choices.length (by decide) return choices[n.val]! -deriving instance Arbitrary for LExprU +-- The output ADT itself, via Specimen's structure-param-aware `Arbitrary` +-- deriving override (`Specimen.DeriveArbitrary`). +deriving instance Arbitrary for LExpr /-! ## The hand-written delegated producer for the de-Bruijn lookup The `bvar` rule's premise is `Δ[i]? = some t` — list indexing, which the deriver cannot invert to *produce* the index `i`. We supply a constrained producer for -exactly that equality; change (2) detects it and delegates production of `i` to -it (rather than generating `i` blindly and filtering, which has a poor hit rate). +exactly that equality; the delegated-producer path detects it and delegates +production of `i` to it (rather than generating `i` blindly and filtering, which +has a poor hit rate). It enumerates the indices `i` of `Δ` whose entry is `t` and picks one at random, so it produces *well-typed, in-scope* de-Bruijn variables directly. -/ @@ -125,45 +105,34 @@ instance lookupProducerSyn (Δ : List LMonoTy) : else return (0, none) -/-! ## The typing relation, transcribed verbatim from `LExpr.HasTypeA` -/ -inductive HasTypeAU : List LMonoTy → LExprU → LMonoTy → Prop where - | const : HasTypeAU Δ (.const m c) c.ty - | op : HasTypeAU Δ (.op m o (some ty)) ty - | fvar : HasTypeAU Δ (.fvar m x (some ty)) ty - | bvar : Δ[i]? = some t → HasTypeAU Δ (.bvar m i) t - | abs : HasTypeAU (aty :: Δ) body rty → - HasTypeAU Δ (.abs m name (some aty) body) (.arrow aty rty) - | quant : HasTypeAU (qty :: Δ) tr τ_tr → - HasTypeAU (qty :: Δ) body .bool → - HasTypeAU Δ (.quant m k name (some qty) tr body) .bool - | app : HasTypeAU Δ fn (.arrow aty rty) → - HasTypeAU Δ arg aty → - HasTypeAU Δ (.app m fn arg) rty - | ite : HasTypeAU Δ c .bool → - HasTypeAU Δ t τ → - HasTypeAU Δ e τ → - HasTypeAU Δ (.ite m c t e) τ - | eq : HasTypeAU Δ e1 τ → - HasTypeAU Δ e2 τ → - HasTypeAU Δ (.eq m e1 e2) .bool - /- Derive a constrained generator that, given a context `Δ` and a type `τ`, - produces a well-typed `LExprU` of type `τ`. + produces a well-typed `LExpr T.mono` of type `τ`, for abstract `T`. - With the two Specimen changes and the hand-written `lookupProducer` instance, - this succeeds — the `bvar` rule's lookup premise is delegated to - `lookupProducer`. We use `derive_mutual` so the recursive rules - (`app`/`eq`/`abs`/`quant`), which must generate a subterm together with its - type, get the needed `ArbitrarySizedSuchThat (LExprU × LMonoTy)` companion - producer — exactly as in `DeriveArbitrarySuchThat/DeriveSTLCGenerator.lean`. + With the structure-parameter handling, the getElem?-premise classification, + and the hand-written `lookupProducer` instance, this succeeds — the `bvar` + rule's lookup premise is delegated to `lookupProducer`. We use `derive_mutual` + so the recursive rules (`app`/`eq`/`abs`/`quant`), which must generate a + subterm together with its type, get the needed + `ArbitrarySizedSuchThat (LExpr T.mono × LMonoTy)` companion producer — exactly + as in `DeriveArbitrarySuchThat/DeriveSTLCGenerator.lean`. (`derive_mutual` also explores synthesis-direction companions; the one for the `eq` rule has a fixed `bool` conclusion with nothing to synthesize, yielding a harmless "no output types" warning that we drop.) -/ #guard_msgs(drop info, drop warning) in -derive_mutual (fun Δ τ => ∃ e : LExprU, HasTypeAU Δ e τ) +derive_mutual (fun (T : LExprParams) (Δ : List LMonoTy) (τ : LMonoTy) => + ∃ e : LExpr T.mono, @LExpr.HasTypeA T Δ e τ) -/-! ## Pretty-printing -/ +/-! ## Soundness check: sampled terms really are well-typed + +Instantiate the abstract parameter at the trivial monomorphic point +(`Unit` expression metadata, `Unit` identifier metadata), sample the derived +generator across several `(context, type)` requests, and assert every produced +term type-checks at the requested type with the vendored `LExpr.typeCheck` +oracle. Throws (failing the build) on any ill-typed sample. -/ + +/-- The trivial monomorphic parameter: `Unit` metadata, `Unit` id-metadata. -/ +abbrev P0 : LExprParams := ⟨Unit, Unit⟩ /-- Pretty-prints a monomorphic type. -/ def ppMonoTy : LMonoTy → String @@ -176,8 +145,8 @@ def ppMonoTy : LMonoTy → String | .ftvar name => name | .tcons name _ => name -/-- Pretty-print an `LExprU` with minimal parenthesization. -/ -def ppLExprU (e : LExprU) (prec : Nat := 0) : String := +/-- Pretty-print an `LExpr P0.mono` with minimal parenthesization. -/ +def ppLExpr (e : LExpr P0.mono) (prec : Nat := 0) : String := let wrap (p : Nat) (s : String) := if prec ≥ p then s!"({s})" else s match e with | .const _ (.boolConst b) => s!"#{b}" @@ -191,50 +160,17 @@ def ppLExprU (e : LExprU) (prec : Nat := 0) : String := | some t => s!"{x.name} : {ppMonoTy t}" | none => s!"{x.name}" | .abs _ _ ty body => wrap 1 <| match ty with - | some t => s!"λ{ppMonoTy t}. {ppLExprU body 0}" - | none => s!"λ_. {ppLExprU body 0}" + | some t => s!"λ{ppMonoTy t}. {ppLExpr body 0}" + | none => s!"λ_. {ppLExpr body 0}" | .quant _ .all _ ty _ body => wrap 1 <| match ty with - | some t => s!"∀{ppMonoTy t}. {ppLExprU body 0}" - | none => s!"∀_. {ppLExprU body 0}" + | some t => s!"∀{ppMonoTy t}. {ppLExpr body 0}" + | none => s!"∀_. {ppLExpr body 0}" | .quant _ .exist _ ty _ body => wrap 1 <| match ty with - | some t => s!"∃{ppMonoTy t}. {ppLExprU body 0}" - | none => s!"∃_. {ppLExprU body 0}" - | .app _ fn arg => wrap 3 <| s!"{ppLExprU fn 2} {ppLExprU arg 3}" - | .ite _ c t e => wrap 1 <| s!"if {ppLExprU c 0} then {ppLExprU t 0} else {ppLExprU e 0}" - | .eq _ e₁ e₂ => wrap 2 <| s!"{ppLExprU e₁ 2} == {ppLExprU e₂ 2}" - -/-! ## Soundness check: sampled terms really are well-typed - -A computable type-checker for `LExprU` (mirroring Strata's `LExpr.typeCheck`), -used to confirm that the derived generator produces *only* well-typed terms. -/ - -/-- Computable type-checker for `LExprU`; returns the type if well-typed. -/ -def typeCheckU (ctx : List LMonoTy) : LExprU → Option LMonoTy - | .const _ c => some c.ty - | .op _ _ (some ty) => some ty - | .op _ _ none => none - | .fvar _ _ (some ty) => some ty - | .fvar _ _ none => none - | .bvar _ i => ctx[i]? - | .abs _ _ (some aty) body => (typeCheckU (aty :: ctx) body).map (.arrow aty ·) - | .abs _ _ none _ => none - | .quant _ _ _ (some qty) tr body => - match typeCheckU (qty :: ctx) tr, typeCheckU (qty :: ctx) body with - | some _, some (.tcons "bool" []) => some .bool - | _, _ => none - | .quant _ _ _ none _ _ => none - | .app _ fn arg => - match typeCheckU ctx fn, typeCheckU ctx arg with - | some (.tcons "arrow" [dom, cod]), some aty => if dom = aty then some cod else none - | _, _ => none - | .ite _ c t e => - match typeCheckU ctx c, typeCheckU ctx t, typeCheckU ctx e with - | some (.tcons "bool" []), some tt, some et => if tt = et then some tt else none - | _, _, _ => none - | .eq _ a b => - match typeCheckU ctx a, typeCheckU ctx b with - | some ta, some tb => if ta = tb then some .bool else none - | _, _ => none + | some t => s!"∃{ppMonoTy t}. {ppLExpr body 0}" + | none => s!"∃_. {ppLExpr body 0}" + | .app _ fn arg => wrap 3 <| s!"{ppLExpr fn 2} {ppLExpr arg 3}" + | .ite _ c t e => wrap 1 <| s!"if {ppLExpr c 0} then {ppLExpr t 0} else {ppLExpr e 0}" + | .eq _ e₁ e₂ => wrap 2 <| s!"{ppLExpr e₁ 2} == {ppLExpr e₂ 2}" /- Sample the derived generator across several `(context, type)` requests and assert every produced term type-checks at the requested type. Throws (failing @@ -249,8 +185,8 @@ def typeCheckU (ctx : List LMonoTy) : LExprU → Option LMonoTy IO.println s!"--- [{ctxStr}] ⊢ _ : {ppMonoTy τ} ---" for s in List.range 12 do let e ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST - (fun e => HasTypeAU ctx e τ) 4) (s * 7 + 1) - IO.println s!" {ppLExprU e}" - unless typeCheckU ctx e == some τ do + (fun e => @LExpr.HasTypeA P0 ctx e τ) 4) (s * 7 + 1) + IO.println s!" {ppLExpr e}" + unless LExpr.typeCheck ctx e == some τ do throw (IO.userError - s!"ill-typed sample for {repr ctx} ⊢ _ : {ppMonoTy τ}: {ppLExprU e} : {repr (typeCheckU ctx e)}") + s!"ill-typed sample for {repr ctx} ⊢ _ : {ppMonoTy τ}: {ppLExpr e} : {repr (LExpr.typeCheck ctx e)}") From e3de8cf4e69c692af36adbb1126fae739b74b250 Mon Sep 17 00:00:00 2001 From: Segev Elazar-Mittelman Date: Thu, 9 Jul 2026 16:49:25 +0000 Subject: [PATCH 3/5] Replace blind struct-field walk with demand-driven binder discovery Instead of expandStructInstBinders (which emits [Arbitrary P.field] for every Type-valued leaf in a struct parameter), compute needed binders from the schedule steps: - Direct leaf: if the step's source IS a projection chain, emit a binder for it directly. - Compound type: if the step contains a projection chain (e.g. List (P.Label)), use synthesis to confirm which leaves are needed. This means a struct with fields Used : Type and Unused : Type only gets [Arbitrary P.Used] if only Used appears in the schedule. Add StructParamPartialLeafTest with 3 scenarios that fail under the old approach (by setting unused fields to Empty which has no Arbitrary instance) and pass under the new one. --- Specimen/DeriveConstrainedProducer.lean | 156 +++++++++++++++++- Specimen/MakeConstrainedProducerInstance.lean | 99 ++--------- SpecimenTest.lean | 1 + .../StructParamPartialLeafTest.lean | 127 ++++++++++++++ 4 files changed, 293 insertions(+), 90 deletions(-) create mode 100644 SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean index 6ce46ea..d353bcd 100644 --- a/Specimen/DeriveConstrainedProducer.lean +++ b/Specimen/DeriveConstrainedProducer.lean @@ -962,6 +962,150 @@ def extractTypeParamRefs (typeParams : Std.HashSet Name) : ConstructorExpr → S args.foldl (fun acc a => acc.union (extractTypeParamRefs typeParams a)) {} | .Lit _ | .CSort _ | .Hole => {} +/-- Returns `true` if `ce` is a projection chain rooted at a struct param, i.e.: + - `.Unknown P` where `P ∈ structParamNames`, or + - `.FuncApp projName [base]` where `projName` is a structure projection and + `base` is itself a projection chain. + This distinguishes genuine field accesses (e.g. `P.info.Metadata`) from arbitrary + function applications that happen to reference a struct param. -/ +partial def isStructProjChain (structParamNames : Std.HashSet Name) (ce : ConstructorExpr) : + MetaM Bool := do + match ce with + | .Unknown n => return structParamNames.contains n + | .FuncApp name [base] => do + if ← Lean.isProjectionFn name then + isStructProjChain structParamNames base + else + return false + | _ => return false + +/-- Collect all projection-chain sub-expressions within a `ConstructorExpr` that are rooted at + a struct param. For `List (Params.Label P)`, returns `[.FuncApp Params.Label [.Unknown P]]`. -/ +partial def collectStructProjChains (structParamNames : Std.HashSet Name) + (ce : ConstructorExpr) : MetaM (List ConstructorExpr) := do + if ← isStructProjChain structParamNames ce then return [ce] + match ce with + | .Ctor _ args | .TyCtor _ args | .FuncApp _ args => + args.foldlM (fun acc arg => (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + | _ => return [] + +/-- Recursively discover `Type`-valued leaf projections of a structure-typed parameter. + For `(P, ExprParams)`, returns syntax for leaves like `ExprParams.VarId P` and + `NodeInfo.Metadata (ExprParams.info P)`. Used to know which projection-typed instance + binders to put in scope during synthesis. -/ +partial def discoverStructLeaves (paramName : Name) (paramType : Expr) : + TermElabM (Array (TSyntax `term)) := do + let baseSyn : TSyntax `term := mkIdent paramName + go paramType baseSyn +where + go (ty : Expr) (syn : TSyntax `term) : TermElabM (Array (TSyntax `term)) := do + if ty.isSort then return #[syn] + let env ← getEnv + let some sName := ty.constName? | return #[] + let some sInfo := getStructureInfo? env sName | return #[] + let mut result : Array (TSyntax `term) := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + let projSyn ← `($(mkIdent projName) $syn) + result := result ++ (← go projType projSyn) + return result + +/-- Compute struct-param leaf binders needed by a spec's schedule steps. + For each `Unconstrained` step whose source is a projection chain (or contains one), + determines the `Type`-valued leaves that need instance binders. + + Returns an array of `(className, leafSyntax)` pairs — e.g. + `(``Plausible.Arbitrary, `(NodeInfo.Metadata (ExprParams.info P)))`. + + `structParams` is `(paramName, paramType)` for non-Sort, non-output params. + The function discovers which leaves actually appear in schedule steps (directly as + a proj-chain step, or wrapped in a compound type like `List (P.Label)`). -/ +def computeStructLeafBinders (allSteps : List ScheduleStep) + (structParams : Array (Name × Expr)) + : TermElabM (Array (Name × TSyntax `term)) := do + if structParams.isEmpty then return #[] + let structParamNames : Std.HashSet Name := + structParams.foldl (fun s (n, _) => s.insert n) {} + -- Discover all Type-valued leaves for each struct param (for synthesis scope) + let mut allLeaves : Array (TSyntax `term) := #[] + for (paramName, paramType) in structParams do + allLeaves := allLeaves ++ (← discoverStructLeaves paramName paramType) + -- Walk all schedule steps and collect which leaves are needed + let mut needed : Array (Name × TSyntax `term) := #[] + for step in allSteps do + match step with + | .Unconstrained _ (.NonRec (indName, args)) ps => + let tcName := match ps with + | .Generator => ``Plausible.Arbitrary + | .Enumerator => ``Enum + -- Check if the full source (indName applied to args) is itself a proj chain + let fullCE := ConstructorExpr.FuncApp indName args + if ← isStructProjChain structParamNames fullCE then + -- Direct leaf: the type being generated IS a projection of the struct param. + -- Emit a binder for it directly. + let argTerms ← args.toArray.mapM (monadLift <| constructorExprToTSyntaxTerm ·) + let leafSyn ← `($(mkIdent indName) $argTerms:term*) + let entry := (tcName, leafSyn) + unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do + needed := needed.push entry + else + -- Compound type case (e.g. `List (Params.Label P)`): an argument contains a + -- proj chain but the overall type is not itself a leaf. Use the same synthesis + -- approach as for Sort-typed params: open the type constructor's telescope, + -- introduce fvars with [Arbitrary/Enum/DecidableEq] for Sort-typed positions, + -- and attempt synthesis. If it succeeds, the struct leaves are needed. + let chains ← args.foldlM (fun acc arg => + (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + if !chains.isEmpty then + -- Attempt synthesis to confirm that having leaf instances suffices + let succeeded ← Meta.withNewMCtxDepth do + let some indInfo ← (try pure (some (← getConstInfoInduct indName)) catch _ => pure none) + | pure true -- non-inductive (e.g. a def) — conservatively assume needed + let indLevels ← indInfo.levelParams.mapM (fun _ => do + let lv ← Meta.mkFreshLevelMVar; pure (.succ lv)) + let argTypes' ← getComponentsOfArrowType indInfo.type + let argTypes' := argTypes'.pop + let rec buildSynth (idx : Nat) (t : Expr) (fvars : Array Expr) : TermElabM Bool := + if idx >= argTypes'.size then do + let body := mkAppN (.const indName indLevels) fvars + let instTy ← try Meta.mkAppM tcName #[body] catch _ => return false + let result ← try Meta.synthInstance? instTy catch _ => pure none + return result.isSome + else do + let argTy := (← inferType t).bindingDomain! + let name := Name.mkSimple s!"arg_{idx}" + let bi := if argTy.isSort then BinderInfo.implicit else .default + withLocalDecl name bi argTy fun fv => do + if argTy.isSort then + let arbTy ← Meta.mkAppM ``Plausible.Arbitrary #[fv] + let enumTy ← Meta.mkAppM ``Enum #[fv] + let decEqTy ← Meta.mkAppM ``DecidableEq #[fv] + withLocalDecl (Name.mkSimple s!"inst_arb_{idx}") .instImplicit arbTy fun _ => + withLocalDecl (Name.mkSimple s!"inst_enum_{idx}") .instImplicit enumTy fun _ => + withLocalDecl (Name.mkSimple s!"inst_deceq_{idx}") .instImplicit decEqTy fun _ => + buildSynth (idx + 1) (.app t fv) (fvars.push fv) + else + buildSynth (idx + 1) (.app t fv) (fvars.push fv) + try buildSynth 0 (.const indName indLevels) #[] + catch _ => pure true -- on error, conservatively assume needed + if succeeded then + for leaf in allLeaves do + let entry := (tcName, leaf) + unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do + needed := needed.push entry + | _ => pure () + return needed + +/-- Convert struct leaf binder specs to actual bracketed binder syntax. + Each `(className, leafSyn)` becomes `[className leafSyn]`. -/ +def structLeafBindersToSyntax (binders : Array (Name × TSyntax `term)) + : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + let result ← binders.mapM fun (cls, syn) => + `(Lean.Elab.Deriving.instBinderF| [$(mkIdent cls):ident $syn]) + return TSyntaxArray.mk result + /-- Synthesize `[tcName type]` for a compound type and extract what constraints the instance requires on Sort-typed params. Used for external deps (already in env). -/ private partial def synthExternalConstraints (indName : Name) (args : List ConstructorExpr) @@ -1343,10 +1487,20 @@ def compileInductiveSchedule (indSched : InductiveSchedule) let mut paramInfo : Array (Name × Expr × TSyntax `term) := #[] for i in [:liveTypes.size] do paramInfo := paramInfo.push (argNames.getD i `x, liveTypes[i]!, liveTypesSyntax[i]!) + -- Compute struct-param leaf binders from the schedule (demand-driven) + let structParams : Array (Name × Expr) := Id.run do + let mut sp := #[] + for i in [:liveTypes.size] do + if i ∉ key.outputIndices && !liveTypes[i]!.isSort then + sp := sp.push (argNames.getD i `x, liveTypes[i]!) + sp + let allSteps := (indSched.baseSchedules ++ indSched.recSchedules).flatMap (fun (_, (steps, _)) => steps) + let leafBinderSpecs ← computeStructLeafBinders allSteps structParams + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs mkConstrainedProducerMutualPieces baseProducers inductiveProducers key.inductiveName indLevels freshArgIdents freshenedOutputNames - outputTypes producerSort (← getLCtx) globalName key.deriveSort (some paramInfo) requiredConstraints + outputTypes producerSort (← getLCtx) globalName key.deriveSort (some paramInfo) requiredConstraints structLeafBinders /-- Recursively derives the best schedule for a SpecKey, populating the memo with all transitive dependencies. Returns the score for this spec. diff --git a/Specimen/MakeConstrainedProducerInstance.lean b/Specimen/MakeConstrainedProducerInstance.lean index 498ee31..b3bbe1f 100644 --- a/Specimen/MakeConstrainedProducerInstance.lean +++ b/Specimen/MakeConstrainedProducerInstance.lean @@ -53,61 +53,6 @@ def mkTypeClassInstanceBinders (typeParams : Array Name) (typeClasses : Array Na `(Lean.Elab.Deriving.instBinderF| [$(mkIdent tc) $(mkIdent param)]) return TSyntaxArray.mk instances -open TSyntax.Compat in -/-- Recursively expand a *structure-typed* parameter into `[className proj]` - instance binders for each leaf field of type `Type u`. Mirrors - `expandStructBinders` in `Specimen.DeriveArbitrary` (the unconstrained - `deriving Arbitrary` path), which is what lets `Arbitrary (LExpr T)` be - derived for a structure parameter `T`: the constrained producer instance - needs the same per-field binders (e.g. `[Arbitrary T.base.Metadata]`) so the - metadata fields carried by each constructor can be generated. - - `ty` is the type being walked (the parameter's type, or a field's type as we - recurse) and `syn` is the matching surface syntax (the parameter identifier, - or a projection chain into it). A leaf `Type u` field yields `[className syn]`; - a structure field recurses into its own fields. Returns `#[]` for fields that - are neither Types nor structures-of-Types — the conservative, - behavior-preserving choice for the constrained path. -/ -partial def expandStructInstBinders (className : Name) (ty : Expr) (syn : TSyntax `term) : - TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do - if ty.isSort then - -- A `Type u` leaf: emit `[className syn]`. - return #[← `(Lean.Elab.Deriving.instBinderF| [$(mkCIdent className):ident $syn])] - let env ← getEnv - let some sName := ty.constName? | return #[] - let some sInfo := getStructureInfo? env sName | return #[] - let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] - for field in sInfo.fieldNames do - let projName := sName ++ field - -- The field's declared type, read as the codomain of the projection's - -- signature `∀ (_ : sName ..), fieldType`. Structure fields here are the - -- metadata-configuration types, whose field types do not depend on the value. - -- Limitation: `mkConst projName` is built without universe-level arguments, so - -- for a *universe-polymorphic* structure parameter `projType` would be computed - -- at the wrong universe. We don't support such parameters (they are rare in - -- practice; all current Strata params are `Type 0`); supporting them would mean - -- extracting `ty`'s universe levels and passing them to `mkConst` here. - let projType ← forallTelescopeReducing (← inferType (mkConst projName)) - (fun _ body => pure body) - let projSyn ← `($(mkIdent projName) $syn) - result := result ++ (← expandStructInstBinders className projType projSyn) - return result - -/-- Build the unconstrained-producer instance binders for a list of - non-target inductive parameters. For a `Sort`-typed parameter `α`, emits - `[className α] [DecidableEq α]` (the existing behavior). For a *structure* - parameter `T`, expands it into per-field binders via `expandStructInstBinders` - (e.g. `[className T.base.Metadata]` …) so the structure's metadata fields can - be generated. Parameters of other types contribute no binders. -/ -def mkProducerParamInstBinders (className : Name) - (params : Array (Name × Expr)) : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do - let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] - for (paramName, paramType) in params do - if paramType.isSort then - result := result ++ (← mkTypeClassInstanceBinders #[paramName] #[className, ``DecidableEq]) - else - result := result ++ (← expandStructInstBinders className paramType (mkIdent paramName)) - return result /-- Finds the index of the argument in the inductive application for the value we wish to generate (i.e. finds `i` s.t. `args[i] == targetVar`) -/ @@ -140,7 +85,8 @@ def mkConstrainedProducerTypeClassInstance (args : TSyntaxArray `term) (targetVars : List Name) (targetTypes : List Expr) (producerSort : ProducerSort) - (topLevelLocalCtx : LocalContext) : TermElabM (TSyntax `command) := do + (topLevelLocalCtx : LocalContext) + (structLeafBinders : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[]) : TermElabM (TSyntax `command) := do -- Produce fresh names for function parameters let freshSizeIdent := mkFreshAccessibleIdent topLevelLocalCtx `size let freshSize' := mkFreshAccessibleIdent topLevelLocalCtx `size' @@ -191,10 +137,6 @@ def mkConstrainedProducerTypeClassInstance let mut outerParams := #[] let mut outputTypeSyntaxes : Array (TSyntax `term) := #[] let mut typeParams := #[] - -- Non-target, non-sort *structure* parameters (e.g. `T : LExprParams`): we - -- need per-field unconstrained-producer instances for these (see - -- `mkProducerParamInstBinders`). - let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do -- Only add a function parameter if the argument to the inductive relation is not a target variable -- (We skip the target variables since those are the values we wish to generate) @@ -212,8 +154,6 @@ def mkConstrainedProducerTypeClassInstance `(Term.letIdBinder| ($innerParamIdent : $paramTypeSyntax)) innerParams := innerParams.push innerParam - if !paramType.isSort then - structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -266,10 +206,7 @@ def mkConstrainedProducerTypeClassInstance | .Enumerator => ``Enum let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] - -- Per-field unconstrained-producer instances for structure parameters (e.g. - -- `[Arbitrary T.base.Metadata]`), so their fields can be generated. - let structParamInstances ← mkProducerParamInstBinders producerUnconstrainedClass structParams - let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structParamInstances + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders let fuelVal := Lean.Option.get (← getOptions) specimen.fuel let fuelLit := Syntax.mkNumLit (toString fuelVal) @@ -292,7 +229,8 @@ def mkConstrainedProducerMutualPieces (topLevelLocalCtx : LocalContext) (globalDefName : Name) (deriveSort : DeriveSort) (precomputedParamInfo : Option (Array (Name × Expr × TSyntax `term)) := none) - (requiredTypeClasses : Option (Array Name) := none) : + (requiredTypeClasses : Option (Array Name) := none) + (structLeafBinders : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[]) : TermElabM (TSyntax `command × TSyntax `command) := do -- Reuse the same computation as mkConstrainedProducerTypeClassInstance let freshSizeIdent := mkFreshAccessibleIdent topLevelLocalCtx `size @@ -330,8 +268,6 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($initSizeIdent : $natIdent))) innerParamBinders := innerParamBinders.push (← `(($sizeIdent : $natIdent))) - -- Non-target, non-sort structure parameters needing per-field producer instances. - let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do if paramType.isSort then typeParams := typeParams.push paramName @@ -342,7 +278,6 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : Sort _))) else innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : $paramTypeSyntax))) - structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -394,15 +329,9 @@ def mkConstrainedProducerMutualPieces | .Enumerator => ``Enum #[producerUnconstrainedClass, ``DecidableEq] let defTypeParamInstances ← mkTypeClassInstanceBinders typeParams typeClasses - -- Per-field producer instances for structure parameters (e.g. - -- `[Arbitrary T.base.Metadata]`). These reference value params (`T`), so they - -- are placed *innermost* — after all value params — where those are in scope. - -- The `def` itself always builds the underlying producer, so it uses the - -- producer-based unconstrained class regardless of `deriveSort`. - let structParamClass := match producerSort with - | .Generator => ``Plausible.Arbitrary - | .Enumerator => ``Enum - let structParamInstances ← mkProducerParamInstBinders structParamClass structParams + -- Struct-param leaf binders (e.g. `[Arbitrary P.info.Metadata]`) are placed + -- innermost — after all value params — where those params are in scope. + let structParamInstances := structLeafBinders -- Emit the def with ∀ type (supports instance binders inline) let defIdent := mkIdent globalDefName @@ -445,9 +374,7 @@ def mkConstrainedProducerMutualPieces let instCmd ← match deriveSort with | .Checker | .Theorem => do let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses - -- Per-field struct-param instances for the wrapper (Checker/Theorem → `Enum`). - let structInsts ← mkProducerParamInstBinders ``Enum structParams - let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $decOptTypeclass (@$(mkIdent inductiveName) $args*) where $unqualifiedDecOptFn:ident := fun $freshSizeIdent => $callExpr) @@ -458,14 +385,8 @@ def mkConstrainedProducerMutualPieces let producerTypeClassFunction := match producerSort with | .Generator => unqualifiedArbitrarySizedSTFn | .Enumerator => unqualifiedEnumSizedSTFn - let producerUnconstrainedClass := match producerSort with - | .Generator => ``Plausible.Arbitrary - | .Enumerator => ``Enum let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses - -- Per-field struct-param instances for the wrapper (Generator/Enumerator - -- → `Arbitrary`/`Enum`). - let structInsts ← mkProducerParamInstBinders producerUnconstrainedClass structParams - let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $producerTypeClass $targetTypeSyntax (fun $targetVarPattern => @$(mkIdent inductiveName) $args*) where $producerTypeClassFunction:ident := fun $freshSizeIdent => $callExpr) diff --git a/SpecimenTest.lean b/SpecimenTest.lean index cfa1ffa..e0eb787 100644 --- a/SpecimenTest.lean +++ b/SpecimenTest.lean @@ -44,6 +44,7 @@ import SpecimenTest.DeriveArbitrary.ParameterizedTypeTest import SpecimenTest.DeriveArbitrary.MutuallyRecursiveTypeTest import SpecimenTest.DeriveArbitrarySuchThat.DeriveSTLCGenerator import SpecimenTest.DeriveArbitrarySuchThat.DeriveStructParamGenerator +import SpecimenTest.DeriveArbitrarySuchThat.StructParamPartialLeafTest import SpecimenTest.DeriveArbitrarySuchThat.NonLinearPatternsTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputSTLCTest diff --git a/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean b/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean new file mode 100644 index 0000000..e4f3c3e --- /dev/null +++ b/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean @@ -0,0 +1,127 @@ +import Plausible.Gen +import Plausible.Arbitrary +import Specimen.Enumerators +import Specimen.EnumeratorCombinators +import Specimen.ArbitrarySizedSuchThat +import Specimen.DeriveConstrainedProducer +import Specimen.DeriveArbitrary +import Specimen.DeriveEnum + +/-! # Demand-driven struct-param binder tests + +Verify that the deriver only emits instance binders for struct-param fields that +actually appear in the schedule. A struct with fields `Used : Type` and +`Unused : Type` should only require `[Arbitrary P.Used]` — not both. + +This is a regression test for the demand-driven approach vs. the old +`expandStructInstBinders` which would blindly walk all fields. -/ + +open Plausible +open ArbitrarySizedSuchThat + +set_option guard_msgs.diff true +set_option specimen.autoDeriveDeps true +set_option specimen.multiOutput true + +namespace PartialLeafTest + +/-! ## Test 1: Only one of two struct fields used + +`TwoFields` has `Used : Type` and `Unused : Type`. The relation `HasVal` only +mentions `P.Used` in its constructors. If the deriver emits `[Arbitrary P.Unused]` +too, it would appear in the generated instance signature — but we deliberately +do NOT provide an `Arbitrary` instance for the `Unused` field's monomorphization, +so if the binder were emitted the instance would fail to synthesize at use-site. -/ + +structure TwoFields where + Used : Type + Unused : Type + +inductive TaggedExpr (P : TwoFields) where + | leaf (x : P.Used) : TaggedExpr P + | node (l r : TaggedExpr P) : TaggedExpr P + +inductive HasVal (P : TwoFields) : TaggedExpr P → Prop where + | leaf : HasVal P (.leaf x) + | node : HasVal P l → HasVal P r → HasVal P (.node l r) + +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : TwoFields) => ∃ e : TaggedExpr P, HasVal P e), + enumerator (fun (P : TwoFields) => ∃ e : TaggedExpr P, HasVal P e) + +/-! Monomorphize: `Used = Nat`, `Unused = Empty` (no Arbitrary instance for Empty). + If the deriver emitted `[Arbitrary P.Unused]`, this #eval would fail to synthesize. -/ +abbrev TF1 : TwoFields := ⟨Nat, Empty⟩ + +#guard_msgs(drop info) in +#eval show IO Unit from do + let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun e => HasVal TF1 e) 3) 42 + IO.println s!"partial-leaf test 1: derived instance synthesizes with Unused = Empty" + +/-! ## Test 2: Struct field used only via compound type + +`Config` has `Label : Type` and `Phantom : Type`. The constructor references +`P.Label` but never `P.Phantom` directly. -/ + +structure Config where + Label : Type + Phantom : Type + +inductive LabelledList (P : Config) where + | nil : LabelledList P + | cons (tag : P.Label) (rest : LabelledList P) : LabelledList P + +inductive IsLabelled (P : Config) : LabelledList P → Prop where + | nil : IsLabelled P .nil + | cons : IsLabelled P rest → IsLabelled P (.cons tag rest) + +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : Config) => ∃ xs : LabelledList P, IsLabelled P xs), + enumerator (fun (P : Config) => ∃ xs : LabelledList P, IsLabelled P xs) + +/-! Monomorphize: `Label = String`, `Phantom = Empty`. -/ +abbrev C1 : Config := ⟨String, Empty⟩ + +#guard_msgs(drop info) in +#eval show IO Unit from do + let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun xs => IsLabelled C1 xs) 3) 42 + IO.println s!"partial-leaf test 2: compound-type case works with Phantom = Empty" + +/-! ## Test 3: Nested struct, only inner field used + +`Outer` has `inner : Inner` and `TopLevel : Type`. `Inner` has `Needed : Type` +and `NotNeeded : Type`. The relation only uses `P.inner.Needed`. -/ + +structure Inner where + Needed : Type + NotNeeded : Type + +structure Outer where + inner : Inner + TopLevel : Type + +inductive Wrapped (P : Outer) where + | mk (v : P.inner.Needed) : Wrapped P + +inductive IsGood (P : Outer) : Wrapped P → Prop where + | mk : IsGood P (.mk v) + +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w), + enumerator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w) + +/-! Monomorphize: `inner.Needed = Bool`, everything else `Empty`. -/ +abbrev O1 : Outer := ⟨⟨Bool, Empty⟩, Empty⟩ + +#guard_msgs(drop info) in +#eval show IO Unit from do + let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun w => @IsGood O1 w) 2) 7 + IO.println s!"partial-leaf test 3: nested struct, only inner.Needed required" + +end PartialLeafTest From 488653aae1ce7190652e7b830bab154a57b163ba Mon Sep 17 00:00:00 2001 From: Michael Hicks Date: Wed, 29 Jul 2026 16:34:11 +0000 Subject: [PATCH 4/5] update to support derive_generator, and to avoid propagating redundant constraints; consolidated tests --- Docs/Struct-param-support.md | 184 +++++++++ Specimen/DeriveConstrainedProducer.lean | 367 ++++++++++-------- SpecimenTest.lean | 2 +- .../StructParamBinderTest.lean | 229 +++++++++++ .../StructParamPartialLeafTest.lean | 127 ------ 5 files changed, 627 insertions(+), 282 deletions(-) create mode 100644 Docs/Struct-param-support.md create mode 100644 SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean delete mode 100644 SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean diff --git a/Docs/Struct-param-support.md b/Docs/Struct-param-support.md new file mode 100644 index 0000000..a27316e --- /dev/null +++ b/Docs/Struct-param-support.md @@ -0,0 +1,184 @@ +# Structure-parameterized output types in the constrained deriver + +## 1. What this supports + +`derive_generator` / `derive_enumerator` / `derive_mutual` can produce values of +an inductive relation whose output type is parameterized by a **structure** `P` +(not just a plain `Sort`/type parameter), with `P` kept **abstract** (no +monomorphization). + +The motivating case is Strata's Lambda IR, where a single structure parameter +bundles the language's configuration types: + +```lean +inductive LExpr (T : LExprParamsT) : Type where + | const (m : T.base.Metadata) (c : LConst) + | bvar (m : T.base.Metadata) (i : Nat) + | ... +``` + +Here `T : LExprParams` is a structure bundling the metadata / identifier / +type-annotation types. Deriving a producer for a relation like +`@LExpr.HasTypeA T …` requires handling three things about `T`: + +1. **The parameter appears as an implicit constructor argument.** `T.mono` + rides along as an implicit argument of every `LExpr` constructor. It is + determined entirely by the producer's inputs and has no `Arbitrary` instance + (and typically lives in a higher universe than the value being generated), so + it must **not** be lifted into a generated unknown. +2. **Constructor fields have projection types.** Fields like + `m : T.base.Metadata` or `name : T.VarId` can only be produced if an + `Arbitrary`/`Enum` instance for that projection type is in scope. The derived + instance must carry the matching binders (e.g. `[Arbitrary T.base.Metadata]`). +3. **Implicit args must be re-inferred, not placed positionally.** The produced + value must omit implicit constructor arguments (like the `T` of + `LExpr.const`) so Lean re-infers them from the explicit arguments. + +**Design invariant — strictly additive.** None of this changes behavior when no +structure parameter is involved. Ordinary fixed value subterms that *do* have an +`Arbitrary` instance (e.g. `n * n : Nat`) still flatten as before; plain `Sort` +parameters are unaffected. + +## 2. Implementation + +Three parts of the pipeline cooperate. All are guarded so the non-struct path is +unchanged. + +### 2a. Don't generate fixed, ungeneratable subterms + +*Files: `Specimen/Utils.lean`, `Specimen/DeriveConstrainedProducer.lean`.* + +Conclusion flattening (`collectUnmatchableSubterms` / +`collectUnmatchableProperSubterms`) normally turns non-matchable subterms into +fresh generated unknowns plus equality hypotheses. A set of **fixed-input +fvars** is threaded through these collectors, and a subterm that is *fixed and +ungeneratable* is left in place instead: + +- `allFVarsFixed fixed e` — every free variable of `e` is a fixed input, so `e` + is fully determined by the producer's inputs. +- `isFixedUngenerable fixed e` — `allFVarsFixed` **and** `e`'s type has no + `Arbitrary` instance. Conservative: returns `false` (old behavior) if the type + has metavariables, and only reports `true` when an `Arbitrary ty` synthesis + probe genuinely fails. This distinguishes `T.mono` (no `Arbitrary` → leave + fixed) from `n * n : Nat` (`Arbitrary Nat` exists → flatten). + +`linearizeAndFlatten` takes a `fixedFVars` parameter; +`getScheduleForInductiveRelationConstructor` computes it as the conclusion's +non-output argument positions that are bare fvars (the inductive's parameters, +including `P`). + +### 2b. Emit demand-driven struct-param leaf binders + +*Files: `Specimen/DeriveConstrainedProducer.lean`, +`Specimen/MakeConstrainedProducerInstance.lean`.* + +`computeStructLeafBinders` scans a spec's schedule steps and returns the +`(className, leafSyntax)` binders the producer needs — one per struct-param +projection leaf that **actually appears**, and none for unused fields. It only +inspects `.Unconstrained` steps (the ones that draw a value from an unconstrained +`Arbitrary`/`Enum` instance) and handles two shapes: + +- **Direct leaf** — the step's source *is* a projection chain rooted at the + struct param (`isStructProjChain`), e.g. generating a value of type `P.Label`. + Emit a binder for that leaf directly. +- **Compound leaf** — an argument *contains* a projection chain but the overall + type is not itself a leaf, e.g. `List P.Label`. `collectStructProjChains` finds + the chains; a synthesis probe (opening the type constructor's telescope with + `[Arbitrary/Enum/DecidableEq]` on its `Sort`-typed positions) confirms leaf + instances suffice; then `resolveChainType` maps **each chain present in the + step** back to its leaf syntax and emits binders for those leaves only. + +`structLeavesFromType` is the shared recursive walk: a `Type u` value is a leaf; +a structure-typed value recurses through each field's projection, building +projection-chain syntax (`P.info` → `NodeInfo.Metadata (P.info)`). +`structLeafBindersToSyntax` renders the results as `[className leaf]` binders. + +These binders are threaded into every emission path in +`MakeConstrainedProducerInstance.lean`: + +- **Single-instance path** (`mkConstrainedProducerTypeClassInstance`): appended + to the type-param instances. +- **Mutual-`def` path** (`mkConstrainedProducerMutualPieces`): placed + **innermost**, after all value params, because a leaf like + `P.info.Metadata` references the value param `P`, which must already be in + scope. Both the `∀`-type and the matching lambda insert them there, and the + wrapper `instance` commands append them too. + +All deriver entry points compute the binders and pass them through: +`deriveConstrainedProducer` (used by `derive_generator` / `derive_enumerator`), +`deriveConstrainedProducerParts` (used by `deriveFromScheduleDep`), and +`compileInductiveSchedule` (the `derive_mutual` path). Each accumulates its +constructors' schedule steps, derives `structParams` from the non-output, +non-`Sort` arguments (named by their freshened names so the emitted binders match +the instance signature), and calls `computeStructLeafBinders`. + +### 2c. Drop implicit constructor args from produced values + +*File: `Specimen/MExp.lean`.* + +`dropImplicitCtorArgsExpr` recursively removes arguments at implicit / +instance-implicit positions of every genuine data-constructor application in the +produced value: + +- `.Ctor c args`: recurse into args; if `c` is a real constructor, use + `forallTelescopeReducing` on its type to keep only the explicit positions. If + the arg count doesn't match the arity, leave it unchanged. `.Ctor` nodes that + are actually abbrevs/defs (e.g. `LExprParams.mono`) are left alone. +- `.TyCtor` / `.FuncApp`: recurse into args but don't filter their own arg lists + (they are emitted implicit-allowing already). + +This drops, e.g., `LExpr.const`'s implicit `T` and `Option.some`'s implicit `α` +so the implicit-allowing emission re-infers them. `scheduleToMExp` applies this +to the producer schedule's `conclusionOutputs` before converting them to `MExp`s. + +## 3. Tests + +- **`SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean`** isolates + the binder logic across three axes: leaf shape (direct field / compound + `List P.Label` / nested `P.inner.Needed`), emission path (single-instance vs. + mutual), and producer sort (generator / enumerator). Every fixture monomorphizes + the *unused* sibling field to `Empty` (which has no `Arbitrary`/`Enum` + instance), so an over-emitted binder would fail to synthesize at use-site; a + computable oracle is `#eval`'d over samples wherever the relation fixes the + value's shape. + +- **`SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean`** is a + self-contained miniature STLC witness: a structure parameter with one nested + field, deriving a generator and enumerator together over the genuine abstract + `Tm P`. + +- **`SpecimenTest/StrataLexprGen.lean`** is the end-to-end witness. It derives a + sound generator for well-typed Strata `LExpr`s from `@LExpr.HasTypeA T …` with + `T` abstract: + + ```lean + derive_mutual (fun (T : LExprParams) (Δ : List LMonoTy) (τ : LMonoTy) => + ∃ e : LExpr T.mono, @LExpr.HasTypeA T Δ e τ) + ``` + + An embedded `#eval` samples the derived generator at the monomorphic + instantiation `P := ⟨Unit, Unit⟩` and type-checks every sample with the + vendored `LExpr.typeCheck` oracle (from `SpecimenTest/StrataDefs/LambdaCore.lean`, + proved equivalent to `HasTypeA` upstream), throwing on any ill-typed term. This + example also relies on two capabilities beyond struct-param support: the + classifier tolerating a function-application premise (the `bvar` de-Bruijn + lookup `Δ[i]? = some t`), and the delegated-producer path routing that equality + to a hand-written `ArbitrarySizedSuchThat`. + +## 4. Open issues / limitations + +- **Compound-leaf enumerators are broken.** A `derive_enumerator` whose + struct-param leaf appears inside a *compound* type (e.g. `List P.Label`) fails + with a spurious `Enum (Except GenError (List P.Label))` synthesis goal. This is + a bug in the enumerator's compound-field emission (an `Except GenError` wrapper + leaking into the enumerated element type), *not* in the binder machinery: it + does not affect direct-leaf enumerators, nor a plain `Type` parameter of the + same shape, nor generators. `StructParamBinderTest.lean` derives a *generator* + only for the compound-leaf case for this reason. + +- **Universe-polymorphic structure parameters are unsupported.** The leaf walk + (`structLeavesFromType` / `resolveChainType`) reads a projection's codomain via + `mkConst projName` with no universe-level arguments, so for a + universe-polymorphic structure parameter the projection type would be computed + at the wrong universe. All current Strata params are `Type 0`. A fix would + extract the parameter type's universe levels and pass them to `mkConst`. diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean index d353bcd..1158947 100644 --- a/Specimen/DeriveConstrainedProducer.lean +++ b/Specimen/DeriveConstrainedProducer.lean @@ -706,6 +706,174 @@ def getProducerScheduleForInductiveConstructor getScheduleForInductiveRelationConstructor inductiveName ctorName inputNames deriveSort (some outputNamesTypesIndices) unknowns localCtx recFnName depMemo memoRef deriveDep +/-- Returns `true` if `ce` is a projection chain rooted at a struct param, i.e.: + - `.Unknown P` where `P ∈ structParamNames`, or + - `.FuncApp projName [base]` where `projName` is a structure projection and + `base` is itself a projection chain. + This distinguishes genuine field accesses (e.g. `P.info.Metadata`) from arbitrary + function applications that happen to reference a struct param. -/ +partial def isStructProjChain (structParamNames : Std.HashSet Name) (ce : ConstructorExpr) : + MetaM Bool := do + match ce with + | .Unknown n => return structParamNames.contains n + | .FuncApp name [base] => do + if ← Lean.isProjectionFn name then + isStructProjChain structParamNames base + else + return false + | _ => return false + +/-- Collect all projection-chain sub-expressions within a `ConstructorExpr` that are rooted at + a struct param. For `List (Params.Label P)`, returns `[.FuncApp Params.Label [.Unknown P]]`. -/ +partial def collectStructProjChains (structParamNames : Std.HashSet Name) + (ce : ConstructorExpr) : MetaM (List ConstructorExpr) := do + if ← isStructProjChain structParamNames ce then return [ce] + match ce with + | .Ctor _ args | .TyCtor _ args | .FuncApp _ args => + args.foldlM (fun acc arg => (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + | _ => return [] + +/-- Recursively discover the `Type`-valued leaf projections *reachable from* a + projection whose value has type `ty` and whose surface syntax is `syn`. + A `Type u` leaf yields `#[syn]`; a structure-typed value recurses into each + field's projection (`sName ++ field` applied to `syn`). For a value of type + `NodeInfo` reached as `ExprParams.info P`, this yields + `NodeInfo.Metadata (ExprParams.info P)`. -/ +partial def structLeavesFromType (ty : Expr) (syn : TSyntax `term) : + TermElabM (Array (TSyntax `term)) := do + if ty.isSort then return #[syn] + let env ← getEnv + let some sName := ty.constName? | return #[] + let some sInfo := getStructureInfo? env sName | return #[] + let mut result : Array (TSyntax `term) := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + let projSyn ← `($(mkIdent projName) $syn) + result := result ++ (← structLeavesFromType projType projSyn) + return result + +/-- Resolve a struct-param projection chain (as a `ConstructorExpr`) to the Lean + type of the value it denotes together with its surface syntax. The chain root + must be one of `structParams`; each `.FuncApp projName [base]` step is a + structure projection whose codomain is read from `projName`'s signature. + Returns `none` if `ce` is not a projection chain rooted at a known struct param + (e.g. it is an arbitrary function application). -/ +partial def resolveChainType (structParams : Array (Name × Expr)) (ce : ConstructorExpr) : + TermElabM (Option (Expr × TSyntax `term)) := do + match ce with + | .Unknown n => + match structParams.find? (fun (pn, _) => pn == n) with + | some (_, pty) => return some (pty, mkIdent n) + | none => return none + | .FuncApp projName [base] => + if ← Lean.isProjectionFn projName then + match ← resolveChainType structParams base with + | some (_, baseSyn) => + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + let projSyn ← `($(mkIdent projName) $baseSyn) + return some (projType, projSyn) + | none => return none + else return none + | _ => return none + +/-- Compute struct-param leaf binders needed by a spec's schedule steps. + For each `Unconstrained` step whose source is a projection chain (or contains one), + determines the `Type`-valued leaves that need instance binders. + + Returns an array of `(className, leafSyntax)` pairs — e.g. + `(``Plausible.Arbitrary, `(NodeInfo.Metadata (ExprParams.info P)))`. + + `structParams` is `(paramName, paramType)` for non-Sort, non-output params. + The function discovers which leaves actually appear in schedule steps (directly as + a proj-chain step, or wrapped in a compound type like `List (P.Label)`). -/ +def computeStructLeafBinders (allSteps : List ScheduleStep) + (structParams : Array (Name × Expr)) + : TermElabM (Array (Name × TSyntax `term)) := do + if structParams.isEmpty then return #[] + let structParamNames : Std.HashSet Name := + structParams.foldl (fun s (n, _) => s.insert n) {} + -- Walk all schedule steps and collect which leaves are needed + let mut needed : Array (Name × TSyntax `term) := #[] + for step in allSteps do + match step with + | .Unconstrained _ (.NonRec (indName, args)) ps => + let tcName := match ps with + | .Generator => ``Plausible.Arbitrary + | .Enumerator => ``Enum + -- Check if the full source (indName applied to args) is itself a proj chain + let fullCE := ConstructorExpr.FuncApp indName args + if ← isStructProjChain structParamNames fullCE then + -- Direct leaf: the type being generated IS a projection of the struct param. + -- Emit a binder for it directly. + let argTerms ← args.toArray.mapM (monadLift <| constructorExprToTSyntaxTerm ·) + let leafSyn ← `($(mkIdent indName) $argTerms:term*) + let entry := (tcName, leafSyn) + unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do + needed := needed.push entry + else + -- Compound type case (e.g. `List (Params.Label P)`): an argument contains a + -- proj chain but the overall type is not itself a leaf. Use the same synthesis + -- approach as for Sort-typed params: open the type constructor's telescope, + -- introduce fvars with [Arbitrary/Enum/DecidableEq] for Sort-typed positions, + -- and attempt synthesis. If it succeeds, the struct leaves are needed. + let chains ← args.foldlM (fun acc arg => + (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + if !chains.isEmpty then + -- Attempt synthesis to confirm that having leaf instances suffices + let succeeded ← Meta.withNewMCtxDepth do + let some indInfo ← (try pure (some (← getConstInfoInduct indName)) catch _ => pure none) + | pure true -- non-inductive (e.g. a def) — conservatively assume needed + let indLevels ← indInfo.levelParams.mapM (fun _ => do + let lv ← Meta.mkFreshLevelMVar; pure (.succ lv)) + let argTypes' ← getComponentsOfArrowType indInfo.type + let argTypes' := argTypes'.pop + let rec buildSynth (idx : Nat) (t : Expr) (fvars : Array Expr) : TermElabM Bool := + if idx >= argTypes'.size then do + let body := mkAppN (.const indName indLevels) fvars + let instTy ← try Meta.mkAppM tcName #[body] catch _ => return false + let result ← try Meta.synthInstance? instTy catch _ => pure none + return result.isSome + else do + let argTy := (← inferType t).bindingDomain! + let name := Name.mkSimple s!"arg_{idx}" + let bi := if argTy.isSort then BinderInfo.implicit else .default + withLocalDecl name bi argTy fun fv => do + if argTy.isSort then + let arbTy ← Meta.mkAppM ``Plausible.Arbitrary #[fv] + let enumTy ← Meta.mkAppM ``Enum #[fv] + let decEqTy ← Meta.mkAppM ``DecidableEq #[fv] + withLocalDecl (Name.mkSimple s!"inst_arb_{idx}") .instImplicit arbTy fun _ => + withLocalDecl (Name.mkSimple s!"inst_enum_{idx}") .instImplicit enumTy fun _ => + withLocalDecl (Name.mkSimple s!"inst_deceq_{idx}") .instImplicit decEqTy fun _ => + buildSynth (idx + 1) (.app t fv) (fvars.push fv) + else + buildSynth (idx + 1) (.app t fv) (fvars.push fv) + try buildSynth 0 (.const indName indLevels) #[] + catch _ => pure true -- on error, conservatively assume needed + if succeeded then + -- Emit binders only for the leaves reachable from the projection chains + -- that actually appear in this step (not every leaf of every struct + -- param) — so an unused field never drags in a spurious binder. + for chain in chains do + if let some (chainTy, chainSyn) ← resolveChainType structParams chain then + for leaf in (← structLeavesFromType chainTy chainSyn) do + let entry := (tcName, leaf) + unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do + needed := needed.push entry + | _ => pure () + return needed + +/-- Convert struct leaf binder specs to actual bracketed binder syntax. + Each `(className, leafSyn)` becomes `[className leafSyn]`. -/ +def structLeafBindersToSyntax (binders : Array (Name × TSyntax `term)) + : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + let result ← binders.mapM fun (cls, syn) => + `(Lean.Elab.Deriving.instBinderF| [$(mkIdent cls):ident $syn]) + return TSyntaxArray.mk result + /-- Produces an instance of a typeclass for a constrained producer (either `ArbitrarySizedSuchThat` or `EnumSizedSuchThat`). The arguments to this function are: @@ -771,7 +939,7 @@ def deriveConstrainedProducer -- Then, derive `baseProducers` & `inductiveProducers` (the code for the sub-producers -- that are invoked when `size = 0` and `size > 0` respectively), -- and obtain freshened versions of the output variables / arguments (`freshenedOutputNames`, `freshArgIdents`) - let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, localCtx) ← + let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, localCtx, structLeafBinders) ← -- Freshen argument names to avoid capture, then derive schedules per constructor withLocalDeclsDND argNamesTypes (fun _ => do let mut localCtx ← getLCtx @@ -802,6 +970,10 @@ def deriveConstrainedProducer let mut nonRecursiveProducers := #[] let mut recursiveProducers := #[] + -- Accumulate every constructor's schedule steps so we can compute the + -- demand-driven struct-param leaf binders (see `computeStructLeafBinders`), + -- mirroring the mutual-def path in `compileInductiveSchedule`. + let mut allScheduleSteps : List ScheduleStep := [] let freshFuelPrimeName := localCtx.getUnusedName `fuel' let freshSizePrimeName := localCtx.getUnusedName `size' @@ -859,6 +1031,7 @@ def deriveConstrainedProducer match resultOption with | some result => let schedule := result.schedule + allScheduleSteps := allScheduleSteps ++ schedule.fst let (subProducer, instances) ← StateT.run (s := #[]) (do let mexp ← MExp.scheduleToMExp schedule (.MId `size) (.MId `initSize) outputType (fuelPrimeName := freshFuelPrimeName) (sizePrimeName := freshSizePrimeName) (targetInductive := inductiveName) MExp.mexpToTSyntax mexp deriveSort) @@ -907,12 +1080,27 @@ def deriveConstrainedProducer let baseProducers ← `([$nonRecursiveProducers,*]) let inductiveProducers ← `([$nonRecursiveProducers,*, $recursiveProducers,*]) - return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx)) + -- Compute the demand-driven struct-param leaf binders (e.g. + -- `[Arbitrary P.info.Metadata]`) from the accumulated schedule steps, so a + -- struct-parameterized output type works on this single-instance path too + -- (mirrors the mutual-def path in `compileInductiveSchedule`). The struct + -- params are the non-output, non-sort arguments, named by their freshened + -- names so the emitted binders match the instance's parameters. + let structParams : Array (Name × Expr) := Id.run do + let mut sp := #[] + for i in [:argTypes.size] do + if i ∉ outputIdxs && !argTypes[i]!.isSort then + sp := sp.push (freshUnknowns[i]!, argTypes[i]!) + sp + let leafBinderSpecs ← computeStructLeafBinders allScheduleSteps structParams + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs + + return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx, structLeafBinders)) -- Create an instance of the appropriate producer typeclass mkConstrainedProducerTypeClassInstance baseProducers inductiveProducers constrainingInductive inductiveLevels freshArgIdents freshenedOutputNames.toList - outputTypes.toList producerSort localCtx + outputTypes.toList producerSort localCtx structLeafBinders /-- Compile a schedule to a weighted sub-producer term. Handles the common pattern of: schedule → MExp → TSyntax, then wrapping with the weight function for the backtracking @@ -962,150 +1150,6 @@ def extractTypeParamRefs (typeParams : Std.HashSet Name) : ConstructorExpr → S args.foldl (fun acc a => acc.union (extractTypeParamRefs typeParams a)) {} | .Lit _ | .CSort _ | .Hole => {} -/-- Returns `true` if `ce` is a projection chain rooted at a struct param, i.e.: - - `.Unknown P` where `P ∈ structParamNames`, or - - `.FuncApp projName [base]` where `projName` is a structure projection and - `base` is itself a projection chain. - This distinguishes genuine field accesses (e.g. `P.info.Metadata`) from arbitrary - function applications that happen to reference a struct param. -/ -partial def isStructProjChain (structParamNames : Std.HashSet Name) (ce : ConstructorExpr) : - MetaM Bool := do - match ce with - | .Unknown n => return structParamNames.contains n - | .FuncApp name [base] => do - if ← Lean.isProjectionFn name then - isStructProjChain structParamNames base - else - return false - | _ => return false - -/-- Collect all projection-chain sub-expressions within a `ConstructorExpr` that are rooted at - a struct param. For `List (Params.Label P)`, returns `[.FuncApp Params.Label [.Unknown P]]`. -/ -partial def collectStructProjChains (structParamNames : Std.HashSet Name) - (ce : ConstructorExpr) : MetaM (List ConstructorExpr) := do - if ← isStructProjChain structParamNames ce then return [ce] - match ce with - | .Ctor _ args | .TyCtor _ args | .FuncApp _ args => - args.foldlM (fun acc arg => (· ++ acc) <$> collectStructProjChains structParamNames arg) [] - | _ => return [] - -/-- Recursively discover `Type`-valued leaf projections of a structure-typed parameter. - For `(P, ExprParams)`, returns syntax for leaves like `ExprParams.VarId P` and - `NodeInfo.Metadata (ExprParams.info P)`. Used to know which projection-typed instance - binders to put in scope during synthesis. -/ -partial def discoverStructLeaves (paramName : Name) (paramType : Expr) : - TermElabM (Array (TSyntax `term)) := do - let baseSyn : TSyntax `term := mkIdent paramName - go paramType baseSyn -where - go (ty : Expr) (syn : TSyntax `term) : TermElabM (Array (TSyntax `term)) := do - if ty.isSort then return #[syn] - let env ← getEnv - let some sName := ty.constName? | return #[] - let some sInfo := getStructureInfo? env sName | return #[] - let mut result : Array (TSyntax `term) := #[] - for field in sInfo.fieldNames do - let projName := sName ++ field - let projType ← forallTelescopeReducing (← inferType (mkConst projName)) - (fun _ body => pure body) - let projSyn ← `($(mkIdent projName) $syn) - result := result ++ (← go projType projSyn) - return result - -/-- Compute struct-param leaf binders needed by a spec's schedule steps. - For each `Unconstrained` step whose source is a projection chain (or contains one), - determines the `Type`-valued leaves that need instance binders. - - Returns an array of `(className, leafSyntax)` pairs — e.g. - `(``Plausible.Arbitrary, `(NodeInfo.Metadata (ExprParams.info P)))`. - - `structParams` is `(paramName, paramType)` for non-Sort, non-output params. - The function discovers which leaves actually appear in schedule steps (directly as - a proj-chain step, or wrapped in a compound type like `List (P.Label)`). -/ -def computeStructLeafBinders (allSteps : List ScheduleStep) - (structParams : Array (Name × Expr)) - : TermElabM (Array (Name × TSyntax `term)) := do - if structParams.isEmpty then return #[] - let structParamNames : Std.HashSet Name := - structParams.foldl (fun s (n, _) => s.insert n) {} - -- Discover all Type-valued leaves for each struct param (for synthesis scope) - let mut allLeaves : Array (TSyntax `term) := #[] - for (paramName, paramType) in structParams do - allLeaves := allLeaves ++ (← discoverStructLeaves paramName paramType) - -- Walk all schedule steps and collect which leaves are needed - let mut needed : Array (Name × TSyntax `term) := #[] - for step in allSteps do - match step with - | .Unconstrained _ (.NonRec (indName, args)) ps => - let tcName := match ps with - | .Generator => ``Plausible.Arbitrary - | .Enumerator => ``Enum - -- Check if the full source (indName applied to args) is itself a proj chain - let fullCE := ConstructorExpr.FuncApp indName args - if ← isStructProjChain structParamNames fullCE then - -- Direct leaf: the type being generated IS a projection of the struct param. - -- Emit a binder for it directly. - let argTerms ← args.toArray.mapM (monadLift <| constructorExprToTSyntaxTerm ·) - let leafSyn ← `($(mkIdent indName) $argTerms:term*) - let entry := (tcName, leafSyn) - unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do - needed := needed.push entry - else - -- Compound type case (e.g. `List (Params.Label P)`): an argument contains a - -- proj chain but the overall type is not itself a leaf. Use the same synthesis - -- approach as for Sort-typed params: open the type constructor's telescope, - -- introduce fvars with [Arbitrary/Enum/DecidableEq] for Sort-typed positions, - -- and attempt synthesis. If it succeeds, the struct leaves are needed. - let chains ← args.foldlM (fun acc arg => - (· ++ acc) <$> collectStructProjChains structParamNames arg) [] - if !chains.isEmpty then - -- Attempt synthesis to confirm that having leaf instances suffices - let succeeded ← Meta.withNewMCtxDepth do - let some indInfo ← (try pure (some (← getConstInfoInduct indName)) catch _ => pure none) - | pure true -- non-inductive (e.g. a def) — conservatively assume needed - let indLevels ← indInfo.levelParams.mapM (fun _ => do - let lv ← Meta.mkFreshLevelMVar; pure (.succ lv)) - let argTypes' ← getComponentsOfArrowType indInfo.type - let argTypes' := argTypes'.pop - let rec buildSynth (idx : Nat) (t : Expr) (fvars : Array Expr) : TermElabM Bool := - if idx >= argTypes'.size then do - let body := mkAppN (.const indName indLevels) fvars - let instTy ← try Meta.mkAppM tcName #[body] catch _ => return false - let result ← try Meta.synthInstance? instTy catch _ => pure none - return result.isSome - else do - let argTy := (← inferType t).bindingDomain! - let name := Name.mkSimple s!"arg_{idx}" - let bi := if argTy.isSort then BinderInfo.implicit else .default - withLocalDecl name bi argTy fun fv => do - if argTy.isSort then - let arbTy ← Meta.mkAppM ``Plausible.Arbitrary #[fv] - let enumTy ← Meta.mkAppM ``Enum #[fv] - let decEqTy ← Meta.mkAppM ``DecidableEq #[fv] - withLocalDecl (Name.mkSimple s!"inst_arb_{idx}") .instImplicit arbTy fun _ => - withLocalDecl (Name.mkSimple s!"inst_enum_{idx}") .instImplicit enumTy fun _ => - withLocalDecl (Name.mkSimple s!"inst_deceq_{idx}") .instImplicit decEqTy fun _ => - buildSynth (idx + 1) (.app t fv) (fvars.push fv) - else - buildSynth (idx + 1) (.app t fv) (fvars.push fv) - try buildSynth 0 (.const indName indLevels) #[] - catch _ => pure true -- on error, conservatively assume needed - if succeeded then - for leaf in allLeaves do - let entry := (tcName, leaf) - unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do - needed := needed.push entry - | _ => pure () - return needed - -/-- Convert struct leaf binder specs to actual bracketed binder syntax. - Each `(className, leafSyn)` becomes `[className leafSyn]`. -/ -def structLeafBindersToSyntax (binders : Array (Name × TSyntax `term)) - : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do - let result ← binders.mapM fun (cls, syn) => - `(Lean.Elab.Deriving.instBinderF| [$(mkIdent cls):ident $syn]) - return TSyntaxArray.mk result - /-- Synthesize `[tcName type]` for a compound type and extract what constraints the instance requires on Sort-typed params. Used for external deps (already in env). -/ private partial def synthExternalConstraints (indName : Name) (args : List ConstructorExpr) @@ -1825,7 +1869,7 @@ def deriveConstrainedProducerParts (constrArgs : Array Expr) (deriveSort : DeriveSort) (scheduleRewriter : List ScheduleStep → List ScheduleStep := id) (recFnNameOverride : Option Name := none) : - TermElabM (TSyntax `term × TSyntax `term × Array Name × TSyntaxArray `term × Array Expr × LocalContext × Name × List Level × ProducerSort) := do + TermElabM (TSyntax `term × TSyntax `term × Array Name × TSyntaxArray `term × Array Expr × LocalContext × Name × List Level × ProducerSort × TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do let producerSort := convertDeriveSortToProducerSort deriveSort -- Identify which argument positions are outputs (to be generated) let inductiveName := constrainingInductive @@ -1854,7 +1898,7 @@ def deriveConstrainedProducerParts let u ← Meta.mkFreshLevelMVar let v ← Meta.mkFreshLevelMVar pure (Lean.mkApp2 (Lean.mkConst ``Prod [u, v]) t rest)) outputTypes.toList - let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, localCtx) ← + let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, localCtx, structLeafBinders) ← -- Freshen argument names to avoid capture, then derive schedules per constructor withLocalDeclsDND argNamesTypes (fun _ => do let mut localCtx ← getLCtx @@ -1871,6 +1915,9 @@ def deriveConstrainedProducerParts (freshenedOutputNames[i]!, outputTypes[i]!, outputIdxs[i]!)) let mut nonRecursiveProducers := #[] let mut recursiveProducers := #[] + -- Accumulate every constructor's (rewritten) schedule steps for the + -- demand-driven struct-param leaf binders (see `computeStructLeafBinders`). + let mut allScheduleSteps : List ScheduleStep := [] let freshFuelPrimeName := localCtx.getUnusedName `fuel' let freshSizePrimeName := localCtx.getUnusedName `size' let freshSize' := mkIdent freshSizePrimeName @@ -1907,6 +1954,7 @@ def deriveConstrainedProducerParts let (scheduleSteps, scheduleSort) := result.schedule let rewrittenSteps := scheduleRewriter scheduleSteps let schedule := (rewrittenSteps, scheduleSort) + allScheduleSteps := allScheduleSteps ++ rewrittenSteps let (subProducer, requiredInsts) ← StateT.run (s := #[]) (do let mexp ← MExp.scheduleToMExp schedule (.MId `size) (.MId `initSize) _outputType (fuelPrimeName := freshFuelPrimeName) (sizePrimeName := freshSizePrimeName) (targetInductive := inductiveName) MExp.mexpToTSyntax mexp deriveSort) @@ -1942,8 +1990,18 @@ def deriveConstrainedProducerParts throwError "Cannot derive constrained producer for '{inductiveName}': all constructors are recursive (no finite base case)" let baseProducers ← `([$nonRecursiveProducers,*]) let inductiveProducers ← `([$nonRecursiveProducers,*, $recursiveProducers,*]) - return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx)) - return (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, inductiveName, inductiveLevels, producerSort) + -- Demand-driven struct-param leaf binders (e.g. `[Arbitrary P.info.Metadata]`), + -- computed from the accumulated schedule steps (see `computeStructLeafBinders`). + let structParams : Array (Name × Expr) := Id.run do + let mut sp := #[] + for i in [:argTypes.size] do + if i ∉ outputIdxs && !argTypes[i]!.isSort then + sp := sp.push (freshUnknowns[i]!, argTypes[i]!) + sp + let leafBinderSpecs ← computeStructLeafBinders allScheduleSteps structParams + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs + return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx, structLeafBinders)) + return (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, inductiveName, inductiveLevels, producerSort, structLeafBinders) private def deriveArbitrarySuchThatInstance' @@ -2136,10 +2194,10 @@ def deriveFromScheduleDep (dep : ScheduleDep) (scheduleRewriter : List ScheduleS let deriveSort := dep.deriveSort let parts ← deriveConstrainedProducerParts inputFVars outputFVars outputTypes.toArray dep.inductiveName indLevels allFVars deriveSort scheduleRewriter recFnNameOverride - let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outTypes, localCtx, _, _, producerSort) := parts + let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outTypes, localCtx, _, _, producerSort, structLeafBinders) := parts mkConstrainedProducerTypeClassInstance baseProducers inductiveProducers dep.inductiveName indLevels freshArgIdents freshenedOutputNames.toList - outTypes.toList producerSort localCtx + outTypes.toList producerSort localCtx structLeafBinders @[command_elab mutual_deriver] def elabDeriveMutual : CommandElab := fun stx => do @@ -2878,10 +2936,11 @@ def elabDeriveMutual : CommandElab := fun stx => do let e ← elabTerm termStx .none withParsedDerivingArgs e fun args outVars outTypes indName indLevels indArgs => do let parts ← deriveConstrainedProducerParts args outVars outTypes indName indLevels indArgs .Generator rewriter (some globalName) - let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, _, inductiveLevels, producerSort) := parts + let (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, _, inductiveLevels, producerSort, structLeafBinders) := parts mkConstrainedProducerMutualPieces baseProducers inductiveProducers indName inductiveLevels freshArgIdents freshenedOutputNames.toList outputTypes.toList producerSort localCtx globalName .Generator + (structLeafBinders := structLeafBinders) defCmds := defCmds.push defCmd instCmds := instCmds.push instCmd let mutualCmd ← `(command| mutual $defCmds* end) diff --git a/SpecimenTest.lean b/SpecimenTest.lean index e0eb787..cd2bdab 100644 --- a/SpecimenTest.lean +++ b/SpecimenTest.lean @@ -44,7 +44,7 @@ import SpecimenTest.DeriveArbitrary.ParameterizedTypeTest import SpecimenTest.DeriveArbitrary.MutuallyRecursiveTypeTest import SpecimenTest.DeriveArbitrarySuchThat.DeriveSTLCGenerator import SpecimenTest.DeriveArbitrarySuchThat.DeriveStructParamGenerator -import SpecimenTest.DeriveArbitrarySuchThat.StructParamPartialLeafTest +import SpecimenTest.DeriveArbitrarySuchThat.StructParamBinderTest import SpecimenTest.DeriveArbitrarySuchThat.NonLinearPatternsTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputTest import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputSTLCTest diff --git a/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean new file mode 100644 index 0000000..7d92d6b --- /dev/null +++ b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean @@ -0,0 +1,229 @@ +import Plausible.Gen +import Plausible.Arbitrary +import Specimen.Enumerators +import Specimen.EnumeratorCombinators +import Specimen.ArbitrarySizedSuchThat +import Specimen.DeriveConstrainedProducer +import Specimen.DeriveArbitrary +import Specimen.DeriveEnum + +/-! # Structure-parameter instance-binder tests + +When an inductive relation's output type is parameterized by a *structure* `P` +(rather than a plain `Sort`), each constructor field of a projection type like +`P.Label` or `P.info.Metadata` can only be produced if the derived instance +carries a matching `[Arbitrary P.Label]` / `[Enum P.Label]` binder. The deriver +computes these **demand-driven**: it emits a binder for exactly the projection +leaves that appear in the schedule — one per *used* leaf, and none for unused +ones. (`DeriveStructParamGenerator.lean` is the larger STLC-shaped witness of the +same capability; this file isolates the binder logic across every axis.) + +The tests vary three things: + +* **Leaf shape** — a *direct* field (`x : P.Used`), a leaf behind a *compound* + type (`tags : List P.Label`), and a *nested* struct chain (`P.inner.Needed`). +* **Emission path** — the single-instance path (`derive_generator` / + `derive_enumerator`) and the mutual path (`derive_mutual`). Both must emit the + binders. +* **Producer sort** — generators and enumerators. + +Every fixture uses the same poison technique to check the *demand-driven* +property: the **unused** sibling field is monomorphized to `Empty`, which has no +`Arbitrary`/`Enum` instance. So if the deriver over-emitted a binder for the +unused field, the instance would fail to synthesize at use-site. Where the +relation pins down the value's shape, an `#eval`'d computable **oracle** also +checks each sample is sound (not just that the instance elaborated). -/ + +open Plausible +open ArbitrarySizedSuchThat + +set_option guard_msgs.diff true +set_option specimen.autoDeriveDeps true +set_option specimen.multiOutput true + +namespace StructParamBinderTest + +/-! ## §1 Direct leaf: a tagged binary tree + +`TwoFields` bundles two abstract types; only `Used` is referenced (as the `leaf` +payload `x : P.Used`), `Unused` is the poison field. `TaggedTree` is recursive, +so generating it exercises the `[Arbitrary/Enum P.Used]` binder both at the base +case and underneath the recursive `node`. Monomorphize `Used = Nat`, +`Unused = Empty` throughout. -/ + +structure TwoFields where + Used : Type + Unused : Type + +inductive TaggedTree (P : TwoFields) where + | leaf (x : P.Used) : TaggedTree P + | node (l r : TaggedTree P) : TaggedTree P + +abbrev TF1 : TwoFields := ⟨Nat, Empty⟩ + +/-- Node count — a soundness oracle confirming a sample is a real `TaggedTree`. -/ +def treeSize {P : TwoFields} : TaggedTree P → Nat + | .leaf _ => 1 + | .node l r => treeSize l + treeSize r + 1 + +/-- `true` iff the tree is a single leaf — the oracle for `IsLeaf`. -/ +def isLeaf {P : TwoFields} : TaggedTree P → Bool + | .leaf _ => true + | .node _ _ => false + +/-- Constrains a tree to be exactly one leaf; deriving `∃ t, IsLeaf P t` must + produce `.leaf x` with `x : P.Used`. Used for the single-instance path. -/ +inductive IsLeaf (P : TwoFields) : TaggedTree P → Prop where + | leaf : IsLeaf P (.leaf x) + +/-- Accepts any well-formed tree (recursive relation). Used for the mutual path; + generating it produces trees with `node`s, exercising the leaf binder in a + recursive context. -/ +inductive IsTree (P : TwoFields) : TaggedTree P → Prop where + | leaf : IsTree P (.leaf x) + | node : IsTree P l → IsTree P r → IsTree P (.node l r) + +/-! ### §1a Single-instance generator (`derive_generator`) + +The single-instance path must emit `[Arbitrary P.Used]` — and nothing for the +`Empty`-monomorphized `Unused`. -/ +#guard_msgs(drop info, drop warning) in +derive_generator (fun (P : TwoFields) => ∃ t : TaggedTree P, IsLeaf P t) + +#guard_msgs(drop info) in +#eval show IO Unit from do + let mut count := 0 + for s in List.range 10 do + let t ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun t => IsLeaf TF1 t) 3) (s * 5 + 1) + if !isLeaf t then + throw (IO.userError "§1a unsound: IsLeaf generator produced a non-leaf") + count := count + 1 + IO.println s!"§1a single-instance generator, direct leaf: {count} sound samples" + +/-! ### §1b Single-instance enumerator (`derive_enumerator`) + +Same relation via the enumerator path — exercises the `[Enum P.Used]` binder. -/ +#guard_msgs(drop info, drop warning) in +derive_enumerator (fun (P : TwoFields) => ∃ t : TaggedTree P, IsLeaf P t) + +#guard_msgs(drop info) in +#eval show IO Unit from do + let mut total := 0 + let results ← runSizedEnum + (EnumSizedSuchThat.enumSizedST (fun t => IsLeaf TF1 t)) 3 + for r in results do + match r with + | .ok t => + if !isLeaf t then + throw (IO.userError "§1b unsound: IsLeaf enumerator produced a non-leaf") + total := total + 1 + | .error _ => pure () + IO.println s!"§1b single-instance enumerator, direct leaf: {total} sound results" + +/-! ### §1c Mutual path, recursive relation (`derive_mutual`) + +Both producer sorts at once, over the recursive `IsTree`. This is the original +demand-driven regression: the blind field-walk would have required +`[Arbitrary P.Unused]`, which cannot synthesize with `Unused = Empty`. -/ +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : TwoFields) => ∃ t : TaggedTree P, IsTree P t), + enumerator (fun (P : TwoFields) => ∃ t : TaggedTree P, IsTree P t) + +#guard_msgs(drop info) in +#eval show IO Unit from do + let mut count := 0 + for s in List.range 8 do + let t ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun t => IsTree TF1 t) 4) (s * 7 + 1) + -- Soundness: every sample is a real, finite `TaggedTree` (size ≥ 1). + if treeSize t < 1 then + throw (IO.userError "§1c unsound: degenerate tree") + count := count + 1 + let results ← runSizedEnum + (EnumSizedSuchThat.enumSizedST (fun t => IsTree TF1 t)) 3 + IO.println s!"§1c mutual, recursive relation: {count} gen samples, {results.length} enum results" + +/-! ## §2 Compound leaf: a struct-param field behind `List` + +`Bag` carries `tags : List P.Label` — the leaf `P.Label` appears only *inside* +`List _`, never as a bare field. The deriver must still emit `[Arbitrary P.Label]` +(and only that — `Phantom` is the `Empty` poison field). Deriving the generator +on the single-instance path covers both fixed behaviors at once: the compound +branch being demand-driven, and the single-instance path being wired. + +NOTE: a `derive_enumerator` for a *compound* struct-param leaf currently fails +with a spurious `Enum (Except GenError (List P.Label))` synthesis goal — a +**separate, pre-existing** bug in the enumerator's compound-field emission (it +reproduces regardless of the struct-param binder work, and does not affect the +*direct*-leaf enumerator in §1b, nor a plain `Type` parameter). It is out of +scope here; this section derives a generator only. -/ + +structure Config where + Label : Type + Phantom : Type + +inductive Bag (P : Config) where + | mk (tags : List P.Label) : Bag P + +def bagTags {P : Config} : Bag P → List P.Label + | .mk tags => tags + +inductive IsBag (P : Config) : Bag P → Prop where + | mk : IsBag P (.mk tags) + +abbrev Cfg1 : Config := ⟨Nat, Empty⟩ + +#guard_msgs(drop info, drop warning) in +derive_generator (fun (P : Config) => ∃ b : Bag P, IsBag P b) + +#guard_msgs(drop info) in +#eval show IO Unit from do + let mut count := 0 + for s in List.range 6 do + let b ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun b => IsBag Cfg1 b) 3) (s * 3 + 2) + -- Soundness: `bagTags` is a genuine `List Nat` we can consume. + let _ : Nat := (bagTags b).length + count := count + 1 + IO.println s!"§2 compound leaf (List P.Label), generator, Phantom = Empty: {count} samples" + +/-! ## §3 Nested struct: a two-step projection chain + +`Outer.inner : Inner` is itself a structure; only `Inner.Needed` is used (reached +by the chain `P.inner.Needed`), so the deriver must emit +`[Arbitrary (Inner.Needed (Outer.inner P))]` and nothing for the other, +`Empty`-monomorphized fields. Derived on the mutual path for both producer +sorts. -/ + +structure Inner where + Needed : Type + NotNeeded : Type + +structure Outer where + inner : Inner + TopLevel : Type + +inductive Wrapped (P : Outer) where + | mk (v : P.inner.Needed) : Wrapped P + +inductive IsGood (P : Outer) : Wrapped P → Prop where + | mk : IsGood P (.mk v) + +abbrev Out1 : Outer := ⟨⟨Bool, Empty⟩, Empty⟩ + +#guard_msgs(drop info, drop warning) in +derive_mutual + generator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w), + enumerator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w) + +#guard_msgs(drop info) in +#eval show IO Unit from do + let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun w => @IsGood Out1 w) 2) 7 + let results ← runSizedEnum + (EnumSizedSuchThat.enumSizedST (fun w => @IsGood Out1 w)) 2 + IO.println s!"§3 nested struct (P.inner.Needed), mutual: ok, {results.length} enum results" + +end StructParamBinderTest diff --git a/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean b/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean deleted file mode 100644 index e4f3c3e..0000000 --- a/SpecimenTest/DeriveArbitrarySuchThat/StructParamPartialLeafTest.lean +++ /dev/null @@ -1,127 +0,0 @@ -import Plausible.Gen -import Plausible.Arbitrary -import Specimen.Enumerators -import Specimen.EnumeratorCombinators -import Specimen.ArbitrarySizedSuchThat -import Specimen.DeriveConstrainedProducer -import Specimen.DeriveArbitrary -import Specimen.DeriveEnum - -/-! # Demand-driven struct-param binder tests - -Verify that the deriver only emits instance binders for struct-param fields that -actually appear in the schedule. A struct with fields `Used : Type` and -`Unused : Type` should only require `[Arbitrary P.Used]` — not both. - -This is a regression test for the demand-driven approach vs. the old -`expandStructInstBinders` which would blindly walk all fields. -/ - -open Plausible -open ArbitrarySizedSuchThat - -set_option guard_msgs.diff true -set_option specimen.autoDeriveDeps true -set_option specimen.multiOutput true - -namespace PartialLeafTest - -/-! ## Test 1: Only one of two struct fields used - -`TwoFields` has `Used : Type` and `Unused : Type`. The relation `HasVal` only -mentions `P.Used` in its constructors. If the deriver emits `[Arbitrary P.Unused]` -too, it would appear in the generated instance signature — but we deliberately -do NOT provide an `Arbitrary` instance for the `Unused` field's monomorphization, -so if the binder were emitted the instance would fail to synthesize at use-site. -/ - -structure TwoFields where - Used : Type - Unused : Type - -inductive TaggedExpr (P : TwoFields) where - | leaf (x : P.Used) : TaggedExpr P - | node (l r : TaggedExpr P) : TaggedExpr P - -inductive HasVal (P : TwoFields) : TaggedExpr P → Prop where - | leaf : HasVal P (.leaf x) - | node : HasVal P l → HasVal P r → HasVal P (.node l r) - -#guard_msgs(drop info, drop warning) in -derive_mutual - generator (fun (P : TwoFields) => ∃ e : TaggedExpr P, HasVal P e), - enumerator (fun (P : TwoFields) => ∃ e : TaggedExpr P, HasVal P e) - -/-! Monomorphize: `Used = Nat`, `Unused = Empty` (no Arbitrary instance for Empty). - If the deriver emitted `[Arbitrary P.Unused]`, this #eval would fail to synthesize. -/ -abbrev TF1 : TwoFields := ⟨Nat, Empty⟩ - -#guard_msgs(drop info) in -#eval show IO Unit from do - let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST - (fun e => HasVal TF1 e) 3) 42 - IO.println s!"partial-leaf test 1: derived instance synthesizes with Unused = Empty" - -/-! ## Test 2: Struct field used only via compound type - -`Config` has `Label : Type` and `Phantom : Type`. The constructor references -`P.Label` but never `P.Phantom` directly. -/ - -structure Config where - Label : Type - Phantom : Type - -inductive LabelledList (P : Config) where - | nil : LabelledList P - | cons (tag : P.Label) (rest : LabelledList P) : LabelledList P - -inductive IsLabelled (P : Config) : LabelledList P → Prop where - | nil : IsLabelled P .nil - | cons : IsLabelled P rest → IsLabelled P (.cons tag rest) - -#guard_msgs(drop info, drop warning) in -derive_mutual - generator (fun (P : Config) => ∃ xs : LabelledList P, IsLabelled P xs), - enumerator (fun (P : Config) => ∃ xs : LabelledList P, IsLabelled P xs) - -/-! Monomorphize: `Label = String`, `Phantom = Empty`. -/ -abbrev C1 : Config := ⟨String, Empty⟩ - -#guard_msgs(drop info) in -#eval show IO Unit from do - let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST - (fun xs => IsLabelled C1 xs) 3) 42 - IO.println s!"partial-leaf test 2: compound-type case works with Phantom = Empty" - -/-! ## Test 3: Nested struct, only inner field used - -`Outer` has `inner : Inner` and `TopLevel : Type`. `Inner` has `Needed : Type` -and `NotNeeded : Type`. The relation only uses `P.inner.Needed`. -/ - -structure Inner where - Needed : Type - NotNeeded : Type - -structure Outer where - inner : Inner - TopLevel : Type - -inductive Wrapped (P : Outer) where - | mk (v : P.inner.Needed) : Wrapped P - -inductive IsGood (P : Outer) : Wrapped P → Prop where - | mk : IsGood P (.mk v) - -#guard_msgs(drop info, drop warning) in -derive_mutual - generator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w), - enumerator (fun (P : Outer) => ∃ w : Wrapped P, IsGood P w) - -/-! Monomorphize: `inner.Needed = Bool`, everything else `Empty`. -/ -abbrev O1 : Outer := ⟨⟨Bool, Empty⟩, Empty⟩ - -#guard_msgs(drop info) in -#eval show IO Unit from do - let _ ← Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST - (fun w => @IsGood O1 w) 2) 7 - IO.println s!"partial-leaf test 3: nested struct, only inner.Needed required" - -end PartialLeafTest From da0e21613e9d18d44fe0f54e05ea003699a1adc0 Mon Sep 17 00:00:00 2001 From: Michael Hicks Date: Wed, 29 Jul 2026 18:53:45 +0000 Subject: [PATCH 5/5] properly propagate typeclass constraints on type variables stored in structure parameters --- Docs/Struct-param-support.md | 114 +++++-- Specimen/DeriveConstrainedProducer.lean | 323 +++++++++++++++--- .../StructParamBinderTest.lean | 50 +++ SpecimenTest/PolymorphicDepConstraints.lean | 90 +++++ 4 files changed, 490 insertions(+), 87 deletions(-) diff --git a/Docs/Struct-param-support.md b/Docs/Struct-param-support.md index a27316e..4e8faa4 100644 --- a/Docs/Struct-param-support.md +++ b/Docs/Struct-param-support.md @@ -74,24 +74,63 @@ including `P`). `computeStructLeafBinders` scans a spec's schedule steps and returns the `(className, leafSyntax)` binders the producer needs — one per struct-param -projection leaf that **actually appears**, and none for unused fields. It only -inspects `.Unconstrained` steps (the ones that draw a value from an unconstrained -`Arbitrary`/`Enum` instance) and handles two shapes: - -- **Direct leaf** — the step's source *is* a projection chain rooted at the - struct param (`isStructProjChain`), e.g. generating a value of type `P.Label`. - Emit a binder for that leaf directly. -- **Compound leaf** — an argument *contains* a projection chain but the overall - type is not itself a leaf, e.g. `List P.Label`. `collectStructProjChains` finds - the chains; a synthesis probe (opening the type constructor's telescope with - `[Arbitrary/Enum/DecidableEq]` on its `Sort`-typed positions) confirms leaf - instances suffice; then `resolveChainType` maps **each chain present in the - step** back to its leaf syntax and emits binders for those leaves only. - -`structLeavesFromType` is the shared recursive walk: a `Type u` value is a leaf; -a structure-typed value recurses through each field's projection, building -projection-chain syntax (`P.info` → `NodeInfo.Metadata (P.info)`). -`structLeafBindersToSyntax` renders the results as `[className leaf]` binders. +projection leaf that **actually appears**, and none for unused fields. This is +the leaf-granularity analogue of the constraint propagation in +`Docs/Constraint-propagation.md` (`computeSpecConstraints`): where that discovers +which classes a spec needs on its plain `Sort` type parameters, this discovers +them for each `Type`-valued projection leaf of a structure parameter. In both, +**the class attached to a leaf is discovered from how the leaf is used, not +hardcoded**, so a leaf gets only the classes it strictly needs. + +Three kinds of step contribute binders: + +- **Unconstrained generation** — a step that draws a value of a leaf type from an + unconstrained `Arbitrary`/`Enum` instance demands the producer's own class + (`Arbitrary` for generators, `Enum` for enumerators). Two shapes: + - *Direct leaf*: the step's source *is* a projection chain rooted at the struct + param (`isStructProjChain`), e.g. generating a value of type `P.Label`. + - *Compound leaf*: an argument *contains* a projection chain but the overall + type is not itself a leaf, e.g. `List P.Label`. `collectStructProjChains` + finds the chains; a synthesis probe (opening the type constructor's telescope + with `[Arbitrary/Enum/DecidableEq]` on its `Sort`-typed positions) confirms + leaf instances suffice; then each chain present in the step is mapped back to + its leaves. +- **Equality check** — an `Eq`/`Ne` `Check` over a leaf type demands + `[DecidableEq leaf]` on that leaf. Equality on a type always needs decidable + equality — the one constraint knowable statically, exactly as + `computeSpecConstraints` special-cases it for plain type params. (Without this, + a relation like `Distinct P (.mk a b)` where `a b : P.Key` and the rule requires + `a ≠ b` would fail to derive: the generated checker needs `DecidableEq P.Key`.) +- **`SuchThat` on a leaf output** — a step that draws a leaf-typed value + satisfying a relation (a *constrained* producer dependency, e.g. finding a + witness `x : P.A`) demands the producer's unconstrained class on that leaf, + because the dependency's own producer requires it. Only *proper* projections + count here: an output that merely mentions the bare parameter inside a compound + (e.g. producing `TaggedTree P`) is handled by that dependency's own binders, so + bare-parameter chains are skipped (`leafProjsInArgs`) to avoid re-expanding all + of `P`'s fields. + +So a leaf used only for generation gets just `Arbitrary`/`Enum` (never a spurious +`DecidableEq`), a leaf used only in an equality check gets just `DecidableEq`, and +a leaf used both ways gets both. `resolveChainType` maps a projection chain to its +root structure type and projection path; `structLeavesFromType` is the shared +recursive walk (a `Type u` value is a leaf; a structure-typed value recurses +through each field's projection). Leaves are represented identifier-agnostically +as `StructLeaf` (root structure + projection-function path), so the *same* leaf +compares equal across specs regardless of how each spec freshens the parameter's +name; `structLeafBindersToSyntax` renders each leaf rooted at the emitting spec's +own parameter identifier. + +**Cross-spec propagation.** A leaf constraint often originates in a *dependency*: +a generator that checks `¬ HasWitness` needs whatever `HasWitness`'s checker needs +to enumerate its leaf-typed witness (`[Enum P.A]`). `propagateStructLeafBinders` +handles this — the leaf-level analogue of `propagateConstraints`. Walking +components in topological order (mutual SCCs to a fixed point), each spec's binders +are its own (`computeOwnStructLeafBinders`) unioned with those of every +relation/checker dependency it uses. Because leaves are identifier-agnostic, a +dependency's leaf re-renders correctly against the dependant's own parameter — all +specs in one `derive_mutual` share the same structure parameter, just under +different freshened names. These binders are threaded into every emission path in `MakeConstrainedProducerInstance.lean`: @@ -105,12 +144,12 @@ These binders are threaded into every emission path in wrapper `instance` commands append them too. All deriver entry points compute the binders and pass them through: -`deriveConstrainedProducer` (used by `derive_generator` / `derive_enumerator`), -`deriveConstrainedProducerParts` (used by `deriveFromScheduleDep`), and -`compileInductiveSchedule` (the `derive_mutual` path). Each accumulates its -constructors' schedule steps, derives `structParams` from the non-output, -non-`Sort` arguments (named by their freshened names so the emitted binders match -the instance signature), and calls `computeStructLeafBinders`. +`deriveConstrainedProducer` (used by `derive_generator` / `derive_enumerator`) +and `deriveConstrainedProducerParts` (used by `deriveFromScheduleDep`) each derive +`structParams` from their non-output, non-`Sort` arguments and call +`computeStructLeafBinders` directly; `compileInductiveSchedule` (the +`derive_mutual` path) instead receives the SCC-propagated binders from +`propagateStructLeafBinders` and falls back to its own only when none is supplied. ### 2c. Drop implicit constructor args from produced values @@ -134,13 +173,14 @@ to the producer schedule's `conclusionOutputs` before converting them to `MExp`s ## 3. Tests - **`SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean`** isolates - the binder logic across three axes: leaf shape (direct field / compound - `List P.Label` / nested `P.inner.Needed`), emission path (single-instance vs. - mutual), and producer sort (generator / enumerator). Every fixture monomorphizes - the *unused* sibling field to `Empty` (which has no `Arbitrary`/`Enum` - instance), so an over-emitted binder would fail to synthesize at use-site; a - computable oracle is `#eval`'d over samples wherever the relation fixes the - value's shape. + the binder logic across leaf shape (direct field / compound `List P.Label` / + nested `P.inner.Needed`), emission path (single-instance vs. mutual), and + producer sort (generator / enumerator), plus a case checking that per-leaf + *constraints* are discovered rather than hardcoded — a leaf compared with `≠` + gets `DecidableEq` on top of `Arbitrary`. Every fixture monomorphizes the + *unused* sibling field to `Empty` (which has no `Arbitrary`/`Enum` instance), so + an over-emitted binder would fail to synthesize at use-site; a computable oracle + is `#eval`'d over samples wherever the relation fixes the value's shape. - **`SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean`** is a self-contained miniature STLC witness: a structure parameter with one nested @@ -182,3 +222,15 @@ to the producer schedule's `conclusionOutputs` before converting them to `MExp`s universe-polymorphic structure parameter the projection type would be computed at the wrong universe. All current Strata params are `Type 0`. A fix would extract the parameter type's universe levels and pass them to `mkConst`. + +- **Leaf constraints are limited to the standard classes.** + `computeStructLeafBinders` attaches to a leaf the producer class + (`Arbitrary`/`Enum`) for generation/`SuchThat` steps and `DecidableEq` for + `Eq`/`Ne` checks, and `propagateStructLeafBinders` carries those across the + dependency graph (so a checker's `[Enum P.A]` reaches a generator that checks + it). It does not run the full `synthExternalConstraints` *read-back* that + `computeSpecConstraints` uses for plain type params, so if a leaf were passed to + a dependency requiring some *non-standard* class (e.g. a custom `[MyHashable + P.A]`), that class would not be discovered. No current example needs this; + covering it would mean reading a dependency's instance binders back at leaf + granularity rather than assuming the standard classes. diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean index 1158947..7e36b46 100644 --- a/Specimen/DeriveConstrainedProducer.lean +++ b/Specimen/DeriveConstrainedProducer.lean @@ -733,70 +733,140 @@ partial def collectStructProjChains (structParamNames : Std.HashSet Name) args.foldlM (fun acc arg => (· ++ acc) <$> collectStructProjChains structParamNames arg) [] | _ => return [] -/-- Recursively discover the `Type`-valued leaf projections *reachable from* a - projection whose value has type `ty` and whose surface syntax is `syn`. - A `Type u` leaf yields `#[syn]`; a structure-typed value recurses into each - field's projection (`sName ++ field` applied to `syn`). For a value of type - `NodeInfo` reached as `ExprParams.info P`, this yields - `NodeInfo.Metadata (ExprParams.info P)`. -/ -partial def structLeavesFromType (ty : Expr) (syn : TSyntax `term) : - TermElabM (Array (TSyntax `term)) := do - if ty.isSort then return #[syn] +/-- A `Type`-valued leaf of a structure parameter, represented *independently of + the parameter's identifier* so it can be compared and re-rendered across specs + (each `derive_mutual` spec freshens the parameter's name differently). It is: + the root structure type (`rootStruct`, e.g. `ExprParams`) and the projection + functions applied to reach the leaf, outermost-first (`projPath`, e.g. + `[NodeInfo.Metadata, ExprParams.info]` for `NodeInfo.Metadata (ExprParams.info P)`; + `[]` denotes the bare parameter itself when its type is already a `Type`). -/ +structure StructLeaf where + rootStruct : Name + projPath : List Name + deriving BEq, Repr + +/-- Render a `StructLeaf` as surface syntax rooted at a given parameter identifier: + fold the projection path over `paramIdent`, outermost projection last applied. -/ +def StructLeaf.toSyntax (leaf : StructLeaf) (paramIdent : Ident) : TermElabM (TSyntax `term) := do + let rec go : List Name → TermElabM (TSyntax `term) + | [] => pure paramIdent + | f :: rest => do let inner ← go rest; `($(mkIdent f) $inner) + go leaf.projPath + +/-- Recursively discover the `Type`-valued leaves *reachable from* a value of type + `ty` reached via `path` (the projections already applied, outermost-first) from + a parameter of structure type `rootStruct`. A `Type u` value is itself a leaf; + a structure-typed value recurses through each field's projection. -/ +partial def structLeavesFromType (rootStruct : Name) (ty : Expr) (path : List Name) : + TermElabM (Array StructLeaf) := do + if ty.isSort then return #[{ rootStruct, projPath := path }] let env ← getEnv let some sName := ty.constName? | return #[] let some sInfo := getStructureInfo? env sName | return #[] - let mut result : Array (TSyntax `term) := #[] + let mut result : Array StructLeaf := #[] for field in sInfo.fieldNames do let projName := sName ++ field let projType ← forallTelescopeReducing (← inferType (mkConst projName)) (fun _ body => pure body) - let projSyn ← `($(mkIdent projName) $syn) - result := result ++ (← structLeavesFromType projType projSyn) + result := result ++ (← structLeavesFromType rootStruct projType (projName :: path)) return result /-- Resolve a struct-param projection chain (as a `ConstructorExpr`) to the Lean - type of the value it denotes together with its surface syntax. The chain root - must be one of `structParams`; each `.FuncApp projName [base]` step is a - structure projection whose codomain is read from `projName`'s signature. - Returns `none` if `ce` is not a projection chain rooted at a known struct param - (e.g. it is an arbitrary function application). -/ + type of the value it denotes together with its root structure type and the + projection path taken (outermost-first). The chain root must be one of + `structParams`; each `.FuncApp projName [base]` step is a structure projection + whose codomain is read from `projName`'s signature. Returns `none` if `ce` is + not a projection chain rooted at a known struct param. -/ partial def resolveChainType (structParams : Array (Name × Expr)) (ce : ConstructorExpr) : - TermElabM (Option (Expr × TSyntax `term)) := do + TermElabM (Option (Expr × Name × List Name)) := do match ce with | .Unknown n => match structParams.find? (fun (pn, _) => pn == n) with - | some (_, pty) => return some (pty, mkIdent n) + | some (_, pty) => + match pty.constName? with + | some rootStruct => return some (pty, rootStruct, []) + | none => return none | none => return none | .FuncApp projName [base] => if ← Lean.isProjectionFn projName then match ← resolveChainType structParams base with - | some (_, baseSyn) => + | some (_, rootStruct, basePath) => let projType ← forallTelescopeReducing (← inferType (mkConst projName)) (fun _ body => pure body) - let projSyn ← `($(mkIdent projName) $baseSyn) - return some (projType, projSyn) + return some (projType, rootStruct, projName :: basePath) | none => return none else return none | _ => return none -/-- Compute struct-param leaf binders needed by a spec's schedule steps. - For each `Unconstrained` step whose source is a projection chain (or contains one), - determines the `Type`-valued leaves that need instance binders. +/-- Collect the `Type`-valued struct-param leaves reachable from the projection + chains contained in `args`. For `[List (Params.Label P)]` this returns the leaf + for `Params.Label P`; for a direct type argument `P.info` it returns the leaves + of `NodeInfo` reached through `ExprParams.info`, etc. -/ +private def leafsInArgs (structParams : Array (Name × Expr)) + (structParamNames : Std.HashSet Name) (args : List ConstructorExpr) : + TermElabM (Array StructLeaf) := do + let chains ← args.foldlM (fun acc arg => + (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + let mut result : Array StructLeaf := #[] + for chain in chains do + if let some (chainTy, rootStruct, chainPath) ← resolveChainType structParams chain then + result := result ++ (← structLeavesFromType rootStruct chainTy chainPath) + return result - Returns an array of `(className, leafSyntax)` pairs — e.g. - `(``Plausible.Arbitrary, `(NodeInfo.Metadata (ExprParams.info P)))`. +/-- Like `leafsInArgs`, but only for *proper* projection chains — those with at + least one field projection applied (`.FuncApp projName [..]`), i.e. `P.A` or + `P.info.Metadata`, never the bare parameter `.Unknown P`. Expanding a bare `P` + would walk *all* of the structure's fields (the blind field-walk), so this is + used where an output type may legitimately mention `P` inside a compound + (e.g. `TaggedTree P`) whose own dependency already carries the right binders. -/ +private def leafProjsInArgs (structParams : Array (Name × Expr)) + (structParamNames : Std.HashSet Name) (args : List ConstructorExpr) : + TermElabM (Array StructLeaf) := do + let chains ← args.foldlM (fun acc arg => + (· ++ acc) <$> collectStructProjChains structParamNames arg) [] + let mut result : Array StructLeaf := #[] + for chain in chains do + match chain with + | .Unknown _ => pure () -- bare parameter: skip (not a leaf projection) + | _ => + if let some (chainTy, rootStruct, chainPath) ← resolveChainType structParams chain then + result := result ++ (← structLeavesFromType rootStruct chainTy chainPath) + return result - `structParams` is `(paramName, paramType)` for non-Sort, non-output params. - The function discovers which leaves actually appear in schedule steps (directly as - a proj-chain step, or wrapped in a compound type like `List (P.Label)`). -/ +/-- Compute the instance binders a spec's schedule needs for the `Type`-valued + *leaves* of its structure parameters (e.g. `[Arbitrary P.info.Metadata]`). + + This mirrors `computeSpecConstraints` (#42), which discovers the constraints a + spec needs on its plain `Sort` type parameters — but applied at the granularity + of an individual projection leaf, since each leaf gets its own binder. Like + #42, the class attached to a leaf is *discovered from how the leaf is used*, + not hardcoded, so a leaf gets only the classes it strictly needs: + + * an `Unconstrained` step that generates a value of a leaf type (directly, or + inside a compound type like `List P.Label`) demands the producer's + unconstrained class — `Arbitrary` for generators, `Enum` for enumerators; + * an `Eq`/`Ne` `Check` over a leaf type demands `DecidableEq` on that leaf + (equality on a type always needs decidable equality — the one constraint we + know statically, exactly as #42 special-cases it for plain type params). + + Returns `(className, leaf)` pairs, deduplicated. Leaves are represented as + identifier-agnostic `StructLeaf`s so they can be compared and re-rendered per + spec (see `propagateStructLeafBinders`). A leaf that appears in no step gets no + binder; a leaf used only for generation never picks up a spurious `DecidableEq`, + and vice versa. + + `structParams` is `(paramName, paramType)` for non-Sort, non-output params. -/ def computeStructLeafBinders (allSteps : List ScheduleStep) (structParams : Array (Name × Expr)) - : TermElabM (Array (Name × TSyntax `term)) := do + : TermElabM (Array (Name × StructLeaf)) := do if structParams.isEmpty then return #[] let structParamNames : Std.HashSet Name := structParams.foldl (fun s (n, _) => s.insert n) {} - -- Walk all schedule steps and collect which leaves are needed - let mut needed : Array (Name × TSyntax `term) := #[] + -- Walk all schedule steps and collect (class, leaf) binders demanded by each. + let mut needed : Array (Name × StructLeaf) := #[] + let pushEntry := fun (needed : Array (Name × StructLeaf)) (cls : Name) (leaf : StructLeaf) => + if needed.any (fun p => p.1 == cls && p.2 == leaf) then needed + else needed.push (cls, leaf) for step in allSteps do match step with | .Unconstrained _ (.NonRec (indName, args)) ps => @@ -807,12 +877,9 @@ def computeStructLeafBinders (allSteps : List ScheduleStep) let fullCE := ConstructorExpr.FuncApp indName args if ← isStructProjChain structParamNames fullCE then -- Direct leaf: the type being generated IS a projection of the struct param. - -- Emit a binder for it directly. - let argTerms ← args.toArray.mapM (monadLift <| constructorExprToTSyntaxTerm ·) - let leafSyn ← `($(mkIdent indName) $argTerms:term*) - let entry := (tcName, leafSyn) - unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do - needed := needed.push entry + -- Emit a producer-class binder for it directly. + if let some (_, rootStruct, path) ← resolveChainType structParams fullCE then + needed := pushEntry needed tcName { rootStruct, projPath := path } else -- Compound type case (e.g. `List (Params.Label P)`): an argument contains a -- proj chain but the overall type is not itself a leaf. Use the same synthesis @@ -857,20 +924,57 @@ def computeStructLeafBinders (allSteps : List ScheduleStep) -- Emit binders only for the leaves reachable from the projection chains -- that actually appear in this step (not every leaf of every struct -- param) — so an unused field never drags in a spurious binder. - for chain in chains do - if let some (chainTy, chainSyn) ← resolveChainType structParams chain then - for leaf in (← structLeavesFromType chainTy chainSyn) do - let entry := (tcName, leaf) - unless needed.any (fun p => p.1 == entry.1 && p.2.raw == entry.2.raw) do - needed := needed.push entry + for leaf in (← leafsInArgs structParams structParamNames args) do + needed := pushEntry needed tcName leaf + | .Check (.NonRec (indName, args)) _ => + -- Equality/disequality over a struct-param leaf demands `DecidableEq` on + -- that leaf, mirroring the Eq/Ne rule in `computeSpecConstraints`. The + -- compared type rides along as the relation's (implicit) type argument, so + -- it is picked up as a projection chain in `args` just like any other. + if indName == ``Eq || indName == ``Ne then + for leaf in (← leafsInArgs structParams structParamNames args) do + needed := pushEntry needed ``DecidableEq leaf + | .SuchThat varsTys _ ps => + -- A `SuchThat` step draws a value satisfying a relation via a *constrained* + -- producer dependency. When such an output is itself a struct-param leaf + -- (e.g. finding a witness `x : P.A`), that dependency's producer requires + -- the leaf's *unconstrained* class in scope — `Enum` for enumerators, + -- `Arbitrary` for generators — so the enclosing instance must carry it. + -- (This is what lets a checker that must enumerate a leaf-typed witness get + -- its `[Enum P.A]` binder, and thus propagate to any generator depending on + -- that checker.) + -- + -- Only *proper* leaf projections count: an output whose type merely mentions + -- the bare parameter `P` inside a compound (e.g. producing `TaggedTree P`) is + -- handled by that dependency's own constraints — we must not expand `P` into + -- all its fields here (that would be the blind field-walk, dragging in unused + -- leaves), so `leafProjsInArgs` skips bare-parameter chains. + let tcName := match ps with + | .Generator => ``Plausible.Arbitrary + | .Enumerator => ``Enum + let outputTypeCEs := varsTys.filterMap Prod.snd + for leaf in (← leafProjsInArgs structParams structParamNames outputTypeCEs) do + needed := pushEntry needed tcName leaf | _ => pure () return needed -/-- Convert struct leaf binder specs to actual bracketed binder syntax. - Each `(className, leafSyn)` becomes `[className leafSyn]`. -/ -def structLeafBindersToSyntax (binders : Array (Name × TSyntax `term)) +/-- Convert struct leaf binder specs to bracketed binder syntax, rendering each + leaf rooted at the identifier of *this spec's* struct parameter of the matching + structure type. `structParams` maps this spec's parameter names to their types; + a leaf is rendered against the parameter whose type is the leaf's `rootStruct`. + (This re-rooting is what makes an inherited dependency's leaf refer to the + dependant's own parameter, so the binder and the conclusion agree.) Leaves whose + root structure has no matching parameter here are dropped. -/ +def structLeafBindersToSyntax (binders : Array (Name × StructLeaf)) + (structParams : Array (Name × Expr)) : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do - let result ← binders.mapM fun (cls, syn) => + -- Resolve each leaf to (class, rendered-syntax), dropping leaves with no matching + -- parameter here, then build the binders (mirrors the original mapM + `.mk`). + let mut clsSyns : Array (Name × TSyntax `term) := #[] + for (cls, leaf) in binders do + if let some (paramName, _) := structParams.find? (fun (_, ty) => ty.constName? == some leaf.rootStruct) then + clsSyns := clsSyns.push (cls, ← leaf.toSyntax (mkIdent paramName)) + let result ← clsSyns.mapM fun (cls, syn) => `(Lean.Elab.Deriving.instBinderF| [$(mkIdent cls):ident $syn]) return TSyntaxArray.mk result @@ -1093,7 +1197,7 @@ def deriveConstrainedProducer sp := sp.push (freshUnknowns[i]!, argTypes[i]!) sp let leafBinderSpecs ← computeStructLeafBinders allScheduleSteps structParams - let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs structParams return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx, structLeafBinders)) @@ -1418,12 +1522,109 @@ def propagateConstraints (components : List (List SpecKey)) result := result.insert key cs return result +/-- Union of two `(class, leaf)` binder-spec arrays, deduplicated by + `(class, leaf-syntax)`. Used to merge struct-leaf binders across specs. -/ +def unionLeafBinders (a b : Array (Name × StructLeaf)) : Array (Name × StructLeaf) := Id.run do + let mut result := a + for entry in b do + unless result.any (fun p => p.1 == entry.1 && p.2 == entry.2) do + result := result.push entry + return result + +/-- Compute a spec's *own* struct-param leaf binders (ignoring dependencies): the + `(class, leaf)` binders demanded directly by its own schedule steps. Mirrors + the `structParams` computation in `compileInductiveSchedule`. -/ +def computeOwnStructLeafBinders (indSched : InductiveSchedule) + : TermElabM (Array (Name × StructLeaf)) := do + let key := indSched.key + let indInfo ← getConstInfoInduct key.inductiveName + let indLevels := indInfo.levelParams.map (Level.param ·) + let numArgs := (← getComponentsOfArrowType indInfo.type).size - 1 + let argNames := (List.range numArgs).map (fun i => indSched.argNames.getD i (Name.mkSimple s!"arg_{i}")) + let argNameTypes : Array (Name × Expr) := (Array.range numArgs).map (fun i => (argNames.getD i `x, mkSort .zero)) + withLocalDeclsDND argNameTypes fun allFVars => do + let liveTypes ← getCorrectTypes allFVars key.inductiveName indLevels + let structParams : Array (Name × Expr) := Id.run do + let mut sp := #[] + for i in [:liveTypes.size] do + if i ∉ key.outputIndices && !liveTypes[i]!.isSort then + sp := sp.push (argNames.getD i `x, liveTypes[i]!) + sp + let allSteps := (indSched.baseSchedules ++ indSched.recSchedules).flatMap (fun (_, (steps, _)) => steps) + computeStructLeafBinders allSteps structParams + +/-- Bottom-up propagation of struct-param leaf binders across specs, the leaf-level + analogue of `propagateConstraints`. A spec's binders are its own (from + `computeOwnStructLeafBinders`) unioned with those of every relation/checker + dependency it uses — so, e.g., a generator that checks `¬ HasWitness` inherits + the `[Enum P.A]` binder that `HasWitness`'s checker needs to enumerate a + leaf-typed witness. All specs in a `derive_mutual` share the same structure + parameter, so a dependency's leaf syntax (`P.A`) is valid verbatim in the + dependant. Components are topological (deps first); mutual SCCs iterate to a + fixed point. -/ +def propagateStructLeafBinders (components : List (List SpecKey)) + (memo : Std.HashMap SpecKey MemoEntry) : TermElabM (Std.HashMap SpecKey (Array (Name × StructLeaf))) := do + -- The relation/checker dep keys a spec references (same filter as `computeSpecSCC`). + let depKeysOf (indSched : InductiveSchedule) : List SpecKey := + let allScheds := indSched.baseSchedules ++ indSched.recSchedules + let deps := allScheds.flatMap (fun (_, (steps, _)) => collectNonRecDeps steps) + let relDeps := deps.filter (fun d => d.kind == .relation || d.kind == .checker) + (relDeps.map (fun d => SpecKey.mk d.inductiveName d.outputIndices d.deriveSort)).eraseDups + let mut result : Std.HashMap SpecKey (Array (Name × StructLeaf)) := {} + for comp in components do + if comp.length == 1 then + let key := comp.head! + match memo[key]? with + | some (.done indSched) => + if indSched.alreadyExists then + result := result.insert key #[] + else + let mut binders ← computeOwnStructLeafBinders indSched + for depKey in depKeysOf indSched do + if let some depBinders := result[depKey]? then + binders := unionLeafBinders binders depBinders + result := result.insert key binders + | _ => result := result.insert key #[] + else + -- Mutual block: fixed-point iteration (binders can only grow → converges). + let mut sibMap : Std.HashMap SpecKey (Array (Name × StructLeaf)) := {} + let mut ownMap : Std.HashMap SpecKey (Array (Name × StructLeaf)) := {} + for key in comp do + sibMap := sibMap.insert key #[] + match memo[key]? with + | some (.done indSched) => + if !indSched.alreadyExists then + ownMap := ownMap.insert key (← computeOwnStructLeafBinders indSched) + | _ => pure () + let mut changed := true + while changed do + changed := false + for key in comp do + match memo[key]? with + | some (.done indSched) => + if indSched.alreadyExists then continue + let mut binders := ownMap[key]?.getD #[] + for depKey in depKeysOf indSched do + -- Dep may be a sibling (this SCC) or an earlier component. + if let some depBinders := sibMap[depKey]? then + binders := unionLeafBinders binders depBinders + if let some depBinders := result[depKey]? then + binders := unionLeafBinders binders depBinders + if binders.size != (sibMap[key]?.getD #[]).size then + changed := true + sibMap := sibMap.insert key binders + | _ => pure () + for (key, bs) in sibMap.toList do + result := result.insert key bs + return result + /-- Compiles an InductiveSchedule from the memo into (def, instance) commands. Uses the pre-derived schedules directly (no re-derivation). `siblings` is the list of specs in the same mutual block (for rewriting to Source.MutRec). -/ def compileInductiveSchedule (indSched : InductiveSchedule) (globalName : Name) (siblings : List (Name × List Nat × Name × DeriveSort)) (requiredConstraints : Option (Array Name) := none) + (propagatedLeafBinders : Option (Array (Name × StructLeaf)) := none) : TermElabM (TSyntax `command × TSyntax `command) := do let key := indSched.key let indInfo ← getConstInfoInduct key.inductiveName @@ -1531,16 +1732,22 @@ def compileInductiveSchedule (indSched : InductiveSchedule) let mut paramInfo : Array (Name × Expr × TSyntax `term) := #[] for i in [:liveTypes.size] do paramInfo := paramInfo.push (argNames.getD i `x, liveTypes[i]!, liveTypesSyntax[i]!) - -- Compute struct-param leaf binders from the schedule (demand-driven) + -- Struct-param leaf binders. Prefer the SCC-propagated set (which also carries + -- binders inherited from dependency specs — e.g. an `[Enum P.A]` a checker + -- needs to enumerate a leaf-typed witness, propagated up to a dependant + -- generator); fall back to this spec's own binders when none was supplied. let structParams : Array (Name × Expr) := Id.run do let mut sp := #[] for i in [:liveTypes.size] do if i ∉ key.outputIndices && !liveTypes[i]!.isSort then sp := sp.push (argNames.getD i `x, liveTypes[i]!) sp - let allSteps := (indSched.baseSchedules ++ indSched.recSchedules).flatMap (fun (_, (steps, _)) => steps) - let leafBinderSpecs ← computeStructLeafBinders allSteps structParams - let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs + let leafBinderSpecs ← match propagatedLeafBinders with + | some bs => pure bs + | none => do + let allSteps := (indSched.baseSchedules ++ indSched.recSchedules).flatMap (fun (_, (steps, _)) => steps) + computeStructLeafBinders allSteps structParams + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs structParams mkConstrainedProducerMutualPieces baseProducers inductiveProducers key.inductiveName indLevels freshArgIdents freshenedOutputNames @@ -1999,7 +2206,7 @@ def deriveConstrainedProducerParts sp := sp.push (freshUnknowns[i]!, argTypes[i]!) sp let leafBinderSpecs ← computeStructLeafBinders allScheduleSteps structParams - let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs + let structLeafBinders ← structLeafBindersToSyntax leafBinderSpecs structParams return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx, structLeafBinders)) return (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, inductiveName, inductiveLevels, producerSort, structLeafBinders) @@ -2288,6 +2495,9 @@ def elabDeriveMutual : CommandElab := fun stx => do | _ => pure () -- Propagate constraints and compile all specs (before HTML so generated code can be shown) let constraintMap ← liftTermElabM <| propagateConstraints components finalMemo + -- Propagate struct-param leaf binders across specs (so a dependant inherits, + -- e.g., the `[Enum P.A]` its checker dependency needs to enumerate a witness). + let leafBinderMap ← liftTermElabM <| propagateStructLeafBinders components finalMemo -- Compute type param indices per spec and detect instance-param constraints (for display) let mut typeParamIdxMap : Std.HashMap SpecKey (Array Nat) := {} let mut displayConstraintMap := constraintMap @@ -2455,8 +2665,9 @@ def elabDeriveMutual : CommandElab := fun stx => do if indSched.alreadyExists then continue try let specConstraints := constraintMap[key]? + let specLeafBinders := leafBinderMap[key]? let (defCmd, instCmd) ← liftTermElabM <| - compileInductiveSchedule indSched globalName compSiblings specConstraints + compileInductiveSchedule indSched globalName compSiblings specConstraints specLeafBinders defCmds := defCmds.push defCmd instCmds := instCmds.push instCmd let defStr ← liftTermElabM <| try diff --git a/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean index 7d92d6b..5713c80 100644 --- a/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean +++ b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean @@ -226,4 +226,54 @@ derive_mutual (EnumSizedSuchThat.enumSizedST (fun w => @IsGood Out1 w)) 2 IO.println s!"§3 nested struct (P.inner.Needed), mutual: ok, {results.length} enum results" +/-! ## §4 Per-leaf constraints are discovered, not hardcoded + +The class attached to a struct-param leaf is determined by *how the leaf is +used*, exactly as constraint propagation (#42) does for plain `Sort` type +params — not fixed to the producer's own class. In particular a leaf that is +*compared by equality* needs `[DecidableEq leaf]`, and a leaf that is only +*generated* must NOT be saddled with a spurious `DecidableEq`. + +`Pair` carries two leaf-typed fields `a b : P.Key`; `Distinct` accepts a pair +iff `a ≠ b`. Deriving `∃ p, Distinct P p` schedules an unconstrained generation +of `a` and `b` (→ `[Arbitrary P.Key]`) and an `Eq`/`Ne` check on them +(→ `[DecidableEq P.Key]`). Both binders are required: with `Key = Nat` (which has +both instances) it derives and runs; the `≠` check would fail to compile without +the discovered `DecidableEq`. `Spare` is the `Empty` poison field, confirming no +binder is emitted for the unused leaf. -/ + +structure KeyConfig where + Key : Type + Spare : Type + +inductive Pair (P : KeyConfig) where + | mk (a b : P.Key) : Pair P + +inductive Distinct (P : KeyConfig) : Pair P → Prop where + | mk : a ≠ b → Distinct P (.mk a b) + +abbrev KC : KeyConfig := ⟨Nat, Empty⟩ + +#guard_msgs(drop info, drop warning) in +derive_generator (fun (P : KeyConfig) => ∃ p : Pair P, Distinct P p) + +#guard_msgs(drop info) in +#eval show IO Unit from do + -- The point is that this instance *synthesizes* — it requires both + -- `[Arbitrary P.Key]` and the discovered `[DecidableEq P.Key]`; the `a ≠ b` + -- check would not compile without the latter. We also assert soundness on any + -- sample we manage to draw (generation is rejection-based, so a size that + -- exhausts backtracking is tolerated, not a failure). + let mut sound := 0 + for s in List.range 12 do + let r ← (Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST + (fun p => Distinct KC p) 6) (s * 5 + 1) |>.toBaseIO) + match r with + | .ok (.mk a b) => + if a == b then + throw (IO.userError "§4 unsound: Distinct generator produced equal components") + sound := sound + 1 + | .error _ => pure () -- backtracking exhausted at this seed; fine + IO.println s!"§4 per-leaf constraints (Arbitrary + discovered DecidableEq on P.Key): {sound} sound samples" + end StructParamBinderTest diff --git a/SpecimenTest/PolymorphicDepConstraints.lean b/SpecimenTest/PolymorphicDepConstraints.lean index e0dc020..c062d53 100644 --- a/SpecimenTest/PolymorphicDepConstraints.lean +++ b/SpecimenTest/PolymorphicDepConstraints.lean @@ -1,5 +1,8 @@ import Specimen.DeriveConstrainedProducer import Specimen.DeriveChecker +import Specimen.DeriveEnum +import Specimen.Enumerators +import Specimen.EnumeratorCombinators /-! # Regression test for issue #38: missing typeclass constraints for polymorphic dependencies @@ -116,3 +119,90 @@ set_option specimen.multiOutput true in derive_mutual checker (fun c n => HasColor c n), generator (fun n => ∃ c, HasColor c n) + +-- ============================================================ +-- Test 6: Enum propagates transitively through a checker that enumerates α +-- +-- Chain: generator (NoWitness) --checks--> ¬HasWitness +-- HasWitness checker --enumerates a witness x : α--> needs [Enum α] +-- so [Enum α] must propagate all the way up to the NoWitness generator. +-- (The negation is essential: `¬ HasWitness` can only be *checked*, not inverted, +-- which is what forces the generator to depend on HasWitness's checker.) +-- ============================================================ + +inductive Witnessed {α : Type} : α → Nat → Prop where + | mk : ∀ (x : α), Witnessed x 0 + +-- Deciding `HasWitness n` means searching for a witness `x : α` — the checker must +-- enumerate α, so it requires [Enum α]. +inductive HasWitness {α : Type} : Nat → Prop where + | mk : ∀ (x : α) n, Witnessed x n → HasWitness n + +-- Generating `∃ n, NoWitness n` must *check* `¬ HasWitness n`, pulling in +-- HasWitness's checker and hence its [Enum α] constraint. +inductive NoWitness {α : Type} : Nat → Prop where + | mk : ∀ n, ¬ HasWitness (α := α) n → NoWitness n + +set_option specimen.autoDeriveDeps true in +set_option specimen.multiOutput true in +#guard_msgs(drop info) in +derive_mutual + checker (fun α x n => @Witnessed α x n), + checker (fun α n => @HasWitness α n), + generator (fun α => ∃ n, @NoWitness α n) + +-- The checker for HasWitness enumerates α, so it needs [Enum α]. +example [Enum α] [DecidableEq α] : DecOpt (@HasWitness α 0) := inferInstance + +-- The generator for NoWitness must have propagated [Enum α] up through the +-- `¬ HasWitness` check — plus [Arbitrary α] (generate the witnesses when +-- exploring) and [DecidableEq α] (checker default). +example [Plausible.Arbitrary α] [Enum α] [DecidableEq α] : + ArbitrarySizedSuchThat Nat (fun n => @NoWitness α n) := inferInstance + +-- And it resolves at a concrete type carrying Enum + DecidableEq. +example : ArbitrarySizedSuchThat Nat (fun n => @NoWitness Bool n) := inferInstance + +-- ============================================================ +-- Test 7: The Test 6 chain, but the shared type A lives inside a STRUCTURE +-- parameter P (as `P.A`). The [Enum P.A] a checker needs to enumerate a +-- leaf-typed witness must still propagate — across specs — up to the generator, +-- re-rooted onto each spec's own copy of the parameter. +-- ============================================================ + +structure Cfg where + A : Type + Spare : Type -- unused: must never acquire a spurious constraint + +inductive RS (P : Cfg) : P.A → Nat → Prop where + | mk : ∀ (x : P.A), RS P x 0 + +-- Deciding `HasWitnessS P n` enumerates a witness `x : P.A` ⇒ checker needs [Enum P.A]. +inductive HasWitnessS (P : Cfg) : Nat → Prop where + | mk : ∀ (x : P.A) n, RS P x n → HasWitnessS P n + +-- Generating `∃ n, NoWitnessS P n` must *check* `¬ HasWitnessS P n`, so [Enum P.A] +-- propagates from the checker up to this generator. +inductive NoWitnessS (P : Cfg) : Nat → Prop where + | mk : ∀ n, ¬ HasWitnessS P n → NoWitnessS P n + +set_option specimen.autoDeriveDeps true in +set_option specimen.multiOutput true in +#guard_msgs(drop info) in +derive_mutual + checker (fun (P : Cfg) x n => @RS P x n), + checker (fun (P : Cfg) n => @HasWitnessS P n), + generator (fun (P : Cfg) => ∃ n, @NoWitnessS P n) + +-- The struct-param leaf `P.A` gets exactly the discovered constraints: +-- the checker enumerates it ⇒ [Enum P.A]. +example [Enum P.A] [DecidableEq P.A] : DecOpt (@HasWitnessS P 0) := inferInstance + +-- ...and the generator inherits [Enum P.A] transitively through `¬ HasWitnessS`. +example [Plausible.Arbitrary P.A] [Enum P.A] [DecidableEq P.A] : + ArbitrarySizedSuchThat Nat (fun n => @NoWitnessS P n) := inferInstance + +-- Concrete instantiation: A = Bool (has the instances), Spare = Empty (no +-- instances) — resolving proves no spurious constraint attached to the unused +-- `Spare` field. +example : ArbitrarySizedSuchThat Nat (fun n => @NoWitnessS ⟨Bool, Empty⟩ n) := inferInstance