diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean index f93ecf1..74e4ff9 100644 --- a/Specimen/DeriveConstrainedProducer.lean +++ b/Specimen/DeriveConstrainedProducer.lean @@ -265,10 +265,14 @@ def getScheduleSort (conclusion : HypothesisExpr) - Note: it is the caller's responsibility to check that `conclusion` does indeed contain a non-trivial function application (e.g. by using `containsNonTrivialFuncApp`) -/ def linearizeAndFlatten - (hypotheses : Array Expr) (conclusion : Expr) (outputIndices : List Nat) (localCtx : LocalContext) : + (hypotheses : Array Expr) (conclusion : Expr) (outputIndices : List Nat) (localCtx : LocalContext) + (fixedFVars : Std.HashSet FVarId := {}) : UnifyM (Array Expr × Expr × List (Name × Expr) × LocalContext) := do - -- Phase 1: flatten function calls into fresh unknowns with equality hypotheses - let funcAppExprs ← collectUnmatchableProperSubterms conclusion + -- Phase 1: flatten function calls into fresh unknowns with equality hypotheses. + -- `fixedFVars` are the producer's fixed inputs; a subterm determined entirely + -- by them (e.g. a type parameter `T.mono` where `T` is an input) is left in + -- place rather than lifted into a generated unknown. + let funcAppExprs ← collectUnmatchableProperSubterms fixedFVars conclusion trace[plausible.deriving.arbitrary] m!"Unmatchable exprs: {funcAppExprs} In conclusion: {conclusion}" withLCtx' localCtx do @@ -473,8 +477,22 @@ def getScheduleForInductiveRelationConstructor -- equal to the result of the function call, and adding an extra hypothesis asserting equality -- between the function call and the variable. -- `freshNamesAndTypes` is a list containing the names & types of the fresh variables produced during this procedure. + -- Identify fixed inputs as fvars, so flattening can leave subterms that are + -- determined entirely by the inputs (e.g. an output type's structure + -- parameter `T.mono`) in place instead of trying to generate them. The + -- conclusion's arguments at non-output (input) positions that are bare + -- variables are exactly those inputs (e.g. the inductive's parameter `T`). + let curLCtx ← getLCtx + let conclArgs := conclusion.getAppArgs + let fixedFVars : Std.HashSet FVarId := Id.run do + let mut s : Std.HashSet FVarId := {} + for h : i in [:conclArgs.size] do + if i ∉ outputIndices then + if let .fvar fid := conclArgs[i] then + s := s.insert fid + return s let (updatedHypotheses, updatedConclusion, freshNamesAndTypes, updatedLocalCtx) ← - linearizeAndFlatten hypotheses conclusion outputIndices (← getLCtx) + linearizeAndFlatten hypotheses conclusion outputIndices curLCtx fixedFVars -- Enter the updated `LocalContext` containing the fresh variable that was created when rewriting the conclusion withLCtx' updatedLocalCtx (do let hypothesisExprs := (← monadLift (updatedHypotheses.toList.mapM (exprToHypothesisExpr ctorName))).toArray diff --git a/Specimen/MExp.lean b/Specimen/MExp.lean index 9d89ac6..f9f14bd 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 @@ -460,21 +492,23 @@ def scheduleStepToMExp (step : ScheduleStep) (defFuel : MExp) (k : MExp) (output - `mfuel` and `defFuel` are auxiliary `MExp`s representing the fuel for the function we are deriving (these correspond to `size` and `initSize` in the QuickChick code for the derived functions) -/ -def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recType : Expr) (fuelPrimeName : Name := `fuel') (sizePrimeName : Name := `size') : CompileScheduleM MExp := +def scheduleToMExp (schedule : Schedule) (mfuel : MExp) (defFuel : MExp) (recType : Expr) (fuelPrimeName : Name := `fuel') (sizePrimeName : Name := `size') : CompileScheduleM MExp := do let (scheduleSteps, scheduleSort) := schedule -- 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 @@ -482,7 +516,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 810e1ba..49e46ae 100644 --- a/Specimen/MakeConstrainedProducerInstance.lean +++ b/Specimen/MakeConstrainedProducerInstance.lean @@ -53,6 +53,62 @@ def mkTypeClassInstanceBinders (typeParams : Array Name) (typeClasses : Array Na `(Lean.Elab.Deriving.instBinderF| [$(mkIdent tc) $(mkIdent param)]) return TSyntaxArray.mk instances +open TSyntax.Compat in +/-- Recursively expand a *structure-typed* parameter into `[className proj]` + instance binders for each leaf field of type `Type u`. Mirrors + `expandStructBinders` in `Specimen.DeriveArbitrary` (the unconstrained + `deriving Arbitrary` path), which is what lets `Arbitrary (LExpr T)` be + derived for a structure parameter `T`: the constrained producer instance + needs the same per-field binders (e.g. `[Arbitrary T.base.Metadata]`) so the + metadata fields carried by each constructor can be generated. + + `ty` is the type being walked (the parameter's type, or a field's type as we + recurse) and `syn` is the matching surface syntax (the parameter identifier, + or a projection chain into it). A leaf `Type u` field yields `[className syn]`; + a structure field recurses into its own fields. Returns `#[]` for fields that + are neither Types nor structures-of-Types — the conservative, + behavior-preserving choice for the constrained path. -/ +partial def expandStructInstBinders (className : Name) (ty : Expr) (syn : TSyntax `term) : + TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + if ty.isSort then + -- A `Type u` leaf: emit `[className syn]`. + return #[← `(Lean.Elab.Deriving.instBinderF| [$(mkCIdent className):ident $syn])] + let env ← getEnv + let some sName := ty.constName? | return #[] + let some sInfo := getStructureInfo? env sName | return #[] + let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + -- The field's declared type, read as the codomain of the projection's + -- signature `∀ (_ : sName ..), fieldType`. Structure fields here are the + -- metadata-configuration types, whose field types do not depend on the value. + -- Limitation: `mkConst projName` is built without universe-level arguments, so + -- for a *universe-polymorphic* structure parameter `projType` would be computed + -- at the wrong universe. We don't support such parameters (they are rare in + -- practice; all current Strata params are `Type 0`); supporting them would mean + -- extracting `ty`'s universe levels and passing them to `mkConst` here. + let projType ← forallTelescopeReducing (← inferType (mkConst projName)) + (fun _ body => pure body) + let projSyn ← `($(mkIdent projName) $syn) + result := result ++ (← expandStructInstBinders className projType projSyn) + return result + +/-- Build the unconstrained-producer instance binders for a list of + non-target inductive parameters. For a `Sort`-typed parameter `α`, emits + `[className α] [DecidableEq α]` (the existing behavior). For a *structure* + parameter `T`, expands it into per-field binders via `expandStructInstBinders` + (e.g. `[className T.base.Metadata]` …) so the structure's metadata fields can + be generated. Parameters of other types contribute no binders. -/ +def mkProducerParamInstBinders (className : Name) + (params : Array (Name × Expr)) : TermElabM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do + let mut result : TSyntaxArray `Lean.Parser.Term.bracketedBinder := #[] + for (paramName, paramType) in params do + if paramType.isSort then + result := result ++ (← mkTypeClassInstanceBinders #[paramName] #[className, ``DecidableEq]) + else + result := result ++ (← expandStructInstBinders className paramType (mkIdent paramName)) + return result + /-- Finds the index of the argument in the inductive application for the value we wish to generate (i.e. finds `i` s.t. `args[i] == targetVar`) -/ def findTargetVarIndex (targetVar : FVarId) (args : Array Expr) : (Option Nat) := do @@ -135,6 +191,10 @@ def mkConstrainedProducerTypeClassInstance let mut outerParams := #[] let mut outputTypeSyntaxes : Array (TSyntax `term) := #[] let mut typeParams := #[] + -- Non-target, non-sort *structure* parameters (e.g. `T : LExprParams`): we + -- need per-field unconstrained-producer instances for these (see + -- `mkProducerParamInstBinders`). + let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do -- Only add a function parameter if the argument to the inductive relation is not a target variable -- (We skip the target variables since those are the values we wish to generate) @@ -152,6 +212,8 @@ def mkConstrainedProducerTypeClassInstance `(Term.letIdBinder| ($innerParamIdent : $paramTypeSyntax)) innerParams := innerParams.push innerParam + if !paramType.isSort then + structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -203,7 +265,11 @@ def mkConstrainedProducerTypeClassInstance | .Generator => ``Plausible.Arbitrary | .Enumerator => ``Enum - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + -- Per-field unconstrained-producer instances for structure parameters (e.g. + -- `[Arbitrary T.base.Metadata]`), so their fields can be generated. + let structParamInstances ← mkProducerParamInstBinders producerUnconstrainedClass structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structParamInstances let fuelVal := Lean.Option.get (← getOptions) specimen.fuel let fuelLit := Syntax.mkNumLit (toString fuelVal) @@ -263,6 +329,8 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($initSizeIdent : $natIdent))) innerParamBinders := innerParamBinders.push (← `(($sizeIdent : $natIdent))) + -- Non-target, non-sort structure parameters needing per-field producer instances. + let mut structParams : Array (Name × Expr) := #[] for (paramName, paramType, paramTypeSyntax) in paramInfo do if paramType.isSort then typeParams := typeParams.push paramName @@ -273,6 +341,7 @@ def mkConstrainedProducerMutualPieces innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : Sort _))) else innerParamBinders := innerParamBinders.push (← `(($(mkIdent paramName) : $paramTypeSyntax))) + structParams := structParams.push (paramName, paramType) else outputTypeSyntaxes := outputTypeSyntaxes.push paramTypeSyntax @@ -320,11 +389,18 @@ def mkConstrainedProducerMutualPieces | .Generator => ``Plausible.Arbitrary | .Enumerator => ``Enum let defTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + -- Per-field producer instances for structure parameters (e.g. + -- `[Arbitrary T.base.Metadata]`). These reference value params (`T`), so they + -- are placed *innermost* — after all value params — where those are in scope. + let structParamInstances ← mkProducerParamInstBinders producerUnconstrainedClass structParams -- Emit the def with ∀ type (supports instance binders inline) let defIdent := mkIdent globalDefName -- Build ∀ type with instance binders interleaved after Sort-typed params let mut defType ← pure optionTProducerType + -- Innermost: structure-parameter field instances (all value params in scope). + for instBinder in structParamInstances.reverse do + defType ← `(∀ $instBinder:bracketedBinder, $defType) -- Add non-Sort value params (from right) let insertIdx := 3 + typeParams.size for (name, ty) in allParamNamesAndTypes[insertIdx:].toArray.reverse do @@ -335,9 +411,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) @@ -348,7 +427,9 @@ def mkConstrainedProducerMutualPieces let callExpr ← `($defIdent $callArgs*) let instCmd ← match deriveSort with | .Checker | .Theorem => do - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[``Enum, ``DecidableEq] + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[``Enum, ``DecidableEq] + let structInsts ← mkProducerParamInstBinders ``Enum structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $decOptTypeclass (@$(mkIdent inductiveName) $args*) where $unqualifiedDecOptFn:ident := fun $freshSizeIdent => $callExpr) @@ -362,7 +443,9 @@ def mkConstrainedProducerMutualPieces let producerUnconstrainedClass := match producerSort with | .Generator => ``Plausible.Arbitrary | .Enumerator => ``Enum - let arbitraryTypeParamInstances ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let arbitraryTypeParamInstances0 ← mkTypeClassInstanceBinders typeParams #[producerUnconstrainedClass, ``DecidableEq] + let structInsts ← mkProducerParamInstBinders producerUnconstrainedClass structParams + let arbitraryTypeParamInstances := arbitraryTypeParamInstances0 ++ structInsts `(command| instance $arbitraryTypeParamInstances:bracketedBinder* : $producerTypeClass $targetTypeSyntax (fun $targetVarPattern => @$(mkIdent inductiveName) $args*) where $producerTypeClassFunction:ident := fun $freshSizeIdent => $callExpr) diff --git a/Specimen/SearchTree.lean b/Specimen/SearchTree.lean index 98ea457..54f8f96 100644 --- a/Specimen/SearchTree.lean +++ b/Specimen/SearchTree.lean @@ -261,8 +261,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/StrataDefs/LambdaCore.lean b/SpecimenTest/StrataDefs/LambdaCore.lean index b23ab83..2c49715 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. -/ @@ -216,7 +222,47 @@ inductive LExpr (T : LExprParamsT) : Type where /-- An equality expression. -/ | eq (m : T.base.Metadata) (e1 e2 : LExpr T) -/-! ## `Denote/LExprAnnotated.lean` — declarative typing for annotated exprs -/ +/-! ## `Denote/LExprAnnotated.lean` — type checking for annotated exprs -/ + +/-- 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`) -/ +@[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 /-- Declarative typing rules for annotated expressions. diff --git a/SpecimenTest/StrataLexprGen.lean b/SpecimenTest/StrataLexprGen.lean index 25e4445..351e4eb 100644 --- a/SpecimenTest/StrataLexprGen.lean +++ b/SpecimenTest/StrataLexprGen.lean @@ -14,28 +14,21 @@ 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`. -/ +This exercises three Specimen capabilities working together on the *real*, +fully-parameterized relation: + +1. The schedule classifier tolerates function-application premises such as the + `bvar` rule's `Δ[i]? = some t` de-Bruijn lookup. +2. The delegated-producer path routes that equality premise to a user-supplied + `ArbitrarySizedSuchThat` instance for the lookup. +3. The constrained deriver handles `LExpr`'s `LExprParamsT` *structure + parameter*: it does not try to generate the parameter itself, and it emits + the per-field `[Arbitrary T.base.Metadata]` …-style instance binders needed + to generate the metadata fields carried by each constructor (mirroring the + unconstrained `deriving Arbitrary` path's `expandStructBinders`). + +Note the relation below is the genuine `@LExpr.HasTypeA T …` with `T` an +abstract `LExprParams` — no monomorphization. -/ open Plausible open ArbitrarySizedSuchThat @@ -45,77 +38,54 @@ 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 - arbitrary := do return (Rat.ofInt (← Arbitrary.arbitrary)) - -deriving instance Arbitrary for QuantifierKind -deriving instance Arbitrary for LConst -deriving instance Arbitrary for Identifier + arbitrary := do + let numerator ← Arbitrary.arbitrary + let denominator ← Arbitrary.arbitrary + return mkRat numerator denominator /-- A *shallow*, terminating `Arbitrary LMonoTy`. The auto-derived generator for `LMonoTy` is unbounded (its `tcons` carries `List LMonoTy`, so it can recurse - without limit and overflow the stack); since the constrained generator only - needs occasional fresh types (e.g. the `app` argument type, binder - annotations), a small fixed selection of base and first-order arrow types is - both sufficient and well-behaved. -/ + without limit and overflow the stack); a small fixed selection of base and + first-order arrow types is sufficient for the occasional fresh types the + constrained generator needs (e.g. the `app` argument type). -/ instance : Arbitrary LMonoTy where arbitrary := do let choices : List LMonoTy := - [.int, .bool, .string, - .arrow .int .bool, .arrow .bool .bool, .arrow .int .int] + [.int, .bool, .string, .arrow .int .bool, .arrow .bool .bool, .arrow .int .int] let n ← Plausible.Gen.chooseNatLt 0 choices.length (by decide) return choices[n.val]! -deriving instance Arbitrary for LExprU +deriving instance Arbitrary for QuantifierKind +deriving instance Arbitrary for LConst +deriving instance Arbitrary for Identifier +-- The output ADT, via Specimen's structure-parameter-aware `Arbitrary` override. +deriving instance Arbitrary for LExpr -/-! ## The hand-written delegated producer for the de-Bruijn lookup +/-! ## The hand-written delegated producers 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). - -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. -/ +cannot invert to *produce* the index `i`. We supply constrained producers for +that equality; the delegated-producer machinery detects them and delegates +production of the lookup to them (rather than generating `i` blindly and +filtering, which has a poor hit rate). + +The first instance produces an index of the requested type; the second is the +synthesis-direction companion (`derive_mutual` derives both directions), which +produces an index *and* the type it points at. Both fail when no in-scope +variable matches, so they never fabricate ill-typed `bvar`s. -/ instance lookupProducer (Δ : List LMonoTy) (t : LMonoTy) : ArbitrarySizedSuchThat Nat (fun i => Δ[i]? = some t) where arbitrarySizedST _ := do - let candidates := (List.range Δ.length).filter (fun i => Δ[i]? = some t) - match candidates with - -- No in-scope variable has type `t`: fail so the caller backtracks to another - -- rule. Returning an arbitrary index here would fabricate an ill-typed `bvar`. + match (List.range Δ.length).filter (fun i => Δ[i]? = some t) with | [] => throw Plausible.Gen.genericFailure | c :: cs => let n ← Plausible.Gen.chooseNatLt 0 (c :: cs).length (by simp) return (c :: cs)[n.val]! -/-- The companion lookup producer for the *synthesis* direction, used when - `derive_mutual` also derives "given a term, find its type": pick an index `i` - into `Δ` and return both `i` and the entry `Δ[i]?` it points at. Producing - both at once satisfies `Δ[i]? = vt`. -/ instance lookupProducerSyn (Δ : List LMonoTy) : ArbitrarySizedSuchThat (Nat × Option LMonoTy) (fun p => Δ[p.1]? = p.2) where arbitrarySizedST _ := do @@ -125,43 +95,16 @@ 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 `τ`. - - 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`. - - (`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.) -/ +/- Derive a constrained generator for well-typed `LExpr T.mono`, for an abstract + structure parameter `T`. With the structure-parameter handling in place, the + constructors' metadata fields (`m : T.base.Metadata`, identifiers, …) are + generated via the auto-emitted per-field `Arbitrary` instance binders, and the + `bvar` lookup is delegated to `lookupProducer`. `derive_mutual` also explores a + synthesis companion whose `eq`-rule has a fixed `bool` conclusion (nothing to + synthesize), producing 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 -/ @@ -176,8 +119,18 @@ 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 := +/-! ## Soundness check: sampled terms really are well-typed + +We instantiate the derived generator at the concrete, monomorphic parameters +`P := ⟨Unit, Unit⟩` and type-check sampled terms with Strata's own computable +checker `LExpr.typeCheck` (vendored in `LambdaCore.lean`), which is proved +equivalent to `HasTypeA` upstream — so this is an authoritative soundness check. -/ + +/-- Concrete, monomorphic expression parameters for sampling. -/ +abbrev P : LExprParams := ⟨Unit, Unit⟩ + +/-- Pretty-print an `LExpr P.mono` with minimal parenthesization. -/ +def ppLExprP (e : LExpr P.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,66 +144,33 @@ 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}. {ppLExprP body 0}" + | none => s!"λ_. {ppLExprP 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}. {ppLExprP body 0}" + | none => s!"∀_. {ppLExprP 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 - -/- Sample the derived generator across several `(context, type)` requests and - assert every produced term type-checks at the requested type. Throws (failing - the build) on any ill-typed sample, so this doubles as a soundness test. -/ + | some t => s!"∃{ppMonoTy t}. {ppLExprP body 0}" + | none => s!"∃_. {ppLExprP body 0}" + | .app _ fn arg => wrap 3 <| s!"{ppLExprP fn 2} {ppLExprP arg 3}" + | .ite _ c t e => wrap 1 <| s!"if {ppLExprP c 0} then {ppLExprP t 0} else {ppLExprP e 0}" + | .eq _ e₁ e₂ => wrap 2 <| s!"{ppLExprP e₁ 2} == {ppLExprP e₂ 2}" + +/- Sample the derived generator (at `T := P`) across several `(context, type)` + requests and assert every produced term type-checks at the requested type. + Throws (failing the build) on any ill-typed sample. -/ #guard_msgs(drop info) in #eval show IO Unit from do let trials : List (List LMonoTy × LMonoTy) := - [([.int, .bool], .bool), ([.int], .int), ([], .bool), + [([.int, .bool], .bool), ([.int], .int), ([], .bool), ([.bool, .int, .string], .string), ([.arrow .int .bool, .int], .bool)] for (ctx, τ) in trials do let ctxStr := String.intercalate ", " (ctx.map ppMonoTy) 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 P ctx e τ) 4) (s * 7 + 1) + IO.println s!" {ppLExprP 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 τ}: {ppLExprP e} : {repr (LExpr.typeCheck ctx e)}")