diff --git a/Docs/Struct-param-support.md b/Docs/Struct-param-support.md new file mode 100644 index 0000000..4e8faa4 --- /dev/null +++ b/Docs/Struct-param-support.md @@ -0,0 +1,236 @@ +# 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. 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`: + +- **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`) +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 + +*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 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 + 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`. + +- **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 4455630..7e36b46 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 @@ -688,6 +706,278 @@ 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 [] + +/-- 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 StructLeaf := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + 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 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 × Name × List Name)) := do + match ce with + | .Unknown n => + match structParams.find? (fun (pn, _) => pn == n) with + | 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 (_, rootStruct, basePath) => + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + return some (projType, rootStruct, projName :: basePath) + | none => return none + else return none + | _ => return none + +/-- 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 + +/-- 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 + +/-- 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 × 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 (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 => + 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 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 + -- 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 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 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 + -- 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 + /-- Produces an instance of a typeclass for a constrained producer (either `ArbitrarySizedSuchThat` or `EnumSizedSuchThat`). The arguments to this function are: @@ -753,7 +1043,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 @@ -784,6 +1074,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' @@ -841,6 +1135,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) @@ -889,12 +1184,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 structParams + + 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 @@ -1212,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 @@ -1325,10 +1732,26 @@ 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]!) + -- 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 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 - 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. @@ -1653,7 +2076,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 @@ -1682,7 +2105,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 @@ -1699,6 +2122,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 @@ -1735,6 +2161,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) @@ -1770,8 +2197,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 structParams + return (baseProducers, inductiveProducers, freshenedOutputNames, Lean.mkIdent <$> freshUnknowns, localCtx, structLeafBinders)) + return (baseProducers, inductiveProducers, freshenedOutputNames, freshArgIdents, outputTypes, localCtx, inductiveName, inductiveLevels, producerSort, structLeafBinders) private def deriveArbitrarySuchThatInstance' @@ -1964,10 +2401,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 @@ -2058,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 @@ -2225,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 @@ -2706,10 +3147,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/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..b3bbe1f 100644 --- a/Specimen/MakeConstrainedProducerInstance.lean +++ b/Specimen/MakeConstrainedProducerInstance.lean @@ -53,6 +53,7 @@ def mkTypeClassInstanceBinders (typeParams : Array Name) (typeClasses : Array Na `(Lean.Elab.Deriving.instBinderF| [$(mkIdent tc) $(mkIdent param)]) return TSyntaxArray.mk instances + /-- 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 @@ -84,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' @@ -203,7 +205,8 @@ def mkConstrainedProducerTypeClassInstance | .Generator => ``Plausible.Arbitrary | .Enumerator => ``Enum - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders let fuelVal := Lean.Option.get (← getOptions) specimen.fuel let fuelLit := Syntax.mkNumLit (toString fuelVal) @@ -226,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 @@ -325,11 +329,17 @@ def mkConstrainedProducerMutualPieces | .Enumerator => ``Enum #[producerUnconstrainedClass, ``DecidableEq] let defTypeParamInstances ← mkTypeClassInstanceBinders typeParams typeClasses + -- 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 -- 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 +350,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 +373,8 @@ def mkConstrainedProducerMutualPieces | .Enumerator => #[``Enum, ``DecidableEq] let instCmd ← match deriveSort with | .Checker | .Theorem => do - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams instTypeClasses + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $decOptTypeclass (@$(mkIdent inductiveName) $args*) where $unqualifiedDecOptFn:ident := fun $freshSizeIdent => $callExpr) @@ -371,7 +385,8 @@ def mkConstrainedProducerMutualPieces let producerTypeClassFunction := match producerSort with | .Generator => unqualifiedArbitrarySizedSTFn | .Enumerator => unqualifiedEnumSizedSTFn - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams instTypeClasses + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams instTypeClasses + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structLeafBinders `(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..cd2bdab 100644 --- a/SpecimenTest.lean +++ b/SpecimenTest.lean @@ -43,6 +43,8 @@ import SpecimenTest.DeriveArbitrary.MissingNonRecursiveConstructorTest import SpecimenTest.DeriveArbitrary.ParameterizedTypeTest import SpecimenTest.DeriveArbitrary.MutuallyRecursiveTypeTest import SpecimenTest.DeriveArbitrarySuchThat.DeriveSTLCGenerator +import SpecimenTest.DeriveArbitrarySuchThat.DeriveStructParamGenerator +import SpecimenTest.DeriveArbitrarySuchThat.StructParamBinderTest 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 diff --git a/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean new file mode 100644 index 0000000..5713c80 --- /dev/null +++ b/SpecimenTest/DeriveArbitrarySuchThat/StructParamBinderTest.lean @@ -0,0 +1,279 @@ +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" + +/-! ## §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 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)}")