diff --git a/Plausible/DeriveArbitrary.lean b/Plausible/DeriveArbitrary.lean index 303421d1..aa81b075 100644 --- a/Plausible/DeriveArbitrary.lean +++ b/Plausible/DeriveArbitrary.lean @@ -96,6 +96,63 @@ def getCtorArgsNamesAndTypes (_header : Header) (indVal : InductiveVal) (ctorNam -- Note: the following functions closely follow the implementation of the deriving handler for `Repr` / `BEq` -- (see https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/Repr.lean). +/-- Recursively expand a structure-typed expression into `[className proj]` binders + for each leaf field of type `Type u`. Nested structures are expanded recursively. + Non-Type, non-structure fields cause an error. -/ +private partial def expandStructBinders (className : Name) (indName : Name) (argName : Name) + (expr : Expr) (syn : TSyntax `term) : TermElabM (Array Syntax) := do + let ty ← inferType expr + if ty.isSort then + try + let c ← mkAppM className #[expr] + if (← isTypeCorrect c) then + return #[← `(instBinderF| [$(mkCIdent className):ident $syn])] + catch _ => pure () + return #[] + else + let env ← getEnv + let some sName := ty.constName? | + throwError m!"Cannot derive {className} for '{indName}': structure parameter \ + '{mkIdent argName}' has a field of type '{ty}', which is not a Type or \ + structure of Types. This makes the type effectively indexed." + let some sInfo := getStructureInfo? env sName | + throwError m!"Cannot derive {className} for '{indName}': structure parameter \ + '{mkIdent argName}' has a field of type '{ty}', which is not a Type or \ + structure of Types. This makes the type effectively indexed." + let mut result : Array Syntax := #[] + for field in sInfo.fieldNames do + let projName := sName ++ field + let projExpr := mkApp (mkConst projName) expr + let projSyn ← `($(mkIdent projName) $syn) + result := result ++ (← expandStructBinders className indName argName projExpr projSyn) + return result + +open TSyntax.Compat in +/-- Creates inst-implicit binders for a typeclass, handling both + normal type parameters and structure parameters (with recursive expansion). + + For a normal `Type` parameter `α`, emits `[className α]`. + For a structure parameter `T : S`, recursively expands `Type`-valued fields + and emits binders like `[className T.Field]` for each. Nested structures + are expanded recursively. Non-Type, non-structure fields cause an error. -/ +def mkArbitraryInstBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : + TermElabM (Array Syntax) := do + forallBoundedTelescope indVal.type indVal.numParams fun params _ => do + let mut binders : Array Syntax := #[] + for h : i in [:params.size] do + let param := params[i] + let argName := argNames[i]! + let normalOk ← try + let c ← mkAppM className #[param] + isTypeCorrect c + catch _ => pure false + if normalOk then + binders := binders.push + (← `(instBinderF| [$(mkCIdent className):ident $(mkIdent argName):ident])) + else + binders := binders ++ (← expandStructBinders className indVal.name argName param (mkIdent argName)) + return binders + open TSyntax.Compat in /-- Variant of `Deriving.Util.mkHeader` where we don't add an explicit binder of the form `($targetName : $targetType)` to the field `binders` @@ -107,7 +164,7 @@ def mkHeaderWithOnlyImplicitBinders (className : Name) (arity : Nat) (indVal : I let mut targetNames := #[] for _ in [:arity] do targetNames := targetNames.push (← mkFreshUserName `x) - let binders := binders ++ (← mkInstImplicitBinders className indVal argNames) + let binders := binders ++ (← mkArbitraryInstBinders className indVal argNames) return { binders := binders argNames := argNames @@ -129,7 +186,7 @@ def mkArbitraryFueledInstanceCmds (ctx : Deriving.Context) (typeNames : Array Na let auxFunName := ctx.auxFunNames[i]! let argNames ← mkInductArgNames indVal let binders ← mkImplicitBinders argNames - let binders := binders ++ (← mkInstImplicitBinders ``Arbitrary indVal argNames) -- this line is changed from + let binders := binders ++ (← mkArbitraryInstBinders ``Arbitrary indVal argNames) let indType ← mkInductiveApp indVal argNames let type ← `($(mkCIdent ``ArbitraryFueled) $indType) let mut val := mkIdent auxFunName diff --git a/PlausibleTest.lean b/PlausibleTest.lean index 9873d17a..866e286b 100644 --- a/PlausibleTest.lean +++ b/PlausibleTest.lean @@ -17,6 +17,7 @@ import PlausibleTest.DeriveArbitrary.BitVecStructureTest import PlausibleTest.DeriveArbitrary.MissingNonRecursiveConstructorTest import PlausibleTest.DeriveArbitrary.ParameterizedTypeTest import PlausibleTest.DeriveArbitrary.MutuallyRecursiveTypeTest +import PlausibleTest.DeriveArbitrary.StructureParameterTest -- Tests for `deriving Shrinkable` import PlausibleTest.DeriveShrinkable.DeriveShrinkableTest diff --git a/PlausibleTest/DeriveArbitrary/StructureParameterTest.lean b/PlausibleTest/DeriveArbitrary/StructureParameterTest.lean new file mode 100644 index 00000000..2a6284cc --- /dev/null +++ b/PlausibleTest/DeriveArbitrary/StructureParameterTest.lean @@ -0,0 +1,90 @@ +import Plausible.Arbitrary +import Plausible.DeriveArbitrary +import Plausible.Attr + +open Plausible + +set_option guard_msgs.diff true + +/-! ## Structure parameter with Type-valued fields -/ + +structure Params where + Meta : Type + IDMeta : Type + +inductive Bar (T : Params) where + | mk : T.Meta → T.IDMeta → Bar T + +instance [Repr T.Meta] [Repr T.IDMeta] : Repr (Bar T) where + reprPrec b _ := match b with + | .mk m i => f!"Bar.mk {repr m} {repr i}" + +deriving instance Arbitrary for Bar + +#guard_msgs(drop info, drop warning) in +#synth Arbitrary (Bar ⟨Bool, Nat⟩) + +#guard_msgs(drop info, drop warning) in +#eval Arbitrary.runArbitrary (α := Bar ⟨Bool, Nat⟩) 5 + +/-! ## Mixed: normal type parameter + structure parameter -/ + +structure Config where + Tag : Type + +inductive Mixed (α : Type) (C : Config) where + | leaf : α → Mixed α C + | tagged : C.Tag → α → Mixed α C + +instance [Repr α] [Repr C.Tag] : Repr (Mixed α C) where + reprPrec m _ := match m with + | .leaf a => f!"Mixed.leaf {repr a}" + | .tagged t a => f!"Mixed.tagged {repr t} {repr a}" + +deriving instance Arbitrary for Mixed + +#guard_msgs(drop info, drop warning) in +#synth Arbitrary (Mixed Nat ⟨Bool⟩) + +#guard_msgs(drop info, drop warning) in +#eval Arbitrary.runArbitrary (α := Mixed Nat ⟨Bool⟩) 5 + +/-! ## Nested structure parameter -/ + +structure Inner where + Meta : Type + IDMeta : Type + +structure Outer where + base : Inner + Extra : Type + +inductive Nested (T : Outer) where + | mk : T.base.Meta → T.base.IDMeta → T.Extra → Nested T + +instance [Repr T.base.Meta] [Repr T.base.IDMeta] [Repr T.Extra] : Repr (Nested T) where + reprPrec n _ := match n with + | .mk m i e => f!"Nested.mk {repr m} {repr i} {repr e}" + +deriving instance Arbitrary for Nested + +#guard_msgs(drop info, drop warning) in +#synth Arbitrary (Nested ⟨⟨Bool, Nat⟩, String⟩) + +#guard_msgs(drop info, drop warning) in +#eval Arbitrary.runArbitrary (α := Nested ⟨⟨Bool, Nat⟩, String⟩) 5 + +/-! ## Rejection of structures with non-Type fields -/ + +structure BadParams where + n : Nat + Meta : Type + +inductive Baz (T : BadParams) where + | mk : T.Meta → BitVec T.n → Baz T + +/-- +error: Cannot derive Plausible.Arbitrary for 'Baz': structure parameter 'T✝' has a field of type 'Nat', which is not a Type or structure of Types. This makes the type effectively indexed. +-/ +#guard_msgs(error) in +deriving instance Arbitrary for Baz