From ad5bb8768f976b48aa10306edc8a15943343b665 Mon Sep 17 00:00:00 2001 From: Daniel Sainati Date: Wed, 8 Oct 2025 15:01:25 -0400 Subject: [PATCH] add function to print sized samples --- Plausible/Sampleable.lean | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean index fc1b1bcb..c894a99b 100644 --- a/Plausible/Sampleable.lean +++ b/Plausible/Sampleable.lean @@ -395,7 +395,17 @@ def printNSamples {t : Type u} [Repr t] (g : Gen t) (n : Nat) : IO PUnit := do -- (and `RandT IO (List t)` isn't type-correct without -- https://github.com/leanprover/lean4/issues/3011), so go via an intermediate let xs : List Std.Format ← Plausible.runRand <| Rand.down <| do - let xs : List t ← (List.range n).mapM (ReaderT.run g ∘ ULift.up) + let xs : List t ← (List.range n).mapM (fun _ => ReaderT.run g (ULift.up 0)) + pure <| ULift.up (xs.map repr) + for x in xs do + IO.println s!"{x}" + +/-- Prints at most `n` `size`-sized samples of a given type (produced by the generator `g`) to `stdout` for debugging -/ +def printNSizedSamples {t : Type u} [Repr t] (g : Gen t) (n : Nat) (size : Nat) : IO PUnit := do + letI : MonadLift Id IO := ⟨fun f => pure <| Id.run f⟩ + do + let xs : List Std.Format ← Plausible.runRand <| Rand.down <| do + let xs : List t ← (List.range n).mapM (fun _ => ReaderT.run g (ULift.up size)) pure <| ULift.up (xs.map repr) for x in xs do IO.println s!"{x}" @@ -406,6 +416,13 @@ Print (at most) 10 samples of a given type to stdout for debugging. def printSamples {t : Type u} [Repr t] (g : Gen t) : IO PUnit := do printNSamples g 10 +/-- +Print (at most) 10 `size`-sized samples of a given type to stdout for debugging. +-/ +def printSizedSamples {t : Type u} [Repr t] (g : Gen t) (size : Nat) : IO PUnit := do + printNSizedSamples g 10 size + + open Lean Meta Elab /--